src/ZF/Constructible/Datatype_absolute.thy
changeset 13363 c26eeb000470
parent 13353 1800e7134d2e
child 13382 b37764a46b16
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 16:28:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 16:29:36 2002 +0200
     1.3 @@ -101,17 +101,14 @@
     1.4  
     1.5    iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
     1.6     "iterates_replacement(M,isF,v) ==
     1.7 -      \<forall>n[M]. n\<in>nat -->
     1.8 +      \<forall>n[M]. n\<in>nat --> 
     1.9           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    1.10  
    1.11  lemma (in M_axioms) iterates_MH_abs:
    1.12    "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    1.13     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.14 -apply (simp add: iterates_MH_def) 
    1.15 -apply (rule nat_case_abs) 
    1.16 -apply (simp_all add: relativize1_def) 
    1.17 -done
    1.18 -
    1.19 +by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
    1.20 +              relativize1_def iterates_MH_def)  
    1.21  
    1.22  lemma (in M_axioms) iterates_imp_wfrec_replacement:
    1.23    "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.24 @@ -159,28 +156,20 @@
    1.25  
    1.26  locale M_datatypes = M_wfrank +
    1.27   assumes list_replacement1: 
    1.28 -   "M(A) ==> \<exists>zero[M]. empty(M,zero) & 
    1.29 -		       iterates_replacement(M, is_list_functor(M,A), zero)"
    1.30 +   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.31    and list_replacement2: 
    1.32 -   "M(A) ==> 
    1.33 -    \<exists>zero[M]. empty(M,zero) & 
    1.34 -	      strong_replacement(M, 
    1.35 +   "M(A) ==> strong_replacement(M, 
    1.36           \<lambda>n y. n\<in>nat & 
    1.37                 (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.38 -               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), zero), 
    1.39 +               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), 
    1.40                          msn, n, y)))"
    1.41  
    1.42 -lemma (in M_datatypes) list_replacement1': 
    1.43 -   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.44 -apply (insert list_replacement1, simp) 
    1.45 -done
    1.46 -
    1.47  lemma (in M_datatypes) list_replacement2': 
    1.48    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
    1.49  apply (insert list_replacement2 [of A]) 
    1.50  apply (rule strong_replacement_cong [THEN iffD1])  
    1.51  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
    1.52 -apply (simp_all add: list_replacement1' relativize1_def) 
    1.53 +apply (simp_all add: list_replacement1 relativize1_def) 
    1.54  done
    1.55  
    1.56  lemma (in M_datatypes) list_closed [intro,simp]: