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
  well-order relations. Note that we consider well-order relations
  {\em non-strict relations},
 .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,
  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}
 -order relations.
  minor variations of those for well-founded relations, they will be useful
  doing away with the tediousness of
  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‹
  define the successor {\em of a set}, and not of an element (the latter is of course
  particular case). Also, we define the maximum {\em of two elements}, ‹max2›,
  the minimum {\em of a set}, ‹minim› -- we chose these variants since we
  them the most useful for well-orders. The minimum is defined in terms of the
  relational operator ‹isMinim›. Then, supremum and successor are
  in terms of minimum as expected.
  minimum is only meaningful for non-empty sets, and the successor is only
  for sets for which strict upper bounds exist.
  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