tidying
authorpaulson
Tue Jun 18 18:45:07 2002 +0200 (2002-06-18)
changeset 1322062c899c77151
parent 13219 7e44aa8a276e
child 13221 e29378f347e4
tidying
src/ZF/Bool.thy
src/ZF/Fixedpt.thy
src/ZF/Let.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Rel.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
     1.1 --- a/src/ZF/Bool.thy	Tue Jun 18 17:58:21 2002 +0200
     1.2 +++ b/src/ZF/Bool.thy	Tue Jun 18 18:45:07 2002 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  Bool = pair + 
     1.5  consts
     1.6      bool        :: i
     1.7 -    cond        :: [i,i,i]=>i
     1.8 -    not         :: i=>i
     1.9 -    "and"       :: [i,i]=>i      (infixl 70)
    1.10 -    or          :: [i,i]=>i      (infixl 65)
    1.11 -    xor         :: [i,i]=>i      (infixl 65)
    1.12 +    cond        :: "[i,i,i]=>i"
    1.13 +    not         :: "i=>i"
    1.14 +    "and"       :: "[i,i]=>i"      (infixl 70)
    1.15 +    or          :: "[i,i]=>i"      (infixl 65)
    1.16 +    xor         :: "[i,i]=>i"      (infixl 65)
    1.17  
    1.18  syntax
    1.19      "1"         :: i             ("1")
     2.1 --- a/src/ZF/Fixedpt.thy	Tue Jun 18 17:58:21 2002 +0200
     2.2 +++ b/src/ZF/Fixedpt.thy	Tue Jun 18 18:45:07 2002 +0200
     2.3 @@ -49,6 +49,18 @@
     2.4  apply (rule Un_least, blast+)
     2.5  done
     2.6  
     2.7 +(*unused*)
     2.8 +lemma bnd_mono_UN:
     2.9 +     "[| bnd_mono(D,h);  \<forall>i\<in>I. A(i) <= D |] 
    2.10 +      ==> (\<Union>i\<in>I. h(A(i))) <= h((\<Union>i\<in>I. A(i)))"
    2.11 +apply (unfold bnd_mono_def) 
    2.12 +apply (rule UN_least)
    2.13 +apply (elim conjE) 
    2.14 +apply (drule_tac x="A(i)" in spec)
    2.15 +apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec) 
    2.16 +apply blast 
    2.17 +done
    2.18 +
    2.19  (*Useful??*)
    2.20  lemma bnd_mono_Int:
    2.21       "[| bnd_mono(D,h);  A <= D;  B <= D |] ==> h(A Int B) <= h(A) Int h(B)"
     3.1 --- a/src/ZF/Let.thy	Tue Jun 18 17:58:21 2002 +0200
     3.2 +++ b/src/ZF/Let.thy	Tue Jun 18 18:45:07 2002 +0200
     3.3 @@ -12,13 +12,13 @@
     3.4    letbinds  letbind
     3.5  
     3.6  consts
     3.7 -  Let           :: ['a::logic, 'a => 'b] => ('b::logic)
     3.8 +  Let           :: "['a::logic, 'a => 'b] => ('b::logic)"
     3.9  
    3.10  syntax
    3.11 -  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
    3.12 -  ""            :: letbind => letbinds              ("_")
    3.13 -  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
    3.14 -  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
    3.15 +  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
    3.16 +  ""            :: "letbind => letbinds"              ("_")
    3.17 +  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
    3.18 +  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
    3.19  
    3.20  translations
    3.21    "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
     4.1 --- a/src/ZF/QPair.thy	Tue Jun 18 17:58:21 2002 +0200
     4.2 +++ b/src/ZF/QPair.thy	Tue Jun 18 18:45:07 2002 +0200
     4.3 @@ -14,19 +14,19 @@
     4.4  QPair = Sum +
     4.5  
     4.6  consts
     4.7 -  QPair     :: [i, i] => i                      ("<(_;/ _)>")
     4.8 -  qfst,qsnd :: i => i
     4.9 -  qsplit    :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
    4.10 -  qconverse :: i => i
    4.11 -  QSigma    :: [i, i => i] => i
    4.12 +  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
    4.13 +  qfst,qsnd :: "i => i"
    4.14 +  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
    4.15 +  qconverse :: "i => i"
    4.16 +  QSigma    :: "[i, i => i] => i"
    4.17  
    4.18 -  "<+>"     :: [i,i]=>i                         (infixr 65)
    4.19 -  QInl,QInr :: i=>i
    4.20 -  qcase     :: [i=>i, i=>i, i]=>i
    4.21 +  "<+>"     :: "[i,i]=>i"                         (infixr 65)
    4.22 +  QInl,QInr :: "i=>i"
    4.23 +  qcase     :: "[i=>i, i=>i, i]=>i"
    4.24  
    4.25  syntax
    4.26 -  "@QSUM"   :: [idt, i, i] => i               ("(3QSUM _:_./ _)" 10)
    4.27 -  "<*>"     :: [i, i] => i                      (infixr 80)
    4.28 +  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    4.29 +  "<*>"     :: "[i, i] => i"                      (infixr 80)
    4.30  
    4.31  translations
    4.32    "QSUM x:A. B"  => "QSigma(A, %x. B)"
     5.1 --- a/src/ZF/QUniv.thy	Tue Jun 18 17:58:21 2002 +0200
     5.2 +++ b/src/ZF/QUniv.thy	Tue Jun 18 18:45:07 2002 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4    case_eqns	qcase_QInl, qcase_QInr
     5.5  
     5.6  constdefs
     5.7 -  quniv :: i => i
     5.8 +  quniv :: "i => i"
     5.9     "quniv(A) == Pow(univ(eclose(A)))"
    5.10  
    5.11  end
     6.1 --- a/src/ZF/Rel.thy	Tue Jun 18 17:58:21 2002 +0200
     6.2 +++ b/src/ZF/Rel.thy	Tue Jun 18 18:45:07 2002 +0200
     6.3 @@ -8,9 +8,14 @@
     6.4  
     6.5  Rel = equalities +
     6.6  consts
     6.7 -    refl,irrefl,equiv      :: [i,i]=>o
     6.8 -    sym,asym,antisym,trans :: i=>o
     6.9 -    trans_on               :: [i,i]=>o  ("trans[_]'(_')")
    6.10 +    refl     :: "[i,i]=>o"
    6.11 +    irrefl   :: "[i,i]=>o"
    6.12 +    equiv    :: "[i,i]=>o"
    6.13 +    sym      :: "i=>o"
    6.14 +    asym     :: "i=>o"
    6.15 +    antisym  :: "i=>o"
    6.16 +    trans    :: "i=>o"
    6.17 +    trans_on :: "[i,i]=>o"  ("trans[_]'(_')")
    6.18  
    6.19  defs
    6.20    refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
     7.1 --- a/src/ZF/Sum.thy	Tue Jun 18 17:58:21 2002 +0200
     7.2 +++ b/src/ZF/Sum.thy	Tue Jun 18 18:45:07 2002 +0200
     7.3 @@ -12,10 +12,11 @@
     7.4  global
     7.5  
     7.6  consts
     7.7 -    "+"         :: [i,i]=>i                     (infixr 65)
     7.8 -    Inl,Inr     :: i=>i
     7.9 -    case        :: [i=>i, i=>i, i]=>i
    7.10 -    Part        :: [i,i=>i] => i
    7.11 +    "+"     :: "[i,i]=>i"                     (infixr 65)
    7.12 +    Inl     :: "i=>i"
    7.13 +    Inr     :: "i=>i"
    7.14 +    "case"  :: "[i=>i, i=>i, i]=>i"
    7.15 +    Part    :: "[i,i=>i] => i"
    7.16  
    7.17  local
    7.18  
     8.1 --- a/src/ZF/Trancl.thy	Tue Jun 18 17:58:21 2002 +0200
     8.2 +++ b/src/ZF/Trancl.thy	Tue Jun 18 18:45:07 2002 +0200
     8.3 @@ -8,8 +8,8 @@
     8.4  
     8.5  Trancl = Fixedpt + Perm + mono + Rel + 
     8.6  consts
     8.7 -    rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
     8.8 -    trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
     8.9 +    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    8.10 +    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    8.11  
    8.12  defs
    8.13      rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
     9.1 --- a/src/ZF/Univ.thy	Tue Jun 18 17:58:21 2002 +0200
     9.2 +++ b/src/ZF/Univ.thy	Tue Jun 18 18:45:07 2002 +0200
     9.3 @@ -15,9 +15,9 @@
     9.4  
     9.5  constdefs
     9.6    Vfrom       :: "[i,i]=>i"
     9.7 -    "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
     9.8 +    "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
     9.9  
    9.10 -syntax   Vset        :: "i=>i"
    9.11 +syntax   Vset :: "i=>i"
    9.12  translations
    9.13      "Vset(x)"   ==      "Vfrom(0,x)"
    9.14  
    9.15 @@ -36,7 +36,7 @@
    9.16  
    9.17  
    9.18  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
    9.19 -lemma Vfrom: "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))"
    9.20 +lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
    9.21  apply (subst Vfrom_def [THEN def_transrec])
    9.22  apply simp
    9.23  done
    9.24 @@ -44,7 +44,7 @@
    9.25  subsubsection{* Monotonicity *}
    9.26  
    9.27  lemma Vfrom_mono [rule_format]:
    9.28 -     "A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
    9.29 +     "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
    9.30  apply (rule_tac a=i in eps_induct)
    9.31  apply (rule impI [THEN allI])
    9.32  apply (subst Vfrom)
    9.33 @@ -53,7 +53,7 @@
    9.34  apply (erule UN_mono, blast) 
    9.35  done
    9.36  
    9.37 -lemma VfromI: "[| a: Vfrom(A,j);  j<i |] ==> a : Vfrom(A,i)"
    9.38 +lemma VfromI: "[| a \<in> Vfrom(A,j);  j<i |] ==> a \<in> Vfrom(A,i)"
    9.39  by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
    9.40  
    9.41  
    9.42 @@ -72,7 +72,7 @@
    9.43  apply (subst Vfrom)
    9.44  apply (rule subset_refl [THEN Un_mono])
    9.45  apply (rule UN_least)
    9.46 -txt{*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*}
    9.47 +txt{*expand rank(x1) = (\<Union>y\<in>x1. succ(rank(y))) in assumptions*}
    9.48  apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
    9.49  apply (rule subset_trans)
    9.50  apply (erule_tac [2] UN_upper)
    9.51 @@ -91,7 +91,7 @@
    9.52  
    9.53  subsection{* Basic closure properties *}
    9.54  
    9.55 -lemma zero_in_Vfrom: "y:x ==> 0 : Vfrom(A,x)"
    9.56 +lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
    9.57  by (subst Vfrom, blast)
    9.58  
    9.59  lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
    9.60 @@ -106,25 +106,25 @@
    9.61  
    9.62  lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
    9.63  
    9.64 -lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"
    9.65 +lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
    9.66  by (subst Vfrom, blast)
    9.67  
    9.68  subsubsection{* Finite sets and ordered pairs *}
    9.69  
    9.70 -lemma singleton_in_Vfrom: "a: Vfrom(A,i) ==> {a} : Vfrom(A,succ(i))"
    9.71 +lemma singleton_in_Vfrom: "a \<in> Vfrom(A,i) ==> {a} \<in> Vfrom(A,succ(i))"
    9.72  by (rule subset_mem_Vfrom, safe)
    9.73  
    9.74  lemma doubleton_in_Vfrom:
    9.75 -     "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> {a,b} : Vfrom(A,succ(i))"
    9.76 +     "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> {a,b} \<in> Vfrom(A,succ(i))"
    9.77  by (rule subset_mem_Vfrom, safe)
    9.78  
    9.79  lemma Pair_in_Vfrom:
    9.80 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i) |] ==> <a,b> : Vfrom(A,succ(succ(i)))"
    9.81 +    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> <a,b> \<in> Vfrom(A,succ(succ(i)))"
    9.82  apply (unfold Pair_def)
    9.83  apply (blast intro: doubleton_in_Vfrom) 
    9.84  done
    9.85  
    9.86 -lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) : Vfrom(A,succ(succ(i)))"
    9.87 +lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) \<in> Vfrom(A,succ(succ(i)))"
    9.88  apply (intro subset_mem_Vfrom succ_subsetI, assumption)
    9.89  apply (erule subset_trans) 
    9.90  apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
    9.91 @@ -153,8 +153,8 @@
    9.92  done
    9.93  
    9.94  (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
    9.95 -  the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
    9.96 -lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))"
    9.97 +  the conclusion to be Vfrom(A,Union(X)) = A Un (\<Union>y\<in>X. Vfrom(A,y)) *)
    9.98 +lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
    9.99  apply (subst Vfrom)
   9.100  apply (rule equalityI)
   9.101  txt{*first inclusion*}
   9.102 @@ -174,16 +174,16 @@
   9.103  subsection{* Vfrom applied to Limit ordinals *}
   9.104  
   9.105  (*NB. limit ordinals are non-empty:
   9.106 -      Vfrom(A,0) = A = A Un (UN y:0. Vfrom(A,y)) *)
   9.107 +      Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
   9.108  lemma Limit_Vfrom_eq:
   9.109 -    "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))"
   9.110 +    "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
   9.111  apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
   9.112  apply (simp add: Limit_Union_eq) 
   9.113  done
   9.114  
   9.115  lemma Limit_VfromE:
   9.116 -    "[| a: Vfrom(A,i);  ~R ==> Limit(i);
   9.117 -        !!x. [| x<i;  a: Vfrom(A,x) |] ==> R
   9.118 +    "[| a \<in> Vfrom(A,i);  ~R ==> Limit(i);
   9.119 +        !!x. [| x<i;  a \<in> Vfrom(A,x) |] ==> R
   9.120       |] ==> R"
   9.121  apply (rule classical)
   9.122  apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
   9.123 @@ -195,7 +195,7 @@
   9.124  lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   9.125  
   9.126  lemma singleton_in_VLimit:
   9.127 -    "[| a: Vfrom(A,i);  Limit(i) |] ==> {a} : Vfrom(A,i)"
   9.128 +    "[| a \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
   9.129  apply (erule Limit_VfromE, assumption)
   9.130  apply (erule singleton_in_Vfrom [THEN VfromI])
   9.131  apply (blast intro: Limit_has_succ) 
   9.132 @@ -208,7 +208,7 @@
   9.133  
   9.134  text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
   9.135  lemma doubleton_in_VLimit:
   9.136 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> {a,b} : Vfrom(A,i)"
   9.137 +    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> {a,b} \<in> Vfrom(A,i)"
   9.138  apply (erule Limit_VfromE, assumption)
   9.139  apply (erule Limit_VfromE, assumption)
   9.140  apply (blast intro:  VfromI [OF doubleton_in_Vfrom]
   9.141 @@ -216,7 +216,7 @@
   9.142  done
   9.143  
   9.144  lemma Pair_in_VLimit:
   9.145 -    "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i) |] ==> <a,b> : Vfrom(A,i)"
   9.146 +    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> <a,b> \<in> Vfrom(A,i)"
   9.147  txt{*Infer that a, b occur at ordinals x,xa < i.*}
   9.148  apply (erule Limit_VfromE, assumption)
   9.149  apply (erule Limit_VfromE, assumption)
   9.150 @@ -234,24 +234,24 @@
   9.151  lemmas nat_subset_VLimit =
   9.152       subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
   9.153  
   9.154 -lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n : Vfrom(A,i)"
   9.155 +lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
   9.156  by (blast intro: nat_subset_VLimit [THEN subsetD])
   9.157  
   9.158  subsubsection{* Closure under disjoint union *}
   9.159  
   9.160  lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
   9.161  
   9.162 -lemma one_in_VLimit: "Limit(i) ==> 1 : Vfrom(A,i)"
   9.163 +lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
   9.164  by (blast intro: nat_into_VLimit)
   9.165  
   9.166  lemma Inl_in_VLimit:
   9.167 -    "[| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"
   9.168 +    "[| a \<in> Vfrom(A,i); Limit(i) |] ==> Inl(a) \<in> Vfrom(A,i)"
   9.169  apply (unfold Inl_def)
   9.170  apply (blast intro: zero_in_VLimit Pair_in_VLimit)
   9.171  done
   9.172  
   9.173  lemma Inr_in_VLimit:
   9.174 -    "[| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"
   9.175 +    "[| b \<in> Vfrom(A,i); Limit(i) |] ==> Inr(b) \<in> Vfrom(A,i)"
   9.176  apply (unfold Inr_def)
   9.177  apply (blast intro: one_in_VLimit Pair_in_VLimit)
   9.178  done
   9.179 @@ -285,21 +285,21 @@
   9.180  
   9.181  lemma Transset_Pair_subset_VLimit:
   9.182       "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |]
   9.183 -      ==> <a,b> : Vfrom(A,i)"
   9.184 +      ==> <a,b> \<in> Vfrom(A,i)"
   9.185  apply (erule Transset_Pair_subset [THEN conjE])
   9.186  apply (erule Transset_Vfrom)
   9.187  apply (blast intro: Pair_in_VLimit)
   9.188  done
   9.189  
   9.190  lemma Union_in_Vfrom:
   9.191 -     "[| X: Vfrom(A,j);  Transset(A) |] ==> Union(X) : Vfrom(A, succ(j))"
   9.192 +     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Union(X) \<in> Vfrom(A, succ(j))"
   9.193  apply (drule Transset_Vfrom)
   9.194  apply (rule subset_mem_Vfrom)
   9.195  apply (unfold Transset_def, blast)
   9.196  done
   9.197  
   9.198  lemma Union_in_VLimit:
   9.199 -     "[| X: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) : Vfrom(A,i)"
   9.200 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) \<in> Vfrom(A,i)"
   9.201  apply (rule Limit_VfromE, assumption+)
   9.202  apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
   9.203  done
   9.204 @@ -312,10 +312,10 @@
   9.205  
   9.206  text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*}
   9.207  lemma in_VLimit:
   9.208 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);
   9.209 -      !!x y j. [| j<i; 1:j; x: Vfrom(A,j); y: Vfrom(A,j) |]
   9.210 -               ==> EX k. h(x,y): Vfrom(A,k) & k<i |]
   9.211 -   ==> h(a,b) : Vfrom(A,i)"
   9.212 +  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);
   9.213 +      !!x y j. [| j<i; 1:j; x \<in> Vfrom(A,j); y \<in> Vfrom(A,j) |]
   9.214 +               ==> EX k. h(x,y) \<in> Vfrom(A,k) & k<i |]
   9.215 +   ==> h(a,b) \<in> Vfrom(A,i)"
   9.216  txt{*Infer that a, b occur at ordinals x,xa < i.*}
   9.217  apply (erule Limit_VfromE, assumption)
   9.218  apply (erule Limit_VfromE, assumption, atomize)
   9.219 @@ -329,8 +329,8 @@
   9.220  subsubsection{* products *}
   9.221  
   9.222  lemma prod_in_Vfrom:
   9.223 -    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |]
   9.224 -     ==> a*b : Vfrom(A, succ(succ(succ(j))))"
   9.225 +    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
   9.226 +     ==> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
   9.227  apply (drule Transset_Vfrom)
   9.228  apply (rule subset_mem_Vfrom)
   9.229  apply (unfold Transset_def)
   9.230 @@ -338,8 +338,8 @@
   9.231  done
   9.232  
   9.233  lemma prod_in_VLimit:
   9.234 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.235 -   ==> a*b : Vfrom(A,i)"
   9.236 +  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.237 +   ==> a*b \<in> Vfrom(A,i)"
   9.238  apply (erule in_VLimit, assumption+)
   9.239  apply (blast intro: prod_in_Vfrom Limit_has_succ)
   9.240  done
   9.241 @@ -347,8 +347,8 @@
   9.242  subsubsection{* Disjoint sums, aka Quine ordered pairs *}
   9.243  
   9.244  lemma sum_in_Vfrom:
   9.245 -    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A);  1:j |]
   9.246 -     ==> a+b : Vfrom(A, succ(succ(succ(j))))"
   9.247 +    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
   9.248 +     ==> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
   9.249  apply (unfold sum_def)
   9.250  apply (drule Transset_Vfrom)
   9.251  apply (rule subset_mem_Vfrom)
   9.252 @@ -357,8 +357,8 @@
   9.253  done
   9.254  
   9.255  lemma sum_in_VLimit:
   9.256 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.257 -   ==> a+b : Vfrom(A,i)"
   9.258 +  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.259 +   ==> a+b \<in> Vfrom(A,i)"
   9.260  apply (erule in_VLimit, assumption+)
   9.261  apply (blast intro: sum_in_Vfrom Limit_has_succ)
   9.262  done
   9.263 @@ -366,8 +366,8 @@
   9.264  subsubsection{* function space! *}
   9.265  
   9.266  lemma fun_in_Vfrom:
   9.267 -    "[| a: Vfrom(A,j);  b: Vfrom(A,j);  Transset(A) |] ==>
   9.268 -          a->b : Vfrom(A, succ(succ(succ(succ(j)))))"
   9.269 +    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
   9.270 +          a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
   9.271  apply (unfold Pi_def)
   9.272  apply (drule Transset_Vfrom)
   9.273  apply (rule subset_mem_Vfrom)
   9.274 @@ -382,14 +382,14 @@
   9.275  done
   9.276  
   9.277  lemma fun_in_VLimit:
   9.278 -  "[| a: Vfrom(A,i);  b: Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.279 -   ==> a->b : Vfrom(A,i)"
   9.280 +  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
   9.281 +   ==> a->b \<in> Vfrom(A,i)"
   9.282  apply (erule in_VLimit, assumption+)
   9.283  apply (blast intro: fun_in_Vfrom Limit_has_succ)
   9.284  done
   9.285  
   9.286  lemma Pow_in_Vfrom:
   9.287 -    "[| a: Vfrom(A,j);  Transset(A) |] ==> Pow(a) : Vfrom(A, succ(succ(j)))"
   9.288 +    "[| a \<in> Vfrom(A,j);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A, succ(succ(j)))"
   9.289  apply (drule Transset_Vfrom)
   9.290  apply (rule subset_mem_Vfrom)
   9.291  apply (unfold Transset_def)
   9.292 @@ -397,13 +397,13 @@
   9.293  done
   9.294  
   9.295  lemma Pow_in_VLimit:
   9.296 -     "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)"
   9.297 +     "[| a \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A,i)"
   9.298  by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
   9.299  
   9.300  
   9.301  subsection{* The set Vset(i) *}
   9.302  
   9.303 -lemma Vset: "Vset(i) = (UN j:i. Pow(Vset(j)))"
   9.304 +lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
   9.305  by (subst Vfrom, blast)
   9.306  
   9.307  lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
   9.308 @@ -411,7 +411,7 @@
   9.309  
   9.310  subsubsection{* Characterisation of the elements of Vset(i) *}
   9.311  
   9.312 -lemma VsetD [rule_format]: "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i"
   9.313 +lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
   9.314  apply (erule trans_induct)
   9.315  apply (subst Vset, safe)
   9.316  apply (subst rank)
   9.317 @@ -419,21 +419,21 @@
   9.318  done
   9.319  
   9.320  lemma VsetI_lemma [rule_format]:
   9.321 -     "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)"
   9.322 +     "Ord(i) ==> \<forall>b. rank(b) \<in> i --> b \<in> Vset(i)"
   9.323  apply (erule trans_induct)
   9.324  apply (rule allI)
   9.325  apply (subst Vset)
   9.326  apply (blast intro!: rank_lt [THEN ltD])
   9.327  done
   9.328  
   9.329 -lemma VsetI: "rank(x)<i ==> x : Vset(i)"
   9.330 +lemma VsetI: "rank(x)<i ==> x \<in> Vset(i)"
   9.331  by (blast intro: VsetI_lemma elim: ltE)
   9.332  
   9.333  text{*Merely a lemma for the next result*}
   9.334 -lemma Vset_Ord_rank_iff: "Ord(i) ==> b : Vset(i) <-> rank(b) < i"
   9.335 +lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
   9.336  by (blast intro: VsetD VsetI)
   9.337  
   9.338 -lemma Vset_rank_iff [simp]: "b : Vset(a) <-> rank(b) < rank(a)"
   9.339 +lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
   9.340  apply (rule Vfrom_rank_eq [THEN subst])
   9.341  apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
   9.342  done
   9.343 @@ -450,7 +450,7 @@
   9.344                      Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
   9.345  done
   9.346  
   9.347 -subsubsection{* Lemmas for reasoning about sets in terms of their elements' ranks *}
   9.348 +subsubsection{* Reasoning about sets in terms of their elements' ranks *}
   9.349  
   9.350  lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
   9.351  apply (rule subsetI)
   9.352 @@ -527,12 +527,12 @@
   9.353  
   9.354  subsubsection{* univ(A) as a limit *}
   9.355  
   9.356 -lemma univ_eq_UN: "univ(A) = (UN i:nat. Vfrom(A,i))"
   9.357 +lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
   9.358  apply (unfold univ_def)
   9.359  apply (rule Limit_nat [THEN Limit_Vfrom_eq])
   9.360  done
   9.361  
   9.362 -lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"
   9.363 +lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (\<Union>i\<in>nat. c Int Vfrom(A,i))"
   9.364  apply (rule subset_UN_iff_eq [THEN iffD1])
   9.365  apply (erule univ_eq_UN [THEN subst])
   9.366  done
   9.367 @@ -558,7 +558,7 @@
   9.368  
   9.369  subsubsection{* Closure properties *}
   9.370  
   9.371 -lemma zero_in_univ: "0 : univ(A)"
   9.372 +lemma zero_in_univ: "0 \<in> univ(A)"
   9.373  apply (unfold univ_def)
   9.374  apply (rule nat_0I [THEN zero_in_Vfrom])
   9.375  done
   9.376 @@ -572,25 +572,25 @@
   9.377  
   9.378  subsubsection{* Closure under unordered and ordered pairs *}
   9.379  
   9.380 -lemma singleton_in_univ: "a: univ(A) ==> {a} : univ(A)"
   9.381 +lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
   9.382  apply (unfold univ_def)
   9.383  apply (blast intro: singleton_in_VLimit Limit_nat)
   9.384  done
   9.385  
   9.386  lemma doubleton_in_univ:
   9.387 -    "[| a: univ(A);  b: univ(A) |] ==> {a,b} : univ(A)"
   9.388 +    "[| a: univ(A);  b: univ(A) |] ==> {a,b} \<in> univ(A)"
   9.389  apply (unfold univ_def)
   9.390  apply (blast intro: doubleton_in_VLimit Limit_nat)
   9.391  done
   9.392  
   9.393  lemma Pair_in_univ:
   9.394 -    "[| a: univ(A);  b: univ(A) |] ==> <a,b> : univ(A)"
   9.395 +    "[| a: univ(A);  b: univ(A) |] ==> <a,b> \<in> univ(A)"
   9.396  apply (unfold univ_def)
   9.397  apply (blast intro: Pair_in_VLimit Limit_nat)
   9.398  done
   9.399  
   9.400  lemma Union_in_univ:
   9.401 -     "[| X: univ(A);  Transset(A) |] ==> Union(X) : univ(A)"
   9.402 +     "[| X: univ(A);  Transset(A) |] ==> Union(X) \<in> univ(A)"
   9.403  apply (unfold univ_def)
   9.404  apply (blast intro: Union_in_VLimit Limit_nat)
   9.405  done
   9.406 @@ -613,13 +613,13 @@
   9.407  
   9.408  subsubsection{* instances for 1 and 2 *}
   9.409  
   9.410 -lemma one_in_univ: "1 : univ(A)"
   9.411 +lemma one_in_univ: "1 \<in> univ(A)"
   9.412  apply (unfold univ_def)
   9.413  apply (rule Limit_nat [THEN one_in_VLimit])
   9.414  done
   9.415  
   9.416  text{*unused!*}
   9.417 -lemma two_in_univ: "2 : univ(A)"
   9.418 +lemma two_in_univ: "2 \<in> univ(A)"
   9.419  by (blast intro: nat_into_univ)
   9.420  
   9.421  lemma bool_subset_univ: "bool <= univ(A)"
   9.422 @@ -632,12 +632,12 @@
   9.423  
   9.424  subsubsection{* Closure under disjoint union *}
   9.425  
   9.426 -lemma Inl_in_univ: "a: univ(A) ==> Inl(a) : univ(A)"
   9.427 +lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
   9.428  apply (unfold univ_def)
   9.429  apply (erule Inl_in_VLimit [OF _ Limit_nat])
   9.430  done
   9.431  
   9.432 -lemma Inr_in_univ: "b: univ(A) ==> Inr(b) : univ(A)"
   9.433 +lemma Inr_in_univ: "b: univ(A) ==> Inr(b) \<in> univ(A)"
   9.434  apply (unfold univ_def)
   9.435  apply (erule Inr_in_VLimit [OF _ Limit_nat])
   9.436  done
   9.437 @@ -728,7 +728,7 @@
   9.438  done
   9.439  
   9.440  lemma FiniteFun_in_univ:
   9.441 -     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f : univ(A)"
   9.442 +     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f \<in> univ(A)"
   9.443  by (erule FiniteFun_univ [THEN subsetD], assumption)
   9.444  
   9.445  text{*Remove <= from the rule above*}
   9.446 @@ -741,25 +741,25 @@
   9.447  
   9.448  text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
   9.449  lemma doubleton_in_Vfrom_D:
   9.450 -     "[| {a,b} : Vfrom(X,succ(i));  Transset(X) |]
   9.451 -      ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)"
   9.452 +     "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
   9.453 +      ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
   9.454  by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], 
   9.455      assumption, fast)
   9.456  
   9.457  text{*This weaker version says a, b exist at the same level*}
   9.458  lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
   9.459  
   9.460 -(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i)
   9.461 -      implies a, b : Vfrom(X,i), which is useless for induction.
   9.462 -    Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i)))
   9.463 -      implies a, b : Vfrom(X,i), leaving the succ(i) case untreated.
   9.464 +(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
   9.465 +      implies a, b \<in> Vfrom(X,i), which is useless for induction.
   9.466 +    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
   9.467 +      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
   9.468      The combination gives a reduction by precisely one level, which is
   9.469        most convenient for proofs.
   9.470  **)
   9.471  
   9.472  lemma Pair_in_Vfrom_D:
   9.473 -    "[| <a,b> : Vfrom(X,succ(i));  Transset(X) |]
   9.474 -     ==> a: Vfrom(X,i)  &  b: Vfrom(X,i)"
   9.475 +    "[| <a,b> \<in> Vfrom(X,succ(i));  Transset(X) |]
   9.476 +     ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
   9.477  apply (unfold Pair_def)
   9.478  apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
   9.479  done