src/ZF/Constructible/Relative.thy
 changeset 13363 c26eeb000470 parent 13353 1800e7134d2e child 13382 b37764a46b16
```     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Jul 16 16:28:49 2002 +0200
1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Jul 16 16:29:36 2002 +0200
1.3 @@ -28,6 +28,15 @@
1.4    successor :: "[i=>o,i,i] => o"
1.5      "successor(M,a,z) == is_cons(M,a,a,z)"
1.6
1.7 +  number1 :: "[i=>o,i] => o"
1.8 +    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
1.9 +
1.10 +  number2 :: "[i=>o,i] => o"
1.11 +    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
1.12 +
1.13 +  number3 :: "[i=>o,i] => o"
1.14 +    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
1.15 +
1.16    powerset :: "[i=>o,i,i] => o"
1.17      "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
1.18
1.19 @@ -161,15 +170,6 @@
1.20      --{*omega is a limit ordinal none of whose elements are limit*}
1.21      "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
1.22
1.23 -  number1 :: "[i=>o,i] => o"
1.24 -    "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
1.25 -
1.26 -  number2 :: "[i=>o,i] => o"
1.27 -    "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
1.28 -
1.29 -  number3 :: "[i=>o,i] => o"
1.30 -    "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
1.31 -
1.32    is_quasinat :: "[i=>o,i] => o"
1.33      "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
1.34
1.35 @@ -177,7 +177,7 @@
1.36      "is_nat_case(M, a, is_b, k, z) ==
1.37         (empty(M,k) --> z=a) &
1.38         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
1.39 -       (is_quasinat(M,k) | z=0)"
1.40 +       (is_quasinat(M,k) | empty(M,z))"
1.41
1.42    relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
1.43      "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
1.44 @@ -669,8 +669,10 @@