(* 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.
*)
header {* Zorn's Lemma *}
theory Zorn
imports Order_Relation Hilbert_Choice
begin
subsection {* Zorn's Lemma for the Subset Relation *}
subsubsection {* Results that do not require an order *}
text {*Let @{text P} be a binary predicate on the set @{text A}.*}
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 {*A chain is a totally ordered subset of @{term A}.*}
definition chain :: "'a set \ bool" where
"chain C \ C \ A \ (\x\C. \y\C. x \ y \ y \ x)"
text {*We call a chain that is a proper superset of some set @{term X},
but not necessarily a chain itself, a superchain of @{term X}.*}
abbreviation superchain :: "'a set \ 'a set \ bool" (infix " chain C \ X \ C"
text {*A maximal chain is a chain that does not have a superchain.*}
definition maxchain :: "'a set \ bool" where
"maxchain C \ chain C \ \ (\S. C 'a set" where
"suc C = (if \ chain C \ maxchain C then C else (SOME D. C 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 \ maxchain C \ suc C \ C"
by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some)
lemma subset_suc:
assumes "X \ Y" shows "X \ suc Y"
using assms by (rule subset_trans) (rule suc_subset)
text {*We build a set @{term \} that is closed under applications
of @{term suc} and contains the union of all its subsets.*}
inductive_set suc_Union_closed ("\") where
suc: "X \ \ \ suc X \ \" |
Union [unfolded Pow_iff]: "X \ Pow \ \ \X \ \"
text {*Since the empty set as well as the set itself is a subset of
every set, @{term \} contains at least @{term "{} \ \"} and
@{term "\\ \ \"}.*}
lemma
suc_Union_closed_empty: "{} \ \" and
suc_Union_closed_Union: "\\ \ \"
using Union [of "{}"] and Union [of "\"] by simp+
text {*Thus closure under @{term suc} will hit a maximal chain
eventually, as is shown below.*}
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+
text {*On chains, @{term suc} yields a chain.*}
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 `chain X` 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 `X \ \`
proof (induct)
case (suc X)
with * show ?case by (blast del: subsetI intro: subset_suc)
qed blast
lemma suc_Union_closed_subsetD:
assumes "Y \ X" and "X \ \" and "Y \ \"
shows "X = Y \ suc Y \ X"
using assms(2-, 1)
proof (induct arbitrary: Y)
case (suc X)
note * = `\Y. \Y \ \; Y \ X\ \ X = Y \ suc Y \ X`
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 `Y \ \` have "X = Y \ suc Y \ 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 `Y \ suc X` show ?thesis by blast
qed
next
case (Union X)
show ?case
proof (rule ccontr)
assume "\ ?thesis"
with `Y \ \X` 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 `X \ \` have "x \ \" by blast
from Union and `x \ X`
have *: "\y. \y \ \; y \ x\ \ x = y \ suc y \ 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 `Y \ \`] have "x = Y \ suc Y \ x" by blast
then show False
proof
assume "x = Y" with `y \ x` and `y \ Y` show False by blast
next
assume "suc Y \ x"
with `x \ X` have "suc Y \ \X" by blast
with `\ suc Y \ \X` show False by contradiction
qed
next
assume "suc x \ Y"
moreover from suc_subset and `y \ x` have "y \ suc x" by blast
ultimately show False using `y \ Y` by blast
qed
qed
qed
text {*The elements of @{term \} are totally ordered by the subset relation.*}
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
then show ?thesis using suc_subset [of Y] 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 `Y \