src/ZF/Epsilon.thy
author paulson
Fri Jan 03 15:01:55 1997 +0100 (1997-01-03)
changeset 2469 b50b8c0eec01
parent 1478 2b8c2a7547ab
child 6070 032babd0120b
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
clasohm@1478
     1
(*  Title:      ZF/epsilon.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Epsilon induction and recursion
clasohm@0
     7
*)
clasohm@0
     8
paulson@2469
     9
Epsilon = Nat + mono +
paulson@2469
    10
constdefs
paulson@2469
    11
  eclose    :: i=>i
paulson@2469
    12
    "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
clasohm@0
    13
paulson@2469
    14
  transrec  :: [i, [i,i]=>i] =>i
paulson@2469
    15
    "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
paulson@2469
    16
 
paulson@2469
    17
  rank      :: i=>i
paulson@2469
    18
    "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
paulson@2469
    19
paulson@2469
    20
  transrec2 :: [i, i, [i,i]=>i] =>i
paulson@2469
    21
    "transrec2(k, a, b) ==                     
paulson@2469
    22
       transrec(k, 
paulson@2469
    23
                %i r. if(i=0, a, 
paulson@2469
    24
                        if(EX j. i=succ(j),        
paulson@2469
    25
                           b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
paulson@2469
    26
                           UN j<i. r`j)))"
paulson@2469
    27
clasohm@0
    28
end