Quelle  BNF_Wellorder_Relation.thy

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

lemma in_notinI:
  assumes "(j,i) ∉ r ∨ j = i" and "i ∈ Field r" and "j ∈ Field r"
  shows "(i,j) ∈ r" using assms max2_def max2_greater_among by fastforce

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

lemma isMinim_unique:
  assumes "isMinim B a" "isMinim B a'"
  shows "a = a'"
  using assms ANTISYM antisym_def[of r] by (auto simp: isMinim_def)

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
  have "∀b'. b' ∈ B ⟶ (b, b') ∈ r"
  proof
    fix b'
    show "b' ∈ B ⟶ (b, b') ∈ r"
    proof
      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 have "b' = b ==> (b, b') ∈ r"
        using ** REFL by (auto simp add: refl_on_def)
      moreover have "b' ≠ b ∧ (b',b) ∉ r ==> (b,b') ∈ r"
        using ** TOTAL by (auto simp add: total_on_def)
      ultimately show "(b,b') ∈ r" by blast
    qed
  qed
  then show ?thesis
    unfolding isMinim_def using * by auto
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"
  using assms minim_isMinim[of B] by (auto simp: isMinim_def)

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"
  using IN AboveS_def[of r] assms suc_AboveS by auto

lemma suc_least_AboveS:
  assumes ABOVES: "a ∈ AboveS B"
  shows "(suc B,a) ∈ r"
  using assms minim_least AboveS_Field[of r] by (auto simp: suc_def)

lemma suc_inField:
  assumes "B ≤ Field r" and "AboveS B ≠ {}"
  shows "suc B ∈ Field r"
  using suc_AboveS assms AboveS_Field[of r] by auto

lemma equals_suc_AboveS:
  assumes "B ≤ Field r" and "a ∈ AboveS B" and "∧ a'. a' ∈ AboveS B ==> (a,a') ∈ r"
  shows "a = suc B"
  using assms equals_minim AboveS_Field[of r B] by (auto simp: suc_def)

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)"
  using TRANS by (auto simp: ofilter_def under_def Field_iff trans_def)

lemma underS_ofilter: "ofilter (underS a)"
  unfolding ofilter_def underS_def under_def
proof safe
  fix b assume "(a, b) ∈ r" "(b, a) ∈ r" and DIFF: "b ≠ a"
  thus False
    using ANTISYM antisym_def[of r] by blast
next
  fix b x
  assume "(b,a) ∈ r" "b ≠ a" "(x,b) ∈ r"
  thus "(x,a) ∈ r"
    using TRANS trans_def[of r] by blast
next
  fix x
  assume "x ≠ a" and "(x, a) ∈ r"
  then show "x ∈ Field r"
    unfolding Field_def
    by auto
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)
    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
        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
        }
        then have "(x,?a) ∈ r" by blast
        thus "x ∈ underS ?a"
          unfolding underS_def by (auto simp add: 12)
      qed
    next
      show "underS ?a ≤ A"
      proof
        fix x
        assume **: "x ∈ underS ?a"
        hence 11: "x ∈ Field r"
          using Field_def unfolding underS_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] ** unfolding underS_def by auto
        }
        thus "x ∈ A" by blast
      qed
    qed
    ultimately have ?One using 2 by blast
    thus ?thesis by simp
  next
    assume "A = Field r"
    then show ?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