diff -r 3f0dfce0e27a -r b5c94200d081 src/HOL/BNF_Wellorder_Relation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Wellorder_Relation.thy	Mon Jan 20 18:24:55 2014 +0100
@@ -0,0 +1,642 @@
+(*  Title:      HOL/BNF_Wellorder_Relation.thy
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Well-order relations (BNF).
+*)
+
+header {* Well-Order Relations (BNF) *}
+
+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 \<equiv> Order_Relation.under r"
+abbreviation underS where "underS \<equiv> Order_Relation.underS r"
+abbreviation Under where "Under \<equiv> Order_Relation.Under r"
+abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r"
+abbreviation above where "above \<equiv> Order_Relation.above r"
+abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r"
+abbreviation Above where "Above \<equiv> Order_Relation.Above r"
+abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS 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: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> 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:
+"\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk>
+             \<Longrightarrow> phi a b"
+using TOTALS by auto
+
+
+lemma cases_Total3:
+"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b);
+              (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> 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: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
+shows "P a"
+proof-
+  have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x"
+  using IND by blast
+  thus "P a" using WF wf_induct[of "r - Id" P a] by blast
+qed
+
+
+definition
+worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+"worec F \<equiv> wfrec (r - Id) F"
+
+
+definition
+adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
+where
+"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> 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}, @{text "max2"},
+and the minimum {\em of a set}, @{text "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 @{text "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 \<Rightarrow> 'a \<Rightarrow> 'a"
+where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
+
+
+definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
+where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
+
+definition minim :: "'a set \<Rightarrow> 'a"
+where "minim A \<equiv> THE b. isMinim A b"
+
+
+definition supr :: "'a set \<Rightarrow> 'a"
+where "supr A \<equiv> minim (Above A)"
+
+definition suc :: "'a set \<Rightarrow> 'a"
+where "suc A \<equiv> minim (AboveS A)"
+
+definition ofilter :: "'a set \<Rightarrow> bool"
+where
+"ofilter A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under a \<le> A)"
+
+
+subsubsection {* Properties of max2 *}
+
+
+lemma max2_greater_among:
+assumes "a \<in> Field r" and "b \<in> Field r"
+shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
+proof-
+  {assume "(a,b) \<in> 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) \<in> r" using REFL  assms
+   by (auto simp add: refl_on_def)
+  }
+  moreover
+  {assume *: "a \<noteq> b \<and> (b,a) \<in> r"
+   hence "(a,b) \<notin> 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 \<in> Field r" and "b \<in> Field r"
+shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
+using assms by (auto simp add: max2_greater_among)
+
+
+lemma max2_among:
+assumes "a \<in> Field r" and "b \<in> Field r"
+shows "max2 a b \<in> {a, b}"
+using assms max2_greater_among[of a b] by simp
+
+
+lemma max2_equals1:
+assumes "a \<in> Field r" and "b \<in> Field r"
+shows "(max2 a b = a) = ((b,a) \<in> r)"
+using assms ANTISYM unfolding antisym_def using TOTALS
+by(auto simp add: max2_def max2_among)
+
+
+lemma max2_equals2:
+assumes "a \<in> Field r" and "b \<in> Field r"
+shows "(max2 a b = b) = ((a,b) \<in> 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 \<in> B"
+   using MINIM isMinim_def by simp
+   hence "(a',a) \<in> r"
+   using MINIM' isMinim_def by simp
+  }
+  moreover
+  {have "a' \<in> B"
+   using MINIM' isMinim_def by simp
+   hence "(a,a') \<in> 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 \<le> Field r" and NE: "B \<noteq> {}"
+shows "\<exists>b. isMinim B b"
+proof-
+  from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
+  *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
+  show ?thesis
+  proof(simp add: isMinim_def, rule exI[of _ b], auto)
+    show "b \<in> B" using * by simp
+  next
+    fix b' assume As: "b' \<in> B"
+    hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
+    (*  *)
+    from As  * have "b' = b \<or> (b',b) \<notin> r" by auto
+    moreover
+    {assume "b' = b"
+     hence "(b,b') \<in> r"
+     using ** REFL by (auto simp add: refl_on_def)
+    }
+    moreover
+    {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
+     hence "(b,b') \<in> r"
+     using ** TOTAL by (auto simp add: total_on_def)
+    }
+    ultimately show "(b,b') \<in> r" by blast
+  qed
+qed
+
+
+lemma minim_isMinim:
+assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
+shows "isMinim B (minim B)"
+proof-
+  let ?phi = "(\<lambda> b. isMinim B b)"
+  from assms Well_order_isMinim_exists
+  obtain b where *: "?phi b" by blast
+  moreover
+  have "\<And> b'. ?phi b' \<Longrightarrow> 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 \<le> Field r" and "B \<noteq> {}"
+shows "minim B \<in> 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 \<le> Field r" and "B \<noteq> {}"
+shows "minim B \<in> Field r"
+proof-
+  have "minim B \<in> B" using assms by (simp add: minim_in)
+  thus ?thesis using assms by blast
+qed
+
+
+lemma minim_least:
+assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
+shows "(minim B, b) \<in> 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 \<le> Field r" and IN: "a \<in> B" and
+        LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> 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 \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
+shows "suc B \<in> AboveS B"
+proof(unfold suc_def)
+  have "AboveS B \<le> Field r"
+  using AboveS_Field[of r] by auto
+  thus "minim (AboveS B) \<in> AboveS B"
+  using assms by (simp add: minim_in)
+qed
+
+
+lemma suc_greater:
+assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
+        IN: "b \<in> B"
+shows "suc B \<noteq> b \<and> (b,suc B) \<in> r"
+proof-
+  from assms suc_AboveS
+  have "suc B \<in> AboveS B" by simp
+  with IN AboveS_def[of r] show ?thesis by simp
+qed
+
+
+lemma suc_least_AboveS:
+assumes ABOVES: "a \<in> AboveS B"
+shows "(suc B,a) \<in> r"
+proof(unfold suc_def)
+  have "AboveS B \<le> Field r"
+  using AboveS_Field[of r] by auto
+  thus "(minim (AboveS B),a) \<in> r"
+  using assms minim_least by simp
+qed
+
+
+lemma suc_inField:
+assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
+shows "suc B \<in> Field r"
+proof-
+  have "suc B \<in> 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 \<le> Field r" and ABV: "a \<in> AboveS B" and
+        MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
+shows "a = suc B"
+proof(unfold suc_def)
+  have "AboveS B \<le> 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 \<in> Field r"
+shows "a = suc (underS a)"
+proof-
+  have "underS a \<le> Field r"
+  using underS_Field[of r] by auto
+  moreover
+  have "a \<in> AboveS (underS a)"
+  using in_AboveS_underS IN by fast
+  moreover
+  have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r"
+  proof(clarify)
+    fix a'
+    assume *: "a' \<in> AboveS (underS a)"
+    hence **: "a' \<in> Field r"
+    using AboveS_Field by fast
+    {assume "(a,a') \<notin> r"
+     hence "a' = a \<or> (a',a) \<in> r"
+     using TOTAL IN ** by (auto simp add: total_on_def)
+     moreover
+     {assume "a' = a"
+      hence "(a,a') \<in> r"
+      using REFL IN ** by (auto simp add: refl_on_def)
+     }
+     moreover
+     {assume "a' \<noteq> a \<and> (a',a) \<in> r"
+      hence "a' \<in> underS a"
+      unfolding underS_def by simp
+      hence "a' \<notin> AboveS (underS a)"
+      using AboveS_disjoint by fast
+      with * have False by simp
+     }
+     ultimately have "(a,a') \<in> r" by blast
+    }
+    thus  "(a, a') \<in> 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) \<in> r" "(x,aa) \<in> r"
+  thus "(x,a) \<in> 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) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
+  thus False
+  using ANTISYM antisym_def[of r] by blast
+next
+  fix aa x
+  assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
+  thus "(x,a) \<in> 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 = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
+proof
+  assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r"
+  thus "ofilter A"
+  by (auto simp: underS_ofilter Field_ofilter)
+next
+  assume *: "ofilter A"
+  let ?One = "(\<exists>a\<in>Field r. A = underS a)"
+  let ?Two = "(A = Field r)"
+  show "?One \<or> ?Two"
+  proof(cases ?Two, simp)
+    let ?B = "(Field r) - A"
+    let ?a = "minim ?B"
+    assume "A \<noteq> Field r"
+    moreover have "A \<le> Field r" using * ofilter_def by simp
+    ultimately have 1: "?B \<noteq> {}" by blast
+    hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast
+    have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast
+    hence 4: "?a \<notin> A" by blast
+    have 5: "A \<le> Field r" using * ofilter_def[of A] by auto
+    (*  *)
+    moreover
+    have "A = underS ?a"
+    proof
+      show "A \<le> underS ?a"
+      proof(unfold underS_def, auto simp add: 4)
+        fix x assume **: "x \<in> A"
+        hence 11: "x \<in> Field r" using 5 by auto
+        have 12: "x \<noteq> ?a" using 4 ** by auto
+        have 13: "under x \<le> A" using * ofilter_def ** by auto
+        {assume "(x,?a) \<notin> r"
+         hence "(?a,x) \<in> r"
+         using TOTAL total_on_def[of "Field r" r]
+               2 4 11 12 by auto
+         hence "?a \<in> under x" using under_def[of r] by auto
+         hence "?a \<in> A" using ** 13 by blast
+         with 4 have False by simp
+        }
+        thus "(x,?a) \<in> r" by blast
+      qed
+    next
+      show "underS ?a \<le> A"
+      proof(unfold underS_def, auto)
+        fix x
+        assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
+        hence 11: "x \<in> Field r" using Field_def by fastforce
+         {assume "x \<notin> A"
+          hence "x \<in> ?B" using 11 by auto
+          hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
+          hence False
+          using ANTISYM antisym_def[of r] ** *** by auto
+         }
+        thus "x \<in> A" by blast
+      qed
+    qed
+    ultimately have ?One using 2 by blast
+    thus ?thesis by simp
+  qed
+qed
+
+
+lemma ofilter_UNION:
+"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
+unfolding ofilter_def by blast
+
+
+lemma ofilter_under_UNION:
+assumes "ofilter A"
+shows "A = (\<Union> a \<in> A. under a)"
+proof
+  have "\<forall>a \<in> A. under a \<le> A"
+  using assms ofilter_def by auto
+  thus "(\<Union> a \<in> A. under a) \<le> A" by blast
+next
+  have "\<forall>a \<in> A. a \<in> under a"
+  using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
+  thus "A \<le> (\<Union> a \<in> A. under a)" by blast
+qed
+
+
+subsubsection{* Other properties *}
+
+
+lemma ofilter_linord:
+assumes OF1: "ofilter A" and OF2: "ofilter B"
+shows "A \<le> B \<or> B \<le> A"
+proof(cases "A = Field r")
+  assume Case1: "A = Field r"
+  hence "B \<le> A" using OF2 ofilter_def by auto
+  thus ?thesis by simp
+next
+  assume Case2: "A \<noteq> Field r"
+  with ofilter_underS_Field OF1 obtain a where
+  1: "a \<in> Field r \<and> A = underS a" by auto
+  show ?thesis
+  proof(cases "B = Field r")
+    assume Case21: "B = Field r"
+    hence "A \<le> B" using OF1 ofilter_def by auto
+    thus ?thesis by simp
+  next
+    assume Case22: "B \<noteq> Field r"
+    with ofilter_underS_Field OF2 obtain b where
+    2: "b \<in> Field r \<and> B = underS b" by auto
+    have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> 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) \<in> r"
+     with underS_incr[of r] TRANS ANTISYM 1 2
+     have "A \<le> B" by auto
+     hence ?thesis by auto
+    }
+    moreover
+     {assume "(b,a) \<in> r"
+     with underS_incr[of r] TRANS ANTISYM 1 2
+     have "B \<le> A" by auto
+     hence ?thesis by auto
+    }
+    ultimately show ?thesis by blast
+  qed
+qed
+
+
+lemma ofilter_AboveS_Field:
+assumes "ofilter A"
+shows "A \<union> (AboveS A) = Field r"
+proof
+  show "A \<union> (AboveS A) \<le> Field r"
+  using assms ofilter_def AboveS_Field[of r] by auto
+next
+  {fix x assume *: "x \<in> Field r" and **: "x \<notin> A"
+   {fix y assume ***: "y \<in> A"
+    with ** have 1: "y \<noteq> x" by auto
+    {assume "(y,x) \<notin> r"
+     moreover
+     have "y \<in> Field r" using assms ofilter_def *** by auto
+     ultimately have "(x,y) \<in> r"
+     using 1 * TOTAL total_on_def[of _ r] by auto
+     with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto
+     with ** have False by contradiction
+    }
+    hence "(y,x) \<in> r" by blast
+    with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto
+   }
+   with * have "x \<in> AboveS A" unfolding AboveS_def by auto
+  }
+  thus "Field r \<le> A \<union> (AboveS A)" by blast
+qed
+
+
+lemma suc_ofilter_in:
+assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
+        REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
+shows "b \<in> A"
+proof-
+  have *: "suc A \<in> Field r \<and> b \<in> Field r"
+  using WELL REL well_order_on_domain[of "Field r"] by auto
+  {assume **: "b \<notin> A"
+   hence "b \<in> AboveS A"
+   using OF * ofilter_AboveS_Field by auto
+   hence "(suc A, b) \<in> 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