1.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 16:20:17 2014 +0100
1.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_FP.thy Thu Jan 16 16:33:19 2014 +0100
1.3 @@ -8,7 +8,7 @@
1.4 header {* Well-Order Embeddings (FP) *}
1.5
1.6 theory Wellorder_Embedding_FP
1.7 -imports "~~/src/HOL/Library/Zorn" Fun_More_FP Wellorder_Relation_FP
1.8 +imports Zorn Fun_More_FP Wellorder_Relation_FP
1.9 begin
1.10
1.11
2.1 --- a/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 16:20:17 2014 +0100
2.2 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy Thu Jan 16 16:33:19 2014 +0100
2.3 @@ -5,7 +5,7 @@
2.4 header {* Extending Well-founded Relations to Wellorders *}
2.5
2.6 theory Wellorder_Extension
2.7 -imports "~~/src/HOL/Library/Zorn" Order_Union
2.8 +imports Zorn Order_Union
2.9 begin
2.10
2.11 subsection {* Extending Well-founded Relations to Wellorders *}
3.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy Thu Jan 16 16:20:17 2014 +0100
3.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Thu Jan 16 16:33:19 2014 +0100
3.3 @@ -5,7 +5,7 @@
3.4 header {* Vector spaces *}
3.5
3.6 theory Vector_Space
3.7 -imports Complex_Main Bounds "~~/src/HOL/Library/Zorn"
3.8 +imports Complex_Main Bounds
3.9 begin
3.10
3.11 subsection {* Signature *}
4.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy Thu Jan 16 16:20:17 2014 +0100
4.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy Thu Jan 16 16:33:19 2014 +0100
4.3 @@ -5,7 +5,7 @@
4.4 header {* Zorn's Lemma *}
4.5
4.6 theory Zorn_Lemma
4.7 -imports "~~/src/HOL/Library/Zorn"
4.8 +imports Main
4.9 begin
4.10
4.11 text {*
5.1 --- a/src/HOL/Library/Library.thy Thu Jan 16 16:20:17 2014 +0100
5.2 +++ b/src/HOL/Library/Library.thy Thu Jan 16 16:33:19 2014 +0100
5.3 @@ -64,7 +64,6 @@
5.4 Sum_of_Squares
5.5 Transitive_Closure_Table
5.6 While_Combinator
5.7 - Zorn
5.8 begin
5.9 end
5.10 (*>*)
6.1 --- a/src/HOL/Library/Zorn.thy Thu Jan 16 16:20:17 2014 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,712 +0,0 @@
6.4 -(* Title: HOL/Library/Zorn.thy
6.5 - Author: Jacques D. Fleuriot
6.6 - Author: Tobias Nipkow, TUM
6.7 - Author: Christian Sternagel, JAIST
6.8 -
6.9 -Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
6.10 -The well-ordering theorem.
6.11 -*)
6.12 -
6.13 -header {* Zorn's Lemma *}
6.14 -
6.15 -theory Zorn
6.16 -imports Main
6.17 -begin
6.18 -
6.19 -subsection {* Zorn's Lemma for the Subset Relation *}
6.20 -
6.21 -subsubsection {* Results that do not require an order *}
6.22 -
6.23 -text {*Let @{text P} be a binary predicate on the set @{text A}.*}
6.24 -locale pred_on =
6.25 - fixes A :: "'a set"
6.26 - and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
6.27 -begin
6.28 -
6.29 -abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) where
6.30 - "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
6.31 -
6.32 -text {*A chain is a totally ordered subset of @{term A}.*}
6.33 -definition chain :: "'a set \<Rightarrow> bool" where
6.34 - "chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
6.35 -
6.36 -text {*We call a chain that is a proper superset of some set @{term X},
6.37 -but not necessarily a chain itself, a superchain of @{term X}.*}
6.38 -abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50) where
6.39 - "X <c C \<equiv> chain C \<and> X \<subset> C"
6.40 -
6.41 -text {*A maximal chain is a chain that does not have a superchain.*}
6.42 -definition maxchain :: "'a set \<Rightarrow> bool" where
6.43 - "maxchain C \<longleftrightarrow> chain C \<and> \<not> (\<exists>S. C <c S)"
6.44 -
6.45 -text {*We define the successor of a set to be an arbitrary
6.46 -superchain, if such exists, or the set itself, otherwise.*}
6.47 -definition suc :: "'a set \<Rightarrow> 'a set" where
6.48 - "suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))"
6.49 -
6.50 -lemma chainI [Pure.intro?]:
6.51 - "\<lbrakk>C \<subseteq> A; \<And>x y. \<lbrakk>x \<in> C; y \<in> C\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> chain C"
6.52 - unfolding chain_def by blast
6.53 -
6.54 -lemma chain_total:
6.55 - "chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
6.56 - by (simp add: chain_def)
6.57 -
6.58 -lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X"
6.59 - by (simp add: suc_def)
6.60 -
6.61 -lemma maxchain_suc [simp]: "maxchain X \<Longrightarrow> suc X = X"
6.62 - by (simp add: suc_def)
6.63 -
6.64 -lemma suc_subset: "X \<subseteq> suc X"
6.65 - by (auto simp: suc_def maxchain_def intro: someI2)
6.66 -
6.67 -lemma chain_empty [simp]: "chain {}"
6.68 - by (auto simp: chain_def)
6.69 -
6.70 -lemma not_maxchain_Some:
6.71 - "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)"
6.72 - by (rule someI_ex) (auto simp: maxchain_def)
6.73 -
6.74 -lemma suc_not_equals:
6.75 - "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
6.76 - by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
6.77 -
6.78 -lemma subset_suc:
6.79 - assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
6.80 - using assms by (rule subset_trans) (rule suc_subset)
6.81 -
6.82 -text {*We build a set @{term \<C>} that is closed under applications
6.83 -of @{term suc} and contains the union of all its subsets.*}
6.84 -inductive_set suc_Union_closed ("\<C>") where
6.85 - suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>" |
6.86 - Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
6.87 -
6.88 -text {*Since the empty set as well as the set itself is a subset of
6.89 -every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and
6.90 -@{term "\<Union>\<C> \<in> \<C>"}.*}
6.91 -lemma
6.92 - suc_Union_closed_empty: "{} \<in> \<C>" and
6.93 - suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>"
6.94 - using Union [of "{}"] and Union [of "\<C>"] by simp+
6.95 -text {*Thus closure under @{term suc} will hit a maximal chain
6.96 -eventually, as is shown below.*}
6.97 -
6.98 -lemma suc_Union_closed_induct [consumes 1, case_names suc Union,
6.99 - induct pred: suc_Union_closed]:
6.100 - assumes "X \<in> \<C>"
6.101 - and "\<And>X. \<lbrakk>X \<in> \<C>; Q X\<rbrakk> \<Longrightarrow> Q (suc X)"
6.102 - and "\<And>X. \<lbrakk>X \<subseteq> \<C>; \<forall>x\<in>X. Q x\<rbrakk> \<Longrightarrow> Q (\<Union>X)"
6.103 - shows "Q X"
6.104 - using assms by (induct) blast+
6.105 -
6.106 -lemma suc_Union_closed_cases [consumes 1, case_names suc Union,
6.107 - cases pred: suc_Union_closed]:
6.108 - assumes "X \<in> \<C>"
6.109 - and "\<And>Y. \<lbrakk>X = suc Y; Y \<in> \<C>\<rbrakk> \<Longrightarrow> Q"
6.110 - and "\<And>Y. \<lbrakk>X = \<Union>Y; Y \<subseteq> \<C>\<rbrakk> \<Longrightarrow> Q"
6.111 - shows "Q"
6.112 - using assms by (cases) simp+
6.113 -
6.114 -text {*On chains, @{term suc} yields a chain.*}
6.115 -lemma chain_suc:
6.116 - assumes "chain X" shows "chain (suc X)"
6.117 - using assms
6.118 - by (cases "\<not> chain X \<or> maxchain X")
6.119 - (force simp: suc_def dest: not_maxchain_Some)+
6.120 -
6.121 -lemma chain_sucD:
6.122 - assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
6.123 -proof -
6.124 - from `chain X` have *: "chain (suc X)" by (rule chain_suc)
6.125 - then have "suc X \<subseteq> A" unfolding chain_def by blast
6.126 - with * show ?thesis by blast
6.127 -qed
6.128 -
6.129 -lemma suc_Union_closed_total':
6.130 - assumes "X \<in> \<C>" and "Y \<in> \<C>"
6.131 - and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
6.132 - shows "X \<subseteq> Y \<or> suc Y \<subseteq> X"
6.133 - using `X \<in> \<C>`
6.134 -proof (induct)
6.135 - case (suc X)
6.136 - with * show ?case by (blast del: subsetI intro: subset_suc)
6.137 -qed blast
6.138 -
6.139 -lemma suc_Union_closed_subsetD:
6.140 - assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>"
6.141 - shows "X = Y \<or> suc Y \<subseteq> X"
6.142 - using assms(2-, 1)
6.143 -proof (induct arbitrary: Y)
6.144 - case (suc X)
6.145 - note * = `\<And>Y. \<lbrakk>Y \<in> \<C>; Y \<subseteq> X\<rbrakk> \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X`
6.146 - with suc_Union_closed_total' [OF `Y \<in> \<C>` `X \<in> \<C>`]
6.147 - have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast
6.148 - then show ?case
6.149 - proof
6.150 - assume "Y \<subseteq> X"
6.151 - with * and `Y \<in> \<C>` have "X = Y \<or> suc Y \<subseteq> X" by blast
6.152 - then show ?thesis
6.153 - proof
6.154 - assume "X = Y" then show ?thesis by simp
6.155 - next
6.156 - assume "suc Y \<subseteq> X"
6.157 - then have "suc Y \<subseteq> suc X" by (rule subset_suc)
6.158 - then show ?thesis by simp
6.159 - qed
6.160 - next
6.161 - assume "suc X \<subseteq> Y"
6.162 - with `Y \<subseteq> suc X` show ?thesis by blast
6.163 - qed
6.164 -next
6.165 - case (Union X)
6.166 - show ?case
6.167 - proof (rule ccontr)
6.168 - assume "\<not> ?thesis"
6.169 - with `Y \<subseteq> \<Union>X` obtain x y z
6.170 - where "\<not> suc Y \<subseteq> \<Union>X"
6.171 - and "x \<in> X" and "y \<in> x" and "y \<notin> Y"
6.172 - and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast
6.173 - with `X \<subseteq> \<C>` have "x \<in> \<C>" by blast
6.174 - from Union and `x \<in> X`
6.175 - have *: "\<And>y. \<lbrakk>y \<in> \<C>; y \<subseteq> x\<rbrakk> \<Longrightarrow> x = y \<or> suc y \<subseteq> x" by blast
6.176 - with suc_Union_closed_total' [OF `Y \<in> \<C>` `x \<in> \<C>`]
6.177 - have "Y \<subseteq> x \<or> suc x \<subseteq> Y" by blast
6.178 - then show False
6.179 - proof
6.180 - assume "Y \<subseteq> x"
6.181 - with * [OF `Y \<in> \<C>`] have "x = Y \<or> suc Y \<subseteq> x" by blast
6.182 - then show False
6.183 - proof
6.184 - assume "x = Y" with `y \<in> x` and `y \<notin> Y` show False by blast
6.185 - next
6.186 - assume "suc Y \<subseteq> x"
6.187 - with `x \<in> X` have "suc Y \<subseteq> \<Union>X" by blast
6.188 - with `\<not> suc Y \<subseteq> \<Union>X` show False by contradiction
6.189 - qed
6.190 - next
6.191 - assume "suc x \<subseteq> Y"
6.192 - moreover from suc_subset and `y \<in> x` have "y \<in> suc x" by blast
6.193 - ultimately show False using `y \<notin> Y` by blast
6.194 - qed
6.195 - qed
6.196 -qed
6.197 -
6.198 -text {*The elements of @{term \<C>} are totally ordered by the subset relation.*}
6.199 -lemma suc_Union_closed_total:
6.200 - assumes "X \<in> \<C>" and "Y \<in> \<C>"
6.201 - shows "X \<subseteq> Y \<or> Y \<subseteq> X"
6.202 -proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y")
6.203 - case True
6.204 - with suc_Union_closed_total' [OF assms]
6.205 - have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast
6.206 - then show ?thesis using suc_subset [of Y] by blast
6.207 -next
6.208 - case False
6.209 - then obtain Z
6.210 - where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y" by blast
6.211 - with suc_Union_closed_subsetD and `Y \<in> \<C>` show ?thesis by blast
6.212 -qed
6.213 -
6.214 -text {*Once we hit a fixed point w.r.t. @{term suc}, all other elements
6.215 -of @{term \<C>} are subsets of this fixed point.*}
6.216 -lemma suc_Union_closed_suc:
6.217 - assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y"
6.218 - shows "X \<subseteq> Y"
6.219 -using `X \<in> \<C>`
6.220 -proof (induct)
6.221 - case (suc X)
6.222 - with `Y \<in> \<C>` and suc_Union_closed_subsetD
6.223 - have "X = Y \<or> suc X \<subseteq> Y" by blast
6.224 - then show ?case by (auto simp: `suc Y = Y`)
6.225 -qed blast
6.226 -
6.227 -lemma eq_suc_Union:
6.228 - assumes "X \<in> \<C>"
6.229 - shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>"
6.230 -proof
6.231 - assume "suc X = X"
6.232 - with suc_Union_closed_suc [OF suc_Union_closed_Union `X \<in> \<C>`]
6.233 - have "\<Union>\<C> \<subseteq> X" .
6.234 - with `X \<in> \<C>` show "X = \<Union>\<C>" by blast
6.235 -next
6.236 - from `X \<in> \<C>` have "suc X \<in> \<C>" by (rule suc)
6.237 - then have "suc X \<subseteq> \<Union>\<C>" by blast
6.238 - moreover assume "X = \<Union>\<C>"
6.239 - ultimately have "suc X \<subseteq> X" by simp
6.240 - moreover have "X \<subseteq> suc X" by (rule suc_subset)
6.241 - ultimately show "suc X = X" ..
6.242 -qed
6.243 -
6.244 -lemma suc_in_carrier:
6.245 - assumes "X \<subseteq> A"
6.246 - shows "suc X \<subseteq> A"
6.247 - using assms
6.248 - by (cases "\<not> chain X \<or> maxchain X")
6.249 - (auto dest: chain_sucD)
6.250 -
6.251 -lemma suc_Union_closed_in_carrier:
6.252 - assumes "X \<in> \<C>"
6.253 - shows "X \<subseteq> A"
6.254 - using assms
6.255 - by (induct) (auto dest: suc_in_carrier)
6.256 -
6.257 -text {*All elements of @{term \<C>} are chains.*}
6.258 -lemma suc_Union_closed_chain:
6.259 - assumes "X \<in> \<C>"
6.260 - shows "chain X"
6.261 -using assms
6.262 -proof (induct)
6.263 - case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
6.264 -next
6.265 - case (Union X)
6.266 - then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
6.267 - moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
6.268 - proof (intro ballI)
6.269 - fix x y
6.270 - assume "x \<in> \<Union>X" and "y \<in> \<Union>X"
6.271 - then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X" by blast
6.272 - with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v" by blast+
6.273 - with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u" by blast
6.274 - then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
6.275 - proof
6.276 - assume "u \<subseteq> v"
6.277 - from `chain v` show ?thesis
6.278 - proof (rule chain_total)
6.279 - show "y \<in> v" by fact
6.280 - show "x \<in> v" using `u \<subseteq> v` and `x \<in> u` by blast
6.281 - qed
6.282 - next
6.283 - assume "v \<subseteq> u"
6.284 - from `chain u` show ?thesis
6.285 - proof (rule chain_total)
6.286 - show "x \<in> u" by fact
6.287 - show "y \<in> u" using `v \<subseteq> u` and `y \<in> v` by blast
6.288 - qed
6.289 - qed
6.290 - qed
6.291 - ultimately show ?case unfolding chain_def ..
6.292 -qed
6.293 -
6.294 -subsubsection {* Hausdorff's Maximum Principle *}
6.295 -
6.296 -text {*There exists a maximal totally ordered subset of @{term A}. (Note that we do not
6.297 -require @{term A} to be partially ordered.)*}
6.298 -
6.299 -theorem Hausdorff: "\<exists>C. maxchain C"
6.300 -proof -
6.301 - let ?M = "\<Union>\<C>"
6.302 - have "maxchain ?M"
6.303 - proof (rule ccontr)
6.304 - assume "\<not> maxchain ?M"
6.305 - then have "suc ?M \<noteq> ?M"
6.306 - using suc_not_equals and
6.307 - suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
6.308 - moreover have "suc ?M = ?M"
6.309 - using eq_suc_Union [OF suc_Union_closed_Union] by simp
6.310 - ultimately show False by contradiction
6.311 - qed
6.312 - then show ?thesis by blast
6.313 -qed
6.314 -
6.315 -text {*Make notation @{term \<C>} available again.*}
6.316 -no_notation suc_Union_closed ("\<C>")
6.317 -
6.318 -lemma chain_extend:
6.319 - "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
6.320 - unfolding chain_def by blast
6.321 -
6.322 -lemma maxchain_imp_chain:
6.323 - "maxchain C \<Longrightarrow> chain C"
6.324 - by (simp add: maxchain_def)
6.325 -
6.326 -end
6.327 -
6.328 -text {*Hide constant @{const pred_on.suc_Union_closed}, which was just needed
6.329 -for the proof of Hausforff's maximum principle.*}
6.330 -hide_const pred_on.suc_Union_closed
6.331 -
6.332 -lemma chain_mono:
6.333 - assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y"
6.334 - and "pred_on.chain A P C"
6.335 - shows "pred_on.chain A Q C"
6.336 - using assms unfolding pred_on.chain_def by blast
6.337 -
6.338 -subsubsection {* Results for the proper subset relation *}
6.339 -
6.340 -interpretation subset: pred_on "A" "op \<subset>" for A .
6.341 -
6.342 -lemma subset_maxchain_max:
6.343 - assumes "subset.maxchain A C" and "X \<in> A" and "\<Union>C \<subseteq> X"
6.344 - shows "\<Union>C = X"
6.345 -proof (rule ccontr)
6.346 - let ?C = "{X} \<union> C"
6.347 - from `subset.maxchain A C` have "subset.chain A C"
6.348 - and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S"
6.349 - by (auto simp: subset.maxchain_def)
6.350 - moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
6.351 - ultimately have "subset.chain A ?C"
6.352 - using subset.chain_extend [of A C X] and `X \<in> A` by auto
6.353 - moreover assume **: "\<Union>C \<noteq> X"
6.354 - moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
6.355 - ultimately show False using * by blast
6.356 -qed
6.357 -
6.358 -subsubsection {* Zorn's lemma *}
6.359 -
6.360 -text {*If every chain has an upper bound, then there is a maximal set.*}
6.361 -lemma subset_Zorn:
6.362 - assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
6.363 - shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
6.364 -proof -
6.365 - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
6.366 - then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
6.367 - with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y" by blast
6.368 - moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X"
6.369 - proof (intro ballI impI)
6.370 - fix X
6.371 - assume "X \<in> A" and "Y \<subseteq> X"
6.372 - show "Y = X"
6.373 - proof (rule ccontr)
6.374 - assume "Y \<noteq> X"
6.375 - with `Y \<subseteq> X` have "\<not> X \<subseteq> Y" by blast
6.376 - from subset.chain_extend [OF `subset.chain A M` `X \<in> A`] and `\<forall>X\<in>M. X \<subseteq> Y`
6.377 - have "subset.chain A ({X} \<union> M)" using `Y \<subseteq> X` by auto
6.378 - moreover have "M \<subset> {X} \<union> M" using `\<forall>X\<in>M. X \<subseteq> Y` and `\<not> X \<subseteq> Y` by auto
6.379 - ultimately show False
6.380 - using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
6.381 - qed
6.382 - qed
6.383 - ultimately show ?thesis by metis
6.384 -qed
6.385 -
6.386 -text{*Alternative version of Zorn's lemma for the subset relation.*}
6.387 -lemma subset_Zorn':
6.388 - assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A"
6.389 - shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
6.390 -proof -
6.391 - from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
6.392 - then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
6.393 - with assms have "\<Union>M \<in> A" .
6.394 - moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z"
6.395 - proof (intro ballI impI)
6.396 - fix Z
6.397 - assume "Z \<in> A" and "\<Union>M \<subseteq> Z"
6.398 - with subset_maxchain_max [OF `subset.maxchain A M`]
6.399 - show "\<Union>M = Z" .
6.400 - qed
6.401 - ultimately show ?thesis by blast
6.402 -qed
6.403 -
6.404 -
6.405 -subsection {* Zorn's Lemma for Partial Orders *}
6.406 -
6.407 -text {*Relate old to new definitions.*}
6.408 -
6.409 -(* Define globally? In Set.thy? *)
6.410 -definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") where
6.411 - "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
6.412 -
6.413 -definition chains :: "'a set set \<Rightarrow> 'a set set set" where
6.414 - "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"
6.415 -
6.416 -(* Define globally? In Relation.thy? *)
6.417 -definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where
6.418 - "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
6.419 -
6.420 -lemma chains_extend:
6.421 - "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
6.422 - by (unfold chains_def chain_subset_def) blast
6.423 -
6.424 -lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
6.425 - unfolding Chains_def by blast
6.426 -
6.427 -lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C"
6.428 - unfolding chain_subset_def subset.chain_def by fast
6.429 -
6.430 -lemma chains_alt_def: "chains A = {C. subset.chain A C}"
6.431 - by (simp add: chains_def chain_subset_alt_def subset.chain_def)
6.432 -
6.433 -lemma Chains_subset:
6.434 - "Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
6.435 - by (force simp add: Chains_def pred_on.chain_def)
6.436 -
6.437 -lemma Chains_subset':
6.438 - assumes "refl r"
6.439 - shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r"
6.440 - using assms
6.441 - by (auto simp add: Chains_def pred_on.chain_def refl_on_def)
6.442 -
6.443 -lemma Chains_alt_def:
6.444 - assumes "refl r"
6.445 - shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
6.446 - using assms
6.447 - by (metis Chains_subset Chains_subset' subset_antisym)
6.448 -
6.449 -lemma Zorn_Lemma:
6.450 - "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
6.451 - using subset_Zorn' [of A] by (force simp: chains_alt_def)
6.452 -
6.453 -lemma Zorn_Lemma2:
6.454 - "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
6.455 - using subset_Zorn [of A] by (auto simp: chains_alt_def)
6.456 -
6.457 -text{*Various other lemmas*}
6.458 -
6.459 -lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
6.460 -by (unfold chains_def chain_subset_def) blast
6.461 -
6.462 -lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
6.463 -by (unfold chains_def) blast
6.464 -
6.465 -lemma Zorns_po_lemma:
6.466 - assumes po: "Partial_order r"
6.467 - and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
6.468 - shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
6.469 -proof -
6.470 - have "Preorder r" using po by (simp add: partial_order_on_def)
6.471 ---{* Mirror r in the set of subsets below (wrt r) elements of A*}
6.472 - let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r"
6.473 - {
6.474 - fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
6.475 - let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
6.476 - have "C = ?B ` ?A" using 1 by (auto simp: image_def)
6.477 - have "?A \<in> Chains r"
6.478 - proof (simp add: Chains_def, intro allI impI, elim conjE)
6.479 - fix a b
6.480 - assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C"
6.481 - hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
6.482 - thus "(a, b) \<in> r \<or> (b, a) \<in> r"
6.483 - using `Preorder r` and `a \<in> Field r` and `b \<in> Field r`
6.484 - by (simp add:subset_Image1_Image1_iff)
6.485 - qed
6.486 - then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto
6.487 - have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u")
6.488 - proof auto
6.489 - fix a B assume aB: "B \<in> C" "a \<in> B"
6.490 - with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto
6.491 - thus "(a, u) \<in> r" using uA and aB and `Preorder r`
6.492 - unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
6.493 - qed
6.494 - then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast
6.495 - }
6.496 - then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
6.497 - by (auto simp: chains_def chain_subset_def)
6.498 - from Zorn_Lemma2 [OF this]
6.499 - obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}"
6.500 - and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B"
6.501 - by auto
6.502 - hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
6.503 - using po and `Preorder r` and `m \<in> Field r`
6.504 - by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
6.505 - thus ?thesis using `m \<in> Field r` by blast
6.506 -qed
6.507 -
6.508 -
6.509 -subsection {* The Well Ordering Theorem *}
6.510 -
6.511 -(* The initial segment of a relation appears generally useful.
6.512 - Move to Relation.thy?
6.513 - Definition correct/most general?
6.514 - Naming?
6.515 -*)
6.516 -definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where
6.517 - "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
6.518 -
6.519 -abbreviation
6.520 - initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55)
6.521 -where
6.522 - "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
6.523 -
6.524 -lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
6.525 - by (simp add: init_seg_of_def)
6.526 -
6.527 -lemma trans_init_seg_of:
6.528 - "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
6.529 - by (simp (no_asm_use) add: init_seg_of_def) blast
6.530 -
6.531 -lemma antisym_init_seg_of:
6.532 - "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
6.533 - unfolding init_seg_of_def by safe
6.534 -
6.535 -lemma Chains_init_seg_of_Union:
6.536 - "R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
6.537 - by (auto simp: init_seg_of_def Ball_def Chains_def) blast
6.538 -
6.539 -lemma chain_subset_trans_Union:
6.540 - "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)"
6.541 -apply (auto simp add: chain_subset_def)
6.542 -apply (simp (no_asm_use) add: trans_def)
6.543 -by (metis subsetD)
6.544 -
6.545 -lemma chain_subset_antisym_Union:
6.546 - "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
6.547 -unfolding chain_subset_def antisym_def
6.548 -apply simp
6.549 -by (metis (no_types) subsetD)
6.550 -
6.551 -lemma chain_subset_Total_Union:
6.552 - assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
6.553 - shows "Total (\<Union>R)"
6.554 -proof (simp add: total_on_def Ball_def, auto del: disjCI)
6.555 - fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b"
6.556 - from `chain\<^sub>\<subseteq> R` and `r \<in> R` and `s \<in> R` have "r \<subseteq> s \<or> s \<subseteq> r"
6.557 - by (auto simp add: chain_subset_def)
6.558 - thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
6.559 - proof
6.560 - assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A
6.561 - by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
6.562 - thus ?thesis using `s \<in> R` by blast
6.563 - next
6.564 - assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A
6.565 - by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
6.566 - thus ?thesis using `r \<in> R` by blast
6.567 - qed
6.568 -qed
6.569 -
6.570 -lemma wf_Union_wf_init_segs:
6.571 - assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r"
6.572 - shows "wf (\<Union>R)"
6.573 -proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
6.574 - fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r"
6.575 - then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto
6.576 - { fix i have "(f (Suc i), f i) \<in> r"
6.577 - proof (induct i)
6.578 - case 0 show ?case by fact
6.579 - next
6.580 - case (Suc i)
6.581 - then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
6.582 - using 1 by auto
6.583 - then have "s initial_segment_of r \<or> r initial_segment_of s"
6.584 - using assms(1) `r \<in> R` by (simp add: Chains_def)
6.585 - with Suc s show ?case by (simp add: init_seg_of_def) blast
6.586 - qed
6.587 - }
6.588 - thus False using assms(2) and `r \<in> R`
6.589 - by (simp add: wf_iff_no_infinite_down_chain) blast
6.590 -qed
6.591 -
6.592 -lemma initial_segment_of_Diff:
6.593 - "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
6.594 - unfolding init_seg_of_def by blast
6.595 -
6.596 -lemma Chains_inits_DiffI:
6.597 - "R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of"
6.598 - unfolding Chains_def by (blast intro: initial_segment_of_Diff)
6.599 -
6.600 -theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"
6.601 -proof -
6.602 --- {*The initial segment relation on well-orders: *}
6.603 - let ?WO = "{r::'a rel. Well_order r}"
6.604 - def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
6.605 - have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def)
6.606 - hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
6.607 - unfolding init_seg_of_def chain_subset_def Chains_def by blast
6.608 - have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
6.609 - by (simp add: Chains_def I_def) blast
6.610 - have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def)
6.611 - hence 0: "Partial_order I"
6.612 - by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
6.613 - trans_def I_def elim!: trans_init_seg_of)
6.614 --- {*I-chains have upper bounds in ?WO wrt I: their Union*}
6.615 - { fix R assume "R \<in> Chains I"
6.616 - hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
6.617 - have subch: "chain\<^sub>\<subseteq> R" using `R : Chains I` I_init
6.618 - by (auto simp: init_seg_of_def chain_subset_def Chains_def)
6.619 - have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
6.620 - and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
6.621 - using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
6.622 - have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` unfolding refl_on_def by fastforce
6.623 - moreover have "trans (\<Union>R)"
6.624 - by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
6.625 - moreover have "antisym (\<Union>R)"
6.626 - by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`])
6.627 - moreover have "Total (\<Union>R)"
6.628 - by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`])
6.629 - moreover have "wf ((\<Union>R) - Id)"
6.630 - proof -
6.631 - have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
6.632 - with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
6.633 - show ?thesis by fastforce
6.634 - qed
6.635 - ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)
6.636 - moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
6.637 - by(simp add: Chains_init_seg_of_Union)
6.638 - ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
6.639 - using mono_Chains [OF I_init] and `R \<in> Chains I`
6.640 - by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
6.641 - }
6.642 - hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
6.643 ---{*Zorn's Lemma yields a maximal well-order m:*}
6.644 - then obtain m::"'a rel" where "Well_order m" and
6.645 - max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
6.646 - using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
6.647 ---{*Now show by contradiction that m covers the whole type:*}
6.648 - { fix x::'a assume "x \<notin> Field m"
6.649 ---{*We assume that x is not covered and extend m at the top with x*}
6.650 - have "m \<noteq> {}"
6.651 - proof
6.652 - assume "m = {}"
6.653 - moreover have "Well_order {(x, x)}"
6.654 - by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def)
6.655 - ultimately show False using max
6.656 - by (auto simp: I_def init_seg_of_def simp del: Field_insert)
6.657 - qed
6.658 - hence "Field m \<noteq> {}" by(auto simp:Field_def)
6.659 - moreover have "wf (m - Id)" using `Well_order m`
6.660 - by (simp add: well_order_on_def)
6.661 ---{*The extension of m by x:*}
6.662 - let ?s = "{(a, x) | a. a \<in> Field m}"
6.663 - let ?m = "insert (x, x) m \<union> ?s"
6.664 - have Fm: "Field ?m = insert x (Field m)"
6.665 - by (auto simp: Field_def)
6.666 - have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
6.667 - using `Well_order m` by (simp_all add: order_on_defs)
6.668 ---{*We show that the extension is a well-order*}
6.669 - have "Refl ?m" using `Refl m` Fm unfolding refl_on_def by blast
6.670 - moreover have "trans ?m" using `trans m` and `x \<notin> Field m`
6.671 - unfolding trans_def Field_def by blast
6.672 - moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m`
6.673 - unfolding antisym_def Field_def by blast
6.674 - moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def)
6.675 - moreover have "wf (?m - Id)"
6.676 - proof -
6.677 - have "wf ?s" using `x \<notin> Field m`
6.678 - by (auto simp add: wf_eq_minimal Field_def) metis
6.679 - thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
6.680 - wf_subset [OF `wf ?s` Diff_subset]
6.681 - unfolding Un_Diff Field_def by (auto intro: wf_Un)
6.682 - qed
6.683 - ultimately have "Well_order ?m" by (simp add: order_on_defs)
6.684 ---{*We show that the extension is above m*}
6.685 - moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m`
6.686 - by (fastforce simp: I_def init_seg_of_def Field_def)
6.687 - ultimately
6.688 ---{*This contradicts maximality of m:*}
6.689 - have False using max and `x \<notin> Field m` unfolding Field_def by blast
6.690 - }
6.691 - hence "Field m = UNIV" by auto
6.692 - with `Well_order m` show ?thesis by blast
6.693 -qed
6.694 -
6.695 -corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
6.696 -proof -
6.697 - obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
6.698 - using well_ordering [where 'a = "'a"] by blast
6.699 - let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
6.700 - have 1: "Field ?r = A" using wo univ
6.701 - by (fastforce simp: Field_def order_on_defs refl_on_def)
6.702 - have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)"
6.703 - using `Well_order r` by (simp_all add: order_on_defs)
6.704 - have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ)
6.705 - moreover have "trans ?r" using `trans r`
6.706 - unfolding trans_def by blast
6.707 - moreover have "antisym ?r" using `antisym r`
6.708 - unfolding antisym_def by blast
6.709 - moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ)
6.710 - moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast
6.711 - ultimately have "Well_order ?r" by (simp add: order_on_defs)
6.712 - with 1 show ?thesis by auto
6.713 -qed
6.714 -
6.715 -end
7.1 --- a/src/HOL/Main.thy Thu Jan 16 16:20:17 2014 +0100
7.2 +++ b/src/HOL/Main.thy Thu Jan 16 16:33:19 2014 +0100
7.3 @@ -1,7 +1,7 @@
7.4 header {* Main HOL *}
7.5
7.6 theory Main
7.7 -imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Order_Relation
7.8 +imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction Zorn
7.9 begin
7.10
7.11 text {*
8.1 --- a/src/HOL/NSA/Filter.thy Thu Jan 16 16:20:17 2014 +0100
8.2 +++ b/src/HOL/NSA/Filter.thy Thu Jan 16 16:33:19 2014 +0100
8.3 @@ -7,7 +7,7 @@
8.4 header {* Filters and Ultrafilters *}
8.5
8.6 theory Filter
8.7 -imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set"
8.8 +imports "~~/src/HOL/Library/Infinite_Set"
8.9 begin
8.10
8.11 subsection {* Definitions and basic properties *}
9.1 --- a/src/HOL/ROOT Thu Jan 16 16:20:17 2014 +0100
9.2 +++ b/src/HOL/ROOT Thu Jan 16 16:33:19 2014 +0100
9.3 @@ -61,7 +61,7 @@
9.4
9.5 This is the proof of the Hahn-Banach theorem for real vectorspaces,
9.6 following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
9.7 - theorem is one of the fundamental theorems of functioal analysis. It is a
9.8 + theorem is one of the fundamental theorems of functional analysis. It is a
9.9 conclusion of Zorn's lemma.
9.10
9.11 Two different formaulations of the theorem are presented, one for general
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Zorn.thy Thu Jan 16 16:33:19 2014 +0100
10.3 @@ -0,0 +1,712 @@
10.4 +(* Title: HOL/Zorn.thy
10.5 + Author: Jacques D. Fleuriot
10.6 + Author: Tobias Nipkow, TUM
10.7 + Author: Christian Sternagel, JAIST
10.8 +
10.9 +Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
10.10 +The well-ordering theorem.
10.11 +*)
10.12 +
10.13 +header {* Zorn's Lemma *}
10.14 +
10.15 +theory Zorn
10.16 +imports Order_Relation Hilbert_Choice
10.17 +begin
10.18 +
10.19 +subsection {* Zorn's Lemma for the Subset Relation *}
10.20 +
10.21 +subsubsection {* Results that do not require an order *}
10.22 +
10.23 +text {*Let @{text P} be a binary predicate on the set @{text A}.*}
10.24 +locale pred_on =
10.25 + fixes A :: "'a set"
10.26 + and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
10.27 +begin
10.28 +
10.29 +abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) where
10.30 + "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
10.31 +
10.32 +text {*A chain is a totally ordered subset of @{term A}.*}
10.33 +definition chain :: "'a set \<Rightarrow> bool" where
10.34 + "chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
10.35 +
10.36 +text {*We call a chain that is a proper superset of some set @{term X},
10.37 +but not necessarily a chain itself, a superchain of @{term X}.*}
10.38 +abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50) where
10.39 + "X <c C \<equiv> chain C \<and> X \<subset> C"
10.40 +
10.41 +text {*A maximal chain is a chain that does not have a superchain.*}
10.42 +definition maxchain :: "'a set \<Rightarrow> bool" where
10.43 + "maxchain C \<longleftrightarrow> chain C \<and> \<not> (\<exists>S. C <c S)"
10.44 +
10.45 +text {*We define the successor of a set to be an arbitrary
10.46 +superchain, if such exists, or the set itself, otherwise.*}
10.47 +definition suc :: "'a set \<Rightarrow> 'a set" where
10.48 + "suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))"
10.49 +
10.50 +lemma chainI [Pure.intro?]:
10.51 + "\<lbrakk>C \<subseteq> A; \<And>x y. \<lbrakk>x \<in> C; y \<in> C\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> chain C"
10.52 + unfolding chain_def by blast
10.53 +
10.54 +lemma chain_total:
10.55 + "chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
10.56 + by (simp add: chain_def)
10.57 +
10.58 +lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X"
10.59 + by (simp add: suc_def)
10.60 +
10.61 +lemma maxchain_suc [simp]: "maxchain X \<Longrightarrow> suc X = X"
10.62 + by (simp add: suc_def)
10.63 +
10.64 +lemma suc_subset: "X \<subseteq> suc X"
10.65 + by (auto simp: suc_def maxchain_def intro: someI2)
10.66 +
10.67 +lemma chain_empty [simp]: "chain {}"
10.68 + by (auto simp: chain_def)
10.69 +
10.70 +lemma not_maxchain_Some:
10.71 + "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)"
10.72 + by (rule someI_ex) (auto simp: maxchain_def)
10.73 +
10.74 +lemma suc_not_equals:
10.75 + "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
10.76 + by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
10.77 +
10.78 +lemma subset_suc:
10.79 + assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y"
10.80 + using assms by (rule subset_trans) (rule suc_subset)
10.81 +
10.82 +text {*We build a set @{term \<C>} that is closed under applications
10.83 +of @{term suc} and contains the union of all its subsets.*}
10.84 +inductive_set suc_Union_closed ("\<C>") where
10.85 + suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>" |
10.86 + Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
10.87 +
10.88 +text {*Since the empty set as well as the set itself is a subset of
10.89 +every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and
10.90 +@{term "\<Union>\<C> \<in> \<C>"}.*}
10.91 +lemma
10.92 + suc_Union_closed_empty: "{} \<in> \<C>" and
10.93 + suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>"
10.94 + using Union [of "{}"] and Union [of "\<C>"] by simp+
10.95 +text {*Thus closure under @{term suc} will hit a maximal chain
10.96 +eventually, as is shown below.*}
10.97 +
10.98 +lemma suc_Union_closed_induct [consumes 1, case_names suc Union,
10.99 + induct pred: suc_Union_closed]:
10.100 + assumes "X \<in> \<C>"
10.101 + and "\<And>X. \<lbrakk>X \<in> \<C>; Q X\<rbrakk> \<Longrightarrow> Q (suc X)"
10.102 + and "\<And>X. \<lbrakk>X \<subseteq> \<C>; \<forall>x\<in>X. Q x\<rbrakk> \<Longrightarrow> Q (\<Union>X)"
10.103 + shows "Q X"
10.104 + using assms by (induct) blast+
10.105 +
10.106 +lemma suc_Union_closed_cases [consumes 1, case_names suc Union,
10.107 + cases pred: suc_Union_closed]:
10.108 + assumes "X \<in> \<C>"
10.109 + and "\<And>Y. \<lbrakk>X = suc Y; Y \<in> \<C>\<rbrakk> \<Longrightarrow> Q"
10.110 + and "\<And>Y. \<lbrakk>X = \<Union>Y; Y \<subseteq> \<C>\<rbrakk> \<Longrightarrow> Q"
10.111 + shows "Q"
10.112 + using assms by (cases) simp+
10.113 +
10.114 +text {*On chains, @{term suc} yields a chain.*}
10.115 +lemma chain_suc:
10.116 + assumes "chain X" shows "chain (suc X)"
10.117 + using assms
10.118 + by (cases "\<not> chain X \<or> maxchain X")
10.119 + (force simp: suc_def dest: not_maxchain_Some)+
10.120 +
10.121 +lemma chain_sucD:
10.122 + assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
10.123 +proof -
10.124 + from `chain X` have *: "chain (suc X)" by (rule chain_suc)
10.125 + then have "suc X \<subseteq> A" unfolding chain_def by blast
10.126 + with * show ?thesis by blast
10.127 +qed
10.128 +
10.129 +lemma suc_Union_closed_total':
10.130 + assumes "X \<in> \<C>" and "Y \<in> \<C>"
10.131 + and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
10.132 + shows "X \<subseteq> Y \<or> suc Y \<subseteq> X"
10.133 + using `X \<in> \<C>`
10.134 +proof (induct)
10.135 + case (suc X)
10.136 + with * show ?case by (blast del: subsetI intro: subset_suc)
10.137 +qed blast
10.138 +
10.139 +lemma suc_Union_closed_subsetD:
10.140 + assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>"
10.141 + shows "X = Y \<or> suc Y \<subseteq> X"
10.142 + using assms(2-, 1)
10.143 +proof (induct arbitrary: Y)
10.144 + case (suc X)
10.145 + note * = `\<And>Y. \<lbrakk>Y \<in> \<C>; Y \<subseteq> X\<rbrakk> \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X`
10.146 + with suc_Union_closed_total' [OF `Y \<in> \<C>` `X \<in> \<C>`]
10.147 + have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast
10.148 + then show ?case
10.149 + proof
10.150 + assume "Y \<subseteq> X"
10.151 + with * and `Y \<in> \<C>` have "X = Y \<or> suc Y \<subseteq> X" by blast
10.152 + then show ?thesis
10.153 + proof
10.154 + assume "X = Y" then show ?thesis by simp
10.155 + next
10.156 + assume "suc Y \<subseteq> X"
10.157 + then have "suc Y \<subseteq> suc X" by (rule subset_suc)
10.158 + then show ?thesis by simp
10.159 + qed
10.160 + next
10.161 + assume "suc X \<subseteq> Y"
10.162 + with `Y \<subseteq> suc X` show ?thesis by blast
10.163 + qed
10.164 +next
10.165 + case (Union X)
10.166 + show ?case
10.167 + proof (rule ccontr)
10.168 + assume "\<not> ?thesis"
10.169 + with `Y \<subseteq> \<Union>X` obtain x y z
10.170 + where "\<not> suc Y \<subseteq> \<Union>X"
10.171 + and "x \<in> X" and "y \<in> x" and "y \<notin> Y"
10.172 + and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast
10.173 + with `X \<subseteq> \<C>` have "x \<in> \<C>" by blast
10.174 + from Union and `x \<in> X`
10.175 + have *: "\<And>y. \<lbrakk>y \<in> \<C>; y \<subseteq> x\<rbrakk> \<Longrightarrow> x = y \<or> suc y \<subseteq> x" by blast
10.176 + with suc_Union_closed_total' [OF `Y \<in> \<C>` `x \<in> \<C>`]
10.177 + have "Y \<subseteq> x \<or> suc x \<subseteq> Y" by blast
10.178 + then show False
10.179 + proof
10.180 + assume "Y \<subseteq> x"
10.181 + with * [OF `Y \<in> \<C>`] have "x = Y \<or> suc Y \<subseteq> x" by blast
10.182 + then show False
10.183 + proof
10.184 + assume "x = Y" with `y \<in> x` and `y \<notin> Y` show False by blast
10.185 + next
10.186 + assume "suc Y \<subseteq> x"
10.187 + with `x \<in> X` have "suc Y \<subseteq> \<Union>X" by blast
10.188 + with `\<not> suc Y \<subseteq> \<Union>X` show False by contradiction
10.189 + qed
10.190 + next
10.191 + assume "suc x \<subseteq> Y"
10.192 + moreover from suc_subset and `y \<in> x` have "y \<in> suc x" by blast
10.193 + ultimately show False using `y \<notin> Y` by blast
10.194 + qed
10.195 + qed
10.196 +qed
10.197 +
10.198 +text {*The elements of @{term \<C>} are totally ordered by the subset relation.*}
10.199 +lemma suc_Union_closed_total:
10.200 + assumes "X \<in> \<C>" and "Y \<in> \<C>"
10.201 + shows "X \<subseteq> Y \<or> Y \<subseteq> X"
10.202 +proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y")
10.203 + case True
10.204 + with suc_Union_closed_total' [OF assms]
10.205 + have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast
10.206 + then show ?thesis using suc_subset [of Y] by blast
10.207 +next
10.208 + case False
10.209 + then obtain Z
10.210 + where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y" by blast
10.211 + with suc_Union_closed_subsetD and `Y \<in> \<C>` show ?thesis by blast
10.212 +qed
10.213 +
10.214 +text {*Once we hit a fixed point w.r.t. @{term suc}, all other elements
10.215 +of @{term \<C>} are subsets of this fixed point.*}
10.216 +lemma suc_Union_closed_suc:
10.217 + assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y"
10.218 + shows "X \<subseteq> Y"
10.219 +using `X \<in> \<C>`
10.220 +proof (induct)
10.221 + case (suc X)
10.222 + with `Y \<in> \<C>` and suc_Union_closed_subsetD
10.223 + have "X = Y \<or> suc X \<subseteq> Y" by blast
10.224 + then show ?case by (auto simp: `suc Y = Y`)
10.225 +qed blast
10.226 +
10.227 +lemma eq_suc_Union:
10.228 + assumes "X \<in> \<C>"
10.229 + shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>"
10.230 +proof
10.231 + assume "suc X = X"
10.232 + with suc_Union_closed_suc [OF suc_Union_closed_Union `X \<in> \<C>`]
10.233 + have "\<Union>\<C> \<subseteq> X" .
10.234 + with `X \<in> \<C>` show "X = \<Union>\<C>" by blast
10.235 +next
10.236 + from `X \<in> \<C>` have "suc X \<in> \<C>" by (rule suc)
10.237 + then have "suc X \<subseteq> \<Union>\<C>" by blast
10.238 + moreover assume "X = \<Union>\<C>"
10.239 + ultimately have "suc X \<subseteq> X" by simp
10.240 + moreover have "X \<subseteq> suc X" by (rule suc_subset)
10.241 + ultimately show "suc X = X" ..
10.242 +qed
10.243 +
10.244 +lemma suc_in_carrier:
10.245 + assumes "X \<subseteq> A"
10.246 + shows "suc X \<subseteq> A"
10.247 + using assms
10.248 + by (cases "\<not> chain X \<or> maxchain X")
10.249 + (auto dest: chain_sucD)
10.250 +
10.251 +lemma suc_Union_closed_in_carrier:
10.252 + assumes "X \<in> \<C>"
10.253 + shows "X \<subseteq> A"
10.254 + using assms
10.255 + by (induct) (auto dest: suc_in_carrier)
10.256 +
10.257 +text {*All elements of @{term \<C>} are chains.*}
10.258 +lemma suc_Union_closed_chain:
10.259 + assumes "X \<in> \<C>"
10.260 + shows "chain X"
10.261 +using assms
10.262 +proof (induct)
10.263 + case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some)
10.264 +next
10.265 + case (Union X)
10.266 + then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier)
10.267 + moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
10.268 + proof (intro ballI)
10.269 + fix x y
10.270 + assume "x \<in> \<Union>X" and "y \<in> \<Union>X"
10.271 + then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X" by blast
10.272 + with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v" by blast+
10.273 + with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u" by blast
10.274 + then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
10.275 + proof
10.276 + assume "u \<subseteq> v"
10.277 + from `chain v` show ?thesis
10.278 + proof (rule chain_total)
10.279 + show "y \<in> v" by fact
10.280 + show "x \<in> v" using `u \<subseteq> v` and `x \<in> u` by blast
10.281 + qed
10.282 + next
10.283 + assume "v \<subseteq> u"
10.284 + from `chain u` show ?thesis
10.285 + proof (rule chain_total)
10.286 + show "x \<in> u" by fact
10.287 + show "y \<in> u" using `v \<subseteq> u` and `y \<in> v` by blast
10.288 + qed
10.289 + qed
10.290 + qed
10.291 + ultimately show ?case unfolding chain_def ..
10.292 +qed
10.293 +
10.294 +subsubsection {* Hausdorff's Maximum Principle *}
10.295 +
10.296 +text {*There exists a maximal totally ordered subset of @{term A}. (Note that we do not
10.297 +require @{term A} to be partially ordered.)*}
10.298 +
10.299 +theorem Hausdorff: "\<exists>C. maxchain C"
10.300 +proof -
10.301 + let ?M = "\<Union>\<C>"
10.302 + have "maxchain ?M"
10.303 + proof (rule ccontr)
10.304 + assume "\<not> maxchain ?M"
10.305 + then have "suc ?M \<noteq> ?M"
10.306 + using suc_not_equals and
10.307 + suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
10.308 + moreover have "suc ?M = ?M"
10.309 + using eq_suc_Union [OF suc_Union_closed_Union] by simp
10.310 + ultimately show False by contradiction
10.311 + qed
10.312 + then show ?thesis by blast
10.313 +qed
10.314 +
10.315 +text {*Make notation @{term \<C>} available again.*}
10.316 +no_notation suc_Union_closed ("\<C>")
10.317 +
10.318 +lemma chain_extend:
10.319 + "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
10.320 + unfolding chain_def by blast
10.321 +
10.322 +lemma maxchain_imp_chain:
10.323 + "maxchain C \<Longrightarrow> chain C"
10.324 + by (simp add: maxchain_def)
10.325 +
10.326 +end
10.327 +
10.328 +text {*Hide constant @{const pred_on.suc_Union_closed}, which was just needed
10.329 +for the proof of Hausforff's maximum principle.*}
10.330 +hide_const pred_on.suc_Union_closed
10.331 +
10.332 +lemma chain_mono:
10.333 + assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y"
10.334 + and "pred_on.chain A P C"
10.335 + shows "pred_on.chain A Q C"
10.336 + using assms unfolding pred_on.chain_def by blast
10.337 +
10.338 +subsubsection {* Results for the proper subset relation *}
10.339 +
10.340 +interpretation subset: pred_on "A" "op \<subset>" for A .
10.341 +
10.342 +lemma subset_maxchain_max:
10.343 + assumes "subset.maxchain A C" and "X \<in> A" and "\<Union>C \<subseteq> X"
10.344 + shows "\<Union>C = X"
10.345 +proof (rule ccontr)
10.346 + let ?C = "{X} \<union> C"
10.347 + from `subset.maxchain A C` have "subset.chain A C"
10.348 + and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S"
10.349 + by (auto simp: subset.maxchain_def)
10.350 + moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
10.351 + ultimately have "subset.chain A ?C"
10.352 + using subset.chain_extend [of A C X] and `X \<in> A` by auto
10.353 + moreover assume **: "\<Union>C \<noteq> X"
10.354 + moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
10.355 + ultimately show False using * by blast
10.356 +qed
10.357 +
10.358 +subsubsection {* Zorn's lemma *}
10.359 +
10.360 +text {*If every chain has an upper bound, then there is a maximal set.*}
10.361 +lemma subset_Zorn:
10.362 + assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
10.363 + shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
10.364 +proof -
10.365 + from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
10.366 + then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
10.367 + with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y" by blast
10.368 + moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X"
10.369 + proof (intro ballI impI)
10.370 + fix X
10.371 + assume "X \<in> A" and "Y \<subseteq> X"
10.372 + show "Y = X"
10.373 + proof (rule ccontr)
10.374 + assume "Y \<noteq> X"
10.375 + with `Y \<subseteq> X` have "\<not> X \<subseteq> Y" by blast
10.376 + from subset.chain_extend [OF `subset.chain A M` `X \<in> A`] and `\<forall>X\<in>M. X \<subseteq> Y`
10.377 + have "subset.chain A ({X} \<union> M)" using `Y \<subseteq> X` by auto
10.378 + moreover have "M \<subset> {X} \<union> M" using `\<forall>X\<in>M. X \<subseteq> Y` and `\<not> X \<subseteq> Y` by auto
10.379 + ultimately show False
10.380 + using `subset.maxchain A M` by (auto simp: subset.maxchain_def)
10.381 + qed
10.382 + qed
10.383 + ultimately show ?thesis by metis
10.384 +qed
10.385 +
10.386 +text{*Alternative version of Zorn's lemma for the subset relation.*}
10.387 +lemma subset_Zorn':
10.388 + assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A"
10.389 + shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
10.390 +proof -
10.391 + from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
10.392 + then have "subset.chain A M" by (rule subset.maxchain_imp_chain)
10.393 + with assms have "\<Union>M \<in> A" .
10.394 + moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z"
10.395 + proof (intro ballI impI)
10.396 + fix Z
10.397 + assume "Z \<in> A" and "\<Union>M \<subseteq> Z"
10.398 + with subset_maxchain_max [OF `subset.maxchain A M`]
10.399 + show "\<Union>M = Z" .
10.400 + qed
10.401 + ultimately show ?thesis by blast
10.402 +qed
10.403 +
10.404 +
10.405 +subsection {* Zorn's Lemma for Partial Orders *}
10.406 +
10.407 +text {*Relate old to new definitions.*}
10.408 +
10.409 +(* Define globally? In Set.thy? *)
10.410 +definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") where
10.411 + "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
10.412 +
10.413 +definition chains :: "'a set set \<Rightarrow> 'a set set set" where
10.414 + "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"
10.415 +
10.416 +(* Define globally? In Relation.thy? *)
10.417 +definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where
10.418 + "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
10.419 +
10.420 +lemma chains_extend:
10.421 + "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"
10.422 + by (unfold chains_def chain_subset_def) blast
10.423 +
10.424 +lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
10.425 + unfolding Chains_def by blast
10.426 +
10.427 +lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C"
10.428 + unfolding chain_subset_def subset.chain_def by fast
10.429 +
10.430 +lemma chains_alt_def: "chains A = {C. subset.chain A C}"
10.431 + by (simp add: chains_def chain_subset_alt_def subset.chain_def)
10.432 +
10.433 +lemma Chains_subset:
10.434 + "Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
10.435 + by (force simp add: Chains_def pred_on.chain_def)
10.436 +
10.437 +lemma Chains_subset':
10.438 + assumes "refl r"
10.439 + shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r"
10.440 + using assms
10.441 + by (auto simp add: Chains_def pred_on.chain_def refl_on_def)
10.442 +
10.443 +lemma Chains_alt_def:
10.444 + assumes "refl r"
10.445 + shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
10.446 + using assms
10.447 + by (metis Chains_subset Chains_subset' subset_antisym)
10.448 +
10.449 +lemma Zorn_Lemma:
10.450 + "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
10.451 + using subset_Zorn' [of A] by (force simp: chains_alt_def)
10.452 +
10.453 +lemma Zorn_Lemma2:
10.454 + "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
10.455 + using subset_Zorn [of A] by (auto simp: chains_alt_def)
10.456 +
10.457 +text{*Various other lemmas*}
10.458 +
10.459 +lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
10.460 +by (unfold chains_def chain_subset_def) blast
10.461 +
10.462 +lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"
10.463 +by (unfold chains_def) blast
10.464 +
10.465 +lemma Zorns_po_lemma:
10.466 + assumes po: "Partial_order r"
10.467 + and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
10.468 + shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
10.469 +proof -
10.470 + have "Preorder r" using po by (simp add: partial_order_on_def)
10.471 +--{* Mirror r in the set of subsets below (wrt r) elements of A*}
10.472 + let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r"
10.473 + {
10.474 + fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
10.475 + let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
10.476 + have "C = ?B ` ?A" using 1 by (auto simp: image_def)
10.477 + have "?A \<in> Chains r"
10.478 + proof (simp add: Chains_def, intro allI impI, elim conjE)
10.479 + fix a b
10.480 + assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C"
10.481 + hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
10.482 + thus "(a, b) \<in> r \<or> (b, a) \<in> r"
10.483 + using `Preorder r` and `a \<in> Field r` and `b \<in> Field r`
10.484 + by (simp add:subset_Image1_Image1_iff)
10.485 + qed
10.486 + then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto
10.487 + have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u")
10.488 + proof auto
10.489 + fix a B assume aB: "B \<in> C" "a \<in> B"
10.490 + with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto
10.491 + thus "(a, u) \<in> r" using uA and aB and `Preorder r`
10.492 + unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
10.493 + qed
10.494 + then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast
10.495 + }
10.496 + then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
10.497 + by (auto simp: chains_def chain_subset_def)
10.498 + from Zorn_Lemma2 [OF this]
10.499 + obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}"
10.500 + and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B"
10.501 + by auto
10.502 + hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
10.503 + using po and `Preorder r` and `m \<in> Field r`
10.504 + by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
10.505 + thus ?thesis using `m \<in> Field r` by blast
10.506 +qed
10.507 +
10.508 +
10.509 +subsection {* The Well Ordering Theorem *}
10.510 +
10.511 +(* The initial segment of a relation appears generally useful.
10.512 + Move to Relation.thy?
10.513 + Definition correct/most general?
10.514 + Naming?
10.515 +*)
10.516 +definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where
10.517 + "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
10.518 +
10.519 +abbreviation
10.520 + initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55)
10.521 +where
10.522 + "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
10.523 +
10.524 +lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
10.525 + by (simp add: init_seg_of_def)
10.526 +
10.527 +lemma trans_init_seg_of:
10.528 + "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
10.529 + by (simp (no_asm_use) add: init_seg_of_def) blast
10.530 +
10.531 +lemma antisym_init_seg_of:
10.532 + "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
10.533 + unfolding init_seg_of_def by safe
10.534 +
10.535 +lemma Chains_init_seg_of_Union:
10.536 + "R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
10.537 + by (auto simp: init_seg_of_def Ball_def Chains_def) blast
10.538 +
10.539 +lemma chain_subset_trans_Union:
10.540 + "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)"
10.541 +apply (auto simp add: chain_subset_def)
10.542 +apply (simp (no_asm_use) add: trans_def)
10.543 +by (metis subsetD)
10.544 +
10.545 +lemma chain_subset_antisym_Union:
10.546 + "chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)"
10.547 +unfolding chain_subset_def antisym_def
10.548 +apply simp
10.549 +by (metis (no_types) subsetD)
10.550 +
10.551 +lemma chain_subset_Total_Union:
10.552 + assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
10.553 + shows "Total (\<Union>R)"
10.554 +proof (simp add: total_on_def Ball_def, auto del: disjCI)
10.555 + fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b"
10.556 + from `chain\<^sub>\<subseteq> R` and `r \<in> R` and `s \<in> R` have "r \<subseteq> s \<or> s \<subseteq> r"
10.557 + by (auto simp add: chain_subset_def)
10.558 + thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
10.559 + proof
10.560 + assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A
10.561 + by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
10.562 + thus ?thesis using `s \<in> R` by blast
10.563 + next
10.564 + assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A
10.565 + by (simp add: total_on_def) (metis (no_types) mono_Field subsetD)
10.566 + thus ?thesis using `r \<in> R` by blast
10.567 + qed
10.568 +qed
10.569 +
10.570 +lemma wf_Union_wf_init_segs:
10.571 + assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r"
10.572 + shows "wf (\<Union>R)"
10.573 +proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
10.574 + fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r"
10.575 + then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto
10.576 + { fix i have "(f (Suc i), f i) \<in> r"
10.577 + proof (induct i)
10.578 + case 0 show ?case by fact
10.579 + next
10.580 + case (Suc i)
10.581 + then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
10.582 + using 1 by auto
10.583 + then have "s initial_segment_of r \<or> r initial_segment_of s"
10.584 + using assms(1) `r \<in> R` by (simp add: Chains_def)
10.585 + with Suc s show ?case by (simp add: init_seg_of_def) blast
10.586 + qed
10.587 + }
10.588 + thus False using assms(2) and `r \<in> R`
10.589 + by (simp add: wf_iff_no_infinite_down_chain) blast
10.590 +qed
10.591 +
10.592 +lemma initial_segment_of_Diff:
10.593 + "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
10.594 + unfolding init_seg_of_def by blast
10.595 +
10.596 +lemma Chains_inits_DiffI:
10.597 + "R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of"
10.598 + unfolding Chains_def by (blast intro: initial_segment_of_Diff)
10.599 +
10.600 +theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"
10.601 +proof -
10.602 +-- {*The initial segment relation on well-orders: *}
10.603 + let ?WO = "{r::'a rel. Well_order r}"
10.604 + def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
10.605 + have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def)
10.606 + hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
10.607 + unfolding init_seg_of_def chain_subset_def Chains_def by blast
10.608 + have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
10.609 + by (simp add: Chains_def I_def) blast
10.610 + have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def)
10.611 + hence 0: "Partial_order I"
10.612 + by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
10.613 + trans_def I_def elim!: trans_init_seg_of)
10.614 +-- {*I-chains have upper bounds in ?WO wrt I: their Union*}
10.615 + { fix R assume "R \<in> Chains I"
10.616 + hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast
10.617 + have subch: "chain\<^sub>\<subseteq> R" using `R : Chains I` I_init
10.618 + by (auto simp: init_seg_of_def chain_subset_def Chains_def)
10.619 + have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
10.620 + and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
10.621 + using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs)
10.622 + have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` unfolding refl_on_def by fastforce
10.623 + moreover have "trans (\<Union>R)"
10.624 + by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`])
10.625 + moreover have "antisym (\<Union>R)"
10.626 + by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`])
10.627 + moreover have "Total (\<Union>R)"
10.628 + by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`])
10.629 + moreover have "wf ((\<Union>R) - Id)"
10.630 + proof -
10.631 + have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
10.632 + with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
10.633 + show ?thesis by fastforce
10.634 + qed
10.635 + ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)
10.636 + moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
10.637 + by(simp add: Chains_init_seg_of_Union)
10.638 + ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)"
10.639 + using mono_Chains [OF I_init] and `R \<in> Chains I`
10.640 + by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)
10.641 + }
10.642 + hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast
10.643 +--{*Zorn's Lemma yields a maximal well-order m:*}
10.644 + then obtain m::"'a rel" where "Well_order m" and
10.645 + max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
10.646 + using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
10.647 +--{*Now show by contradiction that m covers the whole type:*}
10.648 + { fix x::'a assume "x \<notin> Field m"
10.649 +--{*We assume that x is not covered and extend m at the top with x*}
10.650 + have "m \<noteq> {}"
10.651 + proof
10.652 + assume "m = {}"
10.653 + moreover have "Well_order {(x, x)}"
10.654 + by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def)
10.655 + ultimately show False using max
10.656 + by (auto simp: I_def init_seg_of_def simp del: Field_insert)
10.657 + qed
10.658 + hence "Field m \<noteq> {}" by(auto simp:Field_def)
10.659 + moreover have "wf (m - Id)" using `Well_order m`
10.660 + by (simp add: well_order_on_def)
10.661 +--{*The extension of m by x:*}
10.662 + let ?s = "{(a, x) | a. a \<in> Field m}"
10.663 + let ?m = "insert (x, x) m \<union> ?s"
10.664 + have Fm: "Field ?m = insert x (Field m)"
10.665 + by (auto simp: Field_def)
10.666 + have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
10.667 + using `Well_order m` by (simp_all add: order_on_defs)
10.668 +--{*We show that the extension is a well-order*}
10.669 + have "Refl ?m" using `Refl m` Fm unfolding refl_on_def by blast
10.670 + moreover have "trans ?m" using `trans m` and `x \<notin> Field m`
10.671 + unfolding trans_def Field_def by blast
10.672 + moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m`
10.673 + unfolding antisym_def Field_def by blast
10.674 + moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def)
10.675 + moreover have "wf (?m - Id)"
10.676 + proof -
10.677 + have "wf ?s" using `x \<notin> Field m`
10.678 + by (auto simp add: wf_eq_minimal Field_def) metis
10.679 + thus ?thesis using `wf (m - Id)` and `x \<notin> Field m`
10.680 + wf_subset [OF `wf ?s` Diff_subset]
10.681 + unfolding Un_Diff Field_def by (auto intro: wf_Un)
10.682 + qed
10.683 + ultimately have "Well_order ?m" by (simp add: order_on_defs)
10.684 +--{*We show that the extension is above m*}
10.685 + moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m`
10.686 + by (fastforce simp: I_def init_seg_of_def Field_def)
10.687 + ultimately
10.688 +--{*This contradicts maximality of m:*}
10.689 + have False using max and `x \<notin> Field m` unfolding Field_def by blast
10.690 + }
10.691 + hence "Field m = UNIV" by auto
10.692 + with `Well_order m` show ?thesis by blast
10.693 +qed
10.694 +
10.695 +corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
10.696 +proof -
10.697 + obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
10.698 + using well_ordering [where 'a = "'a"] by blast
10.699 + let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
10.700 + have 1: "Field ?r = A" using wo univ
10.701 + by (fastforce simp: Field_def order_on_defs refl_on_def)
10.702 + have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)"
10.703 + using `Well_order r` by (simp_all add: order_on_defs)
10.704 + have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ)
10.705 + moreover have "trans ?r" using `trans r`
10.706 + unfolding trans_def by blast
10.707 + moreover have "antisym ?r" using `antisym r`
10.708 + unfolding antisym_def by blast
10.709 + moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ)
10.710 + moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast
10.711 + ultimately have "Well_order ?r" by (simp add: order_on_defs)
10.712 + with 1 show ?thesis by auto
10.713 +qed
10.714 +
10.715 +end