equal
deleted
inserted
replaced
1 (* Title: ZF/univ.thy |
1 (* Title: ZF/Univ.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
3 Copyright 1992 University of Cambridge |
5 |
4 |
6 Standard notation for Vset(i) is V(i), but users might want V for a variable |
5 Standard notation for Vset(i) is V(i), but users might want V for a |
|
6 variable. |
7 |
7 |
8 NOTE: univ(A) could be a translation; would simplify many proofs! |
8 NOTE: univ(A) could be a translation; would simplify many proofs! |
9 But Ind_Syntax.univ refers to the constant "Univ.univ" |
9 But Ind_Syntax.univ refers to the constant "Univ.univ" |
10 *) |
10 *) |
11 |
11 |
23 |
23 |
24 |
24 |
25 definition |
25 definition |
26 Vrec :: "[i, [i,i]=>i] =>i" where |
26 Vrec :: "[i, [i,i]=>i] =>i" where |
27 "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
27 "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
28 H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
28 H(z, lam w:Vset(x). g`rank(w)`w)) ` a" |
29 |
29 |
30 definition |
30 definition |
31 Vrecursor :: "[[i,i]=>i, i] =>i" where |
31 Vrecursor :: "[[i,i]=>i, i] =>i" where |
32 "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
32 "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)). |
33 H(lam w:Vset(x). g`rank(w)`w, z)) ` a" |
33 H(lam w:Vset(x). g`rank(w)`w, z)) ` a" |
34 |
34 |
35 definition |
35 definition |
36 univ :: "i=>i" where |
36 univ :: "i=>i" where |
37 "univ(A) == Vfrom(A,nat)" |
37 "univ(A) == Vfrom(A,nat)" |
38 |
38 |