author  wenzelm 
Tue, 12 Jan 1999 15:17:37 +0100  
changeset 6093  87bf8c03b169 
parent 6053  8a1059aa01f0 
child 9395  1c9851cdfe9f 
permissions  rwrr 
1478  1 
(* Title: ZF/univ.thy 
0  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
The cumulative hierarchy and a small universe for recursive types 

7 

8 
Standard notation for Vset(i) is V(i), but users might want V for a variable 

516  9 

10 
NOTE: univ(A) could be a translation; would simplify many proofs! 

6093  11 
But Ind_Syntax.univ refers to the constant "Univ.univ" 
0  12 
*) 
13 

2469  14 
Univ = Arith + Sum + Finite + mono + 
3923  15 

0  16 
consts 
1401  17 
Vfrom :: [i,i]=>i 
18 
Vset :: i=>i 

19 
Vrec :: [i, [i,i]=>i] =>i 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset

20 
Vrecursor :: [[i,i]=>i, i] =>i 
1401  21 
univ :: i=>i 
0  22 

23 
translations 

1478  24 
"Vset(x)" == "Vfrom(0,x)" 
0  25 

3923  26 

753  27 
defs 
0  28 
Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" 
29 

30 
Vrec_def 

1478  31 
"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). 
1155  32 
H(z, lam w:Vset(x). g`rank(w)`w)) ` a" 
0  33 

6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset

34 
Vrecursor_def 
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset

35 
"Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)). 
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset

36 
H(lam w:Vset(x). g`rank(w)`w, z)) ` a" 
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3940
diff
changeset

37 

0  38 
univ_def "univ(A) == Vfrom(A,nat)" 
39 

40 
end 