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 @@
    1.45   apply (simp_all add: relativize1_def) 
    1.46  done
    1.47  
    1.48 -(*Needed?  surely better to replace is_nat_case by nat_case?*)
    1.49 -lemma (in M_triv_axioms) is_nat_case_cong [cong]:
    1.50 +(*NOT for the simplifier.  The assumption M(z') is apparently necessary, but 
    1.51 +  causes the error "Failed congruence proof!"  It may be better to replace
    1.52 +  is_nat_case by nat_case before attempting congruence reasoning.*)
    1.53 +lemma (in M_triv_axioms) is_nat_case_cong:
    1.54       "[| a = a'; k = k';  z = z';  M(z');
    1.55         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
    1.56        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"