--- a/src/ZF/ArithSimp.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/ArithSimp.thy Tue Oct 01 13:26:10 2002 +0200
@@ -514,14 +514,13 @@
(P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
apply (case_tac "a < b")
apply (force simp add: nat_lt_imp_diff_eq_0)
-apply (rule iffI, simp_all)
- apply clarify
- apply (rotate_tac -1)
- apply simp
+apply (rule iffI, force)
+apply simp
apply (drule_tac x="a#-b" in bspec)
apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse)
done
+
ML
{*
val diff_self_eq_0 = thm "diff_self_eq_0";
--- a/src/ZF/Cardinal.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Cardinal.thy Tue Oct 01 13:26:10 2002 +0200
@@ -917,8 +917,7 @@
apply (erule Finite_induct, auto)
apply (case_tac "x:A")
apply (subgoal_tac [2] "A-cons (x, B) = A - B")
-apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
-apply (rotate_tac -1, simp)
+apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
apply (drule Diff_sing_Finite, auto)
done
--- a/src/ZF/CardinalArith.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/CardinalArith.thy Tue Oct 01 13:26:10 2002 +0200
@@ -30,7 +30,7 @@
be a cardinal*)
jump_cardinal :: "i=>i"
"jump_cardinal(K) ==
- UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
+ \<Union>X\<in>Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
(*needed because jump_cardinal(K) might not be the successor of K*)
csucc :: "i=>i"
@@ -55,11 +55,11 @@
done
lemma Card_UN:
- "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))"
+ "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))"
by (blast intro: Card_Union)
lemma Card_OUN [simp,intro,TC]:
- "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
+ "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
by (simp add: OUnion_def Card_0)
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
@@ -850,16 +850,15 @@
lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
apply (rule succ_inject)
apply (rule_tac b = "|A|" in trans)
-apply (simp add: Finite_imp_succ_cardinal_Diff)
+ apply (simp add: Finite_imp_succ_cardinal_Diff)
apply (subgoal_tac "1 \<lesssim> A")
prefer 2 apply (blast intro: not_0_is_lepoll_1)
apply (frule Finite_imp_well_ord, clarify)
-apply (rotate_tac -1)
apply (drule well_ord_lepoll_imp_Card_le)
-apply (auto simp add: cardinal_1)
+ apply (auto simp add: cardinal_1)
apply (rule trans)
-apply (rule_tac [2] diff_succ)
-apply (auto simp add: Finite_cardinal_in_nat)
+ apply (rule_tac [2] diff_succ)
+ apply (auto simp add: Finite_cardinal_in_nat)
done
lemma cardinal_lt_imp_Diff_not_0 [rule_format]:
--- a/src/ZF/Cardinal_AC.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy Tue Oct 01 13:26:10 2002 +0200
@@ -28,10 +28,10 @@
lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
by (blast intro: cardinal_cong cardinal_eqE)
-lemma cardinal_disjoint_Un: "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==>
- |A Un C| = |B Un D|"
-apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
-done
+lemma cardinal_disjoint_Un:
+ "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |]
+ ==> |A Un C| = |B Un D|"
+by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
apply (rule AC_well_ord [THEN exE])
@@ -85,7 +85,8 @@
apply (erule CollectE)
apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
apply (fast elim!: apply_Pair)
-apply (blast dest: apply_type Pi_memberD intro: apply_equality Pi_type f_imp_injective)
+apply (blast dest: apply_type Pi_memberD
+ intro: apply_equality Pi_type f_imp_injective)
done
(*Kunen's Lemma 10.20*)
@@ -97,7 +98,8 @@
done
(*Kunen's Lemma 10.21*)
-lemma cardinal_UN_le: "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"
+lemma cardinal_UN_le:
+ "[| InfCard(K); ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
apply (simp add: InfCard_is_Card le_Card_iff)
apply (rule lepoll_trans)
prefer 2
@@ -108,7 +110,8 @@
apply (erule AC_ball_Pi [THEN exE])
apply (rule exI)
(*Lemma needed in both subgoals, for a fixed z*)
-apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K")
+apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
+ (LEAST i. z:X (i)) : K")
prefer 2
apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
elim!: LeastI Ord_in_Ord)
@@ -121,15 +124,14 @@
(*The same again, using csucc*)
lemma cardinal_UN_lt_csucc:
"[| InfCard(K); ALL i:K. |X(i)| < csucc(K) |]
- ==> |UN i:K. X(i)| < csucc(K)"
-apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
-done
+ ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
+by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i),
the least ordinal j such that i:Vfrom(A,j). *)
lemma cardinal_UN_Ord_lt_csucc:
"[| InfCard(K); ALL i:K. j(i) < csucc(K) |]
- ==> (UN i:K. j(i)) < csucc(K)"
+ ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
apply (blast intro!: Ord_UN elim: ltE)
@@ -144,7 +146,7 @@
(*Work backwards along the injection from W into K, given that W~=0.*)
lemma inj_UN_subset:
"[| f: inj(A,B); a:A |] ==>
- (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"
+ (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
apply (rule UN_least)
apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
apply (simp add: inj_is_fun [THEN apply_rangeI])
@@ -155,7 +157,7 @@
be weaker.*)
lemma le_UN_Ord_lt_csucc:
"[| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |]
- ==> (UN w:W. j(w)) < csucc(K)"
+ ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
apply (case_tac "W=0")
(*solve the easy 0 case*)
apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]
--- a/src/ZF/Constructible/AC_in_L.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy Tue Oct 01 13:26:10 2002 +0200
@@ -240,7 +240,6 @@
apply safe
apply (subgoal_tac "Ord(y)")
prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
- apply (rotate_tac -1)
apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
Ord_mem_iff_lt)
apply (blast intro: lt_trans)
--- a/src/ZF/Constructible/Datatype_absolute.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Oct 01 13:26:10 2002 +0200
@@ -683,10 +683,8 @@
Ord(i); M(i); M(z);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
-apply (rotate_tac 2)
-apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
+by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
-done
theorem (in M_eclose) transrec_closed:
@@ -694,10 +692,9 @@
Ord(i); M(i);
\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
==> M(transrec(i,H))"
-apply (rotate_tac 2)
-apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
- transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
-done
+by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
+ transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
+
text{*Helps to prove instances of @{term transrec_replacement}*}
lemma (in M_eclose) transrec_replacementI:
--- a/src/ZF/Constructible/Relative.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Oct 01 13:26:10 2002 +0200
@@ -1203,7 +1203,6 @@
lemma (in M_basic) restriction_is_function:
"[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
==> function(z)"
-apply (rotate_tac 1)
apply (simp add: restriction_def ball_iff_equiv)
apply (unfold function_def, blast)
done
--- a/src/ZF/Constructible/WF_absolute.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Oct 01 13:26:10 2002 +0200
@@ -225,7 +225,6 @@
lemma (in M_trancl) wellfounded_trancl:
"[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
-apply (rotate_tac -1)
apply (simp add: wellfounded_iff_wellfounded_on_field)
apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl)
apply blast
--- a/src/ZF/Constructible/WFrec.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Tue Oct 01 13:26:10 2002 +0200
@@ -143,7 +143,7 @@
apply (drule equalityD1 [THEN subsetD], assumption)
apply (blast dest: pair_components_in_M)
apply (blast elim!: equalityE dest: pair_components_in_M)
- apply (frule transM, assumption, rotate_tac -1)
+ apply (frule transM, assumption)
apply simp
apply blast
apply (subgoal_tac "is_function(M,f)")
@@ -187,7 +187,6 @@
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
apply (frule_tac y="<y,z>" in transM, assumption)
- apply (rotate_tac -1)
apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
apply_recfun is_recfun_cut)
txt{*Opposite inclusion: something in f, show in Y*}
@@ -320,9 +319,7 @@
relativize2(M,MH,H); M(r)|]
==> strong_replacement(M, \<lambda>x z. \<exists>y[M].
pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
-apply (rotate_tac 1)
-apply (simp add: wfrec_replacement_def is_wfrec_abs)
-done
+by (simp add: wfrec_replacement_def is_wfrec_abs)
lemma wfrec_replacement_cong [cong]:
"[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z);
--- a/src/ZF/Constructible/Wellorderings.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Oct 01 13:26:10 2002 +0200
@@ -381,7 +381,7 @@
apply (rule iffI)
prefer 2 apply blast
apply (rule equalityI)
- apply (clarify, frule transM, assumption, rotate_tac -1, simp)
+ apply (clarify, frule transM, assumption, simp)
apply (clarify, frule transM, assumption, force)
done
@@ -392,7 +392,6 @@
==> z \<in> f <->
(\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) &
g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
-apply (rotate_tac 1)
apply (simp add: omap_def Memrel_closed pred_closed)
apply (rule iffI)
apply (drule_tac [2] x=z in rspec)
@@ -432,7 +431,6 @@
lemma (in M_basic) Ord_otype:
"[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
-apply (rotate_tac 1)
apply (rule OrdI)
prefer 2
apply (simp add: Ord_def otype_def omap_def)
@@ -454,7 +452,6 @@
lemma (in M_basic) domain_omap:
"[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |]
==> domain(f) = B"
-apply (rotate_tac 2)
apply (simp add: domain_closed obase_iff)
apply (rule equality_iffI)
apply (simp add: domain_iff omap_iff, blast)
@@ -463,7 +460,7 @@
lemma (in M_basic) omap_subset:
"[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
-apply (rotate_tac 3, clarify)
+apply clarify
apply (simp add: omap_iff obase_iff)
apply (force simp add: otype_iff)
done
@@ -471,7 +468,6 @@
lemma (in M_basic) omap_funtype:
"[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
-apply (rotate_tac 3)
apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff)
apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
done
@@ -519,7 +515,6 @@
apply (rule OrdI)
prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast)
txt{*Hard part is to show that the image is a transitive set.*}
-apply (rotate_tac 3)
apply (simp add: Transset_def, clarify)
apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
apply (rename_tac c j, clarify)
@@ -552,7 +547,6 @@
lemma (in M_basic) obase_equals:
"[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
-apply (rotate_tac 4)
apply (rule equalityI, force simp add: obase_iff, clarify)
apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp)
apply (frule wellordered_is_wellfounded_on, assumption)
--- a/src/ZF/Epsilon.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue Oct 01 13:26:10 2002 +0200
@@ -11,13 +11,13 @@
constdefs
eclose :: "i=>i"
- "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
+ "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))"
transrec :: "[i, [i,i]=>i] =>i"
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
rank :: "i=>i"
- "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
+ "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
transrec2 :: "[i, i, [i,i]=>i] =>i"
"transrec2(k, a, b) ==
@@ -25,7 +25,7 @@
%i r. if(i=0, a,
if(EX j. i=succ(j),
b(THE j. i=succ(j), r`(THE j. i=succ(j))),
- UN j<i. r`j)))"
+ \<Union>j<i. r`j)))"
recursor :: "[i, [i,i]=>i, i]=>i"
"recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
@@ -216,7 +216,7 @@
subsection{*Rank*}
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
-lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
+lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))"
by (subst rank_def [THEN def_transrec], simp)
lemma Ord_rank [simp]: "Ord(rank(a))"
@@ -268,7 +268,7 @@
apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
done
-lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
+lemma rank_Union: "rank(Union(A)) = (\<Union>x\<in>A. rank(x))"
apply (rule equalityI)
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
apply (erule_tac [2] Union_upper)
@@ -350,7 +350,7 @@
done
lemma transrec2_Limit:
- "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
+ "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
apply (rule transrec2_def [THEN def_transrec, THEN trans])
apply (auto simp add: OUnion_def)
done
@@ -359,7 +359,7 @@
"(!!x. f(x)==transrec2(x,a,b))
==> f(0) = a &
f(succ(i)) = b(i, f(i)) &
- (Limit(K) --> f(K) = (UN j<K. f(j)))"
+ (Limit(K) --> f(K) = (\<Union>j<K. f(j)))"
by (simp add: transrec2_Limit)
--- a/src/ZF/Finite.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Finite.thy Tue Oct 01 13:26:10 2002 +0200
@@ -172,7 +172,6 @@
apply (erule Fin.induct)
apply (simp add: FiniteFun.intros, clarify)
apply (case_tac "a:b")
- apply (rotate_tac -1)
apply (simp add: cons_absorb)
apply (subgoal_tac "restrict (f,b) : b -||> B")
prefer 2 apply (blast intro: restrict_type2)
--- a/src/ZF/InfDatatype.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/InfDatatype.thy Tue Oct 01 13:26:10 2002 +0200
@@ -15,7 +15,7 @@
lemma fun_Vcsucc_lemma:
"[| f: D -> Vfrom(A,csucc(K)); |D| le K; InfCard(K) |]
==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"
-apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
+apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d : Vfrom (A,i) " in exI)
apply (rule conjI)
apply (rule_tac [2] le_UN_Ord_lt_csucc)
apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all)
--- a/src/ZF/Integ/EquivClass.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Integ/EquivClass.thy Tue Oct 01 13:26:10 2002 +0200
@@ -149,18 +149,15 @@
==> X=Y"
apply (unfold quotient_def, safe)
apply (rule equiv_class_eq, assumption)
-apply (rotate_tac -2)
apply (simp add: UN_equiv_class [of A r b])
done
subsection{*Defining Binary Operations upon Equivalence Classes*}
-
lemma congruent2_implies_congruent:
"[| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))"
-apply (unfold congruent_def congruent2_def equiv_def refl_def, blast)
-done
+by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
lemma congruent2_implies_congruent_UN:
"[| equiv(A,r); congruent2(r,b); a: A |] ==>
--- a/src/ZF/Integ/IntDiv.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Integ/IntDiv.thy Tue Oct 01 13:26:10 2002 +0200
@@ -658,18 +658,16 @@
(*the case a=0*)
lemma quorem_0: "[|b \<noteq> #0; b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
-apply (rotate_tac -1)
-apply (auto simp add: quorem_def neq_iff_zless)
-done
+by (force simp add: quorem_def neq_iff_zless)
lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
apply (subst posDivAlg_unfold)
-apply (simp (no_asm))
+apply simp
done
lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
apply (subst posDivAlg_unfold)
-apply (simp (no_asm) add: not_zle_iff_zless)
+apply (simp add: not_zle_iff_zless)
done
@@ -710,7 +708,6 @@
lemma divAlg_correct:
"[|b \<noteq> #0; a \<in> int; b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
-apply (rotate_tac 1)
apply (auto simp add: quorem_0 divAlg_def)
apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
posDivAlg_type negDivAlg_type)
@@ -810,7 +807,6 @@
"[|b \<noteq> #0; a \<in> int; b \<in> int |]
==> quorem (<a,b>, <a zdiv b, a zmod b>)"
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
-apply (rotate_tac 1)
apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
neg_mod_sign neg_mod_bound)
done
--- a/src/ZF/List.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/List.thy Tue Oct 01 13:26:10 2002 +0200
@@ -721,8 +721,7 @@
apply (induct_tac "m", auto)
apply (erule_tac a = xs in list.cases)
apply (auto simp add: take_Nil)
-apply (rotate_tac 1)
-apply (erule natE)
+apply (erule_tac n=n in natE)
apply (auto intro: take_0 take_type)
done
--- a/src/ZF/OrdQuant.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/OrdQuant.thy Tue Oct 01 13:26:10 2002 +0200
@@ -20,7 +20,7 @@
(* Ordinal Union *)
OUnion :: "[i, i => i] => i"
- "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
+ "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
syntax
"@oall" :: "[idt, i, o] => o" ("(3ALL _<_./ _)" 10)
@@ -77,31 +77,31 @@
apply (auto simp add: lt_def)
done
-lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i"
+lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i"
by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
-(* No < version; consider (UN i:nat.i)=nat *)
+(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
lemma OUN_least:
- "(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C"
+ "(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C"
by (simp add: OUnion_def UN_least ltI)
-(* No < version; consider (UN i:nat.i)=nat *)
+(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
lemma OUN_least_le:
- "[| Ord(i); !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i"
+ "[| Ord(i); !!x. x<A ==> b(x) \<le> i |] ==> (\<Union>x<A. b(x)) \<le> i"
by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
lemma le_implies_OUN_le_OUN:
- "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))"
+ "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (\<Union>x<A. c(x)) \<le> (\<Union>x<A. d(x))"
by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)
lemma OUN_UN_eq:
"(!!x. x:A ==> Ord(B(x)))
- ==> (UN z < (UN x:A. B(x)). C(z)) = (UN x:A. UN z < B(x). C(z))"
+ ==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))"
by (simp add: OUnion_def)
lemma OUN_Union_eq:
"(!!x. x:X ==> Ord(x))
- ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
+ ==> (\<Union>z < Union(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
by (simp add: OUnion_def)
(*So that rule_format will get rid of ALL x<A...*)
@@ -165,19 +165,19 @@
subsubsection {*Rules for Ordinal-Indexed Unions*}
-lemma OUN_I [intro]: "[| a<i; b: B(a) |] ==> b: (UN z<i. B(z))"
+lemma OUN_I [intro]: "[| a<i; b: B(a) |] ==> b: (\<Union>z<i. B(z))"
by (unfold OUnion_def lt_def, blast)
lemma OUN_E [elim!]:
- "[| b : (UN z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R"
+ "[| b : (\<Union>z<i. B(z)); !!a.[| b: B(a); a<i |] ==> R |] ==> R"
apply (unfold OUnion_def lt_def, blast)
done
-lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
+lemma OUN_iff: "b : (\<Union>x<i. B(x)) <-> (EX x<i. b : B(x))"
by (unfold OUnion_def oex_def lt_def, blast)
lemma OUN_cong [cong]:
- "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
+ "[| i=j; !!x. x<j ==> C(x)=D(x) |] ==> (\<Union>x<i. C(x)) = (\<Union>x<j. D(x))"
by (simp add: OUnion_def lt_def OUN_iff)
lemma lt_induct:
--- a/src/ZF/Order.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Order.thy Tue Oct 01 13:26:10 2002 +0200
@@ -38,7 +38,7 @@
ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*)
"ord_iso_map(A,r,B,s) ==
- UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
+ \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
first :: "[i, i, i] => o"
"first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
--- a/src/ZF/OrderType.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/OrderType.thy Tue Oct 01 13:26:10 2002 +0200
@@ -567,7 +567,7 @@
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
done
-lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"
+lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
apply (rule subsetI [THEN equalityI])
apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
apply (blast intro: Ord_oadd)
@@ -592,12 +592,12 @@
lemma oadd_UN:
"[| !!x. x:A ==> Ord(j(x)); a:A |]
- ==> i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"
+ ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]
oadd_lt_mono2 [THEN ltD]
elim!: ltE dest!: ltI [THEN lt_oadd_disj])
-lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)"
+lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
apply (frule Limit_has_0 [THEN ltD])
apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
@@ -818,7 +818,7 @@
done
lemma omult_unfold:
- "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"
+ "[| Ord(i); Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
apply (rule subsetI [THEN equalityI])
apply (rule lt_omult [THEN exE])
apply (erule_tac [3] ltI)
@@ -901,10 +901,10 @@
lemma omult_UN:
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |]
- ==> i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"
+ ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
-lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"
+lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
--- a/src/ZF/Ordinal.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Ordinal.thy Tue Oct 01 13:26:10 2002 +0200
@@ -102,11 +102,11 @@
by (unfold Inter_def Transset_def, blast)
lemma Transset_UN:
- "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
+ "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))"
by (rule Transset_Union_family, auto)
lemma Transset_INT:
- "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
+ "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))"
by (rule Transset_Inter_family, auto)
@@ -555,7 +555,7 @@
done
lemma Ord_UN [intro,simp,TC]:
- "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
+ "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
by (rule Ord_Union, blast)
lemma Ord_Inter [intro,simp,TC]:
@@ -567,19 +567,19 @@
done
lemma Ord_INT [intro,simp,TC]:
- "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
+ "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
by (rule Ord_Inter, blast)
-(* No < version; consider (UN i:nat.i)=nat *)
+(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
lemma UN_least_le:
- "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"
+ "[| Ord(i); !!x. x:A ==> b(x) le i |] ==> (\<Union>x\<in>A. b(x)) le i"
apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
apply (blast intro: Ord_UN elim: ltE)+
done
lemma UN_succ_least_lt:
- "[| j<i; !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"
+ "[| j<i; !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
apply (rule ltE, assumption)
apply (rule UN_least_le [THEN lt_trans2])
apply (blast intro: succ_leI)+
@@ -590,7 +590,7 @@
by (unfold lt_def, blast)
lemma UN_upper_le:
- "[| a: A; i le b(a); Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))"
+ "[| a: A; i le b(a); Ord(\<Union>x\<in>A. b(x)) |] ==> i le (\<Union>x\<in>A. b(x))"
apply (frule ltD)
apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le])
apply (blast intro: lt_Ord UN_upper)+
@@ -606,13 +606,13 @@
done
lemma le_implies_UN_le_UN:
- "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))"
+ "[| !!x. x:A ==> c(x) le d(x) |] ==> (\<Union>x\<in>A. c(x)) le (\<Union>x\<in>A. d(x))"
apply (rule UN_least_le)
apply (rule_tac [2] UN_upper_le)
apply (blast intro: Ord_UN le_Ord2)+
done
-lemma Ord_equality: "Ord(i) ==> (UN y:i. succ(y)) = i"
+lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i"
by (blast intro: Ord_trans)
(*Holds for all transitive sets, not just ordinals*)
--- a/src/ZF/QPair.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/QPair.thy Tue Oct 01 13:26:10 2002 +0200
@@ -38,7 +38,7 @@
"qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
QSigma :: "[i, i => i] => i"
- "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}"
+ "QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
"@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
--- a/src/ZF/QUniv.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/QUniv.thy Tue Oct 01 13:26:10 2002 +0200
@@ -189,7 +189,7 @@
subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
lemma QPair_Int_Vset_subset_UN:
- "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
+ "Ord(i) ==> <a;b> Int Vset(i) <= (\<Union>j\<in>i. <a Int Vset(j); b Int Vset(j)>)"
apply (erule Ord_cases)
(*0 case*)
apply (simp add: Vfrom_0)
--- a/src/ZF/equalities.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/equalities.thy Tue Oct 01 13:26:10 2002 +0200
@@ -62,10 +62,10 @@
lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
by blast
-lemma ball_UN: "(\<forall>z \<in> (UN x:A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
+lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
by blast
-lemma bex_UN: "(\<exists>z \<in> (UN x:A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
+lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
by blast
subsection{*Converse of a Relation*}
@@ -136,7 +136,7 @@
lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
by blast
-lemma equal_singleton [rule_format]: "[| a: C; ALL y:C. y=b |] ==> C = {b}"
+lemma equal_singleton [rule_format]: "[| a: C; \<forall>y\<in>C. y=b |] ==> C = {b}"
by blast
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
@@ -354,7 +354,7 @@
(** Big Union is the least upper bound of a set **)
-lemma Union_subset_iff: "Union(A) <= C <-> (ALL x:A. x <= C)"
+lemma Union_subset_iff: "Union(A) <= C <-> (\<forall>x\<in>A. x <= C)"
by blast
lemma Union_upper: "B:A ==> B <= Union(A)"
@@ -372,15 +372,15 @@
lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)"
by blast
-lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"
+lemma Union_disjoint: "Union(C) Int A = 0 <-> (\<forall>B\<in>C. B Int A = 0)"
by (blast elim!: equalityE)
-lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)"
+lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
by blast
(** Big Intersection is the greatest lower bound of a nonempty set **)
-lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (ALL x:A. C <= x)"
+lemma Inter_subset_iff: "a: A ==> C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
by blast
lemma Inter_lower: "B:A ==> Inter(A) <= B"
@@ -391,11 +391,11 @@
(** Intersection of a family of sets **)
-lemma INT_lower: "x:A ==> (INT x:A. B(x)) <= B(x)"
+lemma INT_lower: "x:A ==> (\<Inter>x\<in>A. B(x)) <= B(x)"
by blast
lemma INT_greatest:
- "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
+ "[| a:A; !!x. x:A ==> C<=B(x) |] ==> C <= (\<Inter>x\<in>A. B(x))"
by blast
lemma Inter_0: "Inter(0) = 0"
@@ -422,80 +422,80 @@
subsection{*Unions and Intersections of Families*}
-lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"
+lemma subset_UN_iff_eq: "A <= (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
by (blast elim!: equalityE)
-lemma UN_subset_iff: "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
+lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) <= C <-> (\<forall>x\<in>A. B(x) <= C)"
by blast
-lemma UN_upper: "x:A ==> B(x) <= (UN x:A. B(x))"
+lemma UN_upper: "x:A ==> B(x) <= (\<Union>x\<in>A. B(x))"
by (erule RepFunI [THEN Union_upper])
-lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
+lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (\<Union>x\<in>A. B(x)) <= C"
by blast
-lemma Union_eq_UN: "Union(A) = (UN x:A. x)"
+lemma Union_eq_UN: "Union(A) = (\<Union>x\<in>A. x)"
by blast
-lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)"
+lemma Inter_eq_INT: "Inter(A) = (\<Inter>x\<in>A. x)"
by (unfold Inter_def, blast)
-lemma UN_0 [simp]: "(UN i:0. A(i)) = 0"
+lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
by blast
-lemma UN_singleton: "(UN x:A. {x}) = A"
+lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
by blast
-lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))"
+lemma UN_Un: "(\<Union>i\<in> A Un B. C(i)) = (\<Union>i\<in> A. C(i)) Un (\<Union>i\<in>B. C(i))"
by blast
-lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j)
- else if J=0 then INT i:I. A(i)
- else ((INT i:I. A(i)) Int (INT j:J. A(j))))"
+lemma INT_Un: "(\<Inter>i\<in>I Un J. A(i)) = (if I=0 then \<Inter>j\<in>J. A(j)
+ else if J=0 then \<Inter>i\<in>I. A(i)
+ else ((\<Inter>i\<in>I. A(i)) Int (\<Inter>j\<in>J. A(j))))"
apply simp
apply (blast intro!: equalityI)
done
-lemma UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))"
+lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))"
by blast
(*Halmos, Naive Set Theory, page 35.*)
-lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"
+lemma Int_UN_distrib: "B Int (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B Int A(i))"
by blast
-lemma Un_INT_distrib: "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"
+lemma Un_INT_distrib: "i:I ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
by blast
lemma Int_UN_distrib2:
- "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"
+ "(\<Union>i\<in>I. A(i)) Int (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) Int B(j))"
by blast
lemma Un_INT_distrib2: "[| i:I; j:J |] ==>
- (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"
+ (\<Inter>i\<in>I. A(i)) Un (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) Un B(j))"
by blast
-lemma UN_constant: "a: A ==> (UN y:A. c) = c"
+lemma UN_constant: "a: A ==> (\<Union>y\<in>A. c) = c"
by blast
-lemma INT_constant: "a: A ==> (INT y:A. c) = c"
+lemma INT_constant: "a: A ==> (\<Inter>y\<in>A. c) = c"
by blast
-lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))"
+lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
by blast
-lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x)) = (INT a:A. B(f(a)))"
+lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x)) = (\<Inter>a\<in>A. B(f(a)))"
by (auto simp add: Inter_def)
lemma INT_Union_eq:
- "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))"
-apply (simp add: Inter_def)
-apply (subgoal_tac "ALL x:A. x~=0")
-prefer 2 apply blast
-apply (tactic "first_best_tac (claset() addss' simpset()) 1")
+ "0 ~: A ==> (\<Inter>x\<in> Union(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
+apply (subgoal_tac "\<forall>x\<in>A. x~=0")
+ prefer 2 apply blast
+apply (force simp add: Inter_def ball_conj_distrib)
done
-lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0)
- ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))"
+lemma INT_UN_eq:
+ "(\<forall>x\<in>A. B(x) ~= 0)
+ ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
apply (subst INT_Union_eq, blast)
apply (simp add: Inter_def)
done
@@ -505,23 +505,23 @@
Union of a family of unions **)
lemma UN_Un_distrib:
- "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))"
+ "(\<Union>i\<in>I. A(i) Un B(i)) = (\<Union>i\<in>I. A(i)) Un (\<Union>i\<in>I. B(i))"
by blast
lemma INT_Int_distrib:
- "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"
+ "i:I ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
by blast
lemma UN_Int_subset:
- "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))"
+ "(\<Union>z\<in>I Int J. A(z)) <= (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
by blast
(** Devlin, page 12, exercise 5: Complements **)
-lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"
+lemma Diff_UN: "i:I ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
by blast
-lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"
+lemma Diff_INT: "i:I ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
by blast
(** Unions and Intersections with General Sum **)
@@ -541,11 +541,11 @@
by blast
lemma SUM_UN_distrib1:
- "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"
+ "(SUM x:(\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. SUM x:C(y). B(x))"
by blast
lemma SUM_UN_distrib2:
- "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"
+ "(SUM i:I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. SUM i:I. C(i,j))"
by blast
lemma SUM_Un_distrib1:
@@ -573,7 +573,7 @@
by (rule SUM_Int_distrib2)
(*Cf Aczel, Non-Well-Founded Sets, page 115*)
-lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"
+lemma SUM_eq_UN: "(SUM i:I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
by blast
lemma times_subset_iff:
@@ -617,10 +617,10 @@
lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
by blast
-lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"
+lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
by blast
-lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))"
+lemma domain_Union: "domain(Union(A)) = (\<Union>x\<in>A. domain(x))"
by blast
@@ -728,7 +728,7 @@
by blast
(** The Union of a set of relations is a relation -- Lemma for fun_Union **)
-lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>
+lemma rel_Union: "(\<forall>x\<in>S. EX A B. x <= A*B) ==>
Union(S) <= domain(Union(S)) * range(Union(S))"
by blast
@@ -745,7 +745,7 @@
subsection{*Image of a Set under a Function or Relation*}
-lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
+lemma image_iff: "b : r``A <-> (\<exists>x\<in>A. <x,b>:r)"
by (unfold image_def, blast)
lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
@@ -791,7 +791,7 @@
subsection{*Inverse Image of a Set under a Function or Relation*}
lemma vimage_iff:
- "a : r-``B <-> (EX y:B. <a,y>:r)"
+ "a : r-``B <-> (\<exists>y\<in>B. <a,y>:r)"
by (unfold vimage_def image_def converse_def, blast)
lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
@@ -820,7 +820,7 @@
by blast
(*NOT suitable for rewriting*)
-lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})"
+lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
by blast
lemma function_vimage_Int:
@@ -863,12 +863,12 @@
lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
by blast
-lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"
+lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
by blast
(*Unfolding Inter avoids using excluded middle on A=0*)
lemma converse_INT [simp]:
- "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))"
+ "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
apply (unfold Inter_def, blast)
done
@@ -887,7 +887,7 @@
lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)"
by blast
-lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"
+lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) <= Pow(\<Union>x\<in>A. B(x))"
by blast
lemma subset_Pow_Union: "A <= Pow(Union(A))"
@@ -899,7 +899,7 @@
lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
by blast
-lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
+lemma Pow_INT_eq: "x:A ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
by blast
--- a/src/ZF/ex/Limit.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/ex/Limit.thy Tue Oct 01 13:26:10 2002 +0200
@@ -1139,11 +1139,8 @@
apply (assumption | rule cpoI poI)+
apply (simp add: subcpo_rel_eq)
apply (assumption | rule cpo_refl subcpo_subset [THEN subsetD])+
-apply (rotate_tac -3)
apply (simp add: subcpo_rel_eq)
apply (blast intro: subcpo_subset [THEN subsetD] cpo_trans)
-(* Changing the order of the assumptions, otherwise simp doesn't work. *)
-apply (rotate_tac -2)
apply (simp add: subcpo_rel_eq)
apply (blast intro: cpo_antisym subcpo_subset [THEN subsetD])
apply (fast intro: islub_subcpo)
--- a/src/ZF/func.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/func.thy Tue Oct 01 13:26:10 2002 +0200
@@ -261,7 +261,7 @@
done
(*For this lemma and the next, the right-hand side could equivalently
- be written UN x:C. {f`x} *)
+ be written \<Union>x\<in>C. {f`x} *)
lemma image_function:
"[| function(f); C <= domain(f) |] ==> f``C = {f`x. x:C}";
by (simp add: Repfun_function_if)
@@ -505,7 +505,7 @@
by blast
lemma UN_mono:
- "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
+ "[| A<=C; !!x. x:A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) <= (\<Union>x\<in>C. D(x))"
by blast
(*Intersection is ANTI-monotonic. There are TWO premises! *)