--- a/src/ZF/ZF.thy Sun Mar 04 23:20:43 2012 +0100
+++ b/src/ZF/ZF.thy Tue Mar 06 15:15:49 2012 +0000
@@ -200,10 +200,10 @@
0 Pow Inf Union PrimReplace mem
defs (* Bounded Quantifiers *)
- Ball_def: "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
+ Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)"
Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)"
- subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
+ subset_def: "A \<subseteq> B == \<forall>x\<in>A. x\<in>B"
axiomatization where
@@ -212,18 +212,18 @@
Axioms for Union, Pow and Replace state existence only,
uniqueness is derivable using extensionality. *)
- extension: "A = B <-> A <= B & B <= A" and
- Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
- Pow_iff: "A \<in> Pow(B) <-> A <= B" and
+ extension: "A = B <-> A \<subseteq> B & B \<subseteq> A" and
+ Union_iff: "A \<in> \<Union>(C) <-> (\<exists>B\<in>C. A\<in>B)" and
+ Pow_iff: "A \<in> Pow(B) <-> A \<subseteq> B" and
(*We may name this set, though it is not uniquely defined.*)
infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
(*This formulation facilitates case analysis on A.*)
- foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and
+ foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
(*Schema axiom since predicate P is a higher-order variable*)
- replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
+ replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) \<longrightarrow> y=z) ==>
b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))"
@@ -248,18 +248,18 @@
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
- cons_def: "cons(a,A) == Upair(a,a) Un A"
+ cons_def: "cons(a,A) == Upair(a,a) \<union> A"
succ_def: "succ(i) == cons(i, i)"
(* Difference, general intersection, binary union and small intersection *)
Diff_def: "A - B == { x\<in>A . ~(x\<in>B) }"
- Inter_def: "Inter(A) == { x\<in>Union(A) . \<forall>y\<in>A. x\<in>y}"
- Un_def: "A Un B == Union(Upair(A,B))"
- Int_def: "A Int B == Inter(Upair(A,B))"
+ Inter_def: "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
+ Un_def: "A \<union> B == \<Union>(Upair(A,B))"
+ Int_def: "A \<inter> B == \<Inter>(Upair(A,B))"
(* definite descriptions *)
- the_def: "The(P) == Union({y . x \<in> {0}, P(y)})"
+ the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})"
if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b"
(* this "symmetric" definition works better than {{a}, {a,b}} *)
@@ -276,21 +276,21 @@
domain_def: "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}"
range_def: "range(r) == domain(converse(r))"
- field_def: "field(r) == domain(r) Un range(r)"
+ field_def: "field(r) == domain(r) \<union> range(r)"
relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>"
function_def: "function(r) ==
- \<forall>x y. <x,y>:r --> (\<forall>y'. <x,y'>:r --> y=y')"
- image_def: "r `` A == {y : range(r) . \<exists>x\<in>A. <x,y> : r}"
+ \<forall>x y. <x,y>:r \<longrightarrow> (\<forall>y'. <x,y'>:r \<longrightarrow> y=y')"
+ image_def: "r `` A == {y \<in> range(r) . \<exists>x\<in>A. <x,y> \<in> r}"
vimage_def: "r -`` A == converse(r)``A"
(* Abstraction, application and Cartesian product of a family of sets *)
lam_def: "Lambda(A,b) == {<x,b(x)> . x\<in>A}"
- apply_def: "f`a == Union(f``{a})"
+ apply_def: "f`a == \<Union>(f``{a})"
Pi_def: "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
(* Restrict the relation r to the domain A *)
- restrict_def: "restrict(r,A) == {z : r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
+ restrict_def: "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = <x,y>}"
subsection {* Substitution*}
@@ -311,19 +311,19 @@
by (simp add: Ball_def)
(*Instantiates x first: better for automatic theorem proving?*)
-lemma rev_ballE [elim]:
- "[| \<forall>x\<in>A. P(x); x~:A ==> Q; P(x) ==> Q |] ==> Q"
-by (simp add: Ball_def, blast)
+lemma rev_ballE [elim]:
+ "[| \<forall>x\<in>A. P(x); x\<notin>A ==> Q; P(x) ==> Q |] ==> Q"
+by (simp add: Ball_def, blast)
-lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x~:A ==> Q |] ==> Q"
+lemma ballE: "[| \<forall>x\<in>A. P(x); P(x) ==> Q; x\<notin>A ==> Q |] ==> Q"
by blast
(*Used in the datatype package*)
lemma rev_bspec: "[| x: A; \<forall>x\<in>A. P(x) |] ==> P(x)"
by (simp add: Ball_def)
-(*Trival rewrite rule; (\<forall>x\<in>A.P)<->P holds only if A is nonempty!*)
-lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) --> P)"
+(*Trival rewrite rule; @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
+lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
by (simp add: Ball_def)
(*Congruence rule for rewriting*)
@@ -344,23 +344,23 @@
lemma bexI [intro]: "[| P(x); x: A |] ==> \<exists>x\<in>A. P(x)"
by (simp add: Bex_def, blast)
-(*The best argument order when there is only one x\<in>A*)
+(*The best argument order when there is only one @{term"x\<in>A"}*)
lemma rev_bexI: "[| x\<in>A; P(x) |] ==> \<exists>x\<in>A. P(x)"
by blast
-(*Not of the general form for such rules; ~\<exists>has become ALL~ *)
+(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a); a: A |] ==> \<exists>x\<in>A. P(x)"
by blast
lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x); !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
by (simp add: Bex_def, blast)
-(*We do not even have (\<exists>x\<in>A. True) <-> True unless A is nonempty!!*)
+(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
by (simp add: Bex_def)
lemma bex_cong [cong]:
- "[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |]
+ "[| A=A'; !!x. x\<in>A' ==> P(x) <-> P'(x) |]
==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
by (simp add: Bex_def cong: conj_cong)
@@ -369,39 +369,39 @@
subsection{*Rules for subsets*}
lemma subsetI [intro!]:
- "(!!x. x\<in>A ==> x\<in>B) ==> A <= B"
-by (simp add: subset_def)
+ "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
+by (simp add: subset_def)
(*Rule in Modus Ponens style [was called subsetE] *)
-lemma subsetD [elim]: "[| A <= B; c\<in>A |] ==> c\<in>B"
+lemma subsetD [elim]: "[| A \<subseteq> B; c\<in>A |] ==> c\<in>B"
apply (unfold subset_def)
apply (erule bspec, assumption)
done
(*Classical elimination rule*)
lemma subsetCE [elim]:
- "[| A <= B; c~:A ==> P; c\<in>B ==> P |] ==> P"
-by (simp add: subset_def, blast)
+ "[| A \<subseteq> B; c\<notin>A ==> P; c\<in>B ==> P |] ==> P"
+by (simp add: subset_def, blast)
(*Sometimes useful with premises in this order*)
lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
by blast
-lemma contra_subsetD: "[| A <= B; c ~: B |] ==> c ~: A"
+lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
by blast
-lemma rev_contra_subsetD: "[| c ~: B; A <= B |] ==> c ~: A"
+lemma rev_contra_subsetD: "[| c \<notin> B; A \<subseteq> B |] ==> c \<notin> A"
by blast
-lemma subset_refl [simp]: "A <= A"
+lemma subset_refl [simp]: "A \<subseteq> A"
by blast
lemma subset_trans: "[| A<=B; B<=C |] ==> A<=C"
by blast
(*Useful for proving A<=B by rewriting in some cases*)
-lemma subset_iff:
- "A<=B <-> (\<forall>x. x\<in>A --> x\<in>B)"
+lemma subset_iff:
+ "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
apply (unfold subset_def Ball_def)
apply (rule iff_refl)
done
@@ -410,8 +410,8 @@
subsection{*Rules for equality*}
(*Anti-symmetry of the subset relation*)
-lemma equalityI [intro]: "[| A <= B; B <= A |] ==> A = B"
-by (rule extension [THEN iffD2], rule conjI)
+lemma equalityI [intro]: "[| A \<subseteq> B; B \<subseteq> A |] ==> A = B"
+by (rule extension [THEN iffD2], rule conjI)
lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
@@ -421,75 +421,75 @@
lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
-by (blast dest: equalityD1 equalityD2)
+by (blast dest: equalityD1 equalityD2)
lemma equalityCE:
- "[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
-by (erule equalityE, blast)
+ "[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c\<notin>A; c\<notin>B |] ==> P |] ==> P"
+by (erule equalityE, blast)
lemma equality_iffD:
- "A = B ==> (!!x. x : A <-> x : B)"
+ "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
by auto
subsection{*Rules for Replace -- the derived form of replacement*}
-lemma Replace_iff:
- "b : {y. x\<in>A, P(x,y)} <-> (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) --> y=b))"
+lemma Replace_iff:
+ "b \<in> {y. x\<in>A, P(x,y)} <-> (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
apply (unfold Replace_def)
apply (rule replacement [THEN iff_trans], blast+)
done
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
-lemma ReplaceI [intro]:
- "[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==>
- b : {y. x\<in>A, P(x,y)}"
-by (rule Replace_iff [THEN iffD2], blast)
+lemma ReplaceI [intro]:
+ "[| P(x,b); x: A; !!y. P(x,y) ==> y=b |] ==>
+ b \<in> {y. x\<in>A, P(x,y)}"
+by (rule Replace_iff [THEN iffD2], blast)
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
-lemma ReplaceE:
- "[| b : {y. x\<in>A, P(x,y)};
- !!x. [| x: A; P(x,b); \<forall>y. P(x,y)-->y=b |] ==> R
+lemma ReplaceE:
+ "[| b \<in> {y. x\<in>A, P(x,y)};
+ !!x. [| x: A; P(x,b); \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
|] ==> R"
by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
(*As above but without the (generally useless) 3rd assumption*)
-lemma ReplaceE2 [elim!]:
- "[| b : {y. x\<in>A, P(x,y)};
- !!x. [| x: A; P(x,b) |] ==> R
+lemma ReplaceE2 [elim!]:
+ "[| b \<in> {y. x\<in>A, P(x,y)};
+ !!x. [| x: A; P(x,b) |] ==> R
|] ==> R"
-by (erule ReplaceE, blast)
+by (erule ReplaceE, blast)
lemma Replace_cong [cong]:
- "[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
+ "[| A=B; !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
Replace(A,P) = Replace(B,Q)"
-apply (rule equality_iffI)
-apply (simp add: Replace_iff)
+apply (rule equality_iffI)
+apply (simp add: Replace_iff)
done
subsection{*Rules for RepFun*}
-lemma RepFunI: "a \<in> A ==> f(a) : {f(x). x\<in>A}"
+lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
by (simp add: RepFun_def Replace_iff, blast)
(*Useful for coinduction proofs*)
-lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b : {f(x). x\<in>A}"
+lemma RepFun_eqI [intro]: "[| b=f(a); a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
apply (erule ssubst)
apply (erule RepFunI)
done
lemma RepFunE [elim!]:
- "[| b : {f(x). x\<in>A};
- !!x.[| x\<in>A; b=f(x) |] ==> P |] ==>
+ "[| b \<in> {f(x). x\<in>A};
+ !!x.[| x\<in>A; b=f(x) |] ==> P |] ==>
P"
-by (simp add: RepFun_def Replace_iff, blast)
+by (simp add: RepFun_def Replace_iff, blast)
-lemma RepFun_cong [cong]:
+lemma RepFun_cong [cong]:
"[| A=B; !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
by (simp add: RepFun_def)
-lemma RepFun_iff [simp]: "b : {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
+lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
by (unfold Bex_def, blast)
lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
@@ -499,23 +499,23 @@
subsection{*Rules for Collect -- forming a subset by separation*}
(*Separation is derivable from Replacement*)
-lemma separation [simp]: "a : {x\<in>A. P(x)} <-> a\<in>A & P(a)"
+lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
by (unfold Collect_def, blast)
-lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a : {x\<in>A. P(x)}"
+lemma CollectI [intro!]: "[| a\<in>A; P(a) |] ==> a \<in> {x\<in>A. P(x)}"
by simp
-lemma CollectE [elim!]: "[| a : {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R"
+lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)}; [| a\<in>A; P(a) |] ==> R |] ==> R"
by simp
-lemma CollectD1: "a : {x\<in>A. P(x)} ==> a\<in>A"
+lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
by (erule CollectE, assumption)
-lemma CollectD2: "a : {x\<in>A. P(x)} ==> P(a)"
+lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
by (erule CollectE, assumption)
lemma Collect_cong [cong]:
- "[| A=B; !!x. x\<in>B ==> P(x) <-> Q(x) |]
+ "[| A=B; !!x. x\<in>B ==> P(x) <-> Q(x) |]
==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
by (simp add: Collect_def)
@@ -525,17 +525,17 @@
declare Union_iff [simp]
(*The order of the premises presupposes that C is rigid; A may be flexible*)
-lemma UnionI [intro]: "[| B: C; A: B |] ==> A: Union(C)"
+lemma UnionI [intro]: "[| B: C; A: B |] ==> A: \<Union>(C)"
by (simp, blast)
-lemma UnionE [elim!]: "[| A \<in> Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
+lemma UnionE [elim!]: "[| A \<in> \<Union>(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
by (simp, blast)
subsection{*Rules for Unions of families*}
-(* \<Union>x\<in>A. B(x) abbreviates Union({B(x). x\<in>A}) *)
+(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
-lemma UN_iff [simp]: "b : (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
+lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
by (simp add: Bex_def, blast)
(*The order of the premises presupposes that A is rigid; b may be flexible*)
@@ -543,16 +543,16 @@
by (simp, blast)
-lemma UN_E [elim!]:
- "[| b : (\<Union>x\<in>A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"
-by blast
+lemma UN_E [elim!]:
+ "[| b \<in> (\<Union>x\<in>A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"
+by blast
-lemma UN_cong:
+lemma UN_cong:
"[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
-by simp
+by simp
-(*No "Addcongs [UN_cong]" because \<Union>is a combination of constants*)
+(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
(* UN_E appears before UnionE so that it is tried first, to avoid expensive
calls to hyp_subst_tac. Cannot include UN_I as it is unsafe: would enlarge
@@ -561,9 +561,9 @@
subsection{*Rules for the empty set*}
-(*The set {x\<in>0. False} is empty; by foundation it equals 0
+(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
See Suppes, page 21.*)
-lemma not_mem_empty [simp]: "a ~: 0"
+lemma not_mem_empty [simp]: "a \<notin> 0"
apply (cut_tac foundation)
apply (best dest: equalityD2)
done
@@ -571,69 +571,69 @@
lemmas emptyE [elim!] = not_mem_empty [THEN notE]
-lemma empty_subsetI [simp]: "0 <= A"
-by blast
+lemma empty_subsetI [simp]: "0 \<subseteq> A"
+by blast
lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
by blast
-lemma equals0D [dest]: "A=0 ==> a ~: A"
+lemma equals0D [dest]: "A=0 ==> a \<notin> A"
by blast
declare sym [THEN equals0D, dest]
-lemma not_emptyI: "a\<in>A ==> A ~= 0"
+lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
by blast
-lemma not_emptyE: "[| A ~= 0; !!x. x\<in>A ==> R |] ==> R"
+lemma not_emptyE: "[| A \<noteq> 0; !!x. x\<in>A ==> R |] ==> R"
by blast
subsection{*Rules for Inter*}
(*Not obviously useful for proving InterI, InterD, InterE*)
-lemma Inter_iff: "A \<in> Inter(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
+lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
by (simp add: Inter_def Ball_def, blast)
(* Intersection is well-behaved only if the family is non-empty! *)
-lemma InterI [intro!]:
- "[| !!x. x: C ==> A: x; C\<noteq>0 |] ==> A \<in> Inter(C)"
+lemma InterI [intro!]:
+ "[| !!x. x: C ==> A: x; C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
by (simp add: Inter_iff)
(*A "destruct" rule -- every B in C contains A as an element, but
A\<in>B can hold when B\<in>C does not! This rule is analogous to "spec". *)
-lemma InterD [elim, Pure.elim]: "[| A \<in> Inter(C); B \<in> C |] ==> A \<in> B"
+lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C); B \<in> C |] ==> A \<in> B"
by (unfold Inter_def, blast)
-(*"Classical" elimination rule -- does not require exhibiting B\<in>C *)
-lemma InterE [elim]:
- "[| A \<in> Inter(C); B~:C ==> R; A\<in>B ==> R |] ==> R"
-by (simp add: Inter_def, blast)
-
+(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
+lemma InterE [elim]:
+ "[| A \<in> \<Inter>(C); B\<notin>C ==> R; A\<in>B ==> R |] ==> R"
+by (simp add: Inter_def, blast)
+
subsection{*Rules for Intersections of families*}
-(* \<Inter>x\<in>A. B(x) abbreviates Inter({B(x). x\<in>A}) *)
+(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
-lemma INT_iff: "b : (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
+lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
by (force simp add: Inter_def)
lemma INT_I: "[| !!x. x: A ==> b: B(x); A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
by blast
-lemma INT_E: "[| b : (\<Inter>x\<in>A. B(x)); a: A |] ==> b \<in> B(a)"
+lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x)); a: A |] ==> b \<in> B(a)"
by blast
lemma INT_cong:
"[| A=B; !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
by simp
-(*No "Addcongs [INT_cong]" because \<Inter>is a combination of constants*)
+(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
subsection{*Rules for Powersets*}
-lemma PowI: "A <= B ==> A \<in> Pow(B)"
+lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
by (erule Pow_iff [THEN iffD2])
lemma PowD: "A \<in> Pow(B) ==> A<=B"
@@ -641,16 +641,16 @@
declare Pow_iff [iff]
-lemmas Pow_bottom = empty_subsetI [THEN PowI] (* 0 \<in> Pow(B) *)
-lemmas Pow_top = subset_refl [THEN PowI] (* A \<in> Pow(A) *)
+lemmas Pow_bottom = empty_subsetI [THEN PowI] --{* @{term"0 \<in> Pow(B)"} *}
+lemmas Pow_top = subset_refl [THEN PowI] --{* @{term"A \<in> Pow(A)"} *}
subsection{*Cantor's Theorem: There is no surjection from a set to its powerset.*}
-(*The search is undirected. Allowing redundant introduction rules may
+(*The search is undirected. Allowing redundant introduction rules may
make it diverge. Variable b represents ANY map, such as
(lam x\<in>A.b(x)): A->Pow(A). *)
-lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) ~= S"
+lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
end