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.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