src/ZF/Epsilon.thy
changeset 13615 449a70d88b38
parent 13524 604d0f3622d6
child 13784 b9f6154427a4
     1.1 --- a/src/ZF/Epsilon.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -11,13 +11,13 @@
     1.4  
     1.5  constdefs
     1.6    eclose    :: "i=>i"
     1.7 -    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
     1.8 +    "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. Union(r))"
     1.9  
    1.10    transrec  :: "[i, [i,i]=>i] =>i"
    1.11      "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    1.12   
    1.13    rank      :: "i=>i"
    1.14 -    "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
    1.15 +    "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
    1.16  
    1.17    transrec2 :: "[i, i, [i,i]=>i] =>i"
    1.18      "transrec2(k, a, b) ==                     
    1.19 @@ -25,7 +25,7 @@
    1.20                  %i r. if(i=0, a, 
    1.21                          if(EX j. i=succ(j),        
    1.22                             b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    1.23 -                           UN j<i. r`j)))"
    1.24 +                           \<Union>j<i. r`j)))"
    1.25  
    1.26    recursor  :: "[i, [i,i]=>i, i]=>i"
    1.27      "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    1.28 @@ -216,7 +216,7 @@
    1.29  subsection{*Rank*}
    1.30  
    1.31  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    1.32 -lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
    1.33 +lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))"
    1.34  by (subst rank_def [THEN def_transrec], simp)
    1.35  
    1.36  lemma Ord_rank [simp]: "Ord(rank(a))"
    1.37 @@ -268,7 +268,7 @@
    1.38  apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
    1.39  done
    1.40  
    1.41 -lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
    1.42 +lemma rank_Union: "rank(Union(A)) = (\<Union>x\<in>A. rank(x))"
    1.43  apply (rule equalityI)
    1.44  apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
    1.45  apply (erule_tac [2] Union_upper)
    1.46 @@ -350,7 +350,7 @@
    1.47  done
    1.48  
    1.49  lemma transrec2_Limit:
    1.50 -     "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
    1.51 +     "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
    1.52  apply (rule transrec2_def [THEN def_transrec, THEN trans])
    1.53  apply (auto simp add: OUnion_def) 
    1.54  done
    1.55 @@ -359,7 +359,7 @@
    1.56       "(!!x. f(x)==transrec2(x,a,b))
    1.57        ==> f(0) = a & 
    1.58            f(succ(i)) = b(i, f(i)) & 
    1.59 -          (Limit(K) --> f(K) = (UN j<K. f(j)))"
    1.60 +          (Limit(K) --> f(K) = (\<Union>j<K. f(j)))"
    1.61  by (simp add: transrec2_Limit)
    1.62  
    1.63