# HG changeset patch # User wenzelm # Date 1444508084 -7200 # Node ID 6142b282b1646cf22319c7c3e942d0a4b743bfe9 # Parent 8673ec68c798ba1fffc92a3cc83fed6dd6447553 tuned syntax -- more symbols; diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC15_WO6.thy --- a/src/ZF/AC/AC15_WO6.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/AC15_WO6.thy Sat Oct 10 22:14:44 2015 +0200 @@ -67,7 +67,7 @@ lemma lemma4: "[| A \ i; Ord(i) |] ==> {P(a). a \ A} \ i" apply (unfold lepoll_def) apply (erule exE) -apply (rule_tac x = "\x \ RepFun(A,P). LEAST j. \a\A. x=P(a) & f`a=j" +apply (rule_tac x = "\x \ RepFun(A,P). \ j. \a\A. x=P(a) & f`a=j" in exI) apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective) apply (erule RepFunE) @@ -148,7 +148,7 @@ lemma AC15_WO6_aux1: "\x \ Pow(A)-{0}. f`x\0 & f`x \ x & f`x \ m - ==> (\i (\i<\ x. HH(f,A,x)={A}. HH(f,A,i)) = A" apply (simp add: Ord_Least [THEN OUN_eq_UN]) apply (rule equalityI) apply (fast dest!: less_Least_subset_x) @@ -158,7 +158,7 @@ lemma AC15_WO6_aux2: "\x \ Pow(A)-{0}. f`x\0 & f`x \ x & f`x \ m - ==> \x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \ m" + ==> \x < (\ x. HH(f,A,x)={A}). HH(f,A,x) \ m" apply (rule oallI) apply (drule ltD [THEN less_Least_subset_x]) apply (frule HH_subset_imp_eq) @@ -175,8 +175,8 @@ apply (elim bexE conjE exE) apply (rule bexI) apply (rule conjI, assumption) - apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI) - apply (rule_tac x = "\j \ (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) + apply (rule_tac x = "\ i. HH (f,A,i) ={A}" in exI) + apply (rule_tac x = "\j \ (\ i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI) apply (simp_all add: ltD) apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun] elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC16_lemmas.thy --- a/src/ZF/AC/AC16_lemmas.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/AC16_lemmas.thy Sat Oct 10 22:14:44 2015 +0200 @@ -60,7 +60,7 @@ done lemma InfCard_Least_in: - "[| InfCard(x); y \ x; y \ succ(z) |] ==> (LEAST i. i \ y) \ y" + "[| InfCard(x); y \ x; y \ succ(z) |] ==> (\ i. i \ y) \ y" apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN succ_lepoll_imp_not_empty, THEN not_emptyE]) apply (fast intro: LeastI @@ -73,7 +73,7 @@ ==> {y \ Pow(x). y\succ(succ(n))} \ x*{y \ Pow(x). y\succ(n)}" apply (unfold lepoll_def) apply (rule_tac x = "\y \ {y \ Pow(x) . y\succ (succ (n))}. - y, y-{LEAST i. i \ y}>" in exI) + <\ i. i \ y, y-{\ i. i \ y}>" in exI) apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective) apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in) apply (simp, blast intro: InfCard_Least_in) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC17_AC1.thy --- a/src/ZF/AC/AC17_AC1.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/AC17_AC1.thy Sat Oct 10 22:14:44 2015 +0200 @@ -55,7 +55,7 @@ (* *********************************************************************** *) lemma UN_eq_imp_well_ord: - "[| x - (\j \ LEAST i. HH(\X \ Pow(x)-{0}. {f`X}, x, i) = {x}. + "[| x - (\j \ \ i. HH(\X \ Pow(x)-{0}. {f`X}, x, i) = {x}. HH(\X \ Pow(x)-{0}. {f`X}, x, j)) = 0; f \ Pow(x)-{0} -> x |] ==> \r. well_ord(x,r)" @@ -82,7 +82,7 @@ lemma AC17_AC1_aux1: "[| \f \ Pow(x) - {0} -> x. \u \ Pow(x) - {0}. f`u\u; \f \ Pow(x)-{0}->x. - x - (\a \ (LEAST i. HH(\X \ Pow(x)-{0}. {f`X},x,i)={x}). + x - (\a \ (\ i. HH(\X \ Pow(x)-{0}. {f`X},x,i)={x}). HH(\X \ Pow(x)-{0}. {f`X},x,a)) = 0 |] ==> P" apply (erule bexE) @@ -117,7 +117,7 @@ apply (erule not_AC1_imp_ex [THEN exE]) apply (case_tac "\f \ Pow(x)-{0} -> x. - x - (\a \ (LEAST i. HH (\X \ Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\X \ Pow (x) -{0}. {f`X},x,a)) = 0") + x - (\a \ (\ i. HH (\X \ Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\X \ Pow (x) -{0}. {f`X},x,a)) = 0") apply (erule AC17_AC1_aux1, assumption) apply (drule AC17_AC1_aux2) apply (erule allE) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/AC_Equiv.thy Sat Oct 10 22:14:44 2015 +0200 @@ -196,7 +196,7 @@ "[| m \ nat; u \ m |] ==> domain(u) \ m" apply (unfold lepoll_def) apply (erule exE) -apply (rule_tac x = "\x \ domain(u). LEAST i. \y. \ u & f` = i" +apply (rule_tac x = "\x \ domain(u). \ i. \y. \ u & f` = i" in exI) apply (rule_tac d = "%y. fst (converse(f) ` y) " in lam_injective) apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/Cardinal_aux.thy --- a/src/ZF/AC/Cardinal_aux.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/Cardinal_aux.thy Sat Oct 10 22:14:44 2015 +0200 @@ -79,7 +79,7 @@ apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll) done -lemma Least_in_Ord: "[| P(i); i \ j; Ord(j) |] ==> (LEAST i. P(i)) \ j" +lemma Least_in_Ord: "[| P(i); i \ j; Ord(j) |] ==> (\ i. P(i)) \ j" apply (erule Least_le [THEN leE]) apply (erule Ord_in_Ord, assumption) apply (erule ltE) @@ -100,7 +100,7 @@ lemma UN_sing_lepoll: "Ord(a) ==> (\x \ a. {P(x)}) \ a" apply (unfold lepoll_def) -apply (rule_tac x = "\z \ (\x \ a. {P (x) }) . (LEAST i. P (i) =z) " in exI) +apply (rule_tac x = "\z \ (\x \ a. {P (x) }) . (\ i. P (i) =z) " in exI) apply (rule_tac d = "%z. P (z) " in lam_injective) apply (fast intro!: Least_in_Ord) apply (fast intro: LeastI elim!: Ord_in_Ord) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/DC.thy --- a/src/ZF/AC/DC.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/DC.thy Sat Oct 10 22:14:44 2015 +0200 @@ -10,7 +10,7 @@ lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \ a} \ a" apply (unfold lepoll_def) -apply (rule_tac x = "\z \ RepFun (a,P) . LEAST i. z=P (i) " in exI) +apply (rule_tac x = "\z \ RepFun (a,P) . \ i. z=P (i) " in exI) apply (rule_tac d="%z. P (z)" in lam_injective) apply (fast intro!: Least_in_Ord) apply (rule sym) @@ -20,7 +20,7 @@ text\Trivial in the presence of AC, but here we need a wellordering of X\ lemma image_Ord_lepoll: "[| f \ X->Y; Ord(X) |] ==> f``X \ X" apply (unfold lepoll_def) -apply (rule_tac x = "\x \ f``X. LEAST y. f`y = x" in exI) +apply (rule_tac x = "\x \ f``X. \ y. f`y = x" in exI) apply (rule_tac d = "%z. f`z" in lam_injective) apply (fast intro!: Least_in_Ord apply_equality, clarify) apply (rule LeastI) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/HH.thy --- a/src/ZF/AC/HH.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/HH.thy Sat Oct 10 22:14:44 2015 +0200 @@ -116,11 +116,11 @@ elim!: Hartog_lepoll_selfE) done -lemma HH_Least_eq_x: "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}" +lemma HH_Least_eq_x: "HH(f, x, \ i. HH(f, x, i) = {x}) = {x}" by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI) lemma less_Least_subset_x: - "a \ (LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) \ Pow(x)-{0}" + "a \ (\ i. HH(f,x,i)={x}) ==> HH(f,x,a) \ Pow(x)-{0}" apply (rule HH_values [THEN disjE], assumption) apply (rule less_LeastE) apply (erule_tac [2] ltI [OF _ Ord_Least], assumption) @@ -129,17 +129,17 @@ subsection\Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\ lemma lam_Least_HH_inj_Pow: - "(\a \ (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) - \ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})" + "(\a \ (\ i. HH(f,x,i)={x}). HH(f,x,a)) + \ inj(\ i. HH(f,x,i)={x}, Pow(x)-{0})" apply (unfold inj_def, simp) apply (fast intro!: lam_type dest: less_Least_subset_x elim!: HH_eq_imp_arg_eq Ord_Least [THEN Ord_in_Ord]) done lemma lam_Least_HH_inj: - "\a \ (LEAST i. HH(f,x,i)={x}). \z \ x. HH(f,x,a) = {z} - ==> (\a \ (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) - \ inj(LEAST i. HH(f,x,i)={x}, {{y}. y \ x})" + "\a \ (\ i. HH(f,x,i)={x}). \z \ x. HH(f,x,a) = {z} + ==> (\a \ (\ i. HH(f,x,i)={x}). HH(f,x,a)) + \ inj(\ i. HH(f,x,i)={x}, {{y}. y \ x})" by (rule lam_Least_HH_inj_Pow [THEN inj_strengthen_type], simp) lemma lam_surj_sing: @@ -161,7 +161,7 @@ lemma f_subsets_imp_UN_HH_eq_x: "\z \ Pow(x)-{0}. f`z \ Pow(z)-{0} - ==> x - (\j \ (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0" + ==> x - (\j \ (\ i. HH(f,x,i)={x}). HH(f,x,j)) = 0" apply (case_tac "P \ {0}" for P, fast) apply (drule Diff_subset [THEN PowI, THEN DiffI]) apply (drule bspec, assumption) @@ -183,7 +183,7 @@ lemma f_sing_imp_HH_sing: "[| f \ (Pow(x)-{0}) -> {{z}. z \ x}; - a \ (LEAST i. HH(f,x,i)={x}) |] ==> \z \ x. HH(f,x,a) = {z}" + a \ (\ i. HH(f,x,i)={x}) |] ==> \z \ x. HH(f,x,a) = {z}" apply (drule less_Least_subset_x) apply (frule HH_subset_imp_eq) apply (drule apply_type) @@ -192,10 +192,10 @@ done lemma f_sing_lam_bij: - "[| x - (\j \ (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; + "[| x - (\j \ (\ i. HH(f,x,i)={x}). HH(f,x,j)) = 0; f \ (Pow(x)-{0}) -> {{z}. z \ x} |] - ==> (\a \ (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) - \ bij(LEAST i. HH(f,x,i)={x}, {{y}. y \ x})" + ==> (\a \ (\ i. HH(f,x,i)={x}). HH(f,x,a)) + \ bij(\ i. HH(f,x,i)={x}, {{y}. y \ x})" apply (unfold bij_def) apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing) done @@ -219,13 +219,13 @@ converse (converse(\x\x. {x}) O Lambda - (LEAST i. HH(\X\Pow(x) - {0}. {f ` X}, x, i) = {x}, + (\ i. HH(\X\Pow(x) - {0}. {f ` X}, x, i) = {x}, HH(\X\Pow(x) - {0}. {f ` X}, x))) Perhaps it could be simplified. *) lemma bijection: "f \ (\ X \ Pow(x) - {0}. X) - ==> \g. g \ bij(x, LEAST i. HH(\X \ Pow(x)-{0}. {f`X}, x, i) = {x})" + ==> \g. g \ bij(x, \ i. HH(\X \ Pow(x)-{0}. {f`X}, x, i) = {x})" apply (rule exI) apply (rule bij_Least_HH_x [THEN bij_converse_bij]) apply (rule f_subsets_imp_UN_HH_eq_x) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/Hartog.thy --- a/src/ZF/AC/Hartog.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/Hartog.thy Sat Oct 10 22:14:44 2015 +0200 @@ -10,7 +10,7 @@ definition Hartog :: "i => i" where - "Hartog(X) == LEAST i. ~ i \ X" + "Hartog(X) == \ i. ~ i \ X" lemma Ords_in_set: "\a. Ord(a) \ a \ X ==> P" apply (rule_tac X = "{y \ X. Ord (y) }" in ON_class [elim_format]) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/WO2_AC16.thy --- a/src/ZF/AC/WO2_AC16.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/WO2_AC16.thy Sat Oct 10 22:14:44 2015 +0200 @@ -22,7 +22,7 @@ "recfunAC16(f,h,i,a) == transrec2(i, 0, %g r. if (\y \ r. h`g \ y) then r - else r \ {f`(LEAST i. h`g \ f`i & + else r \ {f`(\ i. h`g \ f`i & (\b f`i \ (\t \ r. ~ h`b \ t))))})" (* ********************************************************************** *) @@ -36,7 +36,7 @@ "recfunAC16(f,h,succ(i),a) = (if (\y \ recfunAC16(f,h,i,a). h ` i \ y) then recfunAC16(f,h,i,a) else recfunAC16(f,h,i,a) \ - {f ` (LEAST j. h ` i \ f ` j & + {f ` (\ j. h ` i \ f ` j & (\b f`j \ (\t \ recfunAC16(f,h,i,a). ~ h`b \ t))))})" apply (simp add: recfunAC16_def) @@ -232,11 +232,11 @@ lemma in_Least_Diff: "[| z \ F(x); Ord(x) |] - ==> z \ F(LEAST i. z \ F(i)) - (\j<(LEAST i. z \ F(i)). F(j))" + ==> z \ F(\ i. z \ F(i)) - (\j<(\ i. z \ F(i)). F(j))" by (fast elim: less_LeastE elim!: LeastI) lemma Least_eq_imp_ex: - "[| (LEAST i. w \ F(i)) = (LEAST i. z \ F(i)); + "[| (\ i. w \ F(i)) = (\ i. z \ F(i)); w \ (\i (\i \b (F(b) - (\c (F(b) - (\cij 1; Limit(a) |] ==> (\x a" apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]]) -apply (rule_tac x = "\z \ (\x F (i) " in exI) +apply (rule_tac x = "\z \ (\x i. z \ F (i) " in exI) apply (unfold inj_def) apply (rule CollectI) apply (rule lam_type) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/WO6_WO1.thy --- a/src/ZF/AC/WO6_WO1.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/AC/WO6_WO1.thy Sat Oct 10 22:14:44 2015 +0200 @@ -29,9 +29,9 @@ definition vv1 :: "[i, i, i] => i" where "vv1(f,m,b) == - let g = LEAST g. (\d. Ord(d) & (domain(uu(f,b,g,d)) \ 0 & + let g = \ g. (\d. Ord(d) & (domain(uu(f,b,g,d)) \ 0 & domain(uu(f,b,g,d)) \ m)); - d = LEAST d. domain(uu(f,b,g,d)) \ 0 & + d = \ d. domain(uu(f,b,g,d)) \ 0 & domain(uu(f,b,g,d)) \ m in if f`b \ 0 then domain(uu(f,b,g,d)) else 0" @@ -48,7 +48,7 @@ definition vv2 :: "[i, i, i, i] => i" where "vv2(f,b,g,s) == - if f`g \ 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) \ 0)`s} else 0" + if f`g \ 0 then {uu(f, b, g, \ d. uu(f,b,g,d) \ 0)`s} else 0" definition ww2 :: "[i, i, i, i] => i" where @@ -210,10 +210,10 @@ (* ********************************************************************** *) lemma nested_LeastI: "[| P(a, b); Ord(a); Ord(b); - Least_a = (LEAST a. \x. Ord(x) & P(a, x)) |] - ==> P(Least_a, LEAST b. P(Least_a, b))" + Least_a = (\ a. \x. Ord(x) & P(a, x)) |] + ==> P(Least_a, \ b. P(Least_a, b))" apply (erule ssubst) -apply (rule_tac Q = "%z. P (z, LEAST b. P (z, b))" in LeastI2) +apply (rule_tac Q = "%z. P (z, \ b. P (z, b))" in LeastI2) apply (fast elim!: LeastI)+ done @@ -260,7 +260,7 @@ lemma uu_not_empty: "[| b0; f`g\0; y*y \ y; (\b uu(f,b,g,LEAST d. (uu(f,b,g,d) \ 0)) \ 0" + ==> uu(f,b,g,\ d. (uu(f,b,g,d) \ 0)) \ 0" apply (drule ex_d_uu_not_empty, assumption+) apply (fast elim!: LeastI lt_Ord) done @@ -270,7 +270,7 @@ lemma Least_uu_not_empty_lt_a: "[| b0; f`g\0; y*y \ y; (\b (LEAST d. uu(f,b,g,d) \ 0) < a" + ==> (\ d. uu(f,b,g,d) \ 0) < a" apply (erule ex_d_uu_not_empty [THEN oexE], assumption+) apply (blast intro: Least_le [THEN lt_trans1] lt_Ord) done @@ -298,7 +298,7 @@ \b succ(m); y*y \ y; (\b0; f`g\0; m \ nat; s \ f`b |] - ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\0) \ f`b -> f`g" + ==> uu(f, b, g, \ d. uu(f,b,g,d)\0) \ 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+) @@ -466,7 +466,7 @@ lemma lemma2: "[| (\b y; \b 1; Ord(a) |] - ==> f` (LEAST i. f`i = {x}) = {x}" + ==> f` (\ i. f`i = {x}) = {x}" apply (drule lemma1, assumption+) apply (fast elim!: lt_Ord intro: LeastI) done @@ -475,7 +475,7 @@ apply (unfold NN_def) apply (elim CollectE exE conjE) apply (rule_tac x = a in exI) -apply (rule_tac x = "\x \ y. LEAST i. f`i = {x}" 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+) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Arith.thy --- a/src/ZF/Arith.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/Arith.thy Sat Oct 10 22:14:44 2015 +0200 @@ -72,9 +72,6 @@ mod :: "[i,i]=>i" (infixl "mod" 70) where "m mod n == raw_mod (natify(m), natify(n))" -notation (xsymbols) - mult (infixr "#\" 70) - declare rec_type [simp] nat_0_le [simp] diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/Cardinal.thy Sat Oct 10 22:14:44 2015 +0200 @@ -9,39 +9,33 @@ definition (*least ordinal operator*) - Least :: "(i=>o) => i" (binder "LEAST " 10) where + Least :: "(i=>o) => i" (binder "\ " 10) where "Least(P) == THE i. Ord(i) & P(i) & (\j. j ~P(j))" definition - eqpoll :: "[i,i] => o" (infixl "eqpoll" 50) where - "A eqpoll B == \f. f \ bij(A,B)" + eqpoll :: "[i,i] => o" (infixl "\" 50) where + "A \ B == \f. f \ bij(A,B)" definition - lepoll :: "[i,i] => o" (infixl "lepoll" 50) where - "A lepoll B == \f. f \ inj(A,B)" + lepoll :: "[i,i] => o" (infixl "\" 50) where + "A \ B == \f. f \ inj(A,B)" definition - lesspoll :: "[i,i] => o" (infixl "lesspoll" 50) where - "A lesspoll B == A lepoll B & ~(A eqpoll B)" + lesspoll :: "[i,i] => o" (infixl "\" 50) where + "A \ B == A \ B & ~(A \ B)" definition cardinal :: "i=>i" ("|_|") where - "|A| == (LEAST i. i eqpoll A)" + "|A| == (\ i. i \ A)" definition Finite :: "i=>o" where - "Finite(A) == \n\nat. A eqpoll n" + "Finite(A) == \n\nat. A \ n" definition Card :: "i=>o" where "Card(i) == (i = |i|)" -notation (xsymbols) - eqpoll (infixl "\" 50) and - lepoll (infixl "\" 50) and - lesspoll (infixl "\" 50) and - Least (binder "\" 10) - subsection\The Schroeder-Bernstein Theorem\ text\See Davey and Priestly, page 106\ @@ -89,7 +83,7 @@ apply (erule exI) done -(*A eqpoll A*) +(*A \ A*) lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp] lemma eqpoll_sym: "X \ Y ==> Y \ X" @@ -160,7 +154,7 @@ apply (blast intro: inj_disjoint_Un) done -(*A eqpoll 0 ==> A=0*) +(*A \ 0 ==> A=0*) lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0] lemma eqpoll_0_iff: "A \ 0 \ A=0" @@ -239,7 +233,7 @@ by (blast intro: eqpoll_imp_lepoll lesspoll_trans2) -(** LEAST -- the least number operator [from HOL/Univ.ML] **) +(** \ -- the least number operator [from HOL/Univ.ML] **) lemma Least_equality: "[| P(i); Ord(i); !!x. x ~P(x) |] ==> (\ x. P(x)) = i" @@ -296,7 +290,7 @@ thus ?thesis using P . qed -(*LEAST really is the smallest*) +(*\ really is the smallest*) lemma less_LeastE: "[| P(i); i < (\ x. P(x)) |] ==> Q" apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+) apply (simp add: lt_Ord) @@ -307,7 +301,7 @@ "[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(\ j. P(j))" by (blast intro: LeastI ) -(*If there is no such P then LEAST is vacuously 0*) +(*If there is no such P then \ is vacuously 0*) lemma Least_0: "[| ~ (\i. Ord(i) & P(i)) |] ==> (\ x. P(x)) = 0" apply (unfold Least_def) @@ -636,7 +630,7 @@ done -(** lepoll, \ and natural numbers **) +(** \, \ and natural numbers **) lemma lepoll_succ: "i \ succ(i)" by (blast intro: subset_imp_lepoll) diff -r 8673ec68c798 -r 6142b282b164 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/CardinalArith.thy Sat Oct 10 22:14:44 2015 +0200 @@ -37,7 +37,7 @@ csucc :: "i=>i" where --\needed because @{term "jump_cardinal(K)"} might not be the successor of @{term K}\ - "csucc(K) == LEAST L. Card(L) & K L. Card(L) & K" 65) and diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/Cardinal_AC.thy Sat Oct 10 22:14:44 2015 +0200 @@ -152,16 +152,16 @@ assume z: "z \ (\i\K. X(i))" then obtain i where i: "i \ K" "Ord(i)" "z \ X(i)" by (blast intro: Ord_in_Ord [of K]) - hence "(LEAST i. z \ X(i)) \ i" by (fast intro: Least_le) - hence "(LEAST i. z \ X(i)) < K" by (best intro: lt_trans1 ltI i) - hence "(LEAST i. z \ X(i)) \ K" and "z \ X(LEAST i. z \ X(i))" + hence "(\ i. z \ X(i)) \ i" by (fast intro: Least_le) + hence "(\ i. z \ X(i)) < K" by (best intro: lt_trans1 ltI i) + hence "(\ i. z \ X(i)) \ K" and "z \ X(\ i. z \ X(i))" by (auto intro: LeastI ltD i) } note mems = this have "(\i\K. X(i)) \ K \ K" proof (unfold lepoll_def) show "\f. f \ inj(\RepFun(K, X), K \ K)" apply (rule exI) - apply (rule_tac c = "%z. \LEAST i. z \ X(i), f ` (LEAST i. z \ X(i)) ` z\" + apply (rule_tac c = "%z. \\ i. z \ X(i), f ` (\ i. z \ X(i)) ` z\" and d = "%\i,j\. converse (f`i) ` j" in lam_injective) apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+ done