src/ZF/Epsilon.thy
changeset 2469 b50b8c0eec01
parent 1478 2b8c2a7547ab
child 6070 032babd0120b
     1.1 --- a/src/ZF/Epsilon.thy	Fri Jan 03 10:48:28 1997 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Fri Jan 03 15:01:55 1997 +0100
     1.3 @@ -6,13 +6,23 @@
     1.4  Epsilon induction and recursion
     1.5  *)
     1.6  
     1.7 -Epsilon = Nat + "mono" +
     1.8 -consts
     1.9 -    eclose,rank ::      i=>i
    1.10 -    transrec    ::      [i, [i,i]=>i] =>i
    1.11 +Epsilon = Nat + mono +
    1.12 +constdefs
    1.13 +  eclose    :: i=>i
    1.14 +    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    1.15  
    1.16 -defs
    1.17 -  eclose_def    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    1.18 -  transrec_def  "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    1.19 -  rank_def      "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
    1.20 +  transrec  :: [i, [i,i]=>i] =>i
    1.21 +    "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
    1.22 + 
    1.23 +  rank      :: i=>i
    1.24 +    "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
    1.25 +
    1.26 +  transrec2 :: [i, i, [i,i]=>i] =>i
    1.27 +    "transrec2(k, a, b) ==                     
    1.28 +       transrec(k, 
    1.29 +                %i r. if(i=0, a, 
    1.30 +                        if(EX j. i=succ(j),        
    1.31 +                           b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    1.32 +                           UN j<i. r`j)))"
    1.33 +
    1.34  end