src/HOL/BNF_Wellorder_Relation.thy
changeset 55101 57c875e488bd
parent 55059 ef2e0fb783c6
child 55173 5556470a02b7
     1.1 --- a/src/HOL/BNF_Wellorder_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
     1.3 @@ -11,13 +11,11 @@
     1.4  imports Order_Relation
     1.5  begin
     1.6  
     1.7 -
     1.8  text{* In this section, we develop basic concepts and results pertaining
     1.9  to well-order relations.  Note that we consider well-order relations
    1.10  as {\em non-strict relations},
    1.11  i.e., as containing the diagonals of their fields. *}
    1.12  
    1.13 -
    1.14  locale wo_rel =
    1.15    fixes r :: "'a rel"
    1.16    assumes WELL: "Well_order r"
    1.17 @@ -40,49 +38,39 @@
    1.18  
    1.19  subsection {* Auxiliaries *}
    1.20  
    1.21 -
    1.22  lemma REFL: "Refl r"
    1.23  using WELL order_on_defs[of _ r] by auto
    1.24  
    1.25 -
    1.26  lemma TRANS: "trans r"
    1.27  using WELL order_on_defs[of _ r] by auto
    1.28  
    1.29 -
    1.30  lemma ANTISYM: "antisym r"
    1.31  using WELL order_on_defs[of _ r] by auto
    1.32  
    1.33 -
    1.34  lemma TOTAL: "Total r"
    1.35  using WELL order_on_defs[of _ r] by auto
    1.36  
    1.37 -
    1.38  lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r"
    1.39  using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force
    1.40  
    1.41 -
    1.42  lemma LIN: "Linear_order r"
    1.43  using WELL well_order_on_def[of _ r] by auto
    1.44  
    1.45 -
    1.46  lemma WF: "wf (r - Id)"
    1.47  using WELL well_order_on_def[of _ r] by auto
    1.48  
    1.49 -
    1.50  lemma cases_Total:
    1.51  "\<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>
    1.52               \<Longrightarrow> phi a b"
    1.53  using TOTALS by auto
    1.54  
    1.55 -
    1.56  lemma cases_Total3:
    1.57  "\<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);
    1.58                (a = b \<Longrightarrow> phi a b)\<rbrakk>  \<Longrightarrow> phi a b"
    1.59  using TOTALS by auto
    1.60  
    1.61  
    1.62 -subsection {* Well-founded induction and recursion adapted to non-strict well-order relations  *}
    1.63 -
    1.64 +subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
    1.65  
    1.66  text{* Here we provide induction and recursion principles specific to {\em non-strict}
    1.67  well-order relations.
    1.68 @@ -90,7 +78,6 @@
    1.69  for doing away with the tediousness of
    1.70  having to take out the diagonal each time in order to switch to a well-founded relation. *}
    1.71  
    1.72 -
    1.73  lemma well_order_induct:
    1.74  assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    1.75  shows "P a"
    1.76 @@ -100,19 +87,16 @@
    1.77    thus "P a" using WF wf_induct[of "r - Id" P a] by blast
    1.78  qed
    1.79  
    1.80 -
    1.81  definition
    1.82  worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.83  where
    1.84  "worec F \<equiv> wfrec (r - Id) F"
    1.85  
    1.86 -
    1.87  definition
    1.88  adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.89  where
    1.90  "adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x"
    1.91  
    1.92 -
    1.93  lemma worec_fixpoint:
    1.94  assumes ADM: "adm_wo H"
    1.95  shows "worec H = H (worec H)"
    1.96 @@ -127,8 +111,7 @@
    1.97  qed
    1.98  
    1.99  
   1.100 -subsection {* The notions of maximum, minimum, supremum, successor and order filter  *}
   1.101 -
   1.102 +subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
   1.103  
   1.104  text{*
   1.105  We define the successor {\em of a set}, and not of an element (the latter is of course
   1.106 @@ -141,18 +124,15 @@
   1.107  meaningful for sets for which strict upper bounds exist.
   1.108  Order filters for well-orders are also known as ``initial segments". *}
   1.109  
   1.110 -
   1.111  definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.112  where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
   1.113  
   1.114 -
   1.115  definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool"
   1.116  where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)"
   1.117  
   1.118  definition minim :: "'a set \<Rightarrow> 'a"
   1.119  where "minim A \<equiv> THE b. isMinim A b"
   1.120  
   1.121 -
   1.122  definition supr :: "'a set \<Rightarrow> 'a"
   1.123  where "supr A \<equiv> minim (Above A)"
   1.124  
   1.125 @@ -166,7 +146,6 @@
   1.126  
   1.127  subsubsection {* Properties of max2 *}
   1.128  
   1.129 -
   1.130  lemma max2_greater_among:
   1.131  assumes "a \<in> Field r" and "b \<in> Field r"
   1.132  shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}"
   1.133 @@ -191,26 +170,22 @@
   1.134    total_on_def[of "Field r" r] by blast
   1.135  qed
   1.136  
   1.137 -
   1.138  lemma max2_greater:
   1.139  assumes "a \<in> Field r" and "b \<in> Field r"
   1.140  shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r"
   1.141  using assms by (auto simp add: max2_greater_among)
   1.142  
   1.143 -
   1.144  lemma max2_among:
   1.145  assumes "a \<in> Field r" and "b \<in> Field r"
   1.146  shows "max2 a b \<in> {a, b}"
   1.147  using assms max2_greater_among[of a b] by simp
   1.148  
   1.149 -
   1.150  lemma max2_equals1:
   1.151  assumes "a \<in> Field r" and "b \<in> Field r"
   1.152  shows "(max2 a b = a) = ((b,a) \<in> r)"
   1.153  using assms ANTISYM unfolding antisym_def using TOTALS
   1.154  by(auto simp add: max2_def max2_among)
   1.155  
   1.156 -
   1.157  lemma max2_equals2:
   1.158  assumes "a \<in> Field r" and "b \<in> Field r"
   1.159  shows "(max2 a b = b) = ((a,b) \<in> r)"
   1.160 @@ -220,7 +195,6 @@
   1.161  
   1.162  subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
   1.163  
   1.164 -
   1.165  lemma isMinim_unique:
   1.166  assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
   1.167  shows "a = a'"
   1.168 @@ -240,7 +214,6 @@
   1.169    show ?thesis using ANTISYM antisym_def[of r] by blast
   1.170  qed
   1.171  
   1.172 -
   1.173  lemma Well_order_isMinim_exists:
   1.174  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   1.175  shows "\<exists>b. isMinim B b"
   1.176 @@ -269,7 +242,6 @@
   1.177    qed
   1.178  qed
   1.179  
   1.180 -
   1.181  lemma minim_isMinim:
   1.182  assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}"
   1.183  shows "isMinim B (minim B)"
   1.184 @@ -284,10 +256,8 @@
   1.185    unfolding minim_def using theI[of ?phi b] by blast
   1.186  qed
   1.187  
   1.188 -
   1.189  subsubsection{* Properties of minim *}
   1.190  
   1.191 -
   1.192  lemma minim_in:
   1.193  assumes "B \<le> Field r" and "B \<noteq> {}"
   1.194  shows "minim B \<in> B"
   1.195 @@ -297,7 +267,6 @@
   1.196    thus ?thesis by (simp add: isMinim_def)
   1.197  qed
   1.198  
   1.199 -
   1.200  lemma minim_inField:
   1.201  assumes "B \<le> Field r" and "B \<noteq> {}"
   1.202  shows "minim B \<in> Field r"
   1.203 @@ -306,7 +275,6 @@
   1.204    thus ?thesis using assms by blast
   1.205  qed
   1.206  
   1.207 -
   1.208  lemma minim_least:
   1.209  assumes  SUB: "B \<le> Field r" and IN: "b \<in> B"
   1.210  shows "(minim B, b) \<in> r"
   1.211 @@ -316,7 +284,6 @@
   1.212    thus ?thesis by (auto simp add: isMinim_def IN)
   1.213  qed
   1.214  
   1.215 -
   1.216  lemma equals_minim:
   1.217  assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and
   1.218          LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r"
   1.219 @@ -329,10 +296,8 @@
   1.220    using isMinim_unique by auto
   1.221  qed
   1.222  
   1.223 -
   1.224  subsubsection{* Properties of successor *}
   1.225  
   1.226 -
   1.227  lemma suc_AboveS:
   1.228  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
   1.229  shows "suc B \<in> AboveS B"
   1.230 @@ -343,7 +308,6 @@
   1.231    using assms by (simp add: minim_in)
   1.232  qed
   1.233  
   1.234 -
   1.235  lemma suc_greater:
   1.236  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and
   1.237          IN: "b \<in> B"
   1.238 @@ -354,7 +318,6 @@
   1.239    with IN AboveS_def[of r] show ?thesis by simp
   1.240  qed
   1.241  
   1.242 -
   1.243  lemma suc_least_AboveS:
   1.244  assumes ABOVES: "a \<in> AboveS B"
   1.245  shows "(suc B,a) \<in> r"
   1.246 @@ -365,7 +328,6 @@
   1.247    using assms minim_least by simp
   1.248  qed
   1.249  
   1.250 -
   1.251  lemma suc_inField:
   1.252  assumes "B \<le> Field r" and "AboveS B \<noteq> {}"
   1.253  shows "suc B \<in> Field r"
   1.254 @@ -375,7 +337,6 @@
   1.255    using assms AboveS_Field[of r] by auto
   1.256  qed
   1.257  
   1.258 -
   1.259  lemma equals_suc_AboveS:
   1.260  assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and
   1.261          MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r"
   1.262 @@ -388,7 +349,6 @@
   1.263    by simp
   1.264  qed
   1.265  
   1.266 -
   1.267  lemma suc_underS:
   1.268  assumes IN: "a \<in> Field r"
   1.269  shows "a = suc (underS a)"
   1.270 @@ -432,7 +392,6 @@
   1.271  
   1.272  subsubsection {* Properties of order filters *}
   1.273  
   1.274 -
   1.275  lemma under_ofilter:
   1.276  "ofilter (under a)"
   1.277  proof(unfold ofilter_def under_def, auto simp add: Field_def)
   1.278 @@ -442,7 +401,6 @@
   1.279    using TRANS trans_def[of r] by blast
   1.280  qed
   1.281  
   1.282 -
   1.283  lemma underS_ofilter:
   1.284  "ofilter (underS a)"
   1.285  proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
   1.286 @@ -456,12 +414,10 @@
   1.287    using TRANS trans_def[of r] by blast
   1.288  qed
   1.289  
   1.290 -
   1.291  lemma Field_ofilter:
   1.292  "ofilter (Field r)"
   1.293  by(unfold ofilter_def under_def, auto simp add: Field_def)
   1.294  
   1.295 -
   1.296  lemma ofilter_underS_Field:
   1.297  "ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))"
   1.298  proof
   1.299 @@ -523,12 +479,10 @@
   1.300    qed
   1.301  qed
   1.302  
   1.303 -
   1.304  lemma ofilter_UNION:
   1.305  "(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
   1.306  unfolding ofilter_def by blast
   1.307  
   1.308 -
   1.309  lemma ofilter_under_UNION:
   1.310  assumes "ofilter A"
   1.311  shows "A = (\<Union> a \<in> A. under a)"
   1.312 @@ -542,10 +496,8 @@
   1.313    thus "A \<le> (\<Union> a \<in> A. under a)" by blast
   1.314  qed
   1.315  
   1.316 -
   1.317  subsubsection{* Other properties *}
   1.318  
   1.319 -
   1.320  lemma ofilter_linord:
   1.321  assumes OF1: "ofilter A" and OF2: "ofilter B"
   1.322  shows "A \<le> B \<or> B \<le> A"
   1.323 @@ -587,7 +539,6 @@
   1.324    qed
   1.325  qed
   1.326  
   1.327 -
   1.328  lemma ofilter_AboveS_Field:
   1.329  assumes "ofilter A"
   1.330  shows "A \<union> (AboveS A) = Field r"
   1.331 @@ -614,7 +565,6 @@
   1.332    thus "Field r \<le> A \<union> (AboveS A)" by blast
   1.333  qed
   1.334  
   1.335 -
   1.336  lemma suc_ofilter_in:
   1.337  assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and
   1.338          REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A"
   1.339 @@ -633,10 +583,6 @@
   1.340    thus ?thesis by blast
   1.341  qed
   1.342  
   1.343 -
   1.344 -
   1.345  end (* context wo_rel *)
   1.346  
   1.347 -
   1.348 -
   1.349  end