src/ZF/Constructible/Datatype_absolute.thy
changeset 13348 374d05460db4
parent 13339 0f89104dd377
child 13350 626b79677dfa
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 11 10:48:30 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 11 13:43:24 2002 +0200
     1.3 @@ -121,7 +121,6 @@
     1.4                wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
     1.5  
     1.6  
     1.7 -
     1.8  locale M_datatypes = M_wfrank +
     1.9  (*THEY NEED RELATIVIZATION*)
    1.10    assumes list_replacement1: 
    1.11 @@ -133,7 +132,7 @@
    1.12  		     is_recfun (memr, x,
    1.13  				\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
    1.14  		     y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
    1.15 -      and list_replacement2': 
    1.16 +      and list_replacement2: 
    1.17             "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
    1.18  
    1.19  
    1.20 @@ -146,6 +145,10 @@
    1.21   	       z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x)))"
    1.22  by (insert list_replacement1, simp add: nat_into_M) 
    1.23  
    1.24 +lemma (in M_datatypes) list_replacement2': 
    1.25 +  "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A \<times> X)^x (0))"
    1.26 +by (insert list_replacement2, simp add: nat_into_M) 
    1.27 +
    1.28  
    1.29  lemma (in M_datatypes) list_closed [intro,simp]:
    1.30       "M(A) ==> M(list(A))"