# Theory WellFoundedTransitive

Up to index of Isabelle/HOL/LatticeProperties

theory WellFoundedTransitive
imports Main
`header {*  Well founded and transitive relations  *}theory WellFoundedTransitiveimports Mainbeginclass transitive = ord +  assumes order_trans1: "x < y ==> y < z ==> x < z"  and less_eq_def: "x ≤ y <-> x = y ∨ x < y"beginlemma eq_less_eq [simp]:  "x = y ==> x ≤ y"  by (simp add: less_eq_def)lemma order_trans2 [simp]:  "x ≤ y ==> y < z ==> x < z"  apply (simp add: less_eq_def)  apply auto  apply (erule less_eq_def order_trans1)  by assumptionlemma order_trans3:  "x < y ==> y ≤ z ==> x < z"  apply (simp add: less_eq_def)  apply auto  apply (erule less_eq_def order_trans1)  by assumptionendclass well_founded = ord +  assumes less_induct1 [case_names less]: "(!!x . (!!y . y < x ==> P y) ==> P x) ==> P a"class well_founded_transitive = transitive + well_foundedinstantiation prod:: (ord, ord) ordbegindefinition  less_pair_def: "a < b <->  fst a  < fst b ∨ (fst a = fst b ∧ snd a < snd b)"definition  less_eq_pair_def: "(a::('a::ord * 'b::ord)) <= b <-> a = b ∨ a < b"instance proof qedendinstantiation prod:: (transitive, transitive) transitivebegininstance proof  fix x y z :: "('a::transitive * 'b::transitive)"  assume "x < y" and "y < z" then  show  "x < z"    apply (simp add: less_pair_def)    apply auto    apply (drule  order_trans1)    apply auto    apply (drule  order_trans1)    apply auto    apply (drule  order_trans1)    apply auto    donenext  fix x y :: "'a * 'b"  show  "x ≤ y <-> x = y ∨ x < y"    by (simp add: less_eq_pair_def)qedendinstantiation prod:: (well_founded, well_founded) well_foundedbegininstance proof  fix P::"('a * 'b) => bool"  have a:  "!P . (!x::'a . (!y . y < x --> P y) --> P x) --> (!a . P a)"    apply safe    apply (rule less_induct1)    by blast  have b:  "!P . (!x::'b . (!y . y < x --> P y) --> P x) --> (!a . P a)"    apply safe    apply (rule less_induct1)    by blast  from a and b have c: "(!x . (!y . y < x --> P y) --> P x) --> (!a . P a)"    apply (unfold less_pair_def)    apply (rule impI)    apply (simp (no_asm_use) only: split_paired_All)    apply (unfold fst_conv snd_conv)    apply (drule spec)    apply (erule mp)    apply (rule allI)    apply (rule impI)    apply (drule spec)    apply (erule mp)    by blast  assume A: "(!! x. (!! y. y < x ==> P y) ==> P x)"  fix a  from c A show "P a" by blastqedendinstantiation prod:: (well_founded_transitive, well_founded_transitive) well_founded_transitivebegininstance proof qedendinstantiation "nat" :: transitivebegininstance proof  fix x y z::nat  assume "x < y" and "y < z" then show "x < z" by simp  next  fix x y::nat show "(x ≤ y) <-> (x = y ∨ x < y)"    apply (unfold le_less)    by safe  qedendinstantiation "nat":: well_foundedbegininstance proof  fix P::"nat => bool"   fix a  assume A: "(!!x . (!!y . y < x ==> P y) ==> P x)"  show "P a"  by (rule less_induct, rule A, simp)  qedendinstantiation "nat":: well_founded_transitivebegininstance proof qedendend`