Theory Wellorder_Relation

(*  Title:      HOL/Cardinals/Wellorder_Relation.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Well-order relations.
*)

section {* Well-Order Relations *}

theory Wellorder_Relation
imports BNF_Wellorder_Relation Wellfounded_More
begin

context wo_rel
begin

subsection {* Auxiliaries *}

lemma PREORD: "Preorder r"
using WELL order_on_defs[of _ r] by auto

lemma PARORD: "Partial_order r"
using WELL order_on_defs[of _ r] by auto

lemma cases_Total2:
"⋀ phi a b. ⟦{a,b} ≤ Field r; ((a,b) ∈ r - Id ⟹ phi a b);
              ((b,a) ∈ r - Id ⟹ phi a b); (a = b ⟹ phi a b)⟧
             ⟹ phi a b"
using TOTALS by auto


subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}

lemma worec_unique_fixpoint:
assumes ADM: "adm_wo H" and fp: "f = H f"
shows "f = worec H"
proof-
  have "adm_wf (r - Id) H"
  unfolding adm_wf_def
  using ADM adm_wo_def[of H] underS_def[of r] by auto
  hence "f = wfrec (r - Id) H"
  using fp WF wfrec_unique_fixpoint[of "r - Id" H] by simp
  thus ?thesis unfolding worec_def .
qed


subsubsection {* Properties of max2 *}

lemma max2_iff:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "((max2 a b, c) ∈ r) = ((a,c) ∈ r ∧ (b,c) ∈ r)"
proof
  assume "(max2 a b, c) ∈ r"
  thus "(a,c) ∈ r ∧ (b,c) ∈ r"
  using assms max2_greater[of a b] TRANS trans_def[of r] by blast
next
  assume "(a,c) ∈ r ∧ (b,c) ∈ r"
  thus "(max2 a b, c) ∈ r"
  using assms max2_among[of a b] by auto
qed


subsubsection {* Properties of minim *}

lemma minim_Under:
"⟦B ≤ Field r; B ≠ {}⟧ ⟹ minim B ∈ Under B"
by(auto simp add: Under_def minim_inField minim_least)

lemma equals_minim_Under:
"⟦B ≤ Field r; a ∈ B; a ∈ Under B⟧
 ⟹ a = minim B"
by(auto simp add: Under_def equals_minim)

lemma minim_iff_In_Under:
assumes SUB: "B ≤ Field r" and NE: "B ≠ {}"
shows "(a = minim B) = (a ∈ B ∧ a ∈ Under B)"
proof
  assume "a = minim B"
  thus "a ∈ B ∧ a ∈ Under B"
  using assms minim_in minim_Under by simp
next
  assume "a ∈ B ∧ a ∈ Under B"
  thus "a = minim B"
  using assms equals_minim_Under by simp
qed

lemma minim_Under_under:
assumes NE: "A ≠ {}" and SUB: "A ≤ Field r"
shows "Under A = under (minim A)"
proof-
  (* Preliminary facts *)
  have 1: "minim A ∈ A"
  using assms minim_in by auto
  have 2: "∀x ∈ A. (minim A, x) ∈ r"
  using assms minim_least by auto
  (* Main proof *)
  have "Under A ≤ under (minim A)"
  proof
    fix x assume "x ∈ Under A"
    with 1 Under_def[of r] have "(x,minim A) ∈ r" by auto
    thus "x ∈ under(minim A)" unfolding under_def by simp
  qed
  (*  *)
  moreover
  (*  *)
  have "under (minim A) ≤ Under A"
  proof
    fix x assume "x ∈ under(minim A)"
    hence 11: "(x,minim A) ∈ r" unfolding under_def by simp
    hence "x ∈ Field r" unfolding Field_def by auto
    moreover
    {fix a assume "a ∈ A"
     with 2 have "(minim A, a) ∈ r" by simp
     with 11 have "(x,a) ∈ r"
     using TRANS trans_def[of r] by blast
    }
    ultimately show "x ∈ Under A" by (unfold Under_def, auto)
  qed
  (*  *)
  ultimately show ?thesis by blast
qed

lemma minim_UnderS_underS:
assumes NE: "A ≠ {}" and SUB: "A ≤ Field r"
shows "UnderS A = underS (minim A)"
proof-
  (* Preliminary facts *)
  have 1: "minim A ∈ A"
  using assms minim_in by auto
  have 2: "∀x ∈ A. (minim A, x) ∈ r"
  using assms minim_least by auto
  (* Main proof *)
  have "UnderS A ≤ underS (minim A)"
  proof
    fix x assume "x ∈ UnderS A"
    with 1 UnderS_def[of r] have "x ≠ minim A ∧ (x,minim A) ∈ r" by auto
    thus "x ∈ underS(minim A)" unfolding underS_def by simp
  qed
  (*  *)
  moreover
  (*  *)
  have "underS (minim A) ≤ UnderS A"
  proof
    fix x assume "x ∈ underS(minim A)"
    hence 11: "x ≠ minim A ∧ (x,minim A) ∈ r" unfolding underS_def by simp
    hence "x ∈ Field r" unfolding Field_def by auto
    moreover
    {fix a assume "a ∈ A"
     with 2 have 3: "(minim A, a) ∈ r" by simp
     with 11 have "(x,a) ∈ r"
     using TRANS trans_def[of r] by blast
     moreover
     have "x ≠ a"
     proof
       assume "x = a"
       with 11 3 ANTISYM antisym_def[of r]
       show False by auto
     qed
     ultimately
     have "x ≠ a ∧ (x,a) ∈ r" by simp
    }
    ultimately show "x ∈ UnderS A" by (unfold UnderS_def, auto)
  qed
  (*  *)
  ultimately show ?thesis by blast
qed


subsubsection {* Properties of supr *}

lemma supr_Above:
assumes SUB: "B ≤ Field r" and ABOVE: "Above B ≠ {}"
shows "supr B ∈ Above B"
proof(unfold supr_def)
  have "Above B ≤ Field r"
  using Above_Field[of r] by auto
  thus "minim (Above B) ∈ Above B"
  using assms by (simp add: minim_in)
qed

lemma supr_greater:
assumes SUB: "B ≤ Field r" and ABOVE: "Above B ≠ {}" and
        IN: "b ∈ B"
shows "(b, supr B) ∈ r"
proof-
  from assms supr_Above
  have "supr B ∈ Above B" by simp
  with IN Above_def[of r] show ?thesis by simp
qed

lemma supr_least_Above:
assumes SUB: "B ≤ Field r" and
        ABOVE: "a ∈ Above B"
shows "(supr B, a) ∈ r"
proof(unfold supr_def)
  have "Above B ≤ Field r"
  using Above_Field[of r] by auto
  thus "(minim (Above B), a) ∈ r"
  using assms minim_least
  by simp
qed

lemma supr_least:
"⟦B ≤ Field r; a ∈ Field r; (⋀ b. b ∈ B ⟹ (b,a) ∈ r)⟧
 ⟹ (supr B, a) ∈ r"
by(auto simp add: supr_least_Above Above_def)

lemma equals_supr_Above:
assumes SUB: "B ≤ Field r" and ABV: "a ∈ Above B" and
        MINIM: "⋀ a'. a' ∈ Above B ⟹ (a,a') ∈ r"
shows "a = supr B"
proof(unfold supr_def)
  have "Above B ≤ Field r"
  using Above_Field[of r] by auto
  thus "a = minim (Above B)"
  using assms equals_minim by simp
qed

lemma equals_supr:
assumes SUB: "B ≤ Field r" and IN: "a ∈ Field r" and
        ABV: "⋀ b. b ∈ B ⟹ (b,a) ∈ r" and
        MINIM: "⋀ a'. ⟦ a' ∈ Field r; ⋀ b. b ∈ B ⟹ (b,a') ∈ r⟧ ⟹ (a,a') ∈ r"
shows "a = supr B"
proof-
  have "a ∈ Above B"
  unfolding Above_def using ABV IN by simp
  moreover
  have "⋀ a'. a' ∈ Above B ⟹ (a,a') ∈ r"
  unfolding Above_def using MINIM by simp
  ultimately show ?thesis
  using equals_supr_Above SUB by auto
qed

lemma supr_inField:
assumes "B ≤ Field r" and  "Above B ≠ {}"
shows "supr B ∈ Field r"
proof-
  have "supr B ∈ Above B" using supr_Above assms by simp
  thus ?thesis using assms Above_Field[of r] by auto
qed

lemma supr_above_Above:
assumes SUB: "B ≤ Field r" and  ABOVE: "Above B ≠ {}"
shows "Above B = above (supr B)"
proof(unfold Above_def above_def, auto)
  fix a assume "a ∈ Field r" "∀b ∈ B. (b,a) ∈ r"
  with supr_least assms
  show "(supr B, a) ∈ r" by auto
next
  fix b assume "(supr B, b) ∈ r"
  thus "b ∈ Field r"
  using REFL refl_on_def[of _ r] by auto
next
  fix a b
  assume 1: "(supr B, b) ∈ r" and 2: "a ∈ B"
  with assms supr_greater
  have "(a,supr B) ∈ r" by auto
  thus "(a,b) ∈ r"
  using 1 TRANS trans_def[of r] by blast
qed

lemma supr_under:
assumes IN: "a ∈ Field r"
shows "a = supr (under a)"
proof-
  have "under a ≤ Field r"
  using under_Field[of r] by auto
  moreover
  have "under a ≠ {}"
  using IN Refl_under_in[of r] REFL by auto
  moreover
  have "a ∈ Above (under a)"
  using in_Above_under[of _ r] IN by auto
  moreover
  have "∀a' ∈ Above (under a). (a,a') ∈ r"
  proof(unfold Above_def under_def, auto)
    fix a'
    assume "∀aa. (aa, a) ∈ r ⟶ (aa, a') ∈ r"
    hence "(a,a) ∈ r ⟶ (a,a') ∈ r" by blast
    moreover have "(a,a) ∈ r"
    using REFL IN by (auto simp add: refl_on_def)
    ultimately
    show  "(a, a') ∈ r" by (rule mp)
  qed
  ultimately show ?thesis
  using equals_supr_Above by auto
qed


subsubsection {* Properties of successor *}

lemma suc_least:
"⟦B ≤ Field r; a ∈ Field r; (⋀ b. b ∈ B ⟹ a ≠ b ∧ (b,a) ∈ r)⟧
 ⟹ (suc B, a) ∈ r"
by(auto simp add: suc_least_AboveS AboveS_def)

lemma equals_suc:
assumes SUB: "B ≤ Field r" and IN: "a ∈ Field r" and
 ABVS: "⋀ b. b ∈ B ⟹ a ≠ b ∧ (b,a) ∈ r" and
 MINIM: "⋀ a'. ⟦a' ∈ Field r; ⋀ b. b ∈ B ⟹ a' ≠ b ∧ (b,a') ∈ r⟧ ⟹ (a,a') ∈ r"
shows "a = suc B"
proof-
  have "a ∈ AboveS B"
  unfolding AboveS_def using ABVS IN by simp
  moreover
  have "⋀ a'. a' ∈ AboveS B ⟹ (a,a') ∈ r"
  unfolding AboveS_def using MINIM by simp
  ultimately show ?thesis
  using equals_suc_AboveS SUB by auto
qed

lemma suc_above_AboveS:
assumes SUB: "B ≤ Field r" and
        ABOVE: "AboveS B ≠ {}"
shows "AboveS B = above (suc B)"
proof(unfold AboveS_def above_def, auto)
  fix a assume "a ∈ Field r" "∀b ∈ B. a ≠ b ∧ (b,a) ∈ r"
  with suc_least assms
  show "(suc B,a) ∈ r" by auto
next
  fix b assume "(suc B, b) ∈ r"
  thus "b ∈ Field r"
  using REFL refl_on_def[of _ r] by auto
next
  fix a b
  assume 1: "(suc B, b) ∈ r" and 2: "a ∈ B"
  with assms suc_greater[of B a]
  have "(a,suc B) ∈ r" by auto
  thus "(a,b) ∈ r"
  using 1 TRANS trans_def[of r] by blast
next
  fix a
  assume 1: "(suc B, a) ∈ r" and 2: "a ∈ B"
  with assms suc_greater[of B a]
  have "(a,suc B) ∈ r" by auto
  moreover have "suc B ∈ Field r"
  using assms suc_inField by simp
  ultimately have "a = suc B"
  using 1 2 SUB ANTISYM antisym_def[of r] by auto
  thus False
  using assms suc_greater[of B a] 2 by auto
qed

lemma suc_singl_pred:
assumes IN: "a ∈ Field r" and ABOVE_NE: "aboveS a ≠ {}" and
        REL: "(a',suc {a}) ∈ r" and DIFF: "a' ≠ suc {a}"
shows "a' = a ∨ (a',a) ∈ r"
proof-
  have *: "suc {a} ∈ Field r ∧ a' ∈ Field r"
  using WELL REL well_order_on_domain by metis
  {assume **: "a' ≠ a"
   hence "(a,a') ∈ r ∨ (a',a) ∈ r"
   using TOTAL IN * by (auto simp add: total_on_def)
   moreover
   {assume "(a,a') ∈ r"
    with ** * assms WELL suc_least[of "{a}" a']
    have "(suc {a},a') ∈ r" by auto
    with REL DIFF * ANTISYM antisym_def[of r]
    have False by simp
   }
   ultimately have "(a',a) ∈ r"
   by blast
  }
  thus ?thesis by blast
qed

lemma under_underS_suc:
assumes IN: "a ∈ Field r" and ABV: "aboveS a ≠ {}"
shows "underS (suc {a}) = under a"
proof-
  have 1: "AboveS {a} ≠ {}"
  using ABV aboveS_AboveS_singl[of r] by auto
  have 2: "a ≠ suc {a} ∧ (a,suc {a}) ∈ r"
  using suc_greater[of "{a}" a] IN 1 by auto
  (*   *)
  have "underS (suc {a}) ≤ under a"
  proof(unfold underS_def under_def, auto)
    fix x assume *: "x ≠ suc {a}" and **: "(x,suc {a}) ∈ r"
    with suc_singl_pred[of a x] IN ABV
    have "x = a ∨ (x,a) ∈ r" by auto
    with REFL refl_on_def[of _ r] IN
    show "(x,a) ∈ r" by auto
  qed
  (*  *)
  moreover
  (*   *)
  have "under a ≤ underS (suc {a})"
  proof(unfold underS_def under_def, auto)
    assume "(suc {a}, a) ∈ r"
    with 2 ANTISYM antisym_def[of r]
    show False by auto
  next
    fix x assume *: "(x,a) ∈ r"
    with 2 TRANS trans_def[of r]
    show "(x,suc {a}) ∈ r" by blast
  (*  blast is often better than auto/auto for transitivity-like properties *)
  qed
  (*  *)
  ultimately show ?thesis by blast
qed


subsubsection {* Properties of order filters *}

lemma ofilter_Under[simp]:
assumes "A ≤ Field r"
shows "ofilter(Under A)"
proof(unfold ofilter_def, auto)
  fix x assume "x ∈ Under A"
  thus "x ∈ Field r"
  using Under_Field[of r] assms by auto
next
  fix a x
  assume "a ∈ Under A" and "x ∈ under a"
  thus "x ∈ Under A"
  using TRANS under_Under_trans[of r] by auto
qed

lemma ofilter_UnderS[simp]:
assumes "A ≤ Field r"
shows "ofilter(UnderS A)"
proof(unfold ofilter_def, auto)
  fix x assume "x ∈ UnderS A"
  thus "x ∈ Field r"
  using UnderS_Field[of r] assms by auto
next
  fix a x
  assume "a ∈ UnderS A" and "x ∈ under a"
  thus "x ∈ UnderS A"
  using TRANS ANTISYM under_UnderS_trans[of r] by auto
qed

lemma ofilter_Int[simp]: "⟦ofilter A; ofilter B⟧ ⟹ ofilter(A Int B)"
unfolding ofilter_def by blast

lemma ofilter_Un[simp]: "⟦ofilter A; ofilter B⟧ ⟹ ofilter(A ∪ B)"
unfolding ofilter_def by blast

lemma ofilter_INTER:
"⟦I ≠ {}; ⋀ i. i ∈ I ⟹ ofilter(A i)⟧ ⟹ ofilter (⋂i ∈ I. A i)"
unfolding ofilter_def by blast

lemma ofilter_Inter:
"⟦S ≠ {}; ⋀ A. A ∈ S ⟹ ofilter A⟧ ⟹ ofilter (⋂S)"
unfolding ofilter_def by blast

lemma ofilter_Union:
"(⋀ A. A ∈ S ⟹ ofilter A) ⟹ ofilter (⋃S)"
unfolding ofilter_def by blast

lemma ofilter_under_Union:
"ofilter A ⟹ A = ⋃{under a| a. a ∈ A}"
using ofilter_under_UNION [of A] by auto


subsubsection {* Other properties *}

lemma Trans_Under_regressive:
assumes NE: "A ≠ {}" and SUB: "A ≤ Field r"
shows "Under(Under A) ≤ Under A"
proof
  let ?a = "minim A"
  (*  Preliminary facts *)
  have 1: "minim A ∈ Under A"
  using assms minim_Under by auto
  have 2: "∀y ∈ A. (minim A, y) ∈ r"
  using assms minim_least by auto
  (* Main proof *)
  fix x assume "x ∈ Under(Under A)"
  with 1 have 1: "(x,minim A) ∈ r"
  using Under_def[of r] by auto
  with Field_def have "x ∈ Field r" by fastforce
  moreover
  {fix y assume *: "y ∈ A"
   hence "(x,y) ∈ r"
   using 1 2 TRANS trans_def[of r] by blast
   with Field_def have "(x,y) ∈ r" by auto
  }
  ultimately
  show "x ∈ Under A" unfolding Under_def by auto
qed

lemma ofilter_suc_Field:
assumes OF: "ofilter A" and NE: "A ≠ Field r"
shows "ofilter (A ∪ {suc A})"
proof-
  (* Preliminary facts *)
  have 1: "A ≤ Field r" using OF ofilter_def by auto
  hence 2: "AboveS A ≠ {}"
  using ofilter_AboveS_Field NE OF by blast
  from 1 2 suc_inField
  have 3: "suc A ∈ Field r" by auto
  (* Main proof *)
  show ?thesis
  proof(unfold ofilter_def, auto simp add: 1 3)
    fix a x
    assume "a ∈ A" "x ∈ under a" "x ∉ A"
    with OF ofilter_def have False by auto
    thus "x = suc A" by simp
  next
    fix x assume *: "x ∈ under (suc A)" and **: "x ∉ A"
    hence "x ∈ Field r" using under_def Field_def by fastforce
    with ** have "x ∈ AboveS A"
    using ofilter_AboveS_Field[of A] OF by auto
    hence "(suc A,x) ∈ r"
    using suc_least_AboveS by auto
    moreover
    have "(x,suc A) ∈ r" using * under_def[of r] by auto
    ultimately show "x = suc A"
    using ANTISYM antisym_def[of r] by auto
  qed
qed

(* FIXME: needed? *)
declare
  minim_in[simp]
  minim_inField[simp]
  minim_least[simp]
  under_ofilter[simp]
  underS_ofilter[simp]
  Field_ofilter[simp]

end

abbreviation "worec ≡ wo_rel.worec"
abbreviation "adm_wo ≡ wo_rel.adm_wo"
abbreviation "isMinim ≡ wo_rel.isMinim"
abbreviation "minim ≡ wo_rel.minim"
abbreviation "max2 ≡ wo_rel.max2"
abbreviation "supr ≡ wo_rel.supr"
abbreviation "suc ≡ wo_rel.suc"

end