Numerous cosmetic changes, prompted by the new simplifier
authorpaulson
Tue Oct 01 13:26:10 2002 +0200 (2002-10-01)
changeset 13615449a70d88b38
parent 13614 0b91269c0b13
child 13616 7316f30c37b2
Numerous cosmetic changes, prompted by the new simplifier
src/ZF/ArithSimp.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/InfDatatype.thy
src/ZF/Integ/EquivClass.thy
src/ZF/Integ/IntDiv.thy
src/ZF/List.thy
src/ZF/OrdQuant.thy
src/ZF/Order.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/equalities.thy
src/ZF/ex/Limit.thy
src/ZF/func.thy
     1.1 --- a/src/ZF/ArithSimp.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/ArithSimp.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -514,14 +514,13 @@
     1.4        (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
     1.5  apply (case_tac "a < b")
     1.6   apply (force simp add: nat_lt_imp_diff_eq_0)
     1.7 -apply (rule iffI, simp_all) 
     1.8 - apply clarify 
     1.9 - apply (rotate_tac -1) 
    1.10 - apply simp 
    1.11 +apply (rule iffI, force) 
    1.12 +apply simp 
    1.13  apply (drule_tac x="a#-b" in bspec)
    1.14  apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) 
    1.15  done
    1.16  
    1.17 +
    1.18  ML
    1.19  {*
    1.20  val diff_self_eq_0 = thm "diff_self_eq_0";
     2.1 --- a/src/ZF/Cardinal.thy	Tue Oct 01 11:17:25 2002 +0200
     2.2 +++ b/src/ZF/Cardinal.thy	Tue Oct 01 13:26:10 2002 +0200
     2.3 @@ -917,8 +917,7 @@
     2.4  apply (erule Finite_induct, auto)
     2.5  apply (case_tac "x:A")
     2.6   apply (subgoal_tac [2] "A-cons (x, B) = A - B")
     2.7 -apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}")
     2.8 -apply (rotate_tac -1, simp)
     2.9 +apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
    2.10  apply (drule Diff_sing_Finite, auto)
    2.11  done
    2.12  
     3.1 --- a/src/ZF/CardinalArith.thy	Tue Oct 01 11:17:25 2002 +0200
     3.2 +++ b/src/ZF/CardinalArith.thy	Tue Oct 01 13:26:10 2002 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4      be a cardinal*)
     3.5    jump_cardinal :: "i=>i"
     3.6      "jump_cardinal(K) ==   
     3.7 -         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
     3.8 +         \<Union>X\<in>Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
     3.9    
    3.10    (*needed because jump_cardinal(K) might not be the successor of K*)
    3.11    csucc         :: "i=>i"
    3.12 @@ -55,11 +55,11 @@
    3.13  done
    3.14  
    3.15  lemma Card_UN:
    3.16 -     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 
    3.17 +     "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x\<in>A. K(x))" 
    3.18  by (blast intro: Card_Union) 
    3.19  
    3.20  lemma Card_OUN [simp,intro,TC]:
    3.21 -     "(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))"
    3.22 +     "(!!x. x:A ==> Card(K(x))) ==> Card(\<Union>x<A. K(x))"
    3.23  by (simp add: OUnion_def Card_0) 
    3.24  
    3.25  lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
    3.26 @@ -850,16 +850,15 @@
    3.27  lemma Finite_Diff_sing_eq_diff_1: "[| Finite(A); x:A |] ==> |A-{x}| = |A| #- 1"
    3.28  apply (rule succ_inject)
    3.29  apply (rule_tac b = "|A|" in trans)
    3.30 -apply (simp add: Finite_imp_succ_cardinal_Diff)
    3.31 + apply (simp add: Finite_imp_succ_cardinal_Diff)
    3.32  apply (subgoal_tac "1 \<lesssim> A")
    3.33   prefer 2 apply (blast intro: not_0_is_lepoll_1)
    3.34  apply (frule Finite_imp_well_ord, clarify)
    3.35 -apply (rotate_tac -1)
    3.36  apply (drule well_ord_lepoll_imp_Card_le)
    3.37 -apply (auto simp add: cardinal_1)
    3.38 + apply (auto simp add: cardinal_1)
    3.39  apply (rule trans)
    3.40 -apply (rule_tac [2] diff_succ)
    3.41 -apply (auto simp add: Finite_cardinal_in_nat)
    3.42 + apply (rule_tac [2] diff_succ)
    3.43 +  apply (auto simp add: Finite_cardinal_in_nat)
    3.44  done
    3.45  
    3.46  lemma cardinal_lt_imp_Diff_not_0 [rule_format]:
     4.1 --- a/src/ZF/Cardinal_AC.thy	Tue Oct 01 11:17:25 2002 +0200
     4.2 +++ b/src/ZF/Cardinal_AC.thy	Tue Oct 01 13:26:10 2002 +0200
     4.3 @@ -28,10 +28,10 @@
     4.4  lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
     4.5  by (blast intro: cardinal_cong cardinal_eqE)
     4.6  
     4.7 -lemma cardinal_disjoint_Un: "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==>  
     4.8 -          |A Un C| = |B Un D|"
     4.9 -apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
    4.10 -done
    4.11 +lemma cardinal_disjoint_Un:
    4.12 +     "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] 
    4.13 +      ==> |A Un C| = |B Un D|"
    4.14 +by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
    4.15  
    4.16  lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
    4.17  apply (rule AC_well_ord [THEN exE])
    4.18 @@ -85,7 +85,8 @@
    4.19  apply (erule CollectE)
    4.20  apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
    4.21  apply (fast elim!: apply_Pair)
    4.22 -apply (blast dest: apply_type Pi_memberD intro: apply_equality Pi_type f_imp_injective)
    4.23 +apply (blast dest: apply_type Pi_memberD 
    4.24 +             intro: apply_equality Pi_type f_imp_injective)
    4.25  done
    4.26  
    4.27  (*Kunen's Lemma 10.20*)
    4.28 @@ -97,7 +98,8 @@
    4.29  done
    4.30  
    4.31  (*Kunen's Lemma 10.21*)
    4.32 -lemma cardinal_UN_le: "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"
    4.33 +lemma cardinal_UN_le:
    4.34 +     "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
    4.35  apply (simp add: InfCard_is_Card le_Card_iff)
    4.36  apply (rule lepoll_trans)
    4.37   prefer 2
    4.38 @@ -108,7 +110,8 @@
    4.39  apply (erule AC_ball_Pi [THEN exE])
    4.40  apply (rule exI)
    4.41  (*Lemma needed in both subgoals, for a fixed z*)
    4.42 -apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K")
    4.43 +apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) & 
    4.44 +                    (LEAST i. z:X (i)) : K")
    4.45   prefer 2
    4.46   apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
    4.47               elim!: LeastI Ord_in_Ord)
    4.48 @@ -121,15 +124,14 @@
    4.49  (*The same again, using csucc*)
    4.50  lemma cardinal_UN_lt_csucc:
    4.51       "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
    4.52 -      ==> |UN i:K. X(i)| < csucc(K)"
    4.53 -apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
    4.54 -done
    4.55 +      ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
    4.56 +by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
    4.57  
    4.58  (*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
    4.59    the least ordinal j such that i:Vfrom(A,j). *)
    4.60  lemma cardinal_UN_Ord_lt_csucc:
    4.61       "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
    4.62 -      ==> (UN i:K. j(i)) < csucc(K)"
    4.63 +      ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
    4.64  apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
    4.65  apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
    4.66  apply (blast intro!: Ord_UN elim: ltE)
    4.67 @@ -144,7 +146,7 @@
    4.68  (*Work backwards along the injection from W into K, given that W~=0.*)
    4.69  lemma inj_UN_subset:
    4.70       "[| f: inj(A,B);  a:A |] ==>            
    4.71 -      (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"
    4.72 +      (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
    4.73  apply (rule UN_least)
    4.74  apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
    4.75   apply (simp add: inj_is_fun [THEN apply_rangeI])
    4.76 @@ -155,7 +157,7 @@
    4.77    be weaker.*)
    4.78  lemma le_UN_Ord_lt_csucc:
    4.79       "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
    4.80 -      ==> (UN w:W. j(w)) < csucc(K)"
    4.81 +      ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
    4.82  apply (case_tac "W=0")
    4.83  (*solve the easy 0 case*)
    4.84   apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] 
     5.1 --- a/src/ZF/Constructible/AC_in_L.thy	Tue Oct 01 11:17:25 2002 +0200
     5.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Tue Oct 01 13:26:10 2002 +0200
     5.3 @@ -240,7 +240,6 @@
     5.4   apply safe
     5.5   apply (subgoal_tac "Ord(y)")
     5.6    prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
     5.7 - apply (rotate_tac -1) 
     5.8   apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
     5.9                        Ord_mem_iff_lt) 
    5.10   apply (blast intro: lt_trans) 
     6.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 01 11:17:25 2002 +0200
     6.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 01 13:26:10 2002 +0200
     6.3 @@ -683,10 +683,8 @@
     6.4       Ord(i);  M(i);  M(z);
     6.5       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
     6.6     ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
     6.7 -apply (rotate_tac 2) 
     6.8 -apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
     6.9 +by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
    6.10         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    6.11 -done
    6.12  
    6.13  
    6.14  theorem (in M_eclose) transrec_closed:
    6.15 @@ -694,10 +692,9 @@
    6.16  	Ord(i);  M(i);  
    6.17  	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    6.18        ==> M(transrec(i,H))"
    6.19 -apply (rotate_tac 2) 
    6.20 -apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    6.21 -       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    6.22 -done
    6.23 +by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    6.24 +        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    6.25 +
    6.26  
    6.27  text{*Helps to prove instances of @{term transrec_replacement}*}
    6.28  lemma (in M_eclose) transrec_replacementI: 
     7.1 --- a/src/ZF/Constructible/Relative.thy	Tue Oct 01 11:17:25 2002 +0200
     7.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Oct 01 13:26:10 2002 +0200
     7.3 @@ -1203,7 +1203,6 @@
     7.4  lemma (in M_basic) restriction_is_function: 
     7.5       "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
     7.6        ==> function(z)"
     7.7 -apply (rotate_tac 1)
     7.8  apply (simp add: restriction_def ball_iff_equiv) 
     7.9  apply (unfold function_def, blast) 
    7.10  done
     8.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Oct 01 11:17:25 2002 +0200
     8.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Oct 01 13:26:10 2002 +0200
     8.3 @@ -225,7 +225,6 @@
     8.4  
     8.5  lemma (in M_trancl) wellfounded_trancl:
     8.6       "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)"
     8.7 -apply (rotate_tac -1)
     8.8  apply (simp add: wellfounded_iff_wellfounded_on_field)
     8.9  apply (rule wellfounded_on_subset_A, erule wellfounded_on_trancl)
    8.10     apply blast
     9.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Oct 01 11:17:25 2002 +0200
     9.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Oct 01 13:26:10 2002 +0200
     9.3 @@ -143,7 +143,7 @@
     9.4     apply (drule equalityD1 [THEN subsetD], assumption) 
     9.5     apply (blast dest: pair_components_in_M) 
     9.6    apply (blast elim!: equalityE dest: pair_components_in_M)
     9.7 - apply (frule transM, assumption, rotate_tac -1) 
     9.8 + apply (frule transM, assumption) 
     9.9   apply simp  
    9.10   apply blast
    9.11  apply (subgoal_tac "is_function(M,f)")
    9.12 @@ -187,7 +187,6 @@
    9.13  apply (frule pair_components_in_M, assumption, clarify) 
    9.14  apply (rule iffI)
    9.15   apply (frule_tac y="<y,z>" in transM, assumption)
    9.16 - apply (rotate_tac -1)   
    9.17   apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
    9.18  			   apply_recfun is_recfun_cut) 
    9.19  txt{*Opposite inclusion: something in f, show in Y*}
    9.20 @@ -320,9 +319,7 @@
    9.21       relativize2(M,MH,H);  M(r)|] 
    9.22     ==> strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    9.23                  pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
    9.24 -apply (rotate_tac 1) 
    9.25 -apply (simp add: wfrec_replacement_def is_wfrec_abs) 
    9.26 -done
    9.27 +by (simp add: wfrec_replacement_def is_wfrec_abs) 
    9.28  
    9.29  lemma wfrec_replacement_cong [cong]:
    9.30       "[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z);
    10.1 --- a/src/ZF/Constructible/Wellorderings.thy	Tue Oct 01 11:17:25 2002 +0200
    10.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Oct 01 13:26:10 2002 +0200
    10.3 @@ -381,7 +381,7 @@
    10.4  apply (rule iffI) 
    10.5   prefer 2 apply blast 
    10.6  apply (rule equalityI) 
    10.7 - apply (clarify, frule transM, assumption, rotate_tac -1, simp) 
    10.8 + apply (clarify, frule transM, assumption, simp) 
    10.9  apply (clarify, frule transM, assumption, force)
   10.10  done
   10.11  
   10.12 @@ -392,7 +392,6 @@
   10.13        ==> z \<in> f <->
   10.14        (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
   10.15                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   10.16 -apply (rotate_tac 1) 
   10.17  apply (simp add: omap_def Memrel_closed pred_closed) 
   10.18  apply (rule iffI)
   10.19   apply (drule_tac [2] x=z in rspec)
   10.20 @@ -432,7 +431,6 @@
   10.21  
   10.22  lemma (in M_basic) Ord_otype:
   10.23       "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
   10.24 -apply (rotate_tac 1) 
   10.25  apply (rule OrdI) 
   10.26  prefer 2 
   10.27      apply (simp add: Ord_def otype_def omap_def) 
   10.28 @@ -454,7 +452,6 @@
   10.29  lemma (in M_basic) domain_omap:
   10.30       "[| omap(M,A,r,f);  obase(M,A,r,B); M(A); M(r); M(B); M(f) |] 
   10.31        ==> domain(f) = B"
   10.32 -apply (rotate_tac 2) 
   10.33  apply (simp add: domain_closed obase_iff) 
   10.34  apply (rule equality_iffI) 
   10.35  apply (simp add: domain_iff omap_iff, blast) 
   10.36 @@ -463,7 +460,7 @@
   10.37  lemma (in M_basic) omap_subset: 
   10.38       "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   10.39         M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
   10.40 -apply (rotate_tac 3, clarify) 
   10.41 +apply clarify 
   10.42  apply (simp add: omap_iff obase_iff) 
   10.43  apply (force simp add: otype_iff) 
   10.44  done
   10.45 @@ -471,7 +468,6 @@
   10.46  lemma (in M_basic) omap_funtype: 
   10.47       "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   10.48         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
   10.49 -apply (rotate_tac 3) 
   10.50  apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
   10.51  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   10.52  done
   10.53 @@ -519,7 +515,6 @@
   10.54  apply (rule OrdI) 
   10.55  	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
   10.56  txt{*Hard part is to show that the image is a transitive set.*}
   10.57 -apply (rotate_tac 3)
   10.58  apply (simp add: Transset_def, clarify) 
   10.59  apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
   10.60  apply (rename_tac c j, clarify)
   10.61 @@ -552,7 +547,6 @@
   10.62  lemma (in M_basic) obase_equals: 
   10.63       "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
   10.64         M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
   10.65 -apply (rotate_tac 4)
   10.66  apply (rule equalityI, force simp add: obase_iff, clarify) 
   10.67  apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
   10.68  apply (frule wellordered_is_wellfounded_on, assumption)
    11.1 --- a/src/ZF/Epsilon.thy	Tue Oct 01 11:17:25 2002 +0200
    11.2 +++ b/src/ZF/Epsilon.thy	Tue Oct 01 13:26:10 2002 +0200
    11.3 @@ -11,13 +11,13 @@
    11.4  
    11.5  constdefs
    11.6    eclose    :: "i=>i"
    11.7 -    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    11.8 +    "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))"
    11.9  
   11.10    transrec  :: "[i, [i,i]=>i] =>i"
   11.11      "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
   11.12   
   11.13    rank      :: "i=>i"
   11.14 -    "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
   11.15 +    "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
   11.16  
   11.17    transrec2 :: "[i, i, [i,i]=>i] =>i"
   11.18      "transrec2(k, a, b) ==                     
   11.19 @@ -25,7 +25,7 @@
   11.20                  %i r. if(i=0, a, 
   11.21                          if(EX j. i=succ(j),        
   11.22                             b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
   11.23 -                           UN j<i. r`j)))"
   11.24 +                           \<Union>j<i. r`j)))"
   11.25  
   11.26    recursor  :: "[i, [i,i]=>i, i]=>i"
   11.27      "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
   11.28 @@ -216,7 +216,7 @@
   11.29  subsection{*Rank*}
   11.30  
   11.31  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   11.32 -lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
   11.33 +lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))"
   11.34  by (subst rank_def [THEN def_transrec], simp)
   11.35  
   11.36  lemma Ord_rank [simp]: "Ord(rank(a))"
   11.37 @@ -268,7 +268,7 @@
   11.38  apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
   11.39  done
   11.40  
   11.41 -lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
   11.42 +lemma rank_Union: "rank(Union(A)) = (\<Union>x\<in>A. rank(x))"
   11.43  apply (rule equalityI)
   11.44  apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
   11.45  apply (erule_tac [2] Union_upper)
   11.46 @@ -350,7 +350,7 @@
   11.47  done
   11.48  
   11.49  lemma transrec2_Limit:
   11.50 -     "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
   11.51 +     "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
   11.52  apply (rule transrec2_def [THEN def_transrec, THEN trans])
   11.53  apply (auto simp add: OUnion_def) 
   11.54  done
   11.55 @@ -359,7 +359,7 @@
   11.56       "(!!x. f(x)==transrec2(x,a,b))
   11.57        ==> f(0) = a & 
   11.58            f(succ(i)) = b(i, f(i)) & 
   11.59 -          (Limit(K) --> f(K) = (UN j<K. f(j)))"
   11.60 +          (Limit(K) --> f(K) = (\<Union>j<K. f(j)))"
   11.61  by (simp add: transrec2_Limit)
   11.62  
   11.63  
    12.1 --- a/src/ZF/Finite.thy	Tue Oct 01 11:17:25 2002 +0200
    12.2 +++ b/src/ZF/Finite.thy	Tue Oct 01 13:26:10 2002 +0200
    12.3 @@ -172,7 +172,6 @@
    12.4  apply (erule Fin.induct)
    12.5   apply (simp add: FiniteFun.intros, clarify)
    12.6  apply (case_tac "a:b")
    12.7 - apply (rotate_tac -1)
    12.8   apply (simp add: cons_absorb)
    12.9  apply (subgoal_tac "restrict (f,b) : b -||> B")
   12.10   prefer 2 apply (blast intro: restrict_type2)
    13.1 --- a/src/ZF/InfDatatype.thy	Tue Oct 01 11:17:25 2002 +0200
    13.2 +++ b/src/ZF/InfDatatype.thy	Tue Oct 01 13:26:10 2002 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4  lemma fun_Vcsucc_lemma:
    13.5       "[| f: D -> Vfrom(A,csucc(K));  |D| le K;  InfCard(K) |]   
    13.6        ==> EX j. f: D -> Vfrom(A,j) & j < csucc(K)"
    13.7 -apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
    13.8 +apply (rule_tac x = "\<Union>d\<in>D. LEAST i. f`d : Vfrom (A,i) " in exI)
    13.9  apply (rule conjI)
   13.10  apply (rule_tac [2] le_UN_Ord_lt_csucc) 
   13.11  apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all) 
    14.1 --- a/src/ZF/Integ/EquivClass.thy	Tue Oct 01 11:17:25 2002 +0200
    14.2 +++ b/src/ZF/Integ/EquivClass.thy	Tue Oct 01 13:26:10 2002 +0200
    14.3 @@ -149,18 +149,15 @@
    14.4       ==> X=Y"
    14.5  apply (unfold quotient_def, safe)
    14.6  apply (rule equiv_class_eq, assumption)
    14.7 -apply (rotate_tac -2) 
    14.8  apply (simp add: UN_equiv_class [of A r b])  
    14.9  done
   14.10  
   14.11  
   14.12  subsection{*Defining Binary Operations upon Equivalence Classes*}
   14.13  
   14.14 -
   14.15  lemma congruent2_implies_congruent:
   14.16      "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))"
   14.17 -apply (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   14.18 -done
   14.19 +by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   14.20  
   14.21  lemma congruent2_implies_congruent_UN:
   14.22      "[| equiv(A,r);  congruent2(r,b);  a: A |] ==>
    15.1 --- a/src/ZF/Integ/IntDiv.thy	Tue Oct 01 11:17:25 2002 +0200
    15.2 +++ b/src/ZF/Integ/IntDiv.thy	Tue Oct 01 13:26:10 2002 +0200
    15.3 @@ -658,18 +658,16 @@
    15.4  
    15.5  (*the case a=0*)
    15.6  lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
    15.7 -apply (rotate_tac -1)
    15.8 -apply (auto simp add: quorem_def neq_iff_zless)
    15.9 -done
   15.10 +by (force simp add: quorem_def neq_iff_zless)
   15.11  
   15.12  lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
   15.13  apply (subst posDivAlg_unfold)
   15.14 -apply (simp (no_asm))
   15.15 +apply simp
   15.16  done
   15.17  
   15.18  lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
   15.19  apply (subst posDivAlg_unfold)
   15.20 -apply (simp (no_asm) add: not_zle_iff_zless)
   15.21 +apply (simp add: not_zle_iff_zless)
   15.22  done
   15.23  
   15.24  
   15.25 @@ -710,7 +708,6 @@
   15.26  
   15.27  lemma divAlg_correct:
   15.28       "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
   15.29 -apply (rotate_tac 1)
   15.30  apply (auto simp add: quorem_0 divAlg_def)
   15.31  apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
   15.32                      posDivAlg_type negDivAlg_type) 
   15.33 @@ -810,7 +807,6 @@
   15.34       "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]  
   15.35        ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
   15.36  apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
   15.37 -apply (rotate_tac 1)
   15.38  apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound 
   15.39                        neg_mod_sign neg_mod_bound)
   15.40  done
    16.1 --- a/src/ZF/List.thy	Tue Oct 01 11:17:25 2002 +0200
    16.2 +++ b/src/ZF/List.thy	Tue Oct 01 13:26:10 2002 +0200
    16.3 @@ -721,8 +721,7 @@
    16.4  apply (induct_tac "m", auto)
    16.5  apply (erule_tac a = xs in list.cases)
    16.6  apply (auto simp add: take_Nil)
    16.7 -apply (rotate_tac 1)
    16.8 -apply (erule natE)
    16.9 +apply (erule_tac n=n in natE)
   16.10  apply (auto intro: take_0 take_type)
   16.11  done
   16.12  
    17.1 --- a/src/ZF/OrdQuant.thy	Tue Oct 01 11:17:25 2002 +0200
    17.2 +++ b/src/ZF/OrdQuant.thy	Tue Oct 01 13:26:10 2002 +0200
    17.3 @@ -20,7 +20,7 @@
    17.4  
    17.5    (* Ordinal Union *)
    17.6    OUnion :: "[i, i => i] => i"
    17.7 -    "OUnion(i,B) == {z: UN x:i. B(x). Ord(i)}"
    17.8 +    "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
    17.9  
   17.10  syntax
   17.11    "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
   17.12 @@ -77,31 +77,31 @@
   17.13  apply (auto simp add: lt_def)
   17.14  done
   17.15  
   17.16 -lemma Limit_OUN_eq: "Limit(i) ==> (UN x<i. x) = i"
   17.17 +lemma Limit_OUN_eq: "Limit(i) ==> (\<Union>x<i. x) = i"
   17.18  by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)
   17.19  
   17.20 -(* No < version; consider (UN i:nat.i)=nat *)
   17.21 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
   17.22  lemma OUN_least:
   17.23 -     "(!!x. x<A ==> B(x) \<subseteq> C) ==> (UN x<A. B(x)) \<subseteq> C"
   17.24 +     "(!!x. x<A ==> B(x) \<subseteq> C) ==> (\<Union>x<A. B(x)) \<subseteq> C"
   17.25  by (simp add: OUnion_def UN_least ltI)
   17.26  
   17.27 -(* No < version; consider (UN i:nat.i)=nat *)
   17.28 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
   17.29  lemma OUN_least_le:
   17.30 -     "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (UN x<A. b(x)) \<le> i"
   17.31 +     "[| Ord(i);  !!x. x<A ==> b(x) \<le> i |] ==> (\<Union>x<A. b(x)) \<le> i"
   17.32  by (simp add: OUnion_def UN_least_le ltI Ord_0_le)
   17.33  
   17.34  lemma le_implies_OUN_le_OUN:
   17.35 -     "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (UN x<A. c(x)) \<le> (UN x<A. d(x))"
   17.36 +     "[| !!x. x<A ==> c(x) \<le> d(x) |] ==> (\<Union>x<A. c(x)) \<le> (\<Union>x<A. d(x))"
   17.37  by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)
   17.38  
   17.39  lemma OUN_UN_eq:
   17.40       "(!!x. x:A ==> Ord(B(x)))
   17.41 -      ==> (UN z < (UN x:A. B(x)). C(z)) = (UN  x:A. UN z < B(x). C(z))"
   17.42 +      ==> (\<Union>z < (\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z < B(x). C(z))"
   17.43  by (simp add: OUnion_def)
   17.44  
   17.45  lemma OUN_Union_eq:
   17.46       "(!!x. x:X ==> Ord(x))
   17.47 -      ==> (UN z < Union(X). C(z)) = (UN x:X. UN z < x. C(z))"
   17.48 +      ==> (\<Union>z < Union(X). C(z)) = (\<Union>x\<in>X. \<Union>z < x. C(z))"
   17.49  by (simp add: OUnion_def)
   17.50  
   17.51  (*So that rule_format will get rid of ALL x<A...*)
   17.52 @@ -165,19 +165,19 @@
   17.53  
   17.54  subsubsection {*Rules for Ordinal-Indexed Unions*}
   17.55  
   17.56 -lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (UN z<i. B(z))"
   17.57 +lemma OUN_I [intro]: "[| a<i;  b: B(a) |] ==> b: (\<Union>z<i. B(z))"
   17.58  by (unfold OUnion_def lt_def, blast)
   17.59  
   17.60  lemma OUN_E [elim!]:
   17.61 -    "[| b : (UN z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   17.62 +    "[| b : (\<Union>z<i. B(z));  !!a.[| b: B(a);  a<i |] ==> R |] ==> R"
   17.63  apply (unfold OUnion_def lt_def, blast)
   17.64  done
   17.65  
   17.66 -lemma OUN_iff: "b : (UN x<i. B(x)) <-> (EX x<i. b : B(x))"
   17.67 +lemma OUN_iff: "b : (\<Union>x<i. B(x)) <-> (EX x<i. b : B(x))"
   17.68  by (unfold OUnion_def oex_def lt_def, blast)
   17.69  
   17.70  lemma OUN_cong [cong]:
   17.71 -    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
   17.72 +    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (\<Union>x<i. C(x)) = (\<Union>x<j. D(x))"
   17.73  by (simp add: OUnion_def lt_def OUN_iff)
   17.74  
   17.75  lemma lt_induct:
    18.1 --- a/src/ZF/Order.thy	Tue Oct 01 11:17:25 2002 +0200
    18.2 +++ b/src/ZF/Order.thy	Tue Oct 01 13:26:10 2002 +0200
    18.3 @@ -38,7 +38,7 @@
    18.4  
    18.5    ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)
    18.6     "ord_iso_map(A,r,B,s) ==
    18.7 -     UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
    18.8 +     \<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>}"
    18.9  
   18.10    first :: "[i, i, i] => o"
   18.11      "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
    19.1 --- a/src/ZF/OrderType.thy	Tue Oct 01 11:17:25 2002 +0200
    19.2 +++ b/src/ZF/OrderType.thy	Tue Oct 01 13:26:10 2002 +0200
    19.3 @@ -567,7 +567,7 @@
    19.4  apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
    19.5  done
    19.6  
    19.7 -lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"
    19.8 +lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
    19.9  apply (rule subsetI [THEN equalityI])
   19.10  apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
   19.11  apply (blast intro: Ord_oadd) 
   19.12 @@ -592,12 +592,12 @@
   19.13  
   19.14  lemma oadd_UN:
   19.15       "[| !!x. x:A ==> Ord(j(x));  a:A |]
   19.16 -      ==> i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"
   19.17 +      ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
   19.18  by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD] 
   19.19                   oadd_lt_mono2 [THEN ltD] 
   19.20            elim!: ltE dest!: ltI [THEN lt_oadd_disj])
   19.21  
   19.22 -lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)"
   19.23 +lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
   19.24  apply (frule Limit_has_0 [THEN ltD])
   19.25  apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] 
   19.26                   Union_eq_UN [symmetric] Limit_Union_eq)
   19.27 @@ -818,7 +818,7 @@
   19.28  done
   19.29  
   19.30  lemma omult_unfold:
   19.31 -     "[| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"
   19.32 +     "[| Ord(i);  Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
   19.33  apply (rule subsetI [THEN equalityI])
   19.34  apply (rule lt_omult [THEN exE])
   19.35  apply (erule_tac [3] ltI)
   19.36 @@ -901,10 +901,10 @@
   19.37  
   19.38  lemma omult_UN: 
   19.39       "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |]
   19.40 -      ==> i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"
   19.41 +      ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
   19.42  by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
   19.43  
   19.44 -lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)"
   19.45 +lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
   19.46  by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric] 
   19.47                Union_eq_UN [symmetric] Limit_Union_eq)
   19.48  
    20.1 --- a/src/ZF/Ordinal.thy	Tue Oct 01 11:17:25 2002 +0200
    20.2 +++ b/src/ZF/Ordinal.thy	Tue Oct 01 13:26:10 2002 +0200
    20.3 @@ -102,11 +102,11 @@
    20.4  by (unfold Inter_def Transset_def, blast)
    20.5  
    20.6  lemma Transset_UN:
    20.7 -     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (UN x:A. B(x))"
    20.8 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Union>x\<in>A. B(x))"
    20.9  by (rule Transset_Union_family, auto) 
   20.10  
   20.11  lemma Transset_INT:
   20.12 -     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (INT x:A. B(x))"
   20.13 +     "(!!x. x \<in> A ==> Transset(B(x))) ==> Transset (\<Inter>x\<in>A. B(x))"
   20.14  by (rule Transset_Inter_family, auto) 
   20.15  
   20.16  
   20.17 @@ -555,7 +555,7 @@
   20.18  done
   20.19  
   20.20  lemma Ord_UN [intro,simp,TC]:
   20.21 -     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(UN x:A. B(x))"
   20.22 +     "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Union>x\<in>A. B(x))"
   20.23  by (rule Ord_Union, blast)
   20.24  
   20.25  lemma Ord_Inter [intro,simp,TC]:
   20.26 @@ -567,19 +567,19 @@
   20.27  done
   20.28  
   20.29  lemma Ord_INT [intro,simp,TC]:
   20.30 -    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(INT x:A. B(x))"
   20.31 +    "[| !!x. x:A ==> Ord(B(x)) |] ==> Ord(\<Inter>x\<in>A. B(x))"
   20.32  by (rule Ord_Inter, blast) 
   20.33  
   20.34  
   20.35 -(* No < version; consider (UN i:nat.i)=nat *)
   20.36 +(* No < version; consider (\<Union>i\<in>nat.i)=nat *)
   20.37  lemma UN_least_le:
   20.38 -    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (UN x:A. b(x)) le i"
   20.39 +    "[| Ord(i);  !!x. x:A ==> b(x) le i |] ==> (\<Union>x\<in>A. b(x)) le i"
   20.40  apply (rule le_imp_subset [THEN UN_least, THEN subset_imp_le])
   20.41  apply (blast intro: Ord_UN elim: ltE)+
   20.42  done
   20.43  
   20.44  lemma UN_succ_least_lt:
   20.45 -    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (UN x:A. succ(b(x))) < i"
   20.46 +    "[| j<i;  !!x. x:A ==> b(x)<j |] ==> (\<Union>x\<in>A. succ(b(x))) < i"
   20.47  apply (rule ltE, assumption)
   20.48  apply (rule UN_least_le [THEN lt_trans2])
   20.49  apply (blast intro: succ_leI)+
   20.50 @@ -590,7 +590,7 @@
   20.51  by (unfold lt_def, blast) 
   20.52  
   20.53  lemma UN_upper_le:
   20.54 -     "[| a: A;  i le b(a);  Ord(UN x:A. b(x)) |] ==> i le (UN x:A. b(x))"
   20.55 +     "[| a: A;  i le b(a);  Ord(\<Union>x\<in>A. b(x)) |] ==> i le (\<Union>x\<in>A. b(x))"
   20.56  apply (frule ltD)
   20.57  apply (rule le_imp_subset [THEN subset_trans, THEN subset_imp_le])
   20.58  apply (blast intro: lt_Ord UN_upper)+
   20.59 @@ -606,13 +606,13 @@
   20.60  done
   20.61  
   20.62  lemma le_implies_UN_le_UN:
   20.63 -    "[| !!x. x:A ==> c(x) le d(x) |] ==> (UN x:A. c(x)) le (UN x:A. d(x))"
   20.64 +    "[| !!x. x:A ==> c(x) le d(x) |] ==> (\<Union>x\<in>A. c(x)) le (\<Union>x\<in>A. d(x))"
   20.65  apply (rule UN_least_le)
   20.66  apply (rule_tac [2] UN_upper_le)
   20.67  apply (blast intro: Ord_UN le_Ord2)+ 
   20.68  done
   20.69  
   20.70 -lemma Ord_equality: "Ord(i) ==> (UN y:i. succ(y)) = i"
   20.71 +lemma Ord_equality: "Ord(i) ==> (\<Union>y\<in>i. succ(y)) = i"
   20.72  by (blast intro: Ord_trans)
   20.73  
   20.74  (*Holds for all transitive sets, not just ordinals*)
    21.1 --- a/src/ZF/QPair.thy	Tue Oct 01 11:17:25 2002 +0200
    21.2 +++ b/src/ZF/QPair.thy	Tue Oct 01 13:26:10 2002 +0200
    21.3 @@ -38,7 +38,7 @@
    21.4      "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
    21.5  
    21.6    QSigma    :: "[i, i => i] => i"
    21.7 -    "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
    21.8 +    "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
    21.9  
   21.10  syntax
   21.11    "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    22.1 --- a/src/ZF/QUniv.thy	Tue Oct 01 11:17:25 2002 +0200
    22.2 +++ b/src/ZF/QUniv.thy	Tue Oct 01 13:26:10 2002 +0200
    22.3 @@ -189,7 +189,7 @@
    22.4       subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
    22.5  
    22.6  lemma QPair_Int_Vset_subset_UN:
    22.7 -     "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
    22.8 +     "Ord(i) ==> <a;b> Int Vset(i) <= (\<Union>j\<in>i. <a Int Vset(j); b Int Vset(j)>)"
    22.9  apply (erule Ord_cases)
   22.10  (*0 case*)
   22.11  apply (simp add: Vfrom_0)
    23.1 --- a/src/ZF/equalities.thy	Tue Oct 01 11:17:25 2002 +0200
    23.2 +++ b/src/ZF/equalities.thy	Tue Oct 01 13:26:10 2002 +0200
    23.3 @@ -62,10 +62,10 @@
    23.4  lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) <-> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
    23.5    by blast
    23.6  
    23.7 -lemma ball_UN: "(\<forall>z \<in> (UN x:A. B(x)). P(z)) <-> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
    23.8 +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))"
    23.9    by blast
   23.10  
   23.11 -lemma bex_UN: "(\<exists>z \<in> (UN x:A. B(x)). P(z)) <-> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))"
   23.12 +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))"
   23.13    by blast
   23.14  
   23.15  subsection{*Converse of a Relation*}
   23.16 @@ -136,7 +136,7 @@
   23.17  lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
   23.18  by blast
   23.19  
   23.20 -lemma equal_singleton [rule_format]: "[| a: C;  ALL y:C. y=b |] ==> C = {b}"
   23.21 +lemma equal_singleton [rule_format]: "[| a: C;  \<forall>y\<in>C. y=b |] ==> C = {b}"
   23.22  by blast
   23.23  
   23.24  lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
   23.25 @@ -354,7 +354,7 @@
   23.26  
   23.27  (** Big Union is the least upper bound of a set  **)
   23.28  
   23.29 -lemma Union_subset_iff: "Union(A) <= C <-> (ALL x:A. x <= C)"
   23.30 +lemma Union_subset_iff: "Union(A) <= C <-> (\<forall>x\<in>A. x <= C)"
   23.31  by blast
   23.32  
   23.33  lemma Union_upper: "B:A ==> B <= Union(A)"
   23.34 @@ -372,15 +372,15 @@
   23.35  lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)"
   23.36  by blast
   23.37  
   23.38 -lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)"
   23.39 +lemma Union_disjoint: "Union(C) Int A = 0 <-> (\<forall>B\<in>C. B Int A = 0)"
   23.40  by (blast elim!: equalityE)
   23.41  
   23.42 -lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)"
   23.43 +lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
   23.44  by blast
   23.45  
   23.46  (** Big Intersection is the greatest lower bound of a nonempty set **)
   23.47  
   23.48 -lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (ALL x:A. C <= x)"
   23.49 +lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
   23.50  by blast
   23.51  
   23.52  lemma Inter_lower: "B:A ==> Inter(A) <= B"
   23.53 @@ -391,11 +391,11 @@
   23.54  
   23.55  (** Intersection of a family of sets  **)
   23.56  
   23.57 -lemma INT_lower: "x:A ==> (INT x:A. B(x)) <= B(x)"
   23.58 +lemma INT_lower: "x:A ==> (\<Inter>x\<in>A. B(x)) <= B(x)"
   23.59  by blast
   23.60  
   23.61  lemma INT_greatest: 
   23.62 -    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
   23.63 +    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (\<Inter>x\<in>A. B(x))"
   23.64  by blast 
   23.65  
   23.66  lemma Inter_0: "Inter(0) = 0"
   23.67 @@ -422,80 +422,80 @@
   23.68  
   23.69  subsection{*Unions and Intersections of Families*}
   23.70  
   23.71 -lemma subset_UN_iff_eq: "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))"
   23.72 +lemma subset_UN_iff_eq: "A <= (\<Union>i\<in>I. B(i)) <-> A = (\<Union>i\<in>I. A Int B(i))"
   23.73  by (blast elim!: equalityE)
   23.74  
   23.75 -lemma UN_subset_iff: "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
   23.76 +lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) <= C <-> (\<forall>x\<in>A. B(x) <= C)"
   23.77  by blast
   23.78  
   23.79 -lemma UN_upper: "x:A ==> B(x) <= (UN x:A. B(x))"
   23.80 +lemma UN_upper: "x:A ==> B(x) <= (\<Union>x\<in>A. B(x))"
   23.81  by (erule RepFunI [THEN Union_upper])
   23.82  
   23.83 -lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
   23.84 +lemma UN_least: "[| !!x. x:A ==> B(x)<=C |] ==> (\<Union>x\<in>A. B(x)) <= C"
   23.85  by blast
   23.86  
   23.87 -lemma Union_eq_UN: "Union(A) = (UN x:A. x)"
   23.88 +lemma Union_eq_UN: "Union(A) = (\<Union>x\<in>A. x)"
   23.89  by blast
   23.90  
   23.91 -lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)"
   23.92 +lemma Inter_eq_INT: "Inter(A) = (\<Inter>x\<in>A. x)"
   23.93  by (unfold Inter_def, blast)
   23.94  
   23.95 -lemma UN_0 [simp]: "(UN i:0. A(i)) = 0"
   23.96 +lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0"
   23.97  by blast
   23.98  
   23.99 -lemma UN_singleton: "(UN x:A. {x}) = A"
  23.100 +lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A"
  23.101  by blast
  23.102  
  23.103 -lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))"
  23.104 +lemma UN_Un: "(\<Union>i\<in> A Un B. C(i)) = (\<Union>i\<in> A. C(i)) Un (\<Union>i\<in>B. C(i))"
  23.105  by blast
  23.106  
  23.107 -lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j)  
  23.108 -                              else if J=0 then INT i:I. A(i)  
  23.109 -                              else ((INT i:I. A(i)) Int  (INT j:J. A(j))))"
  23.110 +lemma INT_Un: "(\<Inter>i\<in>I Un J. A(i)) = (if I=0 then \<Inter>j\<in>J. A(j)  
  23.111 +                              else if J=0 then \<Inter>i\<in>I. A(i)  
  23.112 +                              else ((\<Inter>i\<in>I. A(i)) Int  (\<Inter>j\<in>J. A(j))))"
  23.113  apply simp
  23.114  apply (blast intro!: equalityI)
  23.115  done
  23.116  
  23.117 -lemma UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))"
  23.118 +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))"
  23.119  by blast
  23.120  
  23.121  (*Halmos, Naive Set Theory, page 35.*)
  23.122 -lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))"
  23.123 +lemma Int_UN_distrib: "B Int (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B Int A(i))"
  23.124  by blast
  23.125  
  23.126 -lemma Un_INT_distrib: "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))"
  23.127 +lemma Un_INT_distrib: "i:I ==> B Un (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B Un A(i))"
  23.128  by blast
  23.129  
  23.130  lemma Int_UN_distrib2:
  23.131 -     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))"
  23.132 +     "(\<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))"
  23.133  by blast
  23.134  
  23.135  lemma Un_INT_distrib2: "[| i:I;  j:J |] ==>  
  23.136 -      (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))"
  23.137 +      (\<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))"
  23.138  by blast
  23.139  
  23.140 -lemma UN_constant: "a: A ==> (UN y:A. c) = c"
  23.141 +lemma UN_constant: "a: A ==> (\<Union>y\<in>A. c) = c"
  23.142  by blast
  23.143  
  23.144 -lemma INT_constant: "a: A ==> (INT y:A. c) = c"
  23.145 +lemma INT_constant: "a: A ==> (\<Inter>y\<in>A. c) = c"
  23.146  by blast
  23.147  
  23.148 -lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))"
  23.149 +lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))"
  23.150  by blast
  23.151  
  23.152 -lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x))    = (INT a:A. B(f(a)))"
  23.153 +lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x))    = (\<Inter>a\<in>A. B(f(a)))"
  23.154  by (auto simp add: Inter_def)
  23.155  
  23.156  lemma INT_Union_eq:
  23.157 -     "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))"
  23.158 -apply (simp add: Inter_def)
  23.159 -apply (subgoal_tac "ALL x:A. x~=0")
  23.160 -prefer 2 apply blast
  23.161 -apply (tactic "first_best_tac (claset() addss' simpset()) 1")
  23.162 +     "0 ~: A ==> (\<Inter>x\<in> Union(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))"
  23.163 +apply (subgoal_tac "\<forall>x\<in>A. x~=0")
  23.164 + prefer 2 apply blast
  23.165 +apply (force simp add: Inter_def ball_conj_distrib) 
  23.166  done
  23.167  
  23.168 -lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0)  
  23.169 -      ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))"
  23.170 +lemma INT_UN_eq:
  23.171 +     "(\<forall>x\<in>A. B(x) ~= 0)  
  23.172 +      ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))"
  23.173  apply (subst INT_Union_eq, blast)
  23.174  apply (simp add: Inter_def)
  23.175  done
  23.176 @@ -505,23 +505,23 @@
  23.177      Union of a family of unions **)
  23.178  
  23.179  lemma UN_Un_distrib:
  23.180 -     "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))"
  23.181 +     "(\<Union>i\<in>I. A(i) Un B(i)) = (\<Union>i\<in>I. A(i))  Un  (\<Union>i\<in>I. B(i))"
  23.182  by blast
  23.183  
  23.184  lemma INT_Int_distrib:
  23.185 -     "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))"
  23.186 +     "i:I ==> (\<Inter>i\<in>I. A(i) Int B(i)) = (\<Inter>i\<in>I. A(i)) Int (\<Inter>i\<in>I. B(i))"
  23.187  by blast
  23.188  
  23.189  lemma UN_Int_subset:
  23.190 -     "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))"
  23.191 +     "(\<Union>z\<in>I Int J. A(z)) <= (\<Union>z\<in>I. A(z)) Int (\<Union>z\<in>J. A(z))"
  23.192  by blast
  23.193  
  23.194  (** Devlin, page 12, exercise 5: Complements **)
  23.195  
  23.196 -lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))"
  23.197 +lemma Diff_UN: "i:I ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))"
  23.198  by blast
  23.199  
  23.200 -lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))"
  23.201 +lemma Diff_INT: "i:I ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))"
  23.202  by blast
  23.203  
  23.204  (** Unions and Intersections with General Sum **)
  23.205 @@ -541,11 +541,11 @@
  23.206  by blast
  23.207  
  23.208  lemma SUM_UN_distrib1:
  23.209 -     "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))"
  23.210 +     "(SUM x:(\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. SUM x:C(y). B(x))"
  23.211  by blast
  23.212  
  23.213  lemma SUM_UN_distrib2:
  23.214 -     "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))"
  23.215 +     "(SUM i:I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. SUM i:I. C(i,j))"
  23.216  by blast
  23.217  
  23.218  lemma SUM_Un_distrib1:
  23.219 @@ -573,7 +573,7 @@
  23.220  by (rule SUM_Int_distrib2)
  23.221  
  23.222  (*Cf Aczel, Non-Well-Founded Sets, page 115*)
  23.223 -lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))"
  23.224 +lemma SUM_eq_UN: "(SUM i:I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
  23.225  by blast
  23.226  
  23.227  lemma times_subset_iff:
  23.228 @@ -617,10 +617,10 @@
  23.229  lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)"
  23.230  by blast
  23.231  
  23.232 -lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"
  23.233 +lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))"
  23.234  by blast
  23.235  
  23.236 -lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))"
  23.237 +lemma domain_Union: "domain(Union(A)) = (\<Union>x\<in>A. domain(x))"
  23.238  by blast
  23.239  
  23.240  
  23.241 @@ -728,7 +728,7 @@
  23.242  by blast
  23.243  
  23.244  (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
  23.245 -lemma rel_Union: "(ALL x:S. EX A B. x <= A*B) ==>   
  23.246 +lemma rel_Union: "(\<forall>x\<in>S. EX A B. x <= A*B) ==>   
  23.247                    Union(S) <= domain(Union(S)) * range(Union(S))"
  23.248  by blast
  23.249  
  23.250 @@ -745,7 +745,7 @@
  23.251  
  23.252  subsection{*Image of a Set under a Function or Relation*}
  23.253  
  23.254 -lemma image_iff: "b : r``A <-> (EX x:A. <x,b>:r)"
  23.255 +lemma image_iff: "b : r``A <-> (\<exists>x\<in>A. <x,b>:r)"
  23.256  by (unfold image_def, blast)
  23.257  
  23.258  lemma image_singleton_iff: "b : r``{a} <-> <a,b>:r"
  23.259 @@ -791,7 +791,7 @@
  23.260  subsection{*Inverse Image of a Set under a Function or Relation*}
  23.261  
  23.262  lemma vimage_iff: 
  23.263 -    "a : r-``B <-> (EX y:B. <a,y>:r)"
  23.264 +    "a : r-``B <-> (\<exists>y\<in>B. <a,y>:r)"
  23.265  by (unfold vimage_def image_def converse_def, blast)
  23.266  
  23.267  lemma vimage_singleton_iff: "a : r-``{b} <-> <a,b>:r"
  23.268 @@ -820,7 +820,7 @@
  23.269  by blast
  23.270  
  23.271  (*NOT suitable for rewriting*)
  23.272 -lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})"
  23.273 +lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})"
  23.274  by blast
  23.275  
  23.276  lemma function_vimage_Int:
  23.277 @@ -863,12 +863,12 @@
  23.278  lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
  23.279  by blast
  23.280  
  23.281 -lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))"
  23.282 +lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))"
  23.283  by blast
  23.284  
  23.285  (*Unfolding Inter avoids using excluded middle on A=0*)
  23.286  lemma converse_INT [simp]:
  23.287 -     "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))"
  23.288 +     "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))"
  23.289  apply (unfold Inter_def, blast)
  23.290  done
  23.291  
  23.292 @@ -887,7 +887,7 @@
  23.293  lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)"
  23.294  by blast
  23.295  
  23.296 -lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"
  23.297 +lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) <= Pow(\<Union>x\<in>A. B(x))"
  23.298  by blast
  23.299  
  23.300  lemma subset_Pow_Union: "A <= Pow(Union(A))"
  23.301 @@ -899,7 +899,7 @@
  23.302  lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
  23.303  by blast
  23.304  
  23.305 -lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))"
  23.306 +lemma Pow_INT_eq: "x:A ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))"
  23.307  by blast
  23.308  
  23.309  
    24.1 --- a/src/ZF/ex/Limit.thy	Tue Oct 01 11:17:25 2002 +0200
    24.2 +++ b/src/ZF/ex/Limit.thy	Tue Oct 01 13:26:10 2002 +0200
    24.3 @@ -1139,11 +1139,8 @@
    24.4  apply (assumption | rule cpoI poI)+
    24.5  apply (simp add: subcpo_rel_eq)
    24.6  apply (assumption | rule cpo_refl subcpo_subset [THEN subsetD])+
    24.7 -apply (rotate_tac -3)
    24.8  apply (simp add: subcpo_rel_eq)
    24.9  apply (blast intro: subcpo_subset [THEN subsetD] cpo_trans)
   24.10 -(* Changing the order of the assumptions, otherwise simp doesn't work. *)
   24.11 -apply (rotate_tac -2)
   24.12  apply (simp add: subcpo_rel_eq)
   24.13  apply (blast intro: cpo_antisym subcpo_subset [THEN subsetD])
   24.14  apply (fast intro: islub_subcpo)
    25.1 --- a/src/ZF/func.thy	Tue Oct 01 11:17:25 2002 +0200
    25.2 +++ b/src/ZF/func.thy	Tue Oct 01 13:26:10 2002 +0200
    25.3 @@ -261,7 +261,7 @@
    25.4  done
    25.5  
    25.6  (*For this lemma and the next, the right-hand side could equivalently 
    25.7 -  be written UN x:C. {f`x} *)
    25.8 +  be written \<Union>x\<in>C. {f`x} *)
    25.9  lemma image_function:
   25.10       "[| function(f);  C <= domain(f) |] ==> f``C = {f`x. x:C}";
   25.11  by (simp add: Repfun_function_if) 
   25.12 @@ -505,7 +505,7 @@
   25.13  by blast
   25.14  
   25.15  lemma UN_mono:
   25.16 -    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"
   25.17 +    "[| A<=C;  !!x. x:A ==> B(x)<=D(x) |] ==> (\<Union>x\<in>A. B(x)) <= (\<Union>x\<in>C. D(x))"
   25.18  by blast  
   25.19  
   25.20  (*Intersection is ANTI-monotonic.  There are TWO premises! *)