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 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-
  have "minim A  A"
    using assms minim_in by auto
  then have "Under A  under (minim A)"
    by (simp add: Under_decr under_Under_singl)
  moreover have "under (minim A)  Under A"
    by (meson NE SUB TRANS minim_Under subset_eq under_Under_trans)
  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-
  have "minim A  A"
    using assms minim_in by auto
  then have "UnderS A  underS (minim A)"
    by (simp add: UnderS_decr underS_UnderS_singl)
  moreover have "underS (minim A)  UnderS A"
    by (meson ANTISYM NE SUB TRANS minim_Under subset_eq underS_Under_trans)
  ultimately show ?thesis by blast
qed


subsubsection ‹Properties of supr›

lemma supr_Above:
  assumes "Above B  {}"
  shows "supr B  Above B"
  by (simp add: assms Above_Field minim_in supr_def)

lemma supr_greater:
  assumes "Above B  {}" "b  B"
  shows "(b, supr B)  r"
  using assms Above_def supr_Above by fastforce

lemma supr_least_Above:
  assumes "a  Above B"
  shows "(supr B, a)  r"
  by (simp add: assms Above_Field minim_least supr_def)

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 "a  Above B" " a'. a'  Above B  (a,a')  r"
  shows "a = supr B"
  by (simp add: assms Above_Field equals_minim supr_def)

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 "Above B  {}"
  shows "supr B  Field r"
  by (simp add: Above_Field assms minim_inField supr_def)

lemma supr_above_Above:
  assumes SUB: "B  Field r" and  ABOVE: "Above B  {}"
  shows "Above B = above (supr B)"
  apply (clarsimp simp: Above_def above_def set_eq_iff)
  by (meson ABOVE FieldI2 SUB TRANS supr_greater supr_least transD)

lemma supr_under:
  assumes "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 assms Refl_under_in[of r] REFL by auto
  moreover
  have "a  Above (under a)"
    using in_Above_under[of _ r] assms by auto
  moreover
  have "a'  Above (under a). (a,a')  r"
    by (auto simp: Above_def above_def REFL Refl_under_in assms)
  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)"
  using assms
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 "(suc B, a)  r" and 2: "a  B"
  thus False
    by (metis ABOVE ANTISYM SUB antisymD suc_greater)
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 "AboveS {a}  {}"
    using ABV aboveS_AboveS_singl[of r] by auto
  then have 2: "a  suc {a}  (a,suc {a})  r"
    using suc_greater[of "{a}" a] IN  by auto
  have "underS (suc {a})  under a"
    using ABV IN REFL Refl_under_in underS_E under_def wo_rel.suc_singl_pred wo_rel_axioms by fastforce
  moreover
  have "under a  underS (suc {a})"
    by (simp add: "2" ANTISYM TRANS subsetI underS_I under_underS_trans)
  ultimately show ?thesis by blast
qed


subsubsection ‹Properties of order filters›

lemma ofilter_Under[simp]:
  assumes "A  Field r"
  shows "ofilter(Under A)"
  by (clarsimp simp: ofilter_def) (meson TRANS Under_Field subset_eq under_Under_trans)

lemma ofilter_UnderS[simp]:
  assumes "A  Field r"
  shows "ofilter(UnderS A)"
  by (clarsimp simp: ofilter_def) (meson ANTISYM TRANS UnderS_Field subset_eq under_UnderS_trans)

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"
  by (metis INT_E NE REFL Refl_under_Under SUB empty_iff minim_Under minim_Under_under subsetI)

lemma ofilter_suc_Field:
  assumes OF: "ofilter A" and NE: "A  Field r"
  shows "ofilter (A  {suc A})"
  by (metis NE OF REFL Refl_under_underS ofilter_underS_Field suc_underS under_ofilter)

(* 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