--- a/src/ZF/AC.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC.thy Wed Dec 30 17:45:18 2015 +0100
@@ -25,7 +25,7 @@
apply (erule bspec, assumption)
done
-lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)"
+lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Prod>X \<in> Pow(C)-{0}. X)"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
apply (erule_tac [2] exI, blast)
done
@@ -51,7 +51,7 @@
apply (erule_tac [2] fun_weaken_type, blast+)
done
-lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)"
+lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Prod>x \<in> A. x)"
apply (rule AC_Pi)
apply (simp_all add: non_empty_family)
done
--- a/src/ZF/AC/AC15_WO6.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC15_WO6.thy Wed Dec 30 17:45:18 2015 +0100
@@ -263,7 +263,7 @@
lemma AC13_AC1_lemma:
"\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1
- ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi> X \<in> A. X)"
+ ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, assumption)
apply (elim conjE)
--- a/src/ZF/AC/AC17_AC1.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Wed Dec 30 17:45:18 2015 +0100
@@ -15,7 +15,7 @@
(** AC0 is equivalent to AC1.
AC0 comes from Suppes, AC1 from Rubin & Rubin **)
-lemma AC0_AC1_lemma: "[| f:(\<Pi> X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi> X \<in> D. X)"
+lemma AC0_AC1_lemma: "[| f:(\<Prod>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Prod>X \<in> D. X)"
by (fast intro!: lam_type apply_type)
lemma AC0_AC1: "AC0 ==> AC1"
@@ -29,7 +29,7 @@
(**** The proof of AC1 ==> AC17 ****)
-lemma AC1_AC17_lemma: "f \<in> (\<Pi> X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
+lemma AC1_AC17_lemma: "f \<in> (\<Prod>X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
apply (rule Pi_type, assumption)
apply (drule apply_type, assumption, fast)
done
@@ -144,7 +144,7 @@
(* ********************************************************************** *)
lemma AC1_AC2_aux1:
- "[| f:(\<Pi> X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
+ "[| f:(\<Prod>X \<in> A. X); B \<in> A; 0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
by (fast elim!: apply_type)
lemma AC1_AC2_aux2:
@@ -178,7 +178,7 @@
lemma AC2_AC1_aux3:
"\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D \<inter> C = {y}
- ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Pi> X \<in> A. X)"
+ ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Prod>X \<in> A. X)"
apply (rule lam_type)
apply (drule bspec, blast)
apply (blast intro: AC2_AC1_aux2 fst_type)
@@ -234,7 +234,7 @@
(* ********************************************************************** *)
lemma AC3_AC1_lemma:
- "b\<notin>A ==> (\<Pi> x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi> x \<in> A. x)"
+ "b\<notin>A ==> (\<Prod>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Prod>x \<in> A. x)"
apply (simp add: id_def cong add: Pi_cong)
apply (rule_tac b = A in subst_context, fast)
done
@@ -277,7 +277,7 @@
done
lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]
- ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi> x \<in> C. R``{x})"
+ ==> (\<lambda>x \<in> C. snd(g`x)): (\<Prod>x \<in> C. R``{x})"
apply (rule lam_type)
apply (force dest: apply_type)
done
--- a/src/ZF/AC/AC18_AC19.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC18_AC19.thy Wed Dec 30 17:45:18 2015 +0100
@@ -18,14 +18,14 @@
(* ********************************************************************** *)
lemma PROD_subsets:
- "[| f \<in> (\<Pi> b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |]
- ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi> a \<in> A. Q(a))"
+ "[| f \<in> (\<Prod>b \<in> {P(a). a \<in> A}. b); \<forall>a \<in> A. P(a)<=Q(a) |]
+ ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Prod>a \<in> A. Q(a))"
by (rule lam_type, drule apply_type, auto)
lemma lemma_AC18:
- "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |]
+ "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X)); A \<noteq> 0 |]
==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq>
- (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
+ (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
apply (rule subsetI)
apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE)
apply (erule impE, fast)
@@ -68,12 +68,12 @@
done
lemma lemma1_2:
- "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B); a \<in> A |]
+ "[| f`(uu(a)) \<notin> a; f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B); a \<in> A |]
==> f`(uu(a))-{0} \<in> a"
apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)
done
-lemma lemma1: "\<exists>f. f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi> B \<in> A. B)"
+lemma lemma1: "\<exists>f. f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Prod>B \<in> A. B)"
apply (erule exE)
apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})"
in exI)
--- a/src/ZF/AC/AC7_AC9.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC7_AC9.thy Wed Dec 30 17:45:18 2015 +0100
@@ -53,16 +53,16 @@
(* the proof. *)
(* ********************************************************************** *)
-lemma lemma1_1: "y \<in> (\<Pi> B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi> B \<in> A. B)"
+lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)"
by (fast intro!: lam_type snd_type apply_type)
lemma lemma1_2:
- "y \<in> (\<Pi> B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi> B \<in> A. Y*B)"
+ "y \<in> (\<Prod>B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Prod>B \<in> A. Y*B)"
apply (fast intro!: lam_type apply_type)
done
lemma AC7_AC6_lemma1:
- "(\<Pi> B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
+ "(\<Prod>B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Prod>B \<in> A. B) \<noteq> 0"
by (fast intro!: equals0I lemma1_1 lemma1_2)
lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
@@ -92,7 +92,7 @@
done
lemma AC1_AC8_lemma2:
- "[| f \<in> (\<Pi> X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)"
+ "[| f \<in> (\<Prod>X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)"
apply (simp, fast elim!: apply_type)
done
@@ -152,7 +152,7 @@
"\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.
\<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.
f`<B1,B2> \<in> bij(B1, B2)
- ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
+ ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Prod>X \<in> A. X)"
apply (intro lam_type snd_type fst_type)
apply (rule apply_type [OF _ consI1])
apply (fast intro!: fun_weaken_type bij_is_fun)
--- a/src/ZF/AC/AC_Equiv.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Wed Dec 30 17:45:18 2015 +0100
@@ -41,7 +41,7 @@
"WO7 == \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))"
definition
- "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
+ "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Prod>X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
definition
@@ -56,28 +56,28 @@
(* Axioms of Choice *)
definition
- "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
+ "AC0 == \<forall>A. \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)"
definition
- "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
+ "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X))"
definition
"AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)
\<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})"
definition
- "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
+ "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Prod>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
definition
- "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
+ "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Prod>x \<in> domain(R). R``{x})))"
definition
"AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
definition
- "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Pi> B \<in> A. B)\<noteq>0"
+ "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Prod>B \<in> A. B)\<noteq>0"
definition
- "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Pi> B \<in> A. B) \<noteq> 0"
+ "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Prod>B \<in> A. B) \<noteq> 0"
definition
"AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)
@@ -123,12 +123,12 @@
locale AC18 =
assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =
- (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
+ (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
\<comment>"AC18 cannot be expressed within the object-logic"
definition
"AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =
- (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
+ (\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))"
@@ -178,10 +178,10 @@
by (blast dest!: well_ord_imp_ex1_first
[THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
-lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Pi> X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Prod>X \<in> A. X)"
by (fast elim!: first_in_B intro!: lam_type)
-lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
+lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)"
by (fast elim!: well_ord_subset [THEN ex_choice_fun])
--- a/src/ZF/AC/HH.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/HH.thy Wed Dec 30 17:45:18 2015 +0100
@@ -201,8 +201,8 @@
done
lemma lam_singI:
- "f \<in> (\<Pi> X \<in> Pow(x)-{0}. F(X))
- ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi> X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
+ "f \<in> (\<Prod>X \<in> Pow(x)-{0}. F(X))
+ ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Prod>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
by (fast del: DiffI DiffE
intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)
@@ -224,7 +224,7 @@
Perhaps it could be simplified. *)
lemma bijection:
- "f \<in> (\<Pi> X \<in> Pow(x) - {0}. X)
+ "f \<in> (\<Prod>X \<in> Pow(x) - {0}. 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])
--- a/src/ZF/Cardinal_AC.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Cardinal_AC.thy Wed Dec 30 17:45:18 2015 +0100
@@ -119,7 +119,7 @@
assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
proof -
from f AC_Pi [of Y "%y. f-``{y}"]
- obtain z where z: "z \<in> (\<Pi> y\<in>Y. f -`` {y})"
+ obtain z where z: "z \<in> (\<Prod>y\<in>Y. f -`` {y})"
by (auto simp add: surj_def) (fast dest: apply_Pair)
show ?thesis
proof
@@ -146,7 +146,7 @@
have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K)
assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def)
- with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
+ with AC_Pi obtain f where f: "f \<in> (\<Prod>i\<in>K. inj(X(i), K))"
by force
{ fix z
assume z: "z \<in> (\<Union>i\<in>K. X(i))"
--- a/src/ZF/Coind/Map.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Coind/Map.thy Wed Dec 30 17:45:18 2015 +0100
@@ -23,7 +23,7 @@
definition
map_owr :: "[i,i,i]=>i" where
- "map_owr(m,a,b) == \<Sigma> x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
+ "map_owr(m,a,b) == \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
definition
map_app :: "[i,i]=>i" where
--- a/src/ZF/Constructible/Reflection.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Constructible/Reflection.thy Wed Dec 30 17:45:18 2015 +0100
@@ -353,8 +353,8 @@
to be relativized.\<close>
schematic_goal (in reflection)
"Reflects(?Cl,
- \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
- \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
+ \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Prod>X \<in> A. X)),
+ \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Prod>X \<in> A. X)))"
by fast
end
--- a/src/ZF/Induct/Brouwer.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Induct/Brouwer.thy Wed Dec 30 17:45:18 2015 +0100
@@ -50,7 +50,7 @@
monos Pi_mono
type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
-lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))"
+lemma Well_unfold: "Well(A, B) = (\<Sum>x \<in> A. B(x) -> Well(A, B))"
by (fast intro!: Well.intros [unfolded Well.con_defs]
elim: Well.cases [unfolded Well.con_defs])
--- a/src/ZF/OrderArith.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/OrderArith.thy Wed Dec 30 17:45:18 2015 +0100
@@ -557,7 +557,7 @@
text\<open>As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"}\<close>
lemma Pow_Sigma_bij:
"(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
- \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
+ \<in> bij(Pow(Sigma(A,B)), \<Prod>x \<in> A. Pow(B(x)))"
apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
apply (blast intro: lam_type)
apply (blast dest: apply_type, simp_all)
--- a/src/ZF/UNITY/State.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/UNITY/State.thy Wed Dec 30 17:45:18 2015 +0100
@@ -21,7 +21,7 @@
default_val :: "i=>i"
definition
- "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))"
+ "state == \<Prod>x \<in> var. cons(default_val(x), type_of(x))"
definition
"st0 == \<lambda>x \<in> var. default_val(x)"
--- a/src/ZF/ZF.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/ZF.thy Wed Dec 30 17:45:18 2015 +0100
@@ -113,8 +113,8 @@
"_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
"_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
"_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
- "_PROD" :: "[pttrn, i, i] => i" ("(3\<Pi> _\<in>_./ _)" 10)
- "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10)
+ "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10)
"_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
"_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10)
"_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10)
@@ -133,8 +133,8 @@
"{b. x\<in>A}" == "CONST RepFun(A, \<lambda>x. b)"
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
- "\<Pi> x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
- "\<Sigma> x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
+ "\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
+ "\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
"\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)"
"\<forall>x\<in>A. P" == "CONST Ball(A, \<lambda>x. P)"
"\<exists>x\<in>A. P" == "CONST Bex(A, \<lambda>x. P)"
--- a/src/ZF/Zorn.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Zorn.thy Wed Dec 30 17:45:18 2015 +0100
@@ -197,14 +197,14 @@
done
lemma choice_super:
- "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
+ "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
==> ch ` super(S,X) \<in> super(S,X)"
apply (erule apply_type)
apply (unfold super_def maxchain_def, blast)
done
lemma choice_not_equals:
- "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
+ "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |]
==> ch ` super(S,X) \<noteq> X"
apply (rule notI)
apply (drule choice_super, assumption, assumption)
@@ -213,7 +213,7 @@
text\<open>This justifies Definition 4.4\<close>
lemma Hausdorff_next_exists:
- "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
+ "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) ==>
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
apply (rule_tac x="\<lambda>X\<in>Pow(S).
@@ -237,7 +237,7 @@
text\<open>Lemma 4\<close>
lemma TFin_chain_lemma4:
"[| c \<in> TFin(S,next);
- ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
+ ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
next \<in> increasing(S);
\<forall>X \<in> Pow(S). next`X =
if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
@@ -364,14 +364,14 @@
text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
lemma choice_Diff:
- "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
+ "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
apply (erule apply_type)
apply (blast elim!: equalityE)
done
text\<open>This justifies Definition 6.1\<close>
lemma Zermelo_next_exists:
- "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
+ "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) ==>
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
next`X = (if X=S then S else cons(ch`(S-X), X))"
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
@@ -391,7 +391,7 @@
text\<open>The construction of the injection\<close>
lemma choice_imp_injection:
- "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
+ "[| ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
next \<in> increasing(S);
\<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
--- a/src/ZF/equalities.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/equalities.thy Wed Dec 30 17:45:18 2015 +0100
@@ -535,19 +535,19 @@
by blast
lemma SUM_UN_distrib1:
- "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
+ "(\<Sum>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sum>x\<in>C(y). B(x))"
by blast
lemma SUM_UN_distrib2:
- "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
+ "(\<Sum>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sum>i\<in>I. C(i,j))"
by blast
lemma SUM_Un_distrib1:
- "(\<Sigma> i\<in>I \<union> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<union> (\<Sigma> j\<in>J. C(j))"
+ "(\<Sum>i\<in>I \<union> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<union> (\<Sum>j\<in>J. C(j))"
by blast
lemma SUM_Un_distrib2:
- "(\<Sigma> i\<in>I. A(i) \<union> B(i)) = (\<Sigma> i\<in>I. A(i)) \<union> (\<Sigma> i\<in>I. B(i))"
+ "(\<Sum>i\<in>I. A(i) \<union> B(i)) = (\<Sum>i\<in>I. A(i)) \<union> (\<Sum>i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -555,11 +555,11 @@
by (rule SUM_Un_distrib2)
lemma SUM_Int_distrib1:
- "(\<Sigma> i\<in>I \<inter> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<inter> (\<Sigma> j\<in>J. C(j))"
+ "(\<Sum>i\<in>I \<inter> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<inter> (\<Sum>j\<in>J. C(j))"
by blast
lemma SUM_Int_distrib2:
- "(\<Sigma> i\<in>I. A(i) \<inter> B(i)) = (\<Sigma> i\<in>I. A(i)) \<inter> (\<Sigma> i\<in>I. B(i))"
+ "(\<Sum>i\<in>I. A(i) \<inter> B(i)) = (\<Sum>i\<in>I. A(i)) \<inter> (\<Sum>i\<in>I. B(i))"
by blast
(*First-order version of the above, for rewriting*)
@@ -567,7 +567,7 @@
by (rule SUM_Int_distrib2)
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
-lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
+lemma SUM_eq_UN: "(\<Sum>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
by blast
lemma times_subset_iff:
@@ -575,7 +575,7 @@
by blast
lemma Int_Sigma_eq:
- "(\<Sigma> x \<in> A'. B'(x)) \<inter> (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
+ "(\<Sum>x \<in> A'. B'(x)) \<inter> (\<Sum>x \<in> A. B(x)) = (\<Sum>x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
by blast
(** Domain **)
--- a/src/ZF/ex/Limit.thy Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/ex/Limit.thy Wed Dec 30 17:45:18 2015 +0100
@@ -120,8 +120,8 @@
(* Twice, constructions on cpos are more difficult. *)
iprod :: "i=>i" where
"iprod(DD) ==
- <(\<Pi> n \<in> nat. set(DD`n)),
- {x:(\<Pi> n \<in> nat. set(DD`n))*(\<Pi> n \<in> nat. set(DD`n)).
+ <(\<Prod>n \<in> nat. set(DD`n)),
+ {x:(\<Prod>n \<in> nat. set(DD`n))*(\<Prod>n \<in> nat. set(DD`n)).
\<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
definition
@@ -1071,18 +1071,18 @@
(*----------------------------------------------------------------------*)
lemma iprodI:
- "x:(\<Pi> n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
+ "x:(\<Prod>n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
by (simp add: set_def iprod_def)
lemma iprodE:
- "x \<in> set(iprod(DD)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
+ "x \<in> set(iprod(DD)) ==> x:(\<Prod>n \<in> nat. set(DD`n))"
by (simp add: set_def iprod_def)
(* Contains typing conditions in contrast to HOL-ST *)
lemma rel_iprodI:
- "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi> n \<in> nat. set(DD`n));
- g:(\<Pi> n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
+ "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Prod>n \<in> nat. set(DD`n));
+ g:(\<Prod>n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
by (simp add: iprod_def rel_I)
lemma rel_iprodE:
@@ -1252,14 +1252,14 @@
(*----------------------------------------------------------------------*)
lemma DinfI:
- "[|x:(\<Pi> n \<in> nat. set(DD`n));
+ "[|x:(\<Prod>n \<in> nat. set(DD`n));
!!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
==> x \<in> set(Dinf(DD,ee))"
apply (simp add: Dinf_def)
apply (blast intro: mkcpoI iprodI)
done
-lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
+lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Prod>n \<in> nat. set(DD`n))"
apply (simp add: Dinf_def)
apply (erule mkcpoD1 [THEN iprodE])
done
@@ -1273,7 +1273,7 @@
lemma rel_DinfI:
"[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
- x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
+ x:(\<Prod>n \<in> nat. set(DD`n)); y:(\<Prod>n \<in> nat. set(DD`n))|]
==> rel(Dinf(DD,ee),x,y)"
apply (simp add: Dinf_def)
apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)