Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 38 kB

Quelle Zorn.thy Sprache: Isabelle

(* 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).
*)

section \<open>Zorn's Lemma and the Well-ordering Theorem\<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 \ 50)
 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 (\<open>\<C>\<close>)
 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> subset_suc show ?thesis
 by fastforce
 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>] \<open>y \<in> x\<close> \<open>y \<notin> Y\<close> \<open>x \<in> X\<close> \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False
 by blast
 next
 assume "suc x \ Y"
 with \<open>y \<notin> Y\<close> suc_subset \<open>y \<in> x\<close> show False 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 (\<open>\<C>\<close>)

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(4)[OF po] 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 \ rule: finite_induct)
 case (insert 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 \ rule: finite_induct)
 case (insert 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> \" "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>\ \<noteq> {}\<close> that by fastforce
 next
 case False
 show ?thesis
 proof
 show "\\ \ \"
 using sub \<open>\<F> \<subseteq> \\<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 \<open>initial'_segment'_of\<close> 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 "(\ R) \ Field (\ R) \ Field (\ R)"
 unfolding Field_def by auto
 moreover 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)" and
 "m \ Field m \ Field m"
 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 "?m \ Field ?m \ Field ?m"
 using \<open>m \<subseteq> Field m \<times> Field m\<close> by auto
 moreover 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)" and
 "r \ Field r \ Field r"
 by (simp_all add: order_on_defs)
 have "?r \ Field ?r \ Field ?r"
 using \<open>r \<subseteq> Field r \<times> Field r\<close> by (auto simp: 1)
 moreover 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

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: adm_wf_def intro!: arg_cong[where f=Eps] 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

quality99%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.