# Theory LatticeProperties.WellFoundedTransitive

```section ‹Well founded and transitive relations›

theory WellFoundedTransitive
imports Main
begin

class transitive = ord +
assumes order_trans1: "x < y ⟹ y < z ⟹ x < z"
and less_eq_def: "x ≤ y ⟷ x = y ∨ x < y"
begin

lemma eq_less_eq [simp]:
"x = y ⟹ x ≤ y"

lemma order_trans2 [simp]:
"x ≤ y ⟹ y < z ⟹ x < z"
apply auto
apply (erule less_eq_def order_trans1)
by assumption

lemma order_trans3:
"x < y ⟹ y ≤ z ⟹ x < z"
apply auto
apply (erule less_eq_def order_trans1)
by assumption
end

class 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_founded

instantiation prod:: (ord, ord) ord
begin

definition
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 qed
end

instantiation prod:: (transitive, transitive) transitive
begin
instance proof
fix x y z :: "('a::transitive * 'b::transitive)"
assume "x < y" and "y < z" then  show  "x < z"
apply auto
apply (drule  order_trans1)
apply auto
apply (drule  order_trans1)
apply auto
apply (drule  order_trans1)
apply auto
done
next
fix x y :: "'a * 'b"
show  "x ≤ y ⟷ x = y ∨ x < y"
qed
end

instantiation prod:: (well_founded, well_founded) well_founded
begin
instance 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 blast
qed
end

instantiation prod:: (well_founded_transitive, well_founded_transitive) well_founded_transitive
begin
instance proof qed
end

instantiation "nat" :: transitive
begin

instance 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
qed
end

instantiation "nat":: well_founded
begin
instance 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)
qed
end

instantiation "nat":: well_founded_transitive
begin
instance proof qed
end

end
```