Theory WellFoundedTransitive

header {*  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"
  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 assumption

lemma order_trans3:
  "x < y ==> y ≤ z ==> x < z"
  apply (simp add: less_eq_def)
  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 (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
    done
next
  fix x y :: "'a * 'b"
  show  "x ≤ y <-> x = y ∨ x < y"
    by (simp add: less_eq_pair_def)
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