src/ZF/Constructible/Datatype_absolute.thy
changeset 13687 22dce9134953
parent 13655 95b95cdb4704
child 13702 c7cf8fa66534
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:18:23 2002 +0100
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Oct 30 12:44:18 2002 +0100
     1.3 @@ -120,16 +120,16 @@
     1.4          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
     1.5                      n, z)"
     1.6  
     1.7 +  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
     1.8 +    "is_iterates(M,isF,v,n,Z) == 
     1.9 +      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.10 +                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
    1.11 +
    1.12    iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
    1.13     "iterates_replacement(M,isF,v) ==
    1.14        \<forall>n[M]. n\<in>nat --> 
    1.15           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    1.16  
    1.17 -  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
    1.18 -    "is_iterates(M,isF,v,n,Z) == 
    1.19 -      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.20 -                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
    1.21 -
    1.22  lemma (in M_basic) iterates_MH_abs:
    1.23    "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    1.24     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"