--- 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 \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
apply (unfold lepoll_def)
apply (erule exE)
-apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). LEAST j. \<exists>a\<in>A. x=P(a) & f`a=j"
+apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>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:
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
- ==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"
+ ==> (\<Union>i<\<mu> 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:
"\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m
- ==> \<forall>x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
+ ==> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> 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 = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
+ apply (rule_tac x = "\<mu> i. HH (f,A,i) ={A}" in exI)
+ apply (rule_tac x = "\<lambda>j \<in> (\<mu> 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)
--- 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 \<subseteq> x; y \<approx> succ(z) |] ==> (LEAST i. i \<in> y) \<in> y"
+ "[| InfCard(x); y \<subseteq> x; y \<approx> succ(z) |] ==> (\<mu> i. i \<in> y) \<in> 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 \<in> Pow(x). y\<approx>succ(succ(n))} \<lesssim> x*{y \<in> Pow(x). y\<approx>succ(n)}"
apply (unfold lepoll_def)
apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}.
- <LEAST i. i \<in> y, y-{LEAST i. i \<in> y}>" in exI)
+ <\<mu> i. i \<in> y, y-{\<mu> i. i \<in> 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)
--- 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 - (\<Union>j \<in> LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.
+ "[| x - (\<Union>j \<in> \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.
HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, j)) = 0;
f \<in> Pow(x)-{0} -> x |]
==> \<exists>r. well_ord(x,r)"
@@ -82,7 +82,7 @@
lemma AC17_AC1_aux1:
"[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;
\<exists>f \<in> Pow(x)-{0}->x.
- x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).
+ x - (\<Union>a \<in> (\<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).
HH(\<lambda>X \<in> 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
"\<exists>f \<in> Pow(x)-{0} -> x.
- x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
+ x - (\<Union>a \<in> (\<mu> i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
apply (erule AC17_AC1_aux1, assumption)
apply (drule AC17_AC1_aux2)
apply (erule allE)
--- 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 \<in> nat; u \<lesssim> m |] ==> domain(u) \<lesssim> m"
apply (unfold lepoll_def)
apply (erule exE)
-apply (rule_tac x = "\<lambda>x \<in> domain(u). LEAST i. \<exists>y. <x,y> \<in> u & f`<x,y> = i"
+apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. <x,y> \<in> u & f`<x,y> = 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]
--- 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 \<in> j; Ord(j) |] ==> (LEAST i. P(i)) \<in> j"
+lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (\<mu> i. P(i)) \<in> 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) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (LEAST i. P (i) =z) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (\<mu> 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)
--- 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 \<in> a} \<lesssim> a"
apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . LEAST i. z=P (i) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . \<mu> 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\<open>Trivial in the presence of AC, but here we need a wellordering of X\<close>
lemma image_Ord_lepoll: "[| f \<in> X->Y; Ord(X) |] ==> f``X \<lesssim> X"
apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>x \<in> f``X. LEAST y. f`y = x" in exI)
+apply (rule_tac x = "\<lambda>x \<in> f``X. \<mu> 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)
--- 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, \<mu> i. HH(f, x, i) = {x}) = {x}"
by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI)
lemma less_Least_subset_x:
- "a \<in> (LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> Pow(x)-{0}"
+ "a \<in> (\<mu> i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> 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\<open>Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\<close>
lemma lam_Least_HH_inj_Pow:
- "(\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
- \<in> inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"
+ "(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))
+ \<in> inj(\<mu> 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:
- "\<forall>a \<in> (LEAST i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z}
- ==> (\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
- \<in> inj(LEAST i. HH(f,x,i)={x}, {{y}. y \<in> x})"
+ "\<forall>a \<in> (\<mu> i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z}
+ ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))
+ \<in> inj(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> 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:
"\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
- ==> x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
+ ==> x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
apply (case_tac "P \<in> {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 \<in> (Pow(x)-{0}) -> {{z}. z \<in> x};
- a \<in> (LEAST i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> x. HH(f,x,a) = {z}"
+ a \<in> (\<mu> i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> 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 - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0;
+ "[| x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0;
f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x} |]
- ==> (\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))
- \<in> bij(LEAST i. HH(f,x,i)={x}, {{y}. y \<in> x})"
+ ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))
+ \<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> 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(\<lambda>x\<in>x. {x}) O
Lambda
- (LEAST i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x},
+ (\<mu> i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x},
HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x)))
Perhaps it could be simplified. *)
lemma bijection:
"f \<in> (\<Pi> X \<in> Pow(x) - {0}. X)
- ==> \<exists>g. g \<in> bij(x, LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
+ ==> \<exists>g. g \<in> bij(x, \<mu> i. HH(\<lambda>X \<in> 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)
--- 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 \<lesssim> X"
+ "Hartog(X) == \<mu> i. ~ i \<lesssim> X"
lemma Ords_in_set: "\<forall>a. Ord(a) \<longrightarrow> a \<in> X ==> P"
apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
--- 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 (\<exists>y \<in> r. h`g \<subseteq> y) then r
- else r \<union> {f`(LEAST i. h`g \<subseteq> f`i &
+ else r \<union> {f`(\<mu> i. h`g \<subseteq> f`i &
(\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
(* ********************************************************************** *)
@@ -36,7 +36,7 @@
"recfunAC16(f,h,succ(i),a) =
(if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)
else recfunAC16(f,h,i,a) \<union>
- {f ` (LEAST j. h ` i \<subseteq> f ` j &
+ {f ` (\<mu> j. h ` i \<subseteq> f ` j &
(\<forall>b<a. (h`b \<subseteq> f`j
\<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
apply (simp add: recfunAC16_def)
@@ -232,11 +232,11 @@
lemma in_Least_Diff:
"[| z \<in> F(x); Ord(x) |]
- ==> z \<in> F(LEAST i. z \<in> F(i)) - (\<Union>j<(LEAST i. z \<in> F(i)). F(j))"
+ ==> z \<in> F(\<mu> i. z \<in> F(i)) - (\<Union>j<(\<mu> i. z \<in> F(i)). F(j))"
by (fast elim: less_LeastE elim!: LeastI)
lemma Least_eq_imp_ex:
- "[| (LEAST i. w \<in> F(i)) = (LEAST i. z \<in> F(i));
+ "[| (\<mu> i. w \<in> F(i)) = (\<mu> i. z \<in> F(i));
w \<in> (\<Union>i<a. F(i)); z \<in> (\<Union>i<a. F(i)) |]
==> \<exists>b<a. w \<in> (F(b) - (\<Union>c<b. F(c))) & z \<in> (F(b) - (\<Union>c<b. F(c)))"
apply (elim OUN_E)
@@ -255,7 +255,7 @@
"[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |]
==> (\<Union>x<a. F(x)) \<lesssim> a"
apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
-apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). LEAST i. z \<in> F (i) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). \<mu> i. z \<in> F (i) " in exI)
apply (unfold inj_def)
apply (rule CollectI)
apply (rule lam_type)
--- 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. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 &
+ let g = \<mu> g. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m));
- d = LEAST d. domain(uu(f,b,g,d)) \<noteq> 0 &
+ d = \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 &
domain(uu(f,b,g,d)) \<lesssim> m
in if f`b \<noteq> 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 \<noteq> 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) \<noteq> 0)`s} else 0"
+ if f`g \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 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. \<exists>x. Ord(x) & P(a, x)) |]
- ==> P(Least_a, LEAST b. P(Least_a, b))"
+ Least_a = (\<mu> a. \<exists>x. Ord(x) & P(a, x)) |]
+ ==> P(Least_a, \<mu> 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, \<mu> b. P (z, b))" in LeastI2)
apply (fast elim!: LeastI)+
done
@@ -260,7 +260,7 @@
lemma uu_not_empty:
"[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y |]
- ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0"
+ ==> 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
@@ -270,7 +270,7 @@
lemma Least_uu_not_empty_lt_a:
"[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y |]
- ==> (LEAST d. uu(f,b,g,d) \<noteq> 0) < a"
+ ==> (\<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
@@ -298,7 +298,7 @@
\<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
(\<Union>b<a. f`b)=y; b<a; g<a; d<a;
f`b\<noteq>0; f`g\<noteq>0; m \<in> nat; s \<in> f`b |]
- ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g"
+ ==> 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+)
@@ -466,7 +466,7 @@
lemma lemma2:
"[| (\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a) |]
- ==> f` (LEAST i. f`i = {x}) = {x}"
+ ==> f` (\<mu> 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 = "\<lambda>x \<in> y. LEAST i. f`i = {x}" in exI)
+apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI)
apply (rule conjI, assumption)
apply (rule_tac d = "%i. THE x. x \<in> f`i" in lam_injective)
apply (drule lemma1, assumption+)
--- 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 "#\<times>" 70)
-
declare rec_type [simp]
nat_0_le [simp]
--- 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 "\<mu> " 10) where
"Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
definition
- eqpoll :: "[i,i] => o" (infixl "eqpoll" 50) where
- "A eqpoll B == \<exists>f. f \<in> bij(A,B)"
+ eqpoll :: "[i,i] => o" (infixl "\<approx>" 50) where
+ "A \<approx> B == \<exists>f. f \<in> bij(A,B)"
definition
- lepoll :: "[i,i] => o" (infixl "lepoll" 50) where
- "A lepoll B == \<exists>f. f \<in> inj(A,B)"
+ lepoll :: "[i,i] => o" (infixl "\<lesssim>" 50) where
+ "A \<lesssim> B == \<exists>f. f \<in> 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 "\<prec>" 50) where
+ "A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
definition
cardinal :: "i=>i" ("|_|") where
- "|A| == (LEAST i. i eqpoll A)"
+ "|A| == (\<mu> i. i \<approx> A)"
definition
Finite :: "i=>o" where
- "Finite(A) == \<exists>n\<in>nat. A eqpoll n"
+ "Finite(A) == \<exists>n\<in>nat. A \<approx> n"
definition
Card :: "i=>o" where
"Card(i) == (i = |i|)"
-notation (xsymbols)
- eqpoll (infixl "\<approx>" 50) and
- lepoll (infixl "\<lesssim>" 50) and
- lesspoll (infixl "\<prec>" 50) and
- Least (binder "\<mu>" 10)
-
subsection\<open>The Schroeder-Bernstein Theorem\<close>
text\<open>See Davey and Priestly, page 106\<close>
@@ -89,7 +83,7 @@
apply (erule exI)
done
-(*A eqpoll A*)
+(*A \<approx> A*)
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
@@ -160,7 +154,7 @@
apply (blast intro: inj_disjoint_Un)
done
-(*A eqpoll 0 ==> A=0*)
+(*A \<approx> 0 ==> A=0*)
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
@@ -239,7 +233,7 @@
by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
-(** LEAST -- the least number operator [from HOL/Univ.ML] **)
+(** \<mu> -- the least number operator [from HOL/Univ.ML] **)
lemma Least_equality:
"[| P(i); Ord(i); !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
@@ -296,7 +290,7 @@
thus ?thesis using P .
qed
-(*LEAST really is the smallest*)
+(*\<mu> really is the smallest*)
lemma less_LeastE: "[| P(i); i < (\<mu> 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(\<mu> 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 \<mu> is vacuously 0*)
lemma Least_0:
"[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
apply (unfold Least_def)
@@ -636,7 +630,7 @@
done
-(** lepoll, \<prec> and natural numbers **)
+(** \<lesssim>, \<prec> and natural numbers **)
lemma lepoll_succ: "i \<lesssim> succ(i)"
by (blast intro: subset_imp_lepoll)
--- 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
--\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
of @{term K}\<close>
- "csucc(K) == LEAST L. Card(L) & K<L"
+ "csucc(K) == \<mu> L. Card(L) & K<L"
notation (xsymbols)
cadd (infixl "\<oplus>" 65) and
--- 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 \<in> (\<Union>i\<in>K. X(i))"
then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
by (blast intro: Ord_in_Ord [of K])
- hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le)
- hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i)
- hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"
+ hence "(\<mu> i. z \<in> X(i)) \<le> i" by (fast intro: Least_le)
+ hence "(\<mu> i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i)
+ hence "(\<mu> i. z \<in> X(i)) \<in> K" and "z \<in> X(\<mu> i. z \<in> X(i))"
by (auto intro: LeastI ltD i)
} note mems = this
have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K"
proof (unfold lepoll_def)
show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
apply (rule exI)
- apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
+ apply (rule_tac c = "%z. \<langle>\<mu> i. z \<in> X(i), f ` (\<mu> i. z \<in> X(i)) ` z\<rangle>"
and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective)
apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
done