equal
deleted
inserted
replaced
1 (* Title: ZF/univ.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
|
9 *) |
|
10 |
|
11 Univ = Arith + Sum + "mono" + |
|
12 consts |
|
13 Limit :: "i=>o" |
|
14 Vfrom :: "[i,i]=>i" |
|
15 Vset :: "i=>i" |
|
16 Vrec :: "[i, [i,i]=>i] =>i" |
|
17 univ :: "i=>i" |
|
18 |
|
19 translations |
|
20 "Vset(x)" == "Vfrom(0,x)" |
|
21 |
|
22 rules |
|
23 Limit_def "Limit(i) == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)" |
|
24 |
|
25 Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" |
|
26 |
|
27 Vrec_def |
|
28 "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). \ |
|
29 \ H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
|
30 |
|
31 univ_def "univ(A) == Vfrom(A,nat)" |
|
32 |
|
33 end |
|