src/ZF/Zorn.thy
 author wenzelm Thu Dec 14 11:24:26 2017 +0100 (20 months ago) changeset 67198 694f29a5433b parent 61980 6b780867d426 child 67443 3abf6a722518 permissions -rw-r--r--
merged
 clasohm@1478 ` 1` ```(* Title: ZF/Zorn.thy ``` clasohm@1478 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@516 ` 3` ``` Copyright 1994 University of Cambridge ``` lcp@516 ` 4` ```*) ``` lcp@516 ` 5` wenzelm@60770 ` 6` ```section\Zorn's Lemma\ ``` paulson@13356 ` 7` krauss@26056 ` 8` ```theory Zorn imports OrderArith AC Inductive_ZF begin ``` lcp@516 ` 9` wenzelm@60770 ` 10` ```text\Based upon the unpublished article ``Towards the Mechanization of the ``` wenzelm@60770 ` 11` ```Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\ ``` paulson@13356 ` 12` wenzelm@24893 ` 13` ```definition ``` wenzelm@24893 ` 14` ``` Subset_rel :: "i=>i" where ``` paulson@13558 ` 15` ``` "Subset_rel(A) == {z \ A*A . \x y. z= & x<=y & x\y}" ``` paulson@13134 ` 16` wenzelm@24893 ` 17` ```definition ``` wenzelm@24893 ` 18` ``` chain :: "i=>i" where ``` paulson@13558 ` 19` ``` "chain(A) == {F \ Pow(A). \X\F. \Y\F. X<=Y | Y<=X}" ``` lcp@516 ` 20` wenzelm@24893 ` 21` ```definition ``` wenzelm@24893 ` 22` ``` super :: "[i,i]=>i" where ``` wenzelm@14653 ` 23` ``` "super(A,c) == {d \ chain(A). c<=d & c\d}" ``` wenzelm@14653 ` 24` wenzelm@24893 ` 25` ```definition ``` wenzelm@24893 ` 26` ``` maxchain :: "i=>i" where ``` paulson@13558 ` 27` ``` "maxchain(A) == {c \ chain(A). super(A,c)=0}" ``` paulson@13558 ` 28` wenzelm@24893 ` 29` ```definition ``` wenzelm@24893 ` 30` ``` increasing :: "i=>i" where ``` paulson@46820 ` 31` ``` "increasing(A) == {f \ Pow(A)->Pow(A). \x. x<=A \ x<=f`x}" ``` lcp@516 ` 32` paulson@13356 ` 33` wenzelm@60770 ` 34` ```text\Lemma for the inductive definition below\ ``` paulson@46820 ` 35` ```lemma Union_in_Pow: "Y \ Pow(Pow(A)) ==> \(Y) \ Pow(A)" ``` paulson@13356 ` 36` ```by blast ``` paulson@13356 ` 37` paulson@13356 ` 38` wenzelm@60770 ` 39` ```text\We could make the inductive definition conditional on ``` paulson@13356 ` 40` ``` @{term "next \ increasing(S)"} ``` lcp@516 ` 41` ``` but instead we make this a side-condition of an introduction rule. Thus ``` lcp@516 ` 42` ``` the induction rule lets us assume that condition! Many inductive proofs ``` wenzelm@60770 ` 43` ``` are therefore unconditional.\ ``` lcp@516 ` 44` ```consts ``` paulson@13134 ` 45` ``` "TFin" :: "[i,i]=>i" ``` lcp@516 ` 46` lcp@516 ` 47` ```inductive ``` paulson@46820 ` 48` ``` domains "TFin(S,next)" \ "Pow(S)" ``` paulson@13134 ` 49` ``` intros ``` paulson@13558 ` 50` ``` nextI: "[| x \ TFin(S,next); next \ increasing(S) |] ``` paulson@13558 ` 51` ``` ==> next`x \ TFin(S,next)" ``` lcp@516 ` 52` paulson@46820 ` 53` ``` Pow_UnionI: "Y \ Pow(TFin(S,next)) ==> \(Y) \ TFin(S,next)" ``` lcp@516 ` 54` paulson@6053 ` 55` ``` monos Pow_mono ``` paulson@6053 ` 56` ``` con_defs increasing_def ``` paulson@13134 ` 57` ``` type_intros CollectD1 [THEN apply_funtype] Union_in_Pow ``` paulson@13134 ` 58` paulson@13134 ` 59` wenzelm@60770 ` 60` ```subsection\Mathematical Preamble\ ``` paulson@13134 ` 61` paulson@46820 ` 62` ```lemma Union_lemma0: "(\x\C. x<=A | B<=x) ==> \(C)<=A | B<=\(C)" ``` paulson@13269 ` 63` ```by blast ``` paulson@13134 ` 64` paulson@13356 ` 65` ```lemma Inter_lemma0: ``` paulson@46820 ` 66` ``` "[| c \ C; \x\C. A<=x | x<=B |] ==> A \ \(C) | \(C) \ B" ``` paulson@13269 ` 67` ```by blast ``` paulson@13134 ` 68` paulson@13134 ` 69` wenzelm@60770 ` 70` ```subsection\The Transfinite Construction\ ``` paulson@13134 ` 71` paulson@13558 ` 72` ```lemma increasingD1: "f \ increasing(A) ==> f \ Pow(A)->Pow(A)" ``` paulson@13134 ` 73` ```apply (unfold increasing_def) ``` paulson@13134 ` 74` ```apply (erule CollectD1) ``` paulson@13134 ` 75` ```done ``` paulson@13134 ` 76` paulson@46820 ` 77` ```lemma increasingD2: "[| f \ increasing(A); x<=A |] ==> x \ f`x" ``` paulson@13269 ` 78` ```by (unfold increasing_def, blast) ``` paulson@13134 ` 79` wenzelm@45602 ` 80` ```lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI] ``` paulson@13134 ` 81` wenzelm@45602 ` 82` ```lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD] ``` paulson@13134 ` 83` paulson@13134 ` 84` wenzelm@60770 ` 85` ```text\Structural induction on @{term "TFin(S,next)"}\ ``` paulson@13134 ` 86` ```lemma TFin_induct: ``` paulson@13558 ` 87` ``` "[| n \ TFin(S,next); ``` paulson@13558 ` 88` ``` !!x. [| x \ TFin(S,next); P(x); next \ increasing(S) |] ==> P(next`x); ``` paulson@46820 ` 89` ``` !!Y. [| Y \ TFin(S,next); \y\Y. P(y) |] ==> P(\(Y)) ``` paulson@13134 ` 90` ``` |] ==> P(n)" ``` paulson@13356 ` 91` ```by (erule TFin.induct, blast+) ``` paulson@13134 ` 92` paulson@13134 ` 93` wenzelm@60770 ` 94` ```subsection\Some Properties of the Transfinite Construction\ ``` paulson@13134 ` 95` paulson@13558 ` 96` ```lemmas increasing_trans = subset_trans [OF _ increasingD2, ``` paulson@13134 ` 97` ``` OF _ _ TFin_is_subset] ``` paulson@13134 ` 98` wenzelm@60770 ` 99` ```text\Lemma 1 of section 3.1\ ``` paulson@13134 ` 100` ```lemma TFin_linear_lemma1: ``` paulson@13558 ` 101` ``` "[| n \ TFin(S,next); m \ TFin(S,next); ``` paulson@46820 ` 102` ``` \x \ TFin(S,next) . x<=m \ x=m | next`x<=m |] ``` paulson@13134 ` 103` ``` ==> n<=m | next`m<=n" ``` paulson@13134 ` 104` ```apply (erule TFin_induct) ``` paulson@13134 ` 105` ```apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*) ``` paulson@13134 ` 106` ```(*downgrade subsetI from intro! to intro*) ``` paulson@13134 ` 107` ```apply (blast dest: increasing_trans) ``` paulson@13134 ` 108` ```done ``` paulson@13134 ` 109` wenzelm@60770 ` 110` ```text\Lemma 2 of section 3.2. Interesting in its own right! ``` wenzelm@60770 ` 111` ``` Requires @{term "next \ increasing(S)"} in the second induction step.\ ``` paulson@13134 ` 112` ```lemma TFin_linear_lemma2: ``` paulson@13558 ` 113` ``` "[| m \ TFin(S,next); next \ increasing(S) |] ``` paulson@46820 ` 114` ``` ==> \n \ TFin(S,next). n<=m \ n=m | next`n \ m" ``` paulson@13134 ` 115` ```apply (erule TFin_induct) ``` paulson@13134 ` 116` ```apply (rule impI [THEN ballI]) ``` wenzelm@61798 ` 117` ```txt\case split using \TFin_linear_lemma1\\ ``` paulson@13784 ` 118` ```apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], ``` paulson@13134 ` 119` ``` assumption+) ``` paulson@13134 ` 120` ```apply (blast del: subsetI ``` wenzelm@32960 ` 121` ``` intro: increasing_trans subsetI, blast) ``` wenzelm@60770 ` 122` ```txt\second induction step\ ``` paulson@13134 ` 123` ```apply (rule impI [THEN ballI]) ``` paulson@13134 ` 124` ```apply (rule Union_lemma0 [THEN disjE]) ``` paulson@13134 ` 125` ```apply (erule_tac [3] disjI2) ``` paulson@13558 ` 126` ```prefer 2 apply blast ``` paulson@13134 ` 127` ```apply (rule ballI) ``` paulson@13558 ` 128` ```apply (drule bspec, assumption) ``` paulson@13558 ` 129` ```apply (drule subsetD, assumption) ``` paulson@13784 ` 130` ```apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], ``` paulson@13558 ` 131` ``` assumption+, blast) ``` paulson@13134 ` 132` ```apply (erule increasingD2 [THEN subset_trans, THEN disjI1]) ``` paulson@13134 ` 133` ```apply (blast dest: TFin_is_subset)+ ``` paulson@13134 ` 134` ```done ``` paulson@13134 ` 135` wenzelm@60770 ` 136` ```text\a more convenient form for Lemma 2\ ``` paulson@13134 ` 137` ```lemma TFin_subsetD: ``` paulson@13558 ` 138` ``` "[| n<=m; m \ TFin(S,next); n \ TFin(S,next); next \ increasing(S) |] ``` paulson@46820 ` 139` ``` ==> n=m | next`n \ m" ``` paulson@13558 ` 140` ```by (blast dest: TFin_linear_lemma2 [rule_format]) ``` paulson@13134 ` 141` wenzelm@60770 ` 142` ```text\Consequences from section 3.3 -- Property 3.2, the ordering is total\ ``` paulson@13134 ` 143` ```lemma TFin_subset_linear: ``` paulson@13558 ` 144` ``` "[| m \ TFin(S,next); n \ TFin(S,next); next \ increasing(S) |] ``` paulson@46820 ` 145` ``` ==> n \ m | m<=n" ``` paulson@13558 ` 146` ```apply (rule disjE) ``` paulson@13134 ` 147` ```apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2]) ``` paulson@13134 ` 148` ```apply (assumption+, erule disjI2) ``` paulson@13558 ` 149` ```apply (blast del: subsetI ``` paulson@13134 ` 150` ``` intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset) ``` paulson@13134 ` 151` ```done ``` paulson@13134 ` 152` paulson@13134 ` 153` wenzelm@60770 ` 154` ```text\Lemma 3 of section 3.3\ ``` paulson@13134 ` 155` ```lemma equal_next_upper: ``` paulson@46820 ` 156` ``` "[| n \ TFin(S,next); m \ TFin(S,next); m = next`m |] ==> n \ m" ``` paulson@13134 ` 157` ```apply (erule TFin_induct) ``` paulson@13134 ` 158` ```apply (drule TFin_subsetD) ``` paulson@13784 ` 159` ```apply (assumption+, force, blast) ``` paulson@13134 ` 160` ```done ``` paulson@13134 ` 161` wenzelm@60770 ` 162` ```text\Property 3.3 of section 3.3\ ``` paulson@13558 ` 163` ```lemma equal_next_Union: ``` paulson@13558 ` 164` ``` "[| m \ TFin(S,next); next \ increasing(S) |] ``` paulson@46820 ` 165` ``` ==> m = next`m <-> m = \(TFin(S,next))" ``` paulson@13134 ` 166` ```apply (rule iffI) ``` paulson@13134 ` 167` ```apply (rule Union_upper [THEN equalityI]) ``` paulson@13134 ` 168` ```apply (rule_tac [2] equal_next_upper [THEN Union_least]) ``` paulson@13134 ` 169` ```apply (assumption+) ``` paulson@13134 ` 170` ```apply (erule ssubst) ``` paulson@13269 ` 171` ```apply (rule increasingD2 [THEN equalityI], assumption) ``` paulson@13134 ` 172` ```apply (blast del: subsetI ``` wenzelm@32960 ` 173` ``` intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+ ``` paulson@13134 ` 174` ```done ``` paulson@13134 ` 175` paulson@13134 ` 176` wenzelm@60770 ` 177` ```subsection\Hausdorff's Theorem: Every Set Contains a Maximal Chain\ ``` paulson@13356 ` 178` wenzelm@61798 ` 179` ```text\NOTE: We assume the partial ordering is \\\, the subset ``` wenzelm@60770 ` 180` ```relation!\ ``` paulson@13134 ` 181` wenzelm@60770 ` 182` ```text\* Defining the "next" operation for Hausdorff's Theorem *\ ``` paulson@13134 ` 183` paulson@46820 ` 184` ```lemma chain_subset_Pow: "chain(A) \ Pow(A)" ``` paulson@13134 ` 185` ```apply (unfold chain_def) ``` paulson@13134 ` 186` ```apply (rule Collect_subset) ``` paulson@13134 ` 187` ```done ``` paulson@13134 ` 188` paulson@46820 ` 189` ```lemma super_subset_chain: "super(A,c) \ chain(A)" ``` paulson@13134 ` 190` ```apply (unfold super_def) ``` paulson@13134 ` 191` ```apply (rule Collect_subset) ``` paulson@13134 ` 192` ```done ``` paulson@13134 ` 193` paulson@46820 ` 194` ```lemma maxchain_subset_chain: "maxchain(A) \ chain(A)" ``` paulson@13134 ` 195` ```apply (unfold maxchain_def) ``` paulson@13134 ` 196` ```apply (rule Collect_subset) ``` paulson@13134 ` 197` ```done ``` paulson@13134 ` 198` paulson@13558 ` 199` ```lemma choice_super: ``` wenzelm@61980 ` 200` ``` "[| ch \ (\X \ Pow(chain(S)) - {0}. X); X \ chain(S); X \ maxchain(S) |] ``` paulson@13558 ` 201` ``` ==> ch ` super(S,X) \ super(S,X)" ``` paulson@13134 ` 202` ```apply (erule apply_type) ``` paulson@13269 ` 203` ```apply (unfold super_def maxchain_def, blast) ``` paulson@13134 ` 204` ```done ``` paulson@13134 ` 205` paulson@13134 ` 206` ```lemma choice_not_equals: ``` wenzelm@61980 ` 207` ``` "[| ch \ (\X \ Pow(chain(S)) - {0}. X); X \ chain(S); X \ maxchain(S) |] ``` paulson@13558 ` 208` ``` ==> ch ` super(S,X) \ X" ``` paulson@13134 ` 209` ```apply (rule notI) ``` paulson@13784 ` 210` ```apply (drule choice_super, assumption, assumption) ``` paulson@13134 ` 211` ```apply (simp add: super_def) ``` paulson@13134 ` 212` ```done ``` paulson@13134 ` 213` wenzelm@60770 ` 214` ```text\This justifies Definition 4.4\ ``` paulson@13134 ` 215` ```lemma Hausdorff_next_exists: ``` wenzelm@61980 ` 216` ``` "ch \ (\X \ Pow(chain(S))-{0}. X) ==> ``` paulson@13558 ` 217` ``` \next \ increasing(S). \X \ Pow(S). ``` paulson@13558 ` 218` ``` next`X = if(X \ chain(S)-maxchain(S), ch`super(S,X), X)" ``` paulson@13558 ` 219` ```apply (rule_tac x="\X\Pow(S). ``` paulson@13558 ` 220` ``` if X \ chain(S) - maxchain(S) then ch ` super(S, X) else X" ``` paulson@13175 ` 221` ``` in bexI) ``` paulson@13558 ` 222` ```apply force ``` paulson@13134 ` 223` ```apply (unfold increasing_def) ``` paulson@13134 ` 224` ```apply (rule CollectI) ``` paulson@13134 ` 225` ```apply (rule lam_type) ``` paulson@13134 ` 226` ```apply (simp (no_asm_simp)) ``` paulson@13558 ` 227` ```apply (blast dest: super_subset_chain [THEN subsetD] ``` paulson@13558 ` 228` ``` chain_subset_Pow [THEN subsetD] choice_super) ``` wenzelm@60770 ` 229` ```txt\Now, verify that it increases\ ``` paulson@13134 ` 230` ```apply (simp (no_asm_simp) add: Pow_iff subset_refl) ``` paulson@13134 ` 231` ```apply safe ``` paulson@13134 ` 232` ```apply (drule choice_super) ``` paulson@13134 ` 233` ```apply (assumption+) ``` paulson@13269 ` 234` ```apply (simp add: super_def, blast) ``` paulson@13134 ` 235` ```done ``` paulson@13134 ` 236` wenzelm@60770 ` 237` ```text\Lemma 4\ ``` paulson@13134 ` 238` ```lemma TFin_chain_lemma4: ``` paulson@13558 ` 239` ``` "[| c \ TFin(S,next); ``` wenzelm@61980 ` 240` ``` ch \ (\X \ Pow(chain(S))-{0}. X); ``` paulson@13558 ` 241` ``` next \ increasing(S); ``` paulson@13558 ` 242` ``` \X \ Pow(S). next`X = ``` paulson@13558 ` 243` ``` if(X \ chain(S)-maxchain(S), ch`super(S,X), X) |] ``` paulson@13558 ` 244` ``` ==> c \ chain(S)" ``` paulson@13134 ` 245` ```apply (erule TFin_induct) ``` paulson@13558 ` 246` ```apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] ``` paulson@13134 ` 247` ``` choice_super [THEN super_subset_chain [THEN subsetD]]) ``` paulson@13134 ` 248` ```apply (unfold chain_def) ``` paulson@13269 ` 249` ```apply (rule CollectI, blast, safe) ``` paulson@13558 ` 250` ```apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) ``` wenzelm@61798 ` 251` ``` txt\\Blast_tac's\ slow\ ``` paulson@13134 ` 252` ```done ``` paulson@13134 ` 253` paulson@13558 ` 254` ```theorem Hausdorff: "\c. c \ maxchain(S)" ``` paulson@13134 ` 255` ```apply (rule AC_Pi_Pow [THEN exE]) ``` paulson@13269 ` 256` ```apply (rule Hausdorff_next_exists [THEN bexE], assumption) ``` paulson@13134 ` 257` ```apply (rename_tac ch "next") ``` paulson@46820 ` 258` ```apply (subgoal_tac "\(TFin (S,next)) \ chain (S) ") ``` paulson@13134 ` 259` ```prefer 2 ``` paulson@13134 ` 260` ``` apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI]) ``` paulson@46820 ` 261` ```apply (rule_tac x = "\(TFin (S,next))" in exI) ``` paulson@13134 ` 262` ```apply (rule classical) ``` paulson@46820 ` 263` ```apply (subgoal_tac "next ` Union(TFin (S,next)) = \(TFin (S,next))") ``` paulson@13134 ` 264` ```apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric]) ``` paulson@13134 ` 265` ```apply (rule_tac [2] subset_refl [THEN TFin_UnionI]) ``` paulson@13269 ` 266` ```prefer 2 apply assumption ``` paulson@13134 ` 267` ```apply (rule_tac [2] refl) ``` paulson@13558 ` 268` ```apply (simp add: subset_refl [THEN TFin_UnionI, ``` paulson@13134 ` 269` ``` THEN TFin.dom_subset [THEN subsetD, THEN PowD]]) ``` paulson@13134 ` 270` ```apply (erule choice_not_equals [THEN notE]) ``` paulson@13134 ` 271` ```apply (assumption+) ``` paulson@13134 ` 272` ```done ``` paulson@13134 ` 273` paulson@13134 ` 274` wenzelm@60770 ` 275` ```subsection\Zorn's Lemma: If All Chains in S Have Upper Bounds In S, ``` wenzelm@60770 ` 276` ``` then S contains a Maximal Element\ ``` paulson@13356 ` 277` wenzelm@60770 ` 278` ```text\Used in the proof of Zorn's Lemma\ ``` paulson@13558 ` 279` ```lemma chain_extend: ``` paulson@13558 ` 280` ``` "[| c \ chain(A); z \ A; \x \ c. x<=z |] ==> cons(z,c) \ chain(A)" ``` paulson@13356 ` 281` ```by (unfold chain_def, blast) ``` paulson@13134 ` 282` paulson@46820 ` 283` ```lemma Zorn: "\c \ chain(S). \(c) \ S ==> \y \ S. \z \ S. y<=z \ y=z" ``` paulson@13134 ` 284` ```apply (rule Hausdorff [THEN exE]) ``` paulson@13134 ` 285` ```apply (simp add: maxchain_def) ``` paulson@13134 ` 286` ```apply (rename_tac c) ``` paulson@46820 ` 287` ```apply (rule_tac x = "\(c)" in bexI) ``` paulson@13269 ` 288` ```prefer 2 apply blast ``` paulson@13134 ` 289` ```apply safe ``` paulson@13134 ` 290` ```apply (rename_tac z) ``` paulson@13134 ` 291` ```apply (rule classical) ``` paulson@13558 ` 292` ```apply (subgoal_tac "cons (z,c) \ super (S,c) ") ``` paulson@13134 ` 293` ```apply (blast elim: equalityE) ``` paulson@13269 ` 294` ```apply (unfold super_def, safe) ``` paulson@13134 ` 295` ```apply (fast elim: chain_extend) ``` paulson@13134 ` 296` ```apply (fast elim: equalityE) ``` paulson@13134 ` 297` ```done ``` paulson@13134 ` 298` wenzelm@60770 ` 299` ```text \Alternative version of Zorn's Lemma\ ``` ballarin@27704 ` 300` ballarin@27704 ` 301` ```theorem Zorn2: ``` paulson@46820 ` 302` ``` "\c \ chain(S). \y \ S. \x \ c. x \ y ==> \y \ S. \z \ S. y<=z \ y=z" ``` ballarin@27704 ` 303` ```apply (cut_tac Hausdorff maxchain_subset_chain) ``` ballarin@27704 ` 304` ```apply (erule exE) ``` ballarin@27704 ` 305` ```apply (drule subsetD, assumption) ``` ballarin@27704 ` 306` ```apply (drule bspec, assumption, erule bexE) ``` ballarin@27704 ` 307` ```apply (rule_tac x = y in bexI) ``` ballarin@27704 ` 308` ``` prefer 2 apply assumption ``` ballarin@27704 ` 309` ```apply clarify ``` ballarin@27704 ` 310` ```apply rule apply assumption ``` ballarin@27704 ` 311` ```apply rule ``` ballarin@27704 ` 312` ```apply (rule ccontr) ``` ballarin@27704 ` 313` ```apply (frule_tac z=z in chain_extend) ``` ballarin@27704 ` 314` ``` apply (assumption, blast) ``` ballarin@27704 ` 315` ```apply (unfold maxchain_def super_def) ``` ballarin@27704 ` 316` ```apply (blast elim!: equalityCE) ``` ballarin@27704 ` 317` ```done ``` ballarin@27704 ` 318` paulson@13134 ` 319` wenzelm@60770 ` 320` ```subsection\Zermelo's Theorem: Every Set can be Well-Ordered\ ``` paulson@13134 ` 321` wenzelm@60770 ` 322` ```text\Lemma 5\ ``` paulson@13134 ` 323` ```lemma TFin_well_lemma5: ``` paulson@46820 ` 324` ``` "[| n \ TFin(S,next); Z \ TFin(S,next); z:Z; ~ \(Z) \ Z |] ``` paulson@46820 ` 325` ``` ==> \m \ Z. n \ m" ``` paulson@13134 ` 326` ```apply (erule TFin_induct) ``` wenzelm@60770 ` 327` ```prefer 2 apply blast txt\second induction step is easy\ ``` paulson@13134 ` 328` ```apply (rule ballI) ``` paulson@13558 ` 329` ```apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) ``` paulson@46820 ` 330` ```apply (subgoal_tac "m = \(Z) ") ``` paulson@13134 ` 331` ```apply blast+ ``` paulson@13134 ` 332` ```done ``` paulson@13134 ` 333` wenzelm@60770 ` 334` ```text\Well-ordering of @{term "TFin(S,next)"}\ ``` paulson@46820 ` 335` ```lemma well_ord_TFin_lemma: "[| Z \ TFin(S,next); z \ Z |] ==> \(Z) \ Z" ``` paulson@13134 ` 336` ```apply (rule classical) ``` paulson@46820 ` 337` ```apply (subgoal_tac "Z = {\(TFin (S,next))}") ``` paulson@13134 ` 338` ```apply (simp (no_asm_simp) add: Inter_singleton) ``` paulson@13134 ` 339` ```apply (erule equal_singleton) ``` paulson@13134 ` 340` ```apply (rule Union_upper [THEN equalityI]) ``` paulson@13269 ` 341` ```apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+) ``` paulson@13134 ` 342` ```done ``` paulson@13134 ` 343` wenzelm@60770 ` 344` ```text\This theorem just packages the previous result\ ``` paulson@13134 ` 345` ```lemma well_ord_TFin: ``` paulson@13558 ` 346` ``` "next \ increasing(S) ``` paulson@13558 ` 347` ``` ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))" ``` paulson@13134 ` 348` ```apply (rule well_ordI) ``` paulson@13134 ` 349` ```apply (unfold Subset_rel_def linear_def) ``` wenzelm@60770 ` 350` ```txt\Prove the well-foundedness goal\ ``` paulson@13134 ` 351` ```apply (rule wf_onI) ``` paulson@13269 ` 352` ```apply (frule well_ord_TFin_lemma, assumption) ``` paulson@46820 ` 353` ```apply (drule_tac x = "\(Z) " in bspec, assumption) ``` paulson@13134 ` 354` ```apply blast ``` wenzelm@60770 ` 355` ```txt\Now prove the linearity goal\ ``` paulson@13134 ` 356` ```apply (intro ballI) ``` paulson@13134 ` 357` ```apply (case_tac "x=y") ``` paulson@13269 ` 358` ``` apply blast ``` wenzelm@60770 ` 359` ```txt\The @{term "x\y"} case remains\ ``` paulson@13134 ` 360` ```apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE], ``` paulson@13269 ` 361` ``` assumption+, blast+) ``` paulson@13134 ` 362` ```done ``` paulson@13134 ` 363` wenzelm@60770 ` 364` ```text\* Defining the "next" operation for Zermelo's Theorem *\ ``` paulson@13134 ` 365` paulson@13134 ` 366` ```lemma choice_Diff: ``` wenzelm@61980 ` 367` ``` "[| ch \ (\X \ Pow(S) - {0}. X); X \ S; X\S |] ==> ch ` (S-X) \ S-X" ``` paulson@13134 ` 368` ```apply (erule apply_type) ``` paulson@13134 ` 369` ```apply (blast elim!: equalityE) ``` paulson@13134 ` 370` ```done ``` paulson@13134 ` 371` wenzelm@60770 ` 372` ```text\This justifies Definition 6.1\ ``` paulson@13134 ` 373` ```lemma Zermelo_next_exists: ``` wenzelm@61980 ` 374` ``` "ch \ (\X \ Pow(S)-{0}. X) ==> ``` paulson@13558 ` 375` ``` \next \ increasing(S). \X \ Pow(S). ``` paulson@13175 ` 376` ``` next`X = (if X=S then S else cons(ch`(S-X), X))" ``` paulson@13175 ` 377` ```apply (rule_tac x="\X\Pow(S). if X=S then S else cons(ch`(S-X), X)" ``` paulson@13175 ` 378` ``` in bexI) ``` paulson@13558 ` 379` ```apply force ``` paulson@13134 ` 380` ```apply (unfold increasing_def) ``` paulson@13134 ` 381` ```apply (rule CollectI) ``` paulson@13134 ` 382` ```apply (rule lam_type) ``` wenzelm@60770 ` 383` ```txt\Type checking is surprisingly hard!\ ``` paulson@13134 ` 384` ```apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl) ``` paulson@13134 ` 385` ```apply (blast intro!: choice_Diff [THEN DiffD1]) ``` wenzelm@60770 ` 386` ```txt\Verify that it increases\ ``` paulson@13558 ` 387` ```apply (intro allI impI) ``` paulson@13134 ` 388` ```apply (simp add: Pow_iff subset_consI subset_refl) ``` paulson@13134 ` 389` ```done ``` paulson@13134 ` 390` paulson@13134 ` 391` wenzelm@60770 ` 392` ```text\The construction of the injection\ ``` paulson@13134 ` 393` ```lemma choice_imp_injection: ``` wenzelm@61980 ` 394` ``` "[| ch \ (\X \ Pow(S)-{0}. X); ``` paulson@13558 ` 395` ``` next \ increasing(S); ``` paulson@13558 ` 396` ``` \X \ Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |] ``` paulson@46820 ` 397` ``` ==> (\ x \ S. \({y \ TFin(S,next). x \ y})) ``` paulson@13558 ` 398` ``` \ inj(S, TFin(S,next) - {S})" ``` paulson@13134 ` 399` ```apply (rule_tac d = "%y. ch` (S-y) " in lam_injective) ``` paulson@13134 ` 400` ```apply (rule DiffI) ``` paulson@13134 ` 401` ```apply (rule Collect_subset [THEN TFin_UnionI]) ``` paulson@13134 ` 402` ```apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE) ``` paulson@46820 ` 403` ```apply (subgoal_tac "x \ \({y \ TFin (S,next) . x \ y}) ") ``` paulson@13134 ` 404` ```prefer 2 apply (blast elim: equalityE) ``` paulson@46820 ` 405` ```apply (subgoal_tac "\({y \ TFin (S,next) . x \ y}) \ S") ``` paulson@13134 ` 406` ```prefer 2 apply (blast elim: equalityE) ``` wenzelm@61798 ` 407` ```txt\For proving \x \ next`\(...)\. ``` wenzelm@60770 ` 408` ``` Abrial and Laffitte's justification appears to be faulty.\ ``` paulson@46820 ` 409` ```apply (subgoal_tac "~ next ` Union({y \ TFin (S,next) . x \ y}) ``` paulson@46820 ` 410` ``` \ \({y \ TFin (S,next) . x \ y}) ") ``` paulson@13558 ` 411` ``` prefer 2 ``` paulson@13558 ` 412` ``` apply (simp del: Union_iff ``` wenzelm@32960 ` 413` ``` add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] ``` wenzelm@32960 ` 414` ``` Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2]) ``` paulson@46820 ` 415` ```apply (subgoal_tac "x \ next ` Union({y \ TFin (S,next) . x \ y}) ") ``` paulson@13558 ` 416` ``` prefer 2 ``` paulson@13558 ` 417` ``` apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI) ``` wenzelm@60770 ` 418` ```txt\End of the lemmas!\ ``` paulson@13134 ` 419` ```apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]) ``` paulson@13134 ` 420` ```done ``` paulson@13134 ` 421` wenzelm@60770 ` 422` ```text\The wellordering theorem\ ``` paulson@13558 ` 423` ```theorem AC_well_ord: "\r. well_ord(S,r)" ``` paulson@13134 ` 424` ```apply (rule AC_Pi_Pow [THEN exE]) ``` paulson@13269 ` 425` ```apply (rule Zermelo_next_exists [THEN bexE], assumption) ``` paulson@13134 ` 426` ```apply (rule exI) ``` paulson@13134 ` 427` ```apply (rule well_ord_rvimage) ``` paulson@13134 ` 428` ```apply (erule_tac [2] well_ord_TFin) ``` paulson@13269 ` 429` ```apply (rule choice_imp_injection [THEN inj_weaken_type], blast+) ``` paulson@13134 ` 430` ```done ``` paulson@13558 ` 431` ballarin@27704 ` 432` wenzelm@60770 ` 433` ```subsection \Zorn's Lemma for Partial Orders\ ``` ballarin@27704 ` 434` wenzelm@60770 ` 435` ```text \Reimported from HOL by Clemens Ballarin.\ ``` ballarin@27704 ` 436` ballarin@27704 ` 437` ballarin@27704 ` 438` ```definition Chain :: "i => i" where ``` paulson@46820 ` 439` ``` "Chain(r) = {A \ Pow(field(r)). \a\A. \b\A. \ r | \ r}" ``` ballarin@27704 ` 440` ballarin@27704 ` 441` ```lemma mono_Chain: ``` ballarin@27704 ` 442` ``` "r \ s ==> Chain(r) \ Chain(s)" ``` ballarin@27704 ` 443` ``` unfolding Chain_def ``` ballarin@27704 ` 444` ``` by blast ``` ballarin@27704 ` 445` ballarin@27704 ` 446` ```theorem Zorn_po: ``` ballarin@27704 ` 447` ``` assumes po: "Partial_order(r)" ``` paulson@46820 ` 448` ``` and u: "\C\Chain(r). \u\field(r). \a\C. \ r" ``` paulson@46820 ` 449` ``` shows "\m\field(r). \a\field(r). \ r \ a = m" ``` ballarin@27704 ` 450` ```proof - ``` ballarin@27704 ` 451` ``` have "Preorder(r)" using po by (simp add: partial_order_on_def) ``` wenzelm@61798 ` 452` ``` \\Mirror r in the set of subsets below (wrt r) elements of A (?).\ ``` paulson@46820 ` 453` ``` let ?B = "\x\field(r). r -`` {x}" let ?S = "?B `` field(r)" ``` paulson@46820 ` 454` ``` have "\C\chain(?S). \U\?S. \A\C. A \ U" ``` ballarin@27704 ` 455` ``` proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp) ``` ballarin@27704 ` 456` ``` fix C ``` paulson@46820 ` 457` ``` assume 1: "C \ ?S" and 2: "\A\C. \B\C. A \ B | B \ A" ``` paulson@46820 ` 458` ``` let ?A = "{x \ field(r). \M\C. M = ?B`x}" ``` ballarin@27704 ` 459` ``` have "C = ?B `` ?A" using 1 ``` ballarin@27704 ` 460` ``` apply (auto simp: image_def) ``` ballarin@27704 ` 461` ``` apply rule ``` ballarin@27704 ` 462` ``` apply rule ``` ballarin@27704 ` 463` ``` apply (drule subsetD) apply assumption ``` ballarin@27704 ` 464` ``` apply (erule CollectE) ``` ballarin@27704 ` 465` ``` apply rule apply assumption ``` ballarin@27704 ` 466` ``` apply (erule bexE) ``` ballarin@27704 ` 467` ``` apply rule prefer 2 apply assumption ``` ballarin@27704 ` 468` ``` apply rule ``` ballarin@27704 ` 469` ``` apply (erule lamE) apply simp ``` ballarin@27704 ` 470` ``` apply assumption ``` ballarin@27704 ` 471` wenzelm@59788 ` 472` ``` apply (thin_tac "C \ X" for X) ``` ballarin@27704 ` 473` ``` apply (fast elim: lamE) ``` ballarin@27704 ` 474` ``` done ``` paulson@46820 ` 475` ``` have "?A \ Chain(r)" ``` ballarin@27704 ` 476` ``` proof (simp add: Chain_def subsetI, intro conjI ballI impI) ``` ballarin@27704 ` 477` ``` fix a b ``` paulson@46820 ` 478` ``` assume "a \ field(r)" "r -`` {a} \ C" "b \ field(r)" "r -`` {b} \ C" ``` ballarin@27704 ` 479` ``` hence "r -`` {a} \ r -`` {b} | r -`` {b} \ r -`` {a}" using 2 by auto ``` paulson@46820 ` 480` ``` then show " \ r | \ r" ``` wenzelm@60770 ` 481` ``` using \Preorder(r)\ \a \ field(r)\ \b \ field(r)\ ``` wenzelm@32960 ` 482` ``` by (simp add: subset_vimage1_vimage1_iff) ``` ballarin@27704 ` 483` ``` qed ``` paulson@46820 ` 484` ``` then obtain u where uA: "u \ field(r)" "\a\?A. \ r" ``` ballarin@27704 ` 485` ``` using u ``` ballarin@27704 ` 486` ``` apply auto ``` ballarin@27704 ` 487` ``` apply (drule bspec) apply assumption ``` ballarin@27704 ` 488` ``` apply auto ``` ballarin@27704 ` 489` ``` done ``` paulson@46820 ` 490` ``` have "\A\C. A \ r -`` {u}" ``` ballarin@27704 ` 491` ``` proof (auto intro!: vimageI) ``` ballarin@27704 ` 492` ``` fix a B ``` paulson@46820 ` 493` ``` assume aB: "B \ C" "a \ B" ``` paulson@46820 ` 494` ``` with 1 obtain x where "x \ field(r)" "B = r -`` {x}" ``` wenzelm@32960 ` 495` ``` apply - ``` wenzelm@32960 ` 496` ``` apply (drule subsetD) apply assumption ``` wenzelm@32960 ` 497` ``` apply (erule imageE) ``` wenzelm@32960 ` 498` ``` apply (erule lamE) ``` wenzelm@32960 ` 499` ``` apply simp ``` wenzelm@32960 ` 500` ``` done ``` wenzelm@60770 ` 501` ``` then show " \ r" using uA aB \Preorder(r)\ ``` wenzelm@32960 ` 502` ``` by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+ ``` ballarin@27704 ` 503` ``` qed ``` paulson@46820 ` 504` ``` then show "\U\field(r). \A\C. A \ r -`` {U}" ``` wenzelm@60770 ` 505` ``` using \u \ field(r)\ .. ``` ballarin@27704 ` 506` ``` qed ``` ballarin@27704 ` 507` ``` from Zorn2 [OF this] ``` paulson@46820 ` 508` ``` obtain m B where "m \ field(r)" "B = r -`` {m}" ``` paulson@46820 ` 509` ``` "\x\field(r). B \ r -`` {x} \ B = r -`` {x}" ``` ballarin@27704 ` 510` ``` by (auto elim!: lamE simp: ball_image_simp) ``` paulson@46820 ` 511` ``` then have "\a\field(r). \ r \ a = m" ``` wenzelm@60770 ` 512` ``` using po \Preorder(r)\ \m \ field(r)\ ``` ballarin@27704 ` 513` ``` by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff) ``` wenzelm@60770 ` 514` ``` then show ?thesis using \m \ field(r)\ by blast ``` ballarin@27704 ` 515` ```qed ``` ballarin@27704 ` 516` lcp@516 ` 517` ```end ```