Theory BNF_Wellorder_Relation

theory BNF_Wellorder_Relation
imports Order_Relation
(*  Title:      HOL/BNF_Wellorder_Relation.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Well-order relations as needed by bounded natural functors.
*)

section ‹Well-Order Relations as Needed by Bounded Natural Functors›

theory BNF_Wellorder_Relation
imports Order_Relation
begin

text‹In this section, we develop basic concepts and results pertaining
to well-order relations.  Note that we consider well-order relations
as {\em non-strict relations},
i.e., as containing the diagonals of their fields.›

locale wo_rel =
  fixes r :: "'a rel"
  assumes WELL: "Well_order r"
begin

text‹The following context encompasses all this section. In other words,
for the whole section, we consider a fixed well-order relation @{term "r"}.›

(* context wo_rel  *)

abbreviation under where "under ≡ Order_Relation.under r"
abbreviation underS where "underS ≡ Order_Relation.underS r"
abbreviation Under where "Under ≡ Order_Relation.Under r"
abbreviation UnderS where "UnderS ≡ Order_Relation.UnderS r"
abbreviation above where "above ≡ Order_Relation.above r"
abbreviation aboveS where "aboveS ≡ Order_Relation.aboveS r"
abbreviation Above where "Above ≡ Order_Relation.Above r"
abbreviation AboveS where "AboveS ≡ Order_Relation.AboveS r"
abbreviation ofilter where "ofilter ≡ Order_Relation.ofilter r"
lemmas ofilter_def = Order_Relation.ofilter_def[of r]


subsection ‹Auxiliaries›

lemma REFL: "Refl r"
using WELL order_on_defs[of _ r] by auto

lemma TRANS: "trans r"
using WELL order_on_defs[of _ r] by auto

lemma ANTISYM: "antisym r"
using WELL order_on_defs[of _ r] by auto

lemma TOTAL: "Total r"
using WELL order_on_defs[of _ r] by auto

lemma TOTALS: "∀a ∈ Field r. ∀b ∈ Field r. (a,b) ∈ r ∨ (b,a) ∈ r"
using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force

lemma LIN: "Linear_order r"
using WELL well_order_on_def[of _ r] by auto

lemma WF: "wf (r - Id)"
using WELL well_order_on_def[of _ r] by auto

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

lemma cases_Total3:
"⋀ phi a b. ⟦{a,b} ≤ Field r; ((a,b) ∈ r - Id ∨ (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›

text‹Here we provide induction and recursion principles specific to {\em non-strict}
well-order relations.
Although minor variations of those for well-founded relations, they will be useful
for doing away with the tediousness of
having to take out the diagonal each time in order to switch to a well-founded relation.›

lemma well_order_induct:
assumes IND: "⋀x. ∀y. y ≠ x ∧ (y, x) ∈ r ⟶ P y ⟹ P x"
shows "P a"
proof-
  have "⋀x. ∀y. (y, x) ∈ r - Id ⟶ P y ⟹ P x"
  using IND by blast
  thus "P a" using WF wf_induct[of "r - Id" P a] by blast
qed

definition
worec :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ 'a ⇒ 'b"
where
"worec F ≡ wfrec (r - Id) F"

definition
adm_wo :: "(('a ⇒ 'b) ⇒ 'a ⇒ 'b) ⇒ bool"
where
"adm_wo H ≡ ∀f g x. (∀y ∈ underS x. f y = g y) ⟶ H f x = H g x"

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


subsection ‹The notions of maximum, minimum, supremum, successor and order filter›

text‹
We define the successor {\em of a set}, and not of an element (the latter is of course
a particular case).  Also, we define the maximum {\em of two elements}, ‹max2›,
and the minimum {\em of a set}, ‹minim› -- we chose these variants since we
consider them the most useful for well-orders.  The minimum is defined in terms of the
auxiliary relational operator ‹isMinim›.  Then, supremum and successor are
defined in terms of minimum as expected.
The minimum is only meaningful for non-empty sets, and the successor is only
meaningful for sets for which strict upper bounds exist.
Order filters for well-orders are also known as ``initial segments".›

definition max2 :: "'a ⇒ 'a ⇒ 'a"
where "max2 a b ≡ if (a,b) ∈ r then b else a"

definition isMinim :: "'a set ⇒ 'a ⇒ bool"
where "isMinim A b ≡ b ∈ A ∧ (∀a ∈ A. (b,a) ∈ r)"

definition minim :: "'a set ⇒ 'a"
where "minim A ≡ THE b. isMinim A b"

definition supr :: "'a set ⇒ 'a"
where "supr A ≡ minim (Above A)"

definition suc :: "'a set ⇒ 'a"
where "suc A ≡ minim (AboveS A)"


subsubsection ‹Properties of max2›

lemma max2_greater_among:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r ∧ max2 a b ∈ {a,b}"
proof-
  {assume "(a,b) ∈ r"
   hence ?thesis using max2_def assms REFL refl_on_def
   by (auto simp add: refl_on_def)
  }
  moreover
  {assume "a = b"
   hence "(a,b) ∈ r" using REFL  assms
   by (auto simp add: refl_on_def)
  }
  moreover
  {assume *: "a ≠ b ∧ (b,a) ∈ r"
   hence "(a,b) ∉ r" using ANTISYM
   by (auto simp add: antisym_def)
   hence ?thesis using * max2_def assms REFL refl_on_def
   by (auto simp add: refl_on_def)
  }
  ultimately show ?thesis using assms TOTAL
  total_on_def[of "Field r" r] by blast
qed

lemma max2_greater:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(a, max2 a b) ∈ r ∧ (b, max2 a b) ∈ r"
using assms by (auto simp add: max2_greater_among)

lemma max2_among:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "max2 a b ∈ {a, b}"
using assms max2_greater_among[of a b] by simp

lemma max2_equals1:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(max2 a b = a) = ((b,a) ∈ r)"
using assms ANTISYM unfolding antisym_def using TOTALS
by(auto simp add: max2_def max2_among)

lemma max2_equals2:
assumes "a ∈ Field r" and "b ∈ Field r"
shows "(max2 a b = b) = ((a,b) ∈ r)"
using assms ANTISYM unfolding antisym_def using TOTALS
unfolding max2_def by auto


subsubsection ‹Existence and uniqueness for isMinim and well-definedness of minim›

lemma isMinim_unique:
assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
shows "a = a'"
proof-
  {have "a ∈ B"
   using MINIM isMinim_def by simp
   hence "(a',a) ∈ r"
   using MINIM' isMinim_def by simp
  }
  moreover
  {have "a' ∈ B"
   using MINIM' isMinim_def by simp
   hence "(a,a') ∈ r"
   using MINIM isMinim_def by simp
  }
  ultimately
  show ?thesis using ANTISYM antisym_def[of r] by blast
qed

lemma Well_order_isMinim_exists:
assumes SUB: "B ≤ Field r" and NE: "B ≠ {}"
shows "∃b. isMinim B b"
proof-
  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
  *: "b ∈ B ∧ (∀b'. b' ≠ b ∧ (b',b) ∈ r ⟶ b' ∉ B)" by auto
  show ?thesis
  proof(simp add: isMinim_def, rule exI[of _ b], auto)
    show "b ∈ B" using * by simp
  next
    fix b' assume As: "b' ∈ B"
    hence **: "b ∈ Field r ∧ b' ∈ Field r" using As SUB * by auto
    (*  *)
    from As  * have "b' = b ∨ (b',b) ∉ r" by auto
    moreover
    {assume "b' = b"
     hence "(b,b') ∈ r"
     using ** REFL by (auto simp add: refl_on_def)
    }
    moreover
    {assume "b' ≠ b ∧ (b',b) ∉ r"
     hence "(b,b') ∈ r"
     using ** TOTAL by (auto simp add: total_on_def)
    }
    ultimately show "(b,b') ∈ r" by blast
  qed
qed

lemma minim_isMinim:
assumes SUB: "B ≤ Field r" and NE: "B ≠ {}"
shows "isMinim B (minim B)"
proof-
  let ?phi = "(λ b. isMinim B b)"
  from assms Well_order_isMinim_exists
  obtain b where *: "?phi b" by blast
  moreover
  have "⋀ b'. ?phi b' ⟹ b' = b"
  using isMinim_unique * by auto
  ultimately show ?thesis
  unfolding minim_def using theI[of ?phi b] by blast
qed

subsubsection‹Properties of minim›

lemma minim_in:
assumes "B ≤ Field r" and "B ≠ {}"
shows "minim B ∈ B"
proof-
  from minim_isMinim[of B] assms
  have "isMinim B (minim B)" by simp
  thus ?thesis by (simp add: isMinim_def)
qed

lemma minim_inField:
assumes "B ≤ Field r" and "B ≠ {}"
shows "minim B ∈ Field r"
proof-
  have "minim B ∈ B" using assms by (simp add: minim_in)
  thus ?thesis using assms by blast
qed

lemma minim_least:
assumes  SUB: "B ≤ Field r" and IN: "b ∈ B"
shows "(minim B, b) ∈ r"
proof-
  from minim_isMinim[of B] assms
  have "isMinim B (minim B)" by auto
  thus ?thesis by (auto simp add: isMinim_def IN)
qed

lemma equals_minim:
assumes SUB: "B ≤ Field r" and IN: "a ∈ B" and
        LEAST: "⋀ b. b ∈ B ⟹ (a,b) ∈ r"
shows "a = minim B"
proof-
  from minim_isMinim[of B] assms
  have "isMinim B (minim B)" by auto
  moreover have "isMinim B a" using IN LEAST isMinim_def by auto
  ultimately show ?thesis
  using isMinim_unique by auto
qed

subsubsection‹Properties of successor›

lemma suc_AboveS:
assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}"
shows "suc B ∈ AboveS B"
proof(unfold suc_def)
  have "AboveS B ≤ Field r"
  using AboveS_Field[of r] by auto
  thus "minim (AboveS B) ∈ AboveS B"
  using assms by (simp add: minim_in)
qed

lemma suc_greater:
assumes SUB: "B ≤ Field r" and ABOVES: "AboveS B ≠ {}" and
        IN: "b ∈ B"
shows "suc B ≠ b ∧ (b,suc B) ∈ r"
proof-
  from assms suc_AboveS
  have "suc B ∈ AboveS B" by simp
  with IN AboveS_def[of r] show ?thesis by simp
qed

lemma suc_least_AboveS:
assumes ABOVES: "a ∈ AboveS B"
shows "(suc B,a) ∈ r"
proof(unfold suc_def)
  have "AboveS B ≤ Field r"
  using AboveS_Field[of r] by auto
  thus "(minim (AboveS B),a) ∈ r"
  using assms minim_least by simp
qed

lemma suc_inField:
assumes "B ≤ Field r" and "AboveS B ≠ {}"
shows "suc B ∈ Field r"
proof-
  have "suc B ∈ AboveS B" using suc_AboveS assms by simp
  thus ?thesis
  using assms AboveS_Field[of r] by auto
qed

lemma equals_suc_AboveS:
assumes SUB: "B ≤ Field r" and ABV: "a ∈ AboveS B" and
        MINIM: "⋀ a'. a' ∈ AboveS B ⟹ (a,a') ∈ r"
shows "a = suc B"
proof(unfold suc_def)
  have "AboveS B ≤ Field r"
  using AboveS_Field[of r B] by auto
  thus "a = minim (AboveS B)"
  using assms equals_minim
  by simp
qed

lemma suc_underS:
assumes IN: "a ∈ Field r"
shows "a = suc (underS a)"
proof-
  have "underS a ≤ Field r"
  using underS_Field[of r] by auto
  moreover
  have "a ∈ AboveS (underS a)"
  using in_AboveS_underS IN by fast
  moreover
  have "∀a' ∈ AboveS (underS a). (a,a') ∈ r"
  proof(clarify)
    fix a'
    assume *: "a' ∈ AboveS (underS a)"
    hence **: "a' ∈ Field r"
    using AboveS_Field by fast
    {assume "(a,a') ∉ r"
     hence "a' = a ∨ (a',a) ∈ r"
     using TOTAL IN ** by (auto simp add: total_on_def)
     moreover
     {assume "a' = a"
      hence "(a,a') ∈ r"
      using REFL IN ** by (auto simp add: refl_on_def)
     }
     moreover
     {assume "a' ≠ a ∧ (a',a) ∈ r"
      hence "a' ∈ underS a"
      unfolding underS_def by simp
      hence "a' ∉ AboveS (underS a)"
      using AboveS_disjoint by fast
      with * have False by simp
     }
     ultimately have "(a,a') ∈ r" by blast
    }
    thus  "(a, a') ∈ r" by blast
  qed
  ultimately show ?thesis
  using equals_suc_AboveS by auto
qed


subsubsection ‹Properties of order filters›

lemma under_ofilter:
"ofilter (under a)"
proof(unfold ofilter_def under_def, auto simp add: Field_def)
  fix aa x
  assume "(aa,a) ∈ r" "(x,aa) ∈ r"
  thus "(x,a) ∈ r"
  using TRANS trans_def[of r] by blast
qed

lemma underS_ofilter:
"ofilter (underS a)"
proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
  fix aa assume "(a, aa) ∈ r" "(aa, a) ∈ r" and DIFF: "aa ≠ a"
  thus False
  using ANTISYM antisym_def[of r] by blast
next
  fix aa x
  assume "(aa,a) ∈ r" "aa ≠ a" "(x,aa) ∈ r"
  thus "(x,a) ∈ r"
  using TRANS trans_def[of r] by blast
qed

lemma Field_ofilter:
"ofilter (Field r)"
by(unfold ofilter_def under_def, auto simp add: Field_def)

lemma ofilter_underS_Field:
"ofilter A = ((∃a ∈ Field r. A = underS a) ∨ (A = Field r))"
proof
  assume "(∃a∈Field r. A = underS a) ∨ A = Field r"
  thus "ofilter A"
  by (auto simp: underS_ofilter Field_ofilter)
next
  assume *: "ofilter A"
  let ?One = "(∃a∈Field r. A = underS a)"
  let ?Two = "(A = Field r)"
  show "?One ∨ ?Two"
  proof(cases ?Two, simp)
    let ?B = "(Field r) - A"
    let ?a = "minim ?B"
    assume "A ≠ Field r"
    moreover have "A ≤ Field r" using * ofilter_def by simp
    ultimately have 1: "?B ≠ {}" by blast
    hence 2: "?a ∈ Field r" using minim_inField[of ?B] by blast
    have 3: "?a ∈ ?B" using minim_in[of ?B] 1 by blast
    hence 4: "?a ∉ A" by blast
    have 5: "A ≤ Field r" using * ofilter_def by auto
    (*  *)
    moreover
    have "A = underS ?a"
    proof
      show "A ≤ underS ?a"
      proof(unfold underS_def, auto simp add: 4)
        fix x assume **: "x ∈ A"
        hence 11: "x ∈ Field r" using 5 by auto
        have 12: "x ≠ ?a" using 4 ** by auto
        have 13: "under x ≤ A" using * ofilter_def ** by auto
        {assume "(x,?a) ∉ r"
         hence "(?a,x) ∈ r"
         using TOTAL total_on_def[of "Field r" r]
               2 4 11 12 by auto
         hence "?a ∈ under x" using under_def[of r] by auto
         hence "?a ∈ A" using ** 13 by blast
         with 4 have False by simp
        }
        thus "(x,?a) ∈ r" by blast
      qed
    next
      show "underS ?a ≤ A"
      proof(unfold underS_def, auto)
        fix x
        assume **: "x ≠ ?a" and ***: "(x,?a) ∈ r"
        hence 11: "x ∈ Field r" using Field_def by fastforce
         {assume "x ∉ A"
          hence "x ∈ ?B" using 11 by auto
          hence "(?a,x) ∈ r" using 3 minim_least[of ?B x] by blast
          hence False
          using ANTISYM antisym_def[of r] ** *** by auto
         }
        thus "x ∈ A" by blast
      qed
    qed
    ultimately have ?One using 2 by blast
    thus ?thesis by simp
  qed
qed

lemma ofilter_UNION:
"(⋀ i. i ∈ I ⟹ ofilter(A i)) ⟹ ofilter (⋃i ∈ I. A i)"
unfolding ofilter_def by blast

lemma ofilter_under_UNION:
assumes "ofilter A"
shows "A = (⋃a ∈ A. under a)"
proof
  have "∀a ∈ A. under a ≤ A"
  using assms ofilter_def by auto
  thus "(⋃a ∈ A. under a) ≤ A" by blast
next
  have "∀a ∈ A. a ∈ under a"
  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
  thus "A ≤ (⋃a ∈ A. under a)" by blast
qed

subsubsection‹Other properties›

lemma ofilter_linord:
assumes OF1: "ofilter A" and OF2: "ofilter B"
shows "A ≤ B ∨ B ≤ A"
proof(cases "A = Field r")
  assume Case1: "A = Field r"
  hence "B ≤ A" using OF2 ofilter_def by auto
  thus ?thesis by simp
next
  assume Case2: "A ≠ Field r"
  with ofilter_underS_Field OF1 obtain a where
  1: "a ∈ Field r ∧ A = underS a" by auto
  show ?thesis
  proof(cases "B = Field r")
    assume Case21: "B = Field r"
    hence "A ≤ B" using OF1 ofilter_def by auto
    thus ?thesis by simp
  next
    assume Case22: "B ≠ Field r"
    with ofilter_underS_Field OF2 obtain b where
    2: "b ∈ Field r ∧ B = underS b" by auto
    have "a = b ∨ (a,b) ∈ r ∨ (b,a) ∈ r"
    using 1 2 TOTAL total_on_def[of _ r] by auto
    moreover
    {assume "a = b" with 1 2 have ?thesis by auto
    }
    moreover
    {assume "(a,b) ∈ r"
     with underS_incr[of r] TRANS ANTISYM 1 2
     have "A ≤ B" by auto
     hence ?thesis by auto
    }
    moreover
     {assume "(b,a) ∈ r"
     with underS_incr[of r] TRANS ANTISYM 1 2
     have "B ≤ A" by auto
     hence ?thesis by auto
    }
    ultimately show ?thesis by blast
  qed
qed

lemma ofilter_AboveS_Field:
assumes "ofilter A"
shows "A ∪ (AboveS A) = Field r"
proof
  show "A ∪ (AboveS A) ≤ Field r"
  using assms ofilter_def AboveS_Field[of r] by auto
next
  {fix x assume *: "x ∈ Field r" and **: "x ∉ A"
   {fix y assume ***: "y ∈ A"
    with ** have 1: "y ≠ x" by auto
    {assume "(y,x) ∉ r"
     moreover
     have "y ∈ Field r" using assms ofilter_def *** by auto
     ultimately have "(x,y) ∈ r"
     using 1 * TOTAL total_on_def[of _ r] by auto
     with *** assms ofilter_def under_def[of r] have "x ∈ A" by auto
     with ** have False by contradiction
    }
    hence "(y,x) ∈ r" by blast
    with 1 have "y ≠ x ∧ (y,x) ∈ r" by auto
   }
   with * have "x ∈ AboveS A" unfolding AboveS_def by auto
  }
  thus "Field r ≤ A ∪ (AboveS A)" by blast
qed

lemma suc_ofilter_in:
assumes OF: "ofilter A" and ABOVE_NE: "AboveS A ≠ {}" and
        REL: "(b,suc A) ∈ r" and DIFF: "b ≠ suc A"
shows "b ∈ A"
proof-
  have *: "suc A ∈ Field r ∧ b ∈ Field r"
  using WELL REL well_order_on_domain[of "Field r"] by auto
  {assume **: "b ∉ A"
   hence "b ∈ AboveS A"
   using OF * ofilter_AboveS_Field by auto
   hence "(suc A, b) ∈ r"
   using suc_least_AboveS by auto
   hence False using REL DIFF ANTISYM *
   by (auto simp add: antisym_def)
  }
  thus ?thesis by blast
qed

end (* context wo_rel *)

end