Quelle WO6_WO1.thy
Sprache: Isabelle
(* Title: ZF/AC/WO6_WO1.thy Author: Krzysztof Grabczewski Proofs needed to state that formulations WO1,...,WO6 are all equivalent. The only hard one is WO6 \<Longrightarrow> WO1. Every proof (except WO6 \<Longrightarrow> WO1 and WO1 \<Longrightarrow> WO2) are described as "clear" by Rubin & Rubin (page 2). They refer reader to a book by Gödel to see the proof WO1 \<Longrightarrow> WO2. Fortunately order types made this proof also very easy. theory WO6_WO1imports Cardinal_auxbegin (* Auxiliary definitions used in proof *) definition "i \ i" where "NN(y) \ {m \ nat. \a. \f. Ord(a) \ domain(f)=a \ \<Union>b<a. f`b) = y \<and> (\<forall>b<a. f`b \<lesssim> m)}" definition "[i, i, i, i] \ i" where "uu(f, beta, gamma, delta) \ (f`beta * f`gamma) \ f`delta" (** Definitions for case 1 **) definition "[i, i, i] \ i" where "vv1(f,m,b) \ let g = \<mu> g. (\<exists>d. Ord(d) \<and> (domain(uu(f,b,g,d)) \<noteq> 0 \<and> domain (uu(f,b,g,d)) \<lesssim> m)); \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 \<and> domain (uu(f,b,g,d)) \<lesssim> m in if f`b \<noteq> 0 then domain(uu(f,b,g,d)) else 0" definition "[i, i, i] \ i" where "ww1(f,m,b) \ f`b - vv1(f,m,b)" definition "[i, i, i] \ i" where "gg1(f,a,m) \ \b \ a++a. if b(** Definitions for case 2 **) definition "[i, i, i, i] \ i" where "vv2(f,b,g,s) \ if f`g \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 0)`s} else 0" definition "[i, i, i, i] \ i" where "ww2(f,b,g,s) \ f`g - vv2(f,b,g,s)" definition "[i, i, i, i] \ i" where "gg2(f,a,b,s) \ \<lambda>g \<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)" lemma WO2_WO3: "WO2 \ WO3" by (unfold WO2_def WO3_def, fast)(* ********************************************************************** *) lemma WO3_WO1: "WO3 \ WO1" unfolding eqpoll_def WO1_def WO3_defapply (intro allI)apply (drule_tac x=A in spec) apply (blast intro: bij_is_inj well_ord_rvimage THEN well_ord_subset])done (* ********************************************************************** *) lemma WO1_WO2: "WO1 \ WO2" unfolding eqpoll_def WO1_def WO2_defapply (blast intro!: Ord_ordertype ordermap_bij)done (* ********************************************************************** *) lemma lam_sets: "f \ A->B \ (\x \ A. {f`x}): A -> {{b}. b \ B}" by (fast intro!: lam_type apply_type)lemma surj_imp_eq': "f \ surj(A,B) \ (\a \ A. {f`a}) = B" unfolding surj_defapply (fast elim!: apply_type)done lemma surj_imp_eq: "\f \ surj(A,B); Ord(A)\ \ (\aby (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE) lemma WO1_WO4: "WO1 \ WO4(1)" unfolding WO1_def WO4_defapply (rule allI)apply (erule_tac x = A in allE)apply (erule exE)apply (intro exI conjI)apply (erule Ord_ordertype)apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertypeTHEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]done (* ********************************************************************** *) lemma WO4_mono: "\m\n; WO4(m)\ \ WO4(n)" unfolding WO4_defapply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])done (* ********************************************************************** *) lemma WO4_WO5: "\m \ nat; 1\m; WO4(m)\ \ WO5" by (unfold WO4_def WO5_def, blast)(* ********************************************************************** *) lemma WO5_WO6: "WO5 \ WO6" by (unfold WO4_def WO5_def WO6_def, blast)(* ********************************************************************** The proof of "WO6 \<Longrightarrow> WO1". Simplified by L C Paulson. From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, pages 2-5 lemma lt_oadd_odiff_disj:"\k < i++j; Ord(i); Ord(j)\ \<Longrightarrow> k < i | (\<not> k<i \<and> k = i ++ (k--i) \<and> (k--i)<j)" apply (rule_tac i = k and j = i in Ord_linear2)prefer 4 apply (drule odiff_lt_mono2, assumption)apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)apply (auto elim!: lt_Ord)done (* ********************************************************************** *) (* The most complicated part of the proof - lemma ii - p. 2-4 *) (* ********************************************************************** *) (* ********************************************************************** *) (* some properties of relation uu(beta, gamma, delta) - p. 2 *) (* ********************************************************************** *) lemma domain_uu_subset: "domain(uu(f,b,g,d)) \ f`b" by (unfold uu_def, blast)lemma quant_domain_uu_lepoll_m:"\b m \ \bgd m" by (blast intro: domain_uu_subset [THEN subset_imp_lepoll] lepoll_trans)lemma uu_subset1: "uu(f,b,g,d) \ f`b * f`g" by (unfold uu_def, blast)lemma uu_subset2: "uu(f,b,g,d) \ f`d" by (unfold uu_def, blast)lemma uu_lepoll_m: "\\b m; d \ uu(f,b,g,d) \ m" by (blast intro: uu_subset2 [THEN subset_imp_lepoll] lepoll_trans)(* ********************************************************************** *) (* Two cases for lemma ii *) (* ********************************************************************** *) lemma cases: "\bgd m \<Longrightarrow> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow> \<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 \<and> u(f,b,g,d) \<prec> m)) \<exists>b<a. f`b \<noteq> 0 \<and> (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow> \<approx> m))" unfolding lesspoll_defapply (blast del: equalityI)done (* ********************************************************************** *) (* Lemmas used in both cases *) (* ********************************************************************** *) lemma UN_oadd: "Ord(a) \ (\bb C(a++b))" by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)(* ********************************************************************** *) (* Case 1: lemmas *) (* ********************************************************************** *) lemma vv1_subset: "vv1(f,m,b) \ f`b" by (simp add: vv1_def Let_def domain_uu_subset)(* ********************************************************************** *) (* Case 1: Union of images is the whole "y" *) (* ********************************************************************** *) lemma UN_gg1_eq: "\Ord(a); m \ nat\ \ (\bbby (simp add: gg1_def UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt] THEN Diff_partition]lemma domain_gg1: "domain(gg1(f,a,m)) = a++a" by (simp add: lam_funtype [THEN domain_of_fun] gg1_def)(* ********************************************************************** *) (* every value of defined function is less than or equipollent to m *) (* ********************************************************************** *) lemma nested_LeastI:"\P(a, b); Ord(a); Ord(b); \<mu> a. \<exists>x. Ord(x) \<and> P(a, x))\<rbrakk> \<Longrightarrow> P(Least_a, \<mu> b. P(Least_a, b))" apply (erule ssubst)apply (rule_tac Q = "\z. P (z, \ b. P (z, b))" in LeastI2) apply (fast elim!: LeastI)+done lemmas nested_Least_instance ="\g d. domain(uu(f,b,g,d)) \ 0 \ domain (uu(f,b,g,d)) \<lesssim> m"] for f b m lemma gg1_lepoll_m: "\Ord(a); m \ nat; \<forall>b<a. f`b \<noteq>0 \<longrightarrow> \<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<and> domain (uu(f,b,g,d)) \<lesssim> m); \<forall>b<a. f`b \<lesssim> succ(m); b<a++a\<rbrakk> \<Longrightarrow> gg1(f,a,m)`b \<lesssim> m" apply (simp add: gg1_def empty_lepollI)apply (safe dest!: lt_oadd_odiff_disj)(*Case b<a \<in> show vv1(f,m,b) \<lesssim> m *) apply (simp add: vv1_def Let_def empty_lepollI)apply (fast intro: nested_Least_instance [THEN conjunct2](*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *) apply (simp add: ww1_def empty_lepollI)apply (case_tac "f` (b--a) = 0" , simp add: empty_lepollI)apply (rule Diff_lepoll, blast)apply (rule vv1_subset)apply (drule ospec [THEN mp], assumption+)apply (elim oexE conjE)apply (simp add: vv1_def Let_def lt_Ord nested_Least_instance [THEN conjunct1])done (* ********************************************************************** *) (* Case 2: lemmas *) (* ********************************************************************** *) (* ********************************************************************** *) (* Case 2: vv2_subset *) (* ********************************************************************** *) lemma ex_d_uu_not_empty:"\b0; f`g\0; \<subseteq> y; (\<Union>b<a. f`b)=y\<rbrakk> \<Longrightarrow> \<exists>d<a. uu(f,b,g,d) \<noteq> 0" by (unfold uu_def, blast) lemma uu_not_empty:"\b0; f`g\0; y*y \ y; (\b \<Longrightarrow> uu(f,b,g,\<mu> d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0" apply (drule ex_d_uu_not_empty, assumption+)apply (fast elim!: LeastI lt_Ord)done lemma not_empty_rel_imp_domain: "\r \ A*B; r\0\ \ domain(r)\0" by blastlemma Least_uu_not_empty_lt_a:"\b0; f`g\0; y*y \ y; (\b \<Longrightarrow> (\<mu> d. uu(f,b,g,d) \<noteq> 0) < a" apply (erule ex_d_uu_not_empty [THEN oexE], assumption+)apply (blast intro: Least_le [THEN lt_trans1] lt_Ord)done lemma subset_Diff_sing: "\B \ A; a\B\ \ B \ A-{a}" by blast(*Could this be proved more directly?*) lemma supset_lepoll_imp_eq:"\A \ m; m \ B; B \ A; m \ nat\ \ A=B" apply (erule natE)apply (fast dest!: lepoll_0_is_0 intro!: equalityI)apply (safe intro!: equalityI)apply (rule ccontr)apply (rule succ_lepoll_natE)apply (erule lepoll_trans) apply (rule lepoll_trans) apply (erule subset_Diff_sing [THEN subset_imp_lepoll], assumption)apply (rule Diff_sing_lepoll, assumption+) done lemma uu_Least_is_fun:"\\gd0 \ domain (uu(f, b, g, d)) \<approx> succ(m); \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; \<Union>b<a. f`b)=y; b<a; g<a; d<a; \<noteq>0; f`g\<noteq>0; m \<in> nat; s \<in> f`b\<rbrakk> \<Longrightarrow> uu(f, b, g, \<mu> d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g" apply (drule_tac x2=g in ospec [THEN ospec, THEN mp])apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty])apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+)apply (rule rel_is_fun)apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) apply (erule uu_lepoll_m) apply (rule Least_uu_not_empty_lt_a, assumption+) apply (rule uu_subset1)apply (rule supset_lepoll_imp_eq [OF _ eqpoll_sym [THEN eqpoll_imp_lepoll]])apply (fast intro!: domain_uu_subset)+done lemma vv2_subset: "\\gd0 \ domain (uu(f, b, g, d)) \<approx> succ(m); \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; \<Union>b<a. f`b)=y; b<a; g<a; m \<in> nat; s \<in> f`b\<rbrakk> \<Longrightarrow> vv2(f,b,g,s) \<subseteq> f`g" apply (simp add: vv2_def)apply (blast intro: uu_Least_is_fun [THEN apply_type])done (* ********************************************************************** *) (* Case 2: Union of images is the whole "y" *) (* ********************************************************************** *) lemma UN_gg2_eq: "\\gd 0 \ domain (uu(f,b,g,d)) \<approx> succ(m); \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; \<Union>b<a. f`b)=y; Ord(a); m \<in> nat; s \<in> f`b; b<a\<rbrakk> \<Longrightarrow> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y" unfolding gg2_defapply (drule sym) apply (simp add: ltD UN_oadd oadd_le_self [THEN le_imp_not_lt] THEN Diff_partition])done lemma domain_gg2: "domain(gg2(f,a,b,s)) = a++a" by (simp add: lam_funtype [THEN domain_of_fun] gg2_def)(* ********************************************************************** *) (* every value of defined function is less than or equipollent to m *) (* ********************************************************************** *) lemma vv2_lepoll: "\m \ nat; m\0\ \ vv2(f,b,g,s) \ m" unfolding vv2_defapply (simp add: empty_lepollI)apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0] THEN eqpoll_imp_lepoll, THEN lepoll_trans]THEN le_imp_subset, THEN subset_imp_lepoll]done lemma ww2_lepoll: "\\b succ(m); g nat; vv2(f,b,g,d) \ f`g\ \<Longrightarrow> ww2(f,b,g,d) \<lesssim> m" unfolding ww2_defapply (case_tac "f`g = 0" )apply (simp add: empty_lepollI)apply (drule ospec, assumption)apply (rule Diff_lepoll, assumption+)apply (simp add: vv2_def not_emptyI)done lemma gg2_lepoll_m: "\\gd 0 \ domain (uu(f,b,g,d)) \<approx> succ(m); \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y; \<Union>b<a. f`b)=y; b<a; s \<in> f`b; m \<in> nat; m\<noteq> 0; g<a++a\<rbrakk> \<Longrightarrow> gg2(f,a,b,s) ` g \<lesssim> m" apply (simp add: gg2_def empty_lepollI)apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)apply (simp add: vv2_lepoll)apply (simp add: ww2_lepoll vv2_subset)done (* ********************************************************************** *) (* lemma ii *) (* ********************************************************************** *) lemma lemma_ii: "\succ(m) \ NN(y); y*y \ y; m \ nat; m\0\ \ m \ NN(y)" unfolding NN_defapply (elim CollectE exE conjE) apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)(* case 1 *) apply (simp add: lesspoll_succ_iff)apply (rule_tac x = "a++a" in exI)apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)(* case 2 *) apply (elim oexE conjE)apply (rule_tac A = "f`B" for B in not_emptyE, assumption)apply (rule CollectI)apply (erule succ_natD)apply (rule_tac x = "a++a" in exI)apply (rule_tac x = "gg2 (f,a,b,x) " in exI)apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)done (* ********************************************************************** *) (* lemma iv - p. 4: *) (* For every set x there is a set y such that x \<union> (y * y) \<subseteq> y *) (* ********************************************************************** *) (* The leading \<forall>-quantifier looks odd but makes the proofs shorter lemma z_n_subset_z_succ_n:"\n \ nat. rec(n, x, \k r. r \ r*r) \ rec(succ(n), x, \k r. r \ r*r)" by (fast intro: rec_succ [THEN ssubst])lemma le_subsets:"\\n \ nat. f(n)<=f(succ(n)); n\m; n \ nat; m \ nat\ \<Longrightarrow> f(n)<=f(m)" apply (erule_tac P = "n\m" in rev_mp) apply (rule_tac P = "\z. n\z \ f (n) \ f (z) " in nat_induct) apply (auto simp add: le_iff) done lemma le_imp_rec_subset:"\n\m; m \ nat\ \<Longrightarrow> rec(n, x, \<lambda>k r. r \<union> r*r) \<subseteq> rec(m, x, \<lambda>k r. r \<union> r*r)" apply (rule z_n_subset_z_succ_n [THEN le_subsets])apply (blast intro: lt_nat_in_nat)+done lemma lemma_iv: "\y. x \ y*y \ y" apply (rule_tac x = "\n \ nat. rec (n, x, \k r. r \ r*r) " in exI) apply safeapply (rule nat_0I [THEN UN_I], simp)apply (rule_tac a = "succ (n \ na) " in UN_I) apply (erule Un_nat_type [THEN nat_succI], assumption)apply (auto intro: le_imp_rec_subset [THEN subsetD] done (* ********************************************************************** *) (* Rubin & Rubin wrote, *) (* "It follows from (ii) and mathematical induction that if y*y \<subseteq> y then *) (* y can be well-ordered" *) (* In fact we have to prove *) (* * WO6 \<Longrightarrow> NN(y) \<noteq> 0 *) (* * reverse induction which lets us infer that 1 \<in> NN(y) *) (* * 1 \<in> NN(y) \<Longrightarrow> y can be well-ordered *) (* ********************************************************************** *) (* ********************************************************************** *) (* WO6 \<Longrightarrow> NN(y) \<noteq> 0 *) (* ********************************************************************** *) lemma WO6_imp_NN_not_empty: "WO6 \ NN(y) \ 0" by (unfold WO6_def NN_def, clarify, blast)(* ********************************************************************** *) (* 1 \<in> NN(y) \<Longrightarrow> y can be well-ordered *) (* ********************************************************************** *) lemma lemma1:"\(\b y; \b 1; Ord(a)\ \ \cby (fast elim!: lepoll_1_is_sing)lemma lemma2:"\(\b y; \b 1; Ord(a)\ \<Longrightarrow> f` (\<mu> i. f`i = {x}) = {x}" apply (drule lemma1, assumption+)apply (fast elim!: lt_Ord intro: LeastI)done lemma NN_imp_ex_inj: "1 \ NN(y) \ \a f. Ord(a) \ f \ inj(y, a)" unfolding NN_defapply (elim CollectE exE conjE)apply (rule_tac x = a in exI)apply (rule_tac x = "\x \ y. \ i. f`i = {x}" in exI) apply (rule conjI, assumption)apply (rule_tac d = "\i. THE x. x \ f`i" in lam_injective) apply (drule lemma1, assumption+)apply (fast elim!: Least_le [THEN lt_trans1, THEN ltD] lt_Ord)apply (rule lemma2 [THEN ssubst], assumption+, blast)done lemma y_well_ord: "\y*y \ y; 1 \ NN(y)\ \ \r. well_ord(y, r)" apply (drule NN_imp_ex_inj)apply (fast elim!: well_ord_rvimage [OF _ well_ord_Memrel])done (* ********************************************************************** *) (* reverse induction which lets us infer that 1 \<in> NN(y) *) (* ********************************************************************** *) lemma rev_induct_lemma [rule_format]: "\n \ nat; \m. \m \ nat; m\0; P(succ(m))\ \ P(m)\ \<Longrightarrow> n\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)" by (erule nat_induct, blast+)lemma rev_induct:"\n \ nat; P(n); n\0; \<And>m. \<lbrakk>m \<in> nat; m\<noteq>0; P(succ(m))\<rbrakk> \<Longrightarrow> P(m)\<rbrakk> \<Longrightarrow> P(1)" by (rule rev_induct_lemma, blast+)lemma NN_into_nat: "n \ NN(y) \ n \ nat" by (simp add: NN_def)lemma lemma3: "\n \ NN(y); y*y \ y; n\0\ \ 1 \ NN(y)" apply (rule rev_induct [OF NN_into_nat], assumption+)apply (rule lemma_ii, assumption+)done (* ********************************************************************** *) (* Main theorem "WO6 \<Longrightarrow> WO1" *) (* ********************************************************************** *) (* another helpful lemma *) lemma NN_y_0: "0 \ NN(y) \ y=0" unfolding NN_def apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)done lemma WO6_imp_WO1: "WO6 \ WO1" unfolding WO1_defapply (rule allI)apply (case_tac "A=0" )apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])apply (rule_tac x = A in lemma_iv [elim_format])apply (erule exE)apply (drule WO6_imp_NN_not_empty)apply (erule Un_subset_iff [THEN iffD1, THEN conjE])apply (erule_tac A = "NN (y) " in not_emptyE)apply (frule y_well_ord)apply (fast intro!: lemma3 dest!: NN_y_0 elim!: not_emptyE)apply (fast elim: well_ord_subset)done end quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
