(* Title: HOL/Zorn.thy
Author: Jacques D. Fleuriot
Author: Tobias Nipkow, TUM
Author: Christian Sternagel, JAIST
Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
The well-ordering theorem.
*)
section \<open>Zorn's Lemma\<close>
theory Zorn
imports Order_Relation Hilbert_Choice
begin
subsection \<open>Zorn's Lemma for the Subset Relation\<close>
subsubsection \<open>Results that do not require an order\<close>
text \<open>Let \<open>P\<close> be a binary predicate on the set \<open>A\<close>.\<close>
locale pred_on =
fixes A :: "'a set"
and P :: "'a \ 'a \ bool" (infix "\" 50)
begin
abbreviation Peq :: "'a \ 'a \ bool" (infix "\" 50)
where "x \ y \ P\<^sup>=\<^sup>= x y"
text \<open>A chain is a totally ordered subset of \<open>A\<close>.\<close>
definition chain :: "'a set \ bool"
where "chain C \ C \ A \ (\x\C. \y\C. x \ y \ y \ x)"
text \<open>
We call a chain that is a proper superset of some set \<open>X\<close>,
but not necessarily a chain itself, a superchain of \<open>X\<close>.
\<close>
abbreviation superchain :: "'a set \ 'a set \ bool" (infix "
where "X chain C \ X \ C"
text \<open>A maximal chain is a chain that does not have a superchain.\<close>
definition maxchain :: "'a set \ bool"
where "maxchain C \ chain C \ (\S. C
text \<open>
We define the successor of a set to be an arbitrary
superchain, if such exists, or the set itself, otherwise.
\<close>
definition suc :: "'a set \ 'a set"
where "suc C = (if \ chain C \ maxchain C then C else (SOME D. C
lemma chainI [Pure.intro?]: "C \ A \ (\x y. x \ C \ y \ C \ x \ y \ y \ x) \ chain C"
unfolding chain_def by blast
lemma chain_total: "chain C \ x \ C \ y \ C \ x \ y \ y \ x"
by (simp add: chain_def)
lemma not_chain_suc [simp]: "\ chain X \ suc X = X"
by (simp add: suc_def)
lemma maxchain_suc [simp]: "maxchain X \ suc X = X"
by (simp add: suc_def)
lemma suc_subset: "X \ suc X"
by (auto simp: suc_def maxchain_def intro: someI2)
lemma chain_empty [simp]: "chain {}"
by (auto simp: chain_def)
lemma not_maxchain_Some: "chain C \ \ maxchain C \ C
by (rule someI_ex) (auto simp: maxchain_def)
lemma suc_not_equals: "chain C \ \ maxchain C \ suc C \ C"
using not_maxchain_Some by (auto simp: suc_def)
lemma subset_suc:
assumes "X \ Y"
shows "X \ suc Y"
using assms by (rule subset_trans) (rule suc_subset)
text \<open>
We build a set \<^term>\<open>\<C>\<close> that is closed under applications
of \<^term>\<open>suc\<close> and contains the union of all its subsets.
\<close>
inductive_set suc_Union_closed ("\")
where
suc: "X \ \ \ suc X \ \"
| Union [unfolded Pow_iff]: "X \ Pow \ \ \X \ \"
text \<open>
Since the empty set as well as the set itself is a subset of
every set, \<^term>\<open>\<C>\<close> contains at least \<^term>\<open>{} \<in> \<C>\<close> and
\<^term>\<open>\<Union>\<C> \<in> \<C>\<close>.
\<close>
lemma suc_Union_closed_empty: "{} \ \"
and suc_Union_closed_Union: "\\ \ \"
using Union [of "{}"] and Union [of "\"] by simp_all
text \<open>Thus closure under \<^term>\<open>suc\<close> will hit a maximal chain
eventually, as is shown below.\<close>
lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]:
assumes "X \ \"
and "\X. X \ \ \ Q X \ Q (suc X)"
and "\X. X \ \ \ \x\X. Q x \ Q (\X)"
shows "Q X"
using assms by induct blast+
lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]:
assumes "X \ \"
and "\Y. X = suc Y \ Y \ \ \ Q"
and "\Y. X = \Y \ Y \ \ \ Q"
shows "Q"
using assms by cases simp_all
text \<open>On chains, \<^term>\<open>suc\<close> yields a chain.\<close>
lemma chain_suc:
assumes "chain X"
shows "chain (suc X)"
using assms
by (cases "\ chain X \ maxchain X") (force simp: suc_def dest: not_maxchain_Some)+
lemma chain_sucD:
assumes "chain X"
shows "suc X \ A \ chain (suc X)"
proof -
from \<open>chain X\<close> have *: "chain (suc X)"
by (rule chain_suc)
then have "suc X \ A"
unfolding chain_def by blast
with * show ?thesis by blast
qed
lemma suc_Union_closed_total':
assumes "X \ \" and "Y \ \"
and *: "\Z. Z \ \ \ Z \ Y \ Z = Y \ suc Z \ Y"
shows "X \ Y \ suc Y \ X"
using \<open>X \<in> \<C>\<close>
proof induct
case (suc X)
with * show ?case by (blast del: subsetI intro: subset_suc)
next
case Union
then show ?case by blast
qed
lemma suc_Union_closed_subsetD:
assumes "Y \ X" and "X \ \" and "Y \ \"
shows "X = Y \ suc Y \ X"
using assms(2,3,1)
proof (induct arbitrary: Y)
case (suc X)
note * = \<open>\<And>Y. Y \<in> \<C> \<Longrightarrow> Y \<subseteq> X \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X\<close>
with suc_Union_closed_total' [OF \Y \ \\ \X \ \\]
have "Y \ X \ suc X \ Y" by blast
then show ?case
proof
assume "Y \ X"
with * and \<open>Y \<in> \<C>\<close> have "X = Y \<or> suc Y \<subseteq> X" by blast
then show ?thesis
proof
assume "X = Y"
then show ?thesis by simp
next
assume "suc Y \ X"
then have "suc Y \ suc X" by (rule subset_suc)
then show ?thesis by simp
qed
next
assume "suc X \ Y"
with \<open>Y \<subseteq> suc X\<close> show ?thesis by blast
qed
next
case (Union X)
show ?case
proof (rule ccontr)
assume "\ ?thesis"
with \<open>Y \<subseteq> \<Union>X\<close> obtain x y z
where "\ suc Y \ \X"
and "x \ X" and "y \ x" and "y \ Y"
and "z \ suc Y" and "\x\X. z \ x" by blast
with \<open>X \<subseteq> \<C>\<close> have "x \<in> \<C>" by blast
from Union and \<open>x \<in> X\<close> have *: "\<And>y. y \<in> \<C> \<Longrightarrow> y \<subseteq> x \<Longrightarrow> x = y \<or> suc y \<subseteq> x"
by blast
with suc_Union_closed_total' [OF \Y \ \\ \x \ \\] have "Y \ x \ suc x \ Y"
by blast
then show False
proof
assume "Y \ x"
with * [OF \<open>Y \<in> \<C>\<close>] have "x = Y \<or> suc Y \<subseteq> x" by blast
then show False
proof
assume "x = Y"
with \<open>y \<in> x\<close> and \<open>y \<notin> Y\<close> show False by blast
next
assume "suc Y \ x"
with \<open>x \<in> X\<close> have "suc Y \<subseteq> \<Union>X" by blast
with \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False by contradiction
qed
next
assume "suc x \ Y"
moreover from suc_subset and \<open>y \<in> x\<close> have "y \<in> suc x" by blast
ultimately show False using \<open>y \<notin> Y\<close> by blast
qed
qed
qed
text \<open>The elements of \<^term>\<open>\<C>\<close> are totally ordered by the subset relation.\<close>
lemma suc_Union_closed_total:
assumes "X \ \" and "Y \ \"
shows "X \ Y \ Y \ X"
proof (cases "\Z\\. Z \ Y \ Z = Y \ suc Z \ Y")
case True
with suc_Union_closed_total' [OF assms]
have "X \ Y \ suc Y \ X" by blast
with suc_subset [of Y] show ?thesis by blast
next
case False
then obtain Z where "Z \ \" and "Z \ Y" and "Z \ Y" and "\ suc Z \ Y"
by blast
with suc_Union_closed_subsetD and \<open>Y \<in> \<C>\<close> show ?thesis
by blast
qed
text \<open>Once we hit a fixed point w.r.t. \<^term>\<open>suc\<close>, all other elements
of \<^term>\<open>\<C>\<close> are subsets of this fixed point.\<close>
lemma suc_Union_closed_suc:
assumes "X \ \" and "Y \ \" and "suc Y = Y"
shows "X \ Y"
using \<open>X \<in> \<C>\<close>
proof induct
case (suc X)
with \<open>Y \<in> \<C>\<close> and suc_Union_closed_subsetD have "X = Y \<or> suc X \<subseteq> Y"
by blast
then show ?case
by (auto simp: \<open>suc Y = Y\<close>)
next
case Union
then show ?case by blast
qed
lemma eq_suc_Union:
assumes "X \ \"
shows "suc X = X \ X = \\"
(is "?lhs \ ?rhs")
proof
assume ?lhs
then have "\\ \ X"
by (rule suc_Union_closed_suc [OF suc_Union_closed_Union \<open>X \<in> \<C>\<close>])
with \<open>X \<in> \<C>\<close> show ?rhs
by blast
next
from \<open>X \<in> \<C>\<close> have "suc X \<in> \<C>" by (rule suc)
then have "suc X \ \\" by blast
moreover assume ?rhs
ultimately have "suc X \ X" by simp
moreover have "X \ suc X" by (rule suc_subset)
ultimately show ?lhs ..
qed
lemma suc_in_carrier:
assumes "X \ A"
shows "suc X \ A"
using assms
by (cases "\ chain X \ maxchain X") (auto dest: chain_sucD)
lemma suc_Union_closed_in_carrier:
assumes "X \ \"
shows "X \ A"
using assms
by induct (auto dest: suc_in_carrier)
text \<open>All elements of \<^term>\<open>\<C>\<close> are chains.\<close>
lemma suc_Union_closed_chain:
assumes "X \ \"
shows "chain X"
using assms
proof induct
case (suc X)
then show ?case
using not_maxchain_Some by (simp add: suc_def)
next
case (Union X)
then have "\X \ A"
by (auto dest: suc_Union_closed_in_carrier)
moreover have "\x\\X. \y\\X. x \ y \ y \ x"
proof (intro ballI)
fix x y
assume "x \ \X" and "y \ \X"
then obtain u v where "x \ u" and "u \ X" and "y \ v" and "v \ X"
by blast
with Union have "u \ \" and "v \ \" and "chain u" and "chain v"
by blast+
with suc_Union_closed_total have "u \ v \ v \ u"
by blast
then show "x \ y \ y \ x"
proof
assume "u \ v"
from \<open>chain v\<close> show ?thesis
proof (rule chain_total)
show "y \ v" by fact
show "x \ v" using \u \ v\ and \x \ u\ by blast
qed
next
assume "v \ u"
from \<open>chain u\<close> show ?thesis
proof (rule chain_total)
show "x \ u" by fact
show "y \ u" using \v \ u\ and \y \ v\ by blast
qed
qed
qed
ultimately show ?case unfolding chain_def ..
qed
subsubsection \<open>Hausdorff's Maximum Principle\<close>
text \<open>There exists a maximal totally ordered subset of \<open>A\<close>. (Note that we do not
require \<open>A\<close> to be partially ordered.)\<close>
theorem Hausdorff: "\C. maxchain C"
proof -
let ?M = "\\"
have "maxchain ?M"
proof (rule ccontr)
assume "\ ?thesis"
then have "suc ?M \ ?M"
using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
moreover have "suc ?M = ?M"
using eq_suc_Union [OF suc_Union_closed_Union] by simp
ultimately show False by contradiction
qed
then show ?thesis by blast
qed
text \<open>Make notation \<^term>\<open>\<C>\<close> available again.\<close>
no_notation suc_Union_closed ("\")
lemma chain_extend: "chain C \ z \ A \ \x\C. x \ z \ chain ({z} \ C)"
unfolding chain_def by blast
lemma maxchain_imp_chain: "maxchain C \ chain C"
by (simp add: maxchain_def)
end
text \<open>Hide constant \<^const>\<open>pred_on.suc_Union_closed\<close>, which was just needed
for the proof of Hausforff's maximum principle.\
hide_const pred_on.suc_Union_closed
lemma chain_mono:
assumes "\x y. x \ A \ y \ A \ P x y \ Q x y"
and "pred_on.chain A P C"
shows "pred_on.chain A Q C"
using assms unfolding pred_on.chain_def by blast
subsubsection \<open>Results for the proper subset relation\<close>
interpretation subset: pred_on "A" "(\)" for A .
lemma subset_maxchain_max:
assumes "subset.maxchain A C"
and "X \ A"
and "\C \ X"
shows "\C = X"
proof (rule ccontr)
let ?C = "{X} \ C"
from \<open>subset.maxchain A C\<close> have "subset.chain A C"
and *: "\S. subset.chain A S \ \ C \ S"
by (auto simp: subset.maxchain_def)
moreover have "\x\C. x \ X" using \\C \ X\ by auto
ultimately have "subset.chain A ?C"
using subset.chain_extend [of A C X] and \<open>X \<in> A\<close> by auto
moreover assume **: "\C \ X"
moreover from ** have "C \ ?C" using \\C \ X\ by auto
ultimately show False using * by blast
qed
lemma subset_chain_def: "\\. subset.chain \ \ = (\ \ \ \ (\X\\. \Y\\. X \ Y \ Y \ X))"
by (auto simp: subset.chain_def)
lemma subset_chain_insert:
"subset.chain \ (insert B \) \ B \ \ \ (\X\\. X \ B \ B \ X) \ subset.chain \ \"
by (fastforce simp add: subset_chain_def)
subsubsection \<open>Zorn's lemma\<close>
text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
theorem subset_Zorn:
assumes "\C. subset.chain A C \ \U\A. \X\C. X \ U"
shows "\M\A. \X\A. M \ X \ X = M"
proof -
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
then have "subset.chain A M"
by (rule subset.maxchain_imp_chain)
with assms obtain Y where "Y \ A" and "\X\M. X \ Y"
by blast
moreover have "\X\A. Y \ X \ Y = X"
proof (intro ballI impI)
fix X
assume "X \ A" and "Y \ X"
show "Y = X"
proof (rule ccontr)
assume "\ ?thesis"
with \<open>Y \<subseteq> X\<close> have "\<not> X \<subseteq> Y" by blast
from subset.chain_extend [OF \<open>subset.chain A M\<close> \<open>X \<in> A\<close>] and \<open>\<forall>X\<in>M. X \<subseteq> Y\<close>
have "subset.chain A ({X} \ M)"
using \<open>Y \<subseteq> X\<close> by auto
moreover have "M \ {X} \ M"
using \<open>\<forall>X\<in>M. X \<subseteq> Y\<close> and \<open>\<not> X \<subseteq> Y\<close> by auto
ultimately show False
using \<open>subset.maxchain A M\<close> by (auto simp: subset.maxchain_def)
qed
qed
ultimately show ?thesis by blast
qed
text \<open>Alternative version of Zorn's lemma for the subset relation.\<close>
lemma subset_Zorn':
assumes "\C. subset.chain A C \ \C \ A"
shows "\M\A. \X\A. M \ X \ X = M"
proof -
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
then have "subset.chain A M"
by (rule subset.maxchain_imp_chain)
with assms have "\M \ A" .
moreover have "\Z\A. \M \ Z \ \M = Z"
proof (intro ballI impI)
fix Z
assume "Z \ A" and "\M \ Z"
with subset_maxchain_max [OF \<open>subset.maxchain A M\<close>]
show "\M = Z" .
qed
ultimately show ?thesis by blast
qed
subsection \<open>Zorn's Lemma for Partial Orders\<close>
text \<open>Relate old to new definitions.\<close>
definition chain_subset :: "'a set set \ bool" ("chain\<^sub>\") (* Define globally? In Set.thy? *)
where "chain\<^sub>\ C \ (\A\C. \B\C. A \ B \ B \ A)"
definition chains :: "'a set set \ 'a set set set"
where "chains A = {C. C \ A \ chain\<^sub>\ C}"
definition Chains :: "('a \ 'a) set \ 'a set set" (* Define globally? In Relation.thy? *)
where "Chains r = {C. \a\C. \b\C. (a, b) \ r \ (b, a) \ r}"
lemma chains_extend: "c \ chains S \ z \ S \ \x \ c. x \ z \ {z} \ c \ chains S"
for z :: "'a set"
unfolding chains_def chain_subset_def by blast
lemma mono_Chains: "r \ s \ Chains r \ Chains s"
unfolding Chains_def by blast
lemma chain_subset_alt_def: "chain\<^sub>\ C = subset.chain UNIV C"
unfolding chain_subset_def subset.chain_def by fast
lemma chains_alt_def: "chains A = {C. subset.chain A C}"
by (simp add: chains_def chain_subset_alt_def subset.chain_def)
lemma Chains_subset: "Chains r \ {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}"
by (force simp add: Chains_def pred_on.chain_def)
lemma Chains_subset':
assumes "refl r"
shows "{C. pred_on.chain UNIV (\x y. (x, y) \ r) C} \ Chains r"
using assms
by (auto simp add: Chains_def pred_on.chain_def refl_on_def)
lemma Chains_alt_def:
assumes "refl r"
shows "Chains r = {C. pred_on.chain UNIV (\x y. (x, y) \ r) C}"
using assms Chains_subset Chains_subset' by blast
lemma Chains_relation_of:
assumes "C \ Chains (relation_of P A)" shows "C \ A"
using assms unfolding Chains_def relation_of_def by auto
lemma pairwise_chain_Union:
assumes P: "\S. S \ \ \ pairwise R S" and "chain\<^sub>\ \"
shows "pairwise R (\\)"
using \<open>chain\<^sub>\<subseteq> \<C>\<close> unfolding pairwise_def chain_subset_def
by (blast intro: P [unfolded pairwise_def, rule_format])
lemma Zorn_Lemma: "\C\chains A. \C \ A \ \M\A. \X\A. M \ X \ X = M"
using subset_Zorn' [of A] by (force simp: chains_alt_def)
lemma Zorn_Lemma2: "\C\chains A. \U\A. \X\C. X \ U \ \M\A. \X\A. M \ X \ X = M"
using subset_Zorn [of A] by (auto simp: chains_alt_def)
subsection \<open>Other variants of Zorn's Lemma\<close>
lemma chainsD: "c \ chains S \ x \ c \ y \ c \ x \ y \ y \ x"
unfolding chains_def chain_subset_def by blast
lemma chainsD2: "c \ chains S \ c \ S"
unfolding chains_def by blast
lemma Zorns_po_lemma:
assumes po: "Partial_order r"
and u: "\C. C \ Chains r \ \u\Field r. \a\C. (a, u) \ r"
shows "\m\Field r. \a\Field r. (m, a) \ r \ a = m"
proof -
have "Preorder r"
using po by (simp add: partial_order_on_def)
txt \<open>Mirror \<open>r\<close> in the set of subsets below (wrt \<open>r\<close>) elements of \<open>A\<close>.\<close>
let ?B = "\x. r\ `` {x}"
let ?S = "?B ` Field r"
have "\u\Field r. \A\C. A \ r\ `` {u}" (is "\u\Field r. ?P u")
if 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B \ B \ A" for C
proof -
let ?A = "{x\Field r. \M\C. M = ?B x}"
from 1 have "C = ?B ` ?A" by (auto simp: image_def)
have "?A \ Chains r"
proof (simp add: Chains_def, intro allI impI, elim conjE)
fix a b
assume "a \ Field r" and "?B a \ C" and "b \ Field r" and "?B b \ C"
with 2 have "?B a \ ?B b \ ?B b \ ?B a" by auto
then show "(a, b) \ r \ (b, a) \ r"
using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close>
by (simp add:subset_Image1_Image1_iff)
qed
then obtain u where uA: "u \ Field r" "\a\?A. (a, u) \ r"
by (auto simp: dest: u)
have "?P u"
proof auto
fix a B assume aB: "B \ C" "a \ B"
with 1 obtain x where "x \ Field r" and "B = r\ `` {x}" by auto
then show "(a, u) \ r"
using uA and aB and \<open>Preorder r\<close>
unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
qed
then show ?thesis
using \<open>u \<in> Field r\<close> by blast
qed
then have "\C\chains ?S. \U\?S. \A\C. A \ U"
by (auto simp: chains_def chain_subset_def)
from Zorn_Lemma2 [OF this] obtain m B
where "m \ Field r"
and "B = r\ `` {m}"
and "\x\Field r. B \ r\ `` {x} \ r\ `` {x} = B"
by auto
then have "\a\Field r. (m, a) \ r \ a = m"
using po and \<open>Preorder r\<close> and \<open>m \<in> Field r\<close>
by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
then show ?thesis
using \<open>m \<in> Field r\<close> by blast
qed
lemma predicate_Zorn:
assumes po: "partial_order_on A (relation_of P A)"
and ch: "\C. C \ Chains (relation_of P A) \ \u \ A. \a \ C. P a u"
shows "\m \ A. \a \ A. P m a \ a = m"
proof -
have "a \ A" if "C \ Chains (relation_of P A)" and "a \ C" for C a
using that unfolding Chains_def relation_of_def by auto
moreover have "(a, u) \ relation_of P A" if "a \ A" and "u \ A" and "P a u" for a u
unfolding relation_of_def using that by auto
ultimately have "\m\A. \a\A. (m, a) \ relation_of P A \ a = m"
using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
then show ?thesis
by (auto simp: relation_of_def)
qed
lemma Union_in_chain: "\finite \; \ \ {}; subset.chain \ \\ \ \\ \ \"
proof (induction \<B> rule: finite_induct)
case (insert B \<B>)
show ?case
proof (cases "\ = {}")
case False
then show ?thesis
using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\\"])
qed auto
qed simp
lemma Inter_in_chain: "\finite \; \ \ {}; subset.chain \ \\ \ \\ \ \"
proof (induction \<B> rule: finite_induct)
case (insert B \<B>)
show ?case
proof (cases "\ = {}")
case False
then show ?thesis
using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\\"])
qed auto
qed simp
lemma finite_subset_Union_chain:
assumes "finite A" "A \ \\" "\ \ {}" and sub: "subset.chain \ \"
obtains B where "B \ \" "A \ B"
proof -
obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
using assms by (auto intro: finite_subset_Union)
show thesis
proof (cases "\ = {}")
case True
then show ?thesis
using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
next
case False
show ?thesis
proof
show "\\ \ \"
using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
by (simp add: Union_in_chain False subset.chain_def subset_iff)
show "A \ \\"
using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
qed
qed
qed
lemma subset_Zorn_nonempty:
assumes "\ \ {}" and ch: "\\. \\\{}; subset.chain \ \\ \ \\ \ \"
shows "\M\\. \X\\. M \ X \ X = M"
proof (rule subset_Zorn)
show "\U\\. \X\\. X \ U" if "subset.chain \ \" for \
proof (cases "\ = {}")
case True
then show ?thesis
using \<open>\<A> \<noteq> {}\<close> by blast
next
case False
show ?thesis
by (blast intro!: ch False that Union_upper)
qed
qed
subsection \<open>The Well Ordering Theorem\<close>
(* The initial segment of a relation appears generally useful.
Move to Relation.thy?
Definition correct/most general?
Naming?
*)
definition init_seg_of :: "(('a \ 'a) set \ ('a \ 'a) set) set"
where "init_seg_of = {(r, s). r \ s \ (\a b c. (a, b) \ s \ (b, c) \ r \ (a, b) \ r)}"
abbreviation initial_segment_of_syntax :: "('a \ 'a) set \ ('a \ 'a) set \ bool"
(infix "initial'_segment'_of" 55)
where "r initial_segment_of s \ (r, s) \ init_seg_of"
lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
by (simp add: init_seg_of_def)
lemma trans_init_seg_of:
"r initial_segment_of s \ s initial_segment_of t \ r initial_segment_of t"
by (simp (no_asm_use) add: init_seg_of_def) blast
lemma antisym_init_seg_of: "r initial_segment_of s \ s initial_segment_of r \ r = s"
unfolding init_seg_of_def by safe
lemma Chains_init_seg_of_Union: "R \ Chains init_seg_of \ r\R \ r initial_segment_of \R"
by (auto simp: init_seg_of_def Ball_def Chains_def) blast
lemma chain_subset_trans_Union:
assumes "chain\<^sub>\ R" "\r\R. trans r"
shows "trans (\R)"
proof (intro transI, elim UnionE)
fix S1 S2 :: "'a rel" and x y z :: 'a
assume "S1 \ R" "S2 \ R"
with assms(1) have "S1 \ S2 \ S2 \ S1"
unfolding chain_subset_def by blast
moreover assume "(x, y) \ S1" "(y, z) \ S2"
ultimately have "((x, y) \ S1 \ (y, z) \ S1) \ ((x, y) \ S2 \ (y, z) \ S2)"
by blast
with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "(x, z) \<in> \<Union>R"
by (auto elim: transE)
qed
lemma chain_subset_antisym_Union:
assumes "chain\<^sub>\ R" "\r\R. antisym r"
shows "antisym (\R)"
proof (intro antisymI, elim UnionE)
fix S1 S2 :: "'a rel" and x y :: 'a
assume "S1 \ R" "S2 \ R"
with assms(1) have "S1 \ S2 \ S2 \ S1"
unfolding chain_subset_def by blast
moreover assume "(x, y) \ S1" "(y, x) \ S2"
ultimately have "((x, y) \ S1 \ (y, x) \ S1) \ ((x, y) \ S2 \ (y, x) \ S2)"
by blast
with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "x = y"
unfolding antisym_def by auto
qed
lemma chain_subset_Total_Union:
assumes "chain\<^sub>\ R" and "\r\R. Total r"
shows "Total (\R)"
proof (simp add: total_on_def Ball_def, auto del: disjCI)
fix r s a b
assume A: "r \ R" "s \ R" "a \ Field r" "b \ Field s" "a \ b"
from \<open>chain\<^sub>\<subseteq> R\<close> and \<open>r \<in> R\<close> and \<open>s \<in> R\<close> have "r \<subseteq> s \<or> s \<subseteq> r"
by (auto simp add: chain_subset_def)
then show "(\r\R. (a, b) \ r) \ (\r\R. (b, a) \ r)"
proof
assume "r \ s"
then have "(a, b) \ s \ (b, a) \ s"
using assms(2) A mono_Field[of r s]
by (auto simp add: total_on_def)
then show ?thesis
using \<open>s \<in> R\<close> by blast
next
assume "s \ r"
then have "(a, b) \ r \ (b, a) \ r"
using assms(2) A mono_Field[of s r]
by (fastforce simp add: total_on_def)
then show ?thesis
using \<open>r \<in> R\<close> by blast
qed
qed
lemma wf_Union_wf_init_segs:
assumes "R \ Chains init_seg_of"
and "\r\R. wf r"
shows "wf (\R)"
proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
fix f
assume 1: "\i. \r\R. (f (Suc i), f i) \ r"
then obtain r where "r \ R" and "(f (Suc 0), f 0) \ r" by auto
have "(f (Suc i), f i) \ r" for i
proof (induct i)
case 0
show ?case by fact
next
case (Suc i)
then obtain s where s: "s \ R" "(f (Suc (Suc i)), f(Suc i)) \ s"
using 1 by auto
then have "s initial_segment_of r \ r initial_segment_of s"
using assms(1) \<open>r \<in> R\<close> by (simp add: Chains_def)
with Suc s show ?case by (simp add: init_seg_of_def) blast
qed
then show False
using assms(2) and \<open>r \<in> R\<close>
by (simp add: wf_iff_no_infinite_down_chain) blast
qed
lemma initial_segment_of_Diff: "p initial_segment_of q \ p - s initial_segment_of q - s"
unfolding init_seg_of_def by blast
lemma Chains_inits_DiffI: "R \ Chains init_seg_of \ {r - s |r. r \ R} \ Chains init_seg_of"
unfolding Chains_def by (blast intro: initial_segment_of_Diff)
theorem well_ordering: "\r::'a rel. Well_order r \ Field r = UNIV"
proof -
\<comment> \<open>The initial segment relation on well-orders:\<close>
let ?WO = "{r::'a rel. Well_order r}"
define I where "I = init_seg_of \ ?WO \ ?WO"
then have I_init: "I \ init_seg_of" by simp
then have subch: "\R. R \ Chains I \ chain\<^sub>\ R"
unfolding init_seg_of_def chain_subset_def Chains_def by blast
have Chains_wo: "\R r. R \ Chains I \ r \ R \ Well_order r"
by (simp add: Chains_def I_def) blast
have FI: "Field I = ?WO"
by (auto simp add: I_def init_seg_of_def Field_def)
then have 0: "Partial_order I"
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
trans_def I_def elim!: trans_init_seg_of)
\<comment> \<open>\<open>I\<close>-chains have upper bounds in \<open>?WO\<close> wrt \<open>I\<close>: their Union\<close>
have "\R \ ?WO \ (\r\R. (r, \R) \ I)" if "R \ Chains I" for R
proof -
from that have Ris: "R \ Chains init_seg_of"
using mono_Chains [OF I_init] by blast
have subch: "chain\<^sub>\ R"
using \<open>R \<in> Chains I\<close> I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def)
have "\r\R. Refl r" and "\r\R. trans r" and "\r\R. antisym r"
and "\r\R. Total r" and "\r\R. wf (r - Id)"
using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
have "Refl (\R)"
using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
moreover have "trans (\R)"
by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
moreover have "antisym (\R)"
by (rule chain_subset_antisym_Union [OF subch \<open>\<forall>r\<in>R. antisym r\<close>])
moreover have "Total (\R)"
by (rule chain_subset_Total_Union [OF subch \<open>\<forall>r\<in>R. Total r\<close>])
moreover have "wf ((\R) - Id)"
proof -
have "(\R) - Id = \{r - Id | r. r \ R}" by blast
with \<open>\<forall>r\<in>R. wf (r - Id)\<close> and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
show ?thesis by fastforce
qed
ultimately have "Well_order (\R)"
by (simp add:order_on_defs)
moreover have "\r \ R. r initial_segment_of \R"
using Ris by (simp add: Chains_init_seg_of_Union)
ultimately show ?thesis
using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close>
unfolding I_def by blast
qed
then have 1: "\u\Field I. \r\R. (r, u) \ I" if "R \ Chains I" for R
using that by (subst FI) blast
\<comment> \<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close>
then obtain m :: "'a rel"
where "Well_order m"
and max: "\r. Well_order r \ (m, r) \ I \ r = m"
using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
\<comment> \<open>Now show by contradiction that \<open>m\<close> covers the whole type:\<close>
have False if "x \ Field m" for x :: 'a
proof -
\<comment> \<open>Assuming that \<open>x\<close> is not covered and extend \<open>m\<close> at the top with \<open>x\<close>\<close>
have "m \ {}"
proof
assume "m = {}"
moreover have "Well_order {(x, x)}"
by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def)
ultimately show False using max
by (auto simp: I_def init_seg_of_def simp del: Field_insert)
qed
then have "Field m \ {}" by (auto simp: Field_def)
moreover have "wf (m - Id)"
using \<open>Well_order m\<close> by (simp add: well_order_on_def)
\<comment> \<open>The extension of \<open>m\<close> by \<open>x\<close>:\<close>
let ?s = "{(a, x) | a. a \ Field m}"
let ?m = "insert (x, x) m \ ?s"
have Fm: "Field ?m = insert x (Field m)"
by (auto simp: Field_def)
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
\<comment> \<open>We show that the extension is a well-order\<close>
have "Refl ?m"
using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
unfolding trans_def Field_def by blast
moreover have "antisym ?m"
using \<open>antisym m\<close> and \<open>x \<notin> Field m\<close> unfolding antisym_def Field_def by blast
moreover have "Total ?m"
using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
moreover have "wf (?m - Id)"
proof -
have "wf ?s"
using \<open>x \<notin> Field m\<close> by (auto simp: wf_eq_minimal Field_def Bex_def)
then show ?thesis
using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close> wf_subset [OF \<open>wf ?s\<close> Diff_subset]
by (auto simp: Un_Diff Field_def intro: wf_Un)
qed
ultimately have "Well_order ?m"
by (simp add: order_on_defs)
\<comment> \<open>We show that the extension is above \<open>m\<close>\<close>
moreover have "(m, ?m) \ I"
using \<open>Well_order ?m\<close> and \<open>Well_order m\<close> and \<open>x \<notin> Field m\<close>
by (fastforce simp: I_def init_seg_of_def Field_def)
ultimately
\<comment> \<open>This contradicts maximality of \<open>m\<close>:\<close>
show False
using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
qed
then have "Field m = UNIV" by auto
with \<open>Well_order m\<close> show ?thesis by blast
qed
corollary well_order_on: "\r::'a rel. well_order_on A r"
proof -
obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
using well_ordering [where 'a = "'a"] by blast
let ?r = "{(x, y). x \ A \ y \ A \ (x, y) \ r}"
have 1: "Field ?r = A"
using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
by (simp_all add: order_on_defs)
from \<open>Refl r\<close> have "Refl ?r"
by (auto simp: refl_on_def 1 univ)
moreover from \<open>trans r\<close> have "trans ?r"
unfolding trans_def by blast
moreover from \<open>antisym r\<close> have "antisym ?r"
unfolding antisym_def by blast
moreover from \<open>Total r\<close> have "Total ?r"
by (simp add:total_on_def 1 univ)
moreover have "wf (?r - Id)"
by (rule wf_subset [OF \<open>wf (r - Id)\<close>]) blast
ultimately have "Well_order ?r"
by (simp add: order_on_defs)
with 1 show ?thesis by auto
qed
(* Move this to Hilbert Choice and wfrec to Wellfounded*)
lemma wfrec_def_adm: "f \ wfrec R F \ wf R \ adm_wf R F \ f = F f"
using wfrec_fixpoint by simp
lemma dependent_wf_choice:
fixes P :: "('a \ 'b) \ 'a \ 'b \ bool"
assumes "wf R"
and adm: "\f g x r. (\z. (z, x) \ R \ f z = g z) \ P f x r = P g x r"
and P: "\x f. (\y. (y, x) \ R \ P f y (f y)) \ \r. P f x r"
shows "\f. \x. P f x (f x)"
proof (intro exI allI)
fix x
define f where "f \ wfrec R (\f x. SOME r. P f x r)"
from \<open>wf R\<close> show "P f x (f x)"
proof (induct x)
case (less x)
show "P f x (f x)"
proof (subst (2) wfrec_def_adm[OF f_def \<open>wf R\<close>])
show "adm_wf R (\f x. SOME r. P f x r)"
by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
show "P f x (Eps (P f x))"
using P by (rule someI_ex) fact
qed
qed
qed
lemma (in wellorder) dependent_wellorder_choice:
assumes "\r f g x. (\y. y < x \ f y = g y) \ P f x r = P g x r"
and P: "\x f. (\y. y < x \ P f y (f y)) \ \r. P f x r"
shows "\f. \x. P f x (f x)"
using wf by (rule dependent_wf_choice) (auto intro!: assms)
end
¤ Dauer der Verarbeitung: 0.59 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
