src/ZF/Univ.thy
changeset 46820 c656222c4dc1
parent 45602 2a858377c3d2
child 46821 ff6b0c1087f2
     1.1 --- a/src/ZF/Univ.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/Univ.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  definition
     1.6    Vfrom       :: "[i,i]=>i"  where
     1.7 -    "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
     1.8 +    "Vfrom(A,i) == transrec(i, %x f. A \<union> (\<Union>y\<in>x. Pow(f`y)))"
     1.9  
    1.10  abbreviation
    1.11    Vset :: "i=>i" where
    1.12 @@ -24,13 +24,13 @@
    1.13  
    1.14  definition
    1.15    Vrec        :: "[i, [i,i]=>i] =>i"  where
    1.16 -    "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
    1.17 -                           H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
    1.18 +    "Vrec(a,H) == transrec(rank(a), %x g. \<lambda>z\<in>Vset(succ(x)).
    1.19 +                           H(z, \<lambda>w\<in>Vset(x). g`rank(w)`w)) ` a"
    1.20  
    1.21  definition
    1.22    Vrecursor   :: "[[i,i]=>i, i] =>i"  where
    1.23 -    "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
    1.24 -                                H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
    1.25 +    "Vrecursor(H,a) == transrec(rank(a), %x g. \<lambda>z\<in>Vset(succ(x)).
    1.26 +                                H(\<lambda>w\<in>Vset(x). g`rank(w)`w, z)) ` a"
    1.27  
    1.28  definition
    1.29    univ        :: "i=>i"  where
    1.30 @@ -40,30 +40,30 @@
    1.31  subsection{*Immediate Consequences of the Definition of @{term "Vfrom(A,i)"}*}
    1.32  
    1.33  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    1.34 -lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    1.35 +lemma Vfrom: "Vfrom(A,i) = A \<union> (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    1.36  by (subst Vfrom_def [THEN def_transrec], simp)
    1.37  
    1.38  subsubsection{* Monotonicity *}
    1.39  
    1.40  lemma Vfrom_mono [rule_format]:
    1.41 -     "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
    1.42 +     "A<=B ==> \<forall>j. i<=j \<longrightarrow> Vfrom(A,i) \<subseteq> Vfrom(B,j)"
    1.43  apply (rule_tac a=i in eps_induct)
    1.44  apply (rule impI [THEN allI])
    1.45  apply (subst Vfrom [of A])
    1.46  apply (subst Vfrom [of B])
    1.47  apply (erule Un_mono)
    1.48 -apply (erule UN_mono, blast) 
    1.49 +apply (erule UN_mono, blast)
    1.50  done
    1.51  
    1.52  lemma VfromI: "[| a \<in> Vfrom(A,j);  j<i |] ==> a \<in> Vfrom(A,i)"
    1.53 -by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
    1.54 +by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]])
    1.55  
    1.56  
    1.57  subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
    1.58  
    1.59  
    1.60  
    1.61 -lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))"
    1.62 +lemma Vfrom_rank_subset1: "Vfrom(A,x) \<subseteq> Vfrom(A,rank(x))"
    1.63  proof (induct x rule: eps_induct)
    1.64    fix x
    1.65    assume "\<forall>y\<in>x. Vfrom(A,y) \<subseteq> Vfrom(A,rank(y))"
    1.66 @@ -72,7 +72,7 @@
    1.67          blast intro!: rank_lt [THEN ltD])
    1.68  qed
    1.69  
    1.70 -lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)"
    1.71 +lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) \<subseteq> Vfrom(A,x)"
    1.72  apply (rule_tac a=x in eps_induct)
    1.73  apply (subst Vfrom)
    1.74  apply (subst Vfrom, rule subset_refl [THEN Un_mono])
    1.75 @@ -99,19 +99,19 @@
    1.76  lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
    1.77  by (subst Vfrom, blast)
    1.78  
    1.79 -lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
    1.80 +lemma i_subset_Vfrom: "i \<subseteq> Vfrom(A,i)"
    1.81  apply (rule_tac a=i in eps_induct)
    1.82  apply (subst Vfrom, blast)
    1.83  done
    1.84  
    1.85 -lemma A_subset_Vfrom: "A <= Vfrom(A,i)"
    1.86 +lemma A_subset_Vfrom: "A \<subseteq> Vfrom(A,i)"
    1.87  apply (subst Vfrom)
    1.88  apply (rule Un_upper1)
    1.89  done
    1.90  
    1.91  lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
    1.92  
    1.93 -lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
    1.94 +lemma subset_mem_Vfrom: "a \<subseteq> Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
    1.95  by (subst Vfrom, blast)
    1.96  
    1.97  subsubsection{* Finite sets and ordered pairs *}
    1.98 @@ -126,13 +126,13 @@
    1.99  lemma Pair_in_Vfrom:
   1.100      "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> <a,b> \<in> Vfrom(A,succ(succ(i)))"
   1.101  apply (unfold Pair_def)
   1.102 -apply (blast intro: doubleton_in_Vfrom) 
   1.103 +apply (blast intro: doubleton_in_Vfrom)
   1.104  done
   1.105  
   1.106 -lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) \<in> Vfrom(A,succ(succ(i)))"
   1.107 +lemma succ_in_Vfrom: "a \<subseteq> Vfrom(A,i) ==> succ(a) \<in> Vfrom(A,succ(succ(i)))"
   1.108  apply (intro subset_mem_Vfrom succ_subsetI, assumption)
   1.109 -apply (erule subset_trans) 
   1.110 -apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
   1.111 +apply (erule subset_trans)
   1.112 +apply (rule Vfrom_mono [OF subset_refl subset_succI])
   1.113  done
   1.114  
   1.115  subsection{* 0, Successor and Limit Equations for @{term Vfrom} *}
   1.116 @@ -140,9 +140,9 @@
   1.117  lemma Vfrom_0: "Vfrom(A,0) = A"
   1.118  by (subst Vfrom, blast)
   1.119  
   1.120 -lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   1.121 +lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A \<union> Pow(Vfrom(A,i))"
   1.122  apply (rule Vfrom [THEN trans])
   1.123 -apply (rule equalityI [THEN subst_context, 
   1.124 +apply (rule equalityI [THEN subst_context,
   1.125                         OF _ succI1 [THEN RepFunI, THEN Union_upper]])
   1.126  apply (rule UN_least)
   1.127  apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono])
   1.128 @@ -150,7 +150,7 @@
   1.129  apply (erule Ord_succ)
   1.130  done
   1.131  
   1.132 -lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
   1.133 +lemma Vfrom_succ: "Vfrom(A,succ(i)) = A \<union> Pow(Vfrom(A,i))"
   1.134  apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
   1.135  apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
   1.136  apply (subst rank_succ)
   1.137 @@ -158,8 +158,8 @@
   1.138  done
   1.139  
   1.140  (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   1.141 -  the conclusion to be Vfrom(A,Union(X)) = A Un (\<Union>y\<in>X. Vfrom(A,y)) *)
   1.142 -lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
   1.143 +  the conclusion to be Vfrom(A,\<Union>(X)) = A \<union> (\<Union>y\<in>X. Vfrom(A,y)) *)
   1.144 +lemma Vfrom_Union: "y:X ==> Vfrom(A,\<Union>(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
   1.145  apply (subst Vfrom)
   1.146  apply (rule equalityI)
   1.147  txt{*first inclusion*}
   1.148 @@ -179,11 +179,11 @@
   1.149  subsection{* @{term Vfrom} applied to Limit Ordinals *}
   1.150  
   1.151  (*NB. limit ordinals are non-empty:
   1.152 -      Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
   1.153 +      Vfrom(A,0) = A = A \<union> (\<Union>y\<in>0. Vfrom(A,y)) *)
   1.154  lemma Limit_Vfrom_eq:
   1.155      "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
   1.156  apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
   1.157 -apply (simp add: Limit_Union_eq) 
   1.158 +apply (simp add: Limit_Union_eq)
   1.159  done
   1.160  
   1.161  lemma Limit_VfromE:
   1.162 @@ -193,7 +193,7 @@
   1.163  apply (rule classical)
   1.164  apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
   1.165    prefer 2 apply assumption
   1.166 - apply blast 
   1.167 + apply blast
   1.168  apply (blast intro: ltI Limit_is_Ord)
   1.169  done
   1.170  
   1.171 @@ -201,12 +201,12 @@
   1.172      "[| a \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
   1.173  apply (erule Limit_VfromE, assumption)
   1.174  apply (erule singleton_in_Vfrom [THEN VfromI])
   1.175 -apply (blast intro: Limit_has_succ) 
   1.176 +apply (blast intro: Limit_has_succ)
   1.177  done
   1.178  
   1.179 -lemmas Vfrom_UnI1 = 
   1.180 +lemmas Vfrom_UnI1 =
   1.181      Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
   1.182 -lemmas Vfrom_UnI2 = 
   1.183 +lemmas Vfrom_UnI2 =
   1.184      Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
   1.185  
   1.186  text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
   1.187 @@ -223,12 +223,12 @@
   1.188  txt{*Infer that a, b occur at ordinals x,xa < i.*}
   1.189  apply (erule Limit_VfromE, assumption)
   1.190  apply (erule Limit_VfromE, assumption)
   1.191 -txt{*Infer that succ(succ(x Un xa)) < i *}
   1.192 +txt{*Infer that @{term"succ(succ(x \<union> xa)) < i"} *}
   1.193  apply (blast intro: VfromI [OF Pair_in_Vfrom]
   1.194                      Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
   1.195  done
   1.196  
   1.197 -lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
   1.198 +lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) \<subseteq> Vfrom(A,i)"
   1.199  by (blast intro: Pair_in_VLimit)
   1.200  
   1.201  lemmas Sigma_subset_VLimit =
   1.202 @@ -259,7 +259,7 @@
   1.203  apply (blast intro: one_in_VLimit Pair_in_VLimit)
   1.204  done
   1.205  
   1.206 -lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"
   1.207 +lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) \<subseteq> Vfrom(C,i)"
   1.208  by (blast intro!: Inl_in_VLimit Inr_in_VLimit)
   1.209  
   1.210  lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
   1.211 @@ -283,11 +283,11 @@
   1.212  apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]])
   1.213  done
   1.214  
   1.215 -lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C"
   1.216 +lemma Transset_Pair_subset: "[| <a,b> \<subseteq> C; Transset(C) |] ==> a: C & b: C"
   1.217  by (unfold Pair_def Transset_def, blast)
   1.218  
   1.219  lemma Transset_Pair_subset_VLimit:
   1.220 -     "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |]
   1.221 +     "[| <a,b> \<subseteq> Vfrom(A,i);  Transset(A);  Limit(i) |]
   1.222        ==> <a,b> \<in> Vfrom(A,i)"
   1.223  apply (erule Transset_Pair_subset [THEN conjE])
   1.224  apply (erule Transset_Vfrom)
   1.225 @@ -295,14 +295,14 @@
   1.226  done
   1.227  
   1.228  lemma Union_in_Vfrom:
   1.229 -     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Union(X) \<in> Vfrom(A, succ(j))"
   1.230 +     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> \<Union>(X) \<in> Vfrom(A, succ(j))"
   1.231  apply (drule Transset_Vfrom)
   1.232  apply (rule subset_mem_Vfrom)
   1.233  apply (unfold Transset_def, blast)
   1.234  done
   1.235  
   1.236  lemma Union_in_VLimit:
   1.237 -     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) \<in> Vfrom(A,i)"
   1.238 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> \<Union>(X) \<in> Vfrom(A,i)"
   1.239  apply (rule Limit_VfromE, assumption+)
   1.240  apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
   1.241  done
   1.242 @@ -317,15 +317,15 @@
   1.243  lemma in_VLimit:
   1.244    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);
   1.245        !!x y j. [| j<i; 1:j; x \<in> Vfrom(A,j); y \<in> Vfrom(A,j) |]
   1.246 -               ==> EX k. h(x,y) \<in> Vfrom(A,k) & k<i |]
   1.247 +               ==> \<exists>k. h(x,y) \<in> Vfrom(A,k) & k<i |]
   1.248     ==> h(a,b) \<in> Vfrom(A,i)"
   1.249  txt{*Infer that a, b occur at ordinals x,xa < i.*}
   1.250  apply (erule Limit_VfromE, assumption)
   1.251  apply (erule Limit_VfromE, assumption, atomize)
   1.252 -apply (drule_tac x=a in spec) 
   1.253 -apply (drule_tac x=b in spec) 
   1.254 -apply (drule_tac x="x Un xa Un 2" in spec) 
   1.255 -apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
   1.256 +apply (drule_tac x=a in spec)
   1.257 +apply (drule_tac x=b in spec)
   1.258 +apply (drule_tac x="x \<union> xa \<union> 2" in spec)
   1.259 +apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2)
   1.260  apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
   1.261  done
   1.262  
   1.263 @@ -414,15 +414,15 @@
   1.264  
   1.265  subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
   1.266  
   1.267 -lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
   1.268 +lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) \<longrightarrow> rank(b) < i"
   1.269  apply (erule trans_induct)
   1.270  apply (subst Vset, safe)
   1.271  apply (subst rank)
   1.272 -apply (blast intro: ltI UN_succ_least_lt) 
   1.273 +apply (blast intro: ltI UN_succ_least_lt)
   1.274  done
   1.275  
   1.276  lemma VsetI_lemma [rule_format]:
   1.277 -     "Ord(i) ==> \<forall>b. rank(b) \<in> i --> b \<in> Vset(i)"
   1.278 +     "Ord(i) ==> \<forall>b. rank(b) \<in> i \<longrightarrow> b \<in> Vset(i)"
   1.279  apply (erule trans_induct)
   1.280  apply (rule allI)
   1.281  apply (subst Vset)
   1.282 @@ -447,30 +447,30 @@
   1.283  lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i"
   1.284  apply (subst rank)
   1.285  apply (rule equalityI, safe)
   1.286 -apply (blast intro: VsetD [THEN ltD]) 
   1.287 -apply (blast intro: VsetD [THEN ltD] Ord_trans) 
   1.288 +apply (blast intro: VsetD [THEN ltD])
   1.289 +apply (blast intro: VsetD [THEN ltD] Ord_trans)
   1.290  apply (blast intro: i_subset_Vfrom [THEN subsetD]
   1.291                      Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   1.292  done
   1.293  
   1.294  lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
   1.295  apply (erule nat_induct)
   1.296 - apply (simp add: Vfrom_0) 
   1.297 -apply (simp add: Vset_succ) 
   1.298 + apply (simp add: Vfrom_0)
   1.299 +apply (simp add: Vset_succ)
   1.300  done
   1.301  
   1.302  subsubsection{* Reasoning about Sets in Terms of Their Elements' Ranks *}
   1.303  
   1.304 -lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   1.305 +lemma arg_subset_Vset_rank: "a \<subseteq> Vset(rank(a))"
   1.306  apply (rule subsetI)
   1.307  apply (erule rank_lt [THEN VsetI])
   1.308  done
   1.309  
   1.310  lemma Int_Vset_subset:
   1.311 -    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"
   1.312 -apply (rule subset_trans) 
   1.313 +    "[| !!i. Ord(i) ==> a \<inter> Vset(i) \<subseteq> b |] ==> a \<subseteq> b"
   1.314 +apply (rule subset_trans)
   1.315  apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
   1.316 -apply (blast intro: Ord_rank) 
   1.317 +apply (blast intro: Ord_rank)
   1.318  done
   1.319  
   1.320  subsubsection{* Set Up an Environment for Simplification *}
   1.321 @@ -490,7 +490,7 @@
   1.322  subsubsection{* Recursion over Vset Levels! *}
   1.323  
   1.324  text{*NOT SUITABLE FOR REWRITING: recursive!*}
   1.325 -lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
   1.326 +lemma Vrec: "Vrec(a,H) = H(a, \<lambda>x\<in>Vset(rank(a)). Vrec(x,H))"
   1.327  apply (unfold Vrec_def)
   1.328  apply (subst transrec, simp)
   1.329  apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
   1.330 @@ -499,14 +499,14 @@
   1.331  text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   1.332  lemma def_Vrec:
   1.333      "[| !!x. h(x)==Vrec(x,H) |] ==>
   1.334 -     h(a) = H(a, lam x: Vset(rank(a)). h(x))"
   1.335 -apply simp 
   1.336 +     h(a) = H(a, \<lambda>x\<in>Vset(rank(a)). h(x))"
   1.337 +apply simp
   1.338  apply (rule Vrec)
   1.339  done
   1.340  
   1.341  text{*NOT SUITABLE FOR REWRITING: recursive!*}
   1.342  lemma Vrecursor:
   1.343 -     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)"
   1.344 +     "Vrecursor(H,a) = H(\<lambda>x\<in>Vset(rank(a)). Vrecursor(H,x),  a)"
   1.345  apply (unfold Vrecursor_def)
   1.346  apply (subst transrec, simp)
   1.347  apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
   1.348 @@ -514,7 +514,7 @@
   1.349  
   1.350  text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
   1.351  lemma def_Vrecursor:
   1.352 -     "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)"
   1.353 +     "h == Vrecursor(H) ==> h(a) = H(\<lambda>x\<in>Vset(rank(a)). h(x),  a)"
   1.354  apply simp
   1.355  apply (rule Vrecursor)
   1.356  done
   1.357 @@ -522,7 +522,7 @@
   1.358  
   1.359  subsection{* The Datatype Universe: @{term "univ(A)"} *}
   1.360  
   1.361 -lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
   1.362 +lemma univ_mono: "A<=B ==> univ(A) \<subseteq> univ(B)"
   1.363  apply (unfold univ_def)
   1.364  apply (erule Vfrom_mono)
   1.365  apply (rule subset_refl)
   1.366 @@ -540,28 +540,28 @@
   1.367  apply (rule Limit_nat [THEN Limit_Vfrom_eq])
   1.368  done
   1.369  
   1.370 -lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (\<Union>i\<in>nat. c Int Vfrom(A,i))"
   1.371 +lemma subset_univ_eq_Int: "c \<subseteq> univ(A) ==> c = (\<Union>i\<in>nat. c \<inter> Vfrom(A,i))"
   1.372  apply (rule subset_UN_iff_eq [THEN iffD1])
   1.373  apply (erule univ_eq_UN [THEN subst])
   1.374  done
   1.375  
   1.376  lemma univ_Int_Vfrom_subset:
   1.377 -    "[| a <= univ(X);
   1.378 -        !!i. i:nat ==> a Int Vfrom(X,i) <= b |]
   1.379 -     ==> a <= b"
   1.380 +    "[| a \<subseteq> univ(X);
   1.381 +        !!i. i:nat ==> a \<inter> Vfrom(X,i) \<subseteq> b |]
   1.382 +     ==> a \<subseteq> b"
   1.383  apply (subst subset_univ_eq_Int, assumption)
   1.384 -apply (rule UN_least, simp) 
   1.385 +apply (rule UN_least, simp)
   1.386  done
   1.387  
   1.388  lemma univ_Int_Vfrom_eq:
   1.389 -    "[| a <= univ(X);   b <= univ(X);
   1.390 -        !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i)
   1.391 +    "[| a \<subseteq> univ(X);   b \<subseteq> univ(X);
   1.392 +        !!i. i:nat ==> a \<inter> Vfrom(X,i) = b \<inter> Vfrom(X,i)
   1.393       |] ==> a = b"
   1.394  apply (rule equalityI)
   1.395  apply (rule univ_Int_Vfrom_subset, assumption)
   1.396 -apply (blast elim: equalityCE) 
   1.397 +apply (blast elim: equalityCE)
   1.398  apply (rule univ_Int_Vfrom_subset, assumption)
   1.399 -apply (blast elim: equalityCE) 
   1.400 +apply (blast elim: equalityCE)
   1.401  done
   1.402  
   1.403  subsection{* Closure Properties for @{term "univ(A)"}*}
   1.404 @@ -571,10 +571,10 @@
   1.405  apply (rule nat_0I [THEN zero_in_Vfrom])
   1.406  done
   1.407  
   1.408 -lemma zero_subset_univ: "{0} <= univ(A)"
   1.409 +lemma zero_subset_univ: "{0} \<subseteq> univ(A)"
   1.410  by (blast intro: zero_in_univ)
   1.411  
   1.412 -lemma A_subset_univ: "A <= univ(A)"
   1.413 +lemma A_subset_univ: "A \<subseteq> univ(A)"
   1.414  apply (unfold univ_def)
   1.415  apply (rule A_subset_Vfrom)
   1.416  done
   1.417 @@ -601,12 +601,12 @@
   1.418  done
   1.419  
   1.420  lemma Union_in_univ:
   1.421 -     "[| X: univ(A);  Transset(A) |] ==> Union(X) \<in> univ(A)"
   1.422 +     "[| X: univ(A);  Transset(A) |] ==> \<Union>(X) \<in> univ(A)"
   1.423  apply (unfold univ_def)
   1.424  apply (blast intro: Union_in_VLimit Limit_nat)
   1.425  done
   1.426  
   1.427 -lemma product_univ: "univ(A)*univ(A) <= univ(A)"
   1.428 +lemma product_univ: "univ(A)*univ(A) \<subseteq> univ(A)"
   1.429  apply (unfold univ_def)
   1.430  apply (rule Limit_nat [THEN product_VLimit])
   1.431  done
   1.432 @@ -614,7 +614,7 @@
   1.433  
   1.434  subsubsection{* The Natural Numbers *}
   1.435  
   1.436 -lemma nat_subset_univ: "nat <= univ(A)"
   1.437 +lemma nat_subset_univ: "nat \<subseteq> univ(A)"
   1.438  apply (unfold univ_def)
   1.439  apply (rule i_subset_Vfrom)
   1.440  done
   1.441 @@ -633,7 +633,7 @@
   1.442  lemma two_in_univ: "2 \<in> univ(A)"
   1.443  by (blast intro: nat_into_univ)
   1.444  
   1.445 -lemma bool_subset_univ: "bool <= univ(A)"
   1.446 +lemma bool_subset_univ: "bool \<subseteq> univ(A)"
   1.447  apply (unfold bool_def)
   1.448  apply (blast intro!: zero_in_univ one_in_univ)
   1.449  done
   1.450 @@ -653,7 +653,7 @@
   1.451  apply (erule Inr_in_VLimit [OF _ Limit_nat])
   1.452  done
   1.453  
   1.454 -lemma sum_univ: "univ(C)+univ(C) <= univ(C)"
   1.455 +lemma sum_univ: "univ(C)+univ(C) \<subseteq> univ(C)"
   1.456  apply (unfold univ_def)
   1.457  apply (rule Limit_nat [THEN sum_VLimit])
   1.458  done
   1.459 @@ -663,7 +663,7 @@
   1.460  lemma Sigma_subset_univ:
   1.461    "[|A \<subseteq> univ(D); \<And>x. x \<in> A \<Longrightarrow> B(x) \<subseteq> univ(D)|] ==> Sigma(A,B) \<subseteq> univ(D)"
   1.462  apply (simp add: univ_def)
   1.463 -apply (blast intro: Sigma_subset_VLimit del: subsetI) 
   1.464 +apply (blast intro: Sigma_subset_VLimit del: subsetI)
   1.465  done
   1.466  
   1.467  
   1.468 @@ -677,14 +677,14 @@
   1.469  subsubsection{* Closure under Finite Powerset *}
   1.470  
   1.471  lemma Fin_Vfrom_lemma:
   1.472 -     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
   1.473 +     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> \<exists>j. b \<subseteq> Vfrom(A,j) & j<i"
   1.474  apply (erule Fin_induct)
   1.475  apply (blast dest!: Limit_has_0, safe)
   1.476  apply (erule Limit_VfromE, assumption)
   1.477  apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
   1.478  done
   1.479  
   1.480 -lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"
   1.481 +lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) \<subseteq> Vfrom(A,i)"
   1.482  apply (rule subsetI)
   1.483  apply (drule Fin_Vfrom_lemma, safe)
   1.484  apply (rule Vfrom [THEN ssubst])
   1.485 @@ -693,7 +693,7 @@
   1.486  
   1.487  lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
   1.488  
   1.489 -lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
   1.490 +lemma Fin_univ: "Fin(univ(A)) \<subseteq> univ(A)"
   1.491  apply (unfold univ_def)
   1.492  apply (rule Limit_nat [THEN Fin_VLimit])
   1.493  done
   1.494 @@ -701,7 +701,7 @@
   1.495  subsubsection{* Closure under Finite Powers: Functions from a Natural Number *}
   1.496  
   1.497  lemma nat_fun_VLimit:
   1.498 -     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
   1.499 +     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) \<subseteq> Vfrom(A,i)"
   1.500  apply (erule nat_fun_subset_Fin [THEN subset_trans])
   1.501  apply (blast del: subsetI
   1.502      intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit)
   1.503 @@ -709,7 +709,7 @@
   1.504  
   1.505  lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
   1.506  
   1.507 -lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)"
   1.508 +lemma nat_fun_univ: "n: nat ==> n -> univ(A) \<subseteq> univ(A)"
   1.509  apply (unfold univ_def)
   1.510  apply (erule nat_fun_VLimit [OF _ Limit_nat])
   1.511  done
   1.512 @@ -719,36 +719,36 @@
   1.513  
   1.514  text{*General but seldom-used version; normally the domain is fixed*}
   1.515  lemma FiniteFun_VLimit1:
   1.516 -     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
   1.517 +     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) \<subseteq> Vfrom(A,i)"
   1.518  apply (rule FiniteFun.dom_subset [THEN subset_trans])
   1.519  apply (blast del: subsetI
   1.520               intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl)
   1.521  done
   1.522  
   1.523 -lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)"
   1.524 +lemma FiniteFun_univ1: "univ(A) -||> univ(A) \<subseteq> univ(A)"
   1.525  apply (unfold univ_def)
   1.526  apply (rule Limit_nat [THEN FiniteFun_VLimit1])
   1.527  done
   1.528  
   1.529  text{*Version for a fixed domain*}
   1.530  lemma FiniteFun_VLimit:
   1.531 -     "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"
   1.532 -apply (rule subset_trans) 
   1.533 +     "[| W \<subseteq> Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) \<subseteq> Vfrom(A,i)"
   1.534 +apply (rule subset_trans)
   1.535  apply (erule FiniteFun_mono [OF _ subset_refl])
   1.536  apply (erule FiniteFun_VLimit1)
   1.537  done
   1.538  
   1.539  lemma FiniteFun_univ:
   1.540 -    "W <= univ(A) ==> W -||> univ(A) <= univ(A)"
   1.541 +    "W \<subseteq> univ(A) ==> W -||> univ(A) \<subseteq> univ(A)"
   1.542  apply (unfold univ_def)
   1.543  apply (erule FiniteFun_VLimit [OF _ Limit_nat])
   1.544  done
   1.545  
   1.546  lemma FiniteFun_in_univ:
   1.547 -     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f \<in> univ(A)"
   1.548 +     "[| f: W -||> univ(A);  W \<subseteq> univ(A) |] ==> f \<in> univ(A)"
   1.549  by (erule FiniteFun_univ [THEN subsetD], assumption)
   1.550  
   1.551 -text{*Remove <= from the rule above*}
   1.552 +text{*Remove @{text "\<subseteq>"} from the rule above*}
   1.553  lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
   1.554  
   1.555  
   1.556 @@ -760,16 +760,16 @@
   1.557  lemma doubleton_in_Vfrom_D:
   1.558       "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
   1.559        ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
   1.560 -by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], 
   1.561 +by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD],
   1.562      assumption, fast)
   1.563  
   1.564  text{*This weaker version says a, b exist at the same level*}
   1.565  lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
   1.566  
   1.567 -(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
   1.568 -      implies a, b \<in> Vfrom(X,i), which is useless for induction.
   1.569 -    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
   1.570 -      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
   1.571 +(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   1.572 +      implies a, b : Vfrom(X,i), which is useless for induction.
   1.573 +    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   1.574 +      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   1.575      The combination gives a reduction by precisely one level, which is
   1.576        most convenient for proofs.
   1.577  **)
   1.578 @@ -783,13 +783,13 @@
   1.579  
   1.580  lemma product_Int_Vfrom_subset:
   1.581       "Transset(X) ==>
   1.582 -      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"
   1.583 +      (a*b) \<inter> Vfrom(X, succ(i)) \<subseteq> (a \<inter> Vfrom(X,i)) * (b \<inter> Vfrom(X,i))"
   1.584  by (blast dest!: Pair_in_Vfrom_D)
   1.585  
   1.586  
   1.587  ML
   1.588  {*
   1.589 -val rank_ss = @{simpset} addsimps [@{thm VsetI}] 
   1.590 +val rank_ss = @{simpset} addsimps [@{thm VsetI}]
   1.591                addsimps @{thms rank_rls} @ (@{thms rank_rls} RLN (2, [@{thm lt_trans}]));
   1.592  *}
   1.593