towards relativization of "iterates" and "wfrec"
authorpaulson
Fri Jul 12 16:41:39 2002 +0200 (2002-07-12)
changeset 133531800e7134d2e
parent 13352 3cd767f8d78b
child 13354 8c8eafb63746
towards relativization of "iterates" and "wfrec"
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 12 11:24:40 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 12 16:41:39 2002 +0200
     1.3 @@ -92,33 +92,58 @@
     1.4  
     1.5  subsection {*Absoluteness for "Iterates"*}
     1.6  
     1.7 -lemma (in M_trancl) iterates_relativize:
     1.8 -  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
     1.9 -     strong_replacement(M, 
    1.10 -       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) &
    1.11 -              M_is_recfun(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    1.12 -                          Memrel(succ(n)), x, g) &
    1.13 -              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
    1.14 -   ==> iterates(F,n,v) = z <-> 
    1.15 -       (\<exists>g[M]. is_recfun(Memrel(succ(n)), n, 
    1.16 -                             \<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n), g) &
    1.17 -            z = nat_case(v, \<lambda>m. F(g`m), n))"
    1.18 -by (simp add: iterates_nat_def recursor_def transrec_def 
    1.19 -              eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
    1.20 -              wf_Memrel trans_Memrel relation_Memrel
    1.21 -              is_recfun_abs [of "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.22 +constdefs
    1.23 +
    1.24 +  iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
    1.25 +   "iterates_MH(M,isF,v,n,g,z) ==
    1.26 +        is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
    1.27 +                    n, z)"
    1.28 +
    1.29 +  iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
    1.30 +   "iterates_replacement(M,isF,v) ==
    1.31 +      \<forall>n[M]. n\<in>nat -->
    1.32 +         wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
    1.33 +
    1.34 +lemma (in M_axioms) iterates_MH_abs:
    1.35 +  "[| relativize1(M,isF,F); M(n); M(g); M(z) |] 
    1.36 +   ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.37 +apply (simp add: iterates_MH_def) 
    1.38 +apply (rule nat_case_abs) 
    1.39 +apply (simp_all add: relativize1_def) 
    1.40 +done
    1.41 +
    1.42 +
    1.43 +lemma (in M_axioms) iterates_imp_wfrec_replacement:
    1.44 +  "[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|] 
    1.45 +   ==> wfrec_replacement(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    1.46 +                       Memrel(succ(n)))" 
    1.47 +by (simp add: iterates_replacement_def iterates_MH_abs)
    1.48 +
    1.49 +theorem (in M_trancl) iterates_abs:
    1.50 +  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    1.51 +      n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |] 
    1.52 +   ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
    1.53 +       z = iterates(F,n,v)" 
    1.54 +apply (frule iterates_imp_wfrec_replacement, assumption+)
    1.55 +apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    1.56 +                 relativize2_def iterates_MH_abs 
    1.57 +                 iterates_nat_def recursor_def transrec_def 
    1.58 +                 eclose_sing_Ord_eq nat_into_M
    1.59 +         trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.60 +done
    1.61 +
    1.62  
    1.63  lemma (in M_wfrank) iterates_closed [intro,simp]:
    1.64 -  "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
    1.65 -     strong_replacement(M, 
    1.66 -       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
    1.67 -              is_recfun (Memrel(succ(n)), x,
    1.68 -                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
    1.69 -              y = nat_case(v, \<lambda>m. F(g`m), x))|] 
    1.70 +  "[| iterates_replacement(M,isF,v); relativize1(M,isF,F);
    1.71 +      n \<in> nat; M(v); \<forall>x[M]. M(F(x)) |] 
    1.72     ==> M(iterates(F,n,v))"
    1.73 -by (simp add: iterates_nat_def recursor_def transrec_def 
    1.74 -              eclose_sing_Ord_eq trans_wfrec_closed nat_into_M
    1.75 -              wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
    1.76 +apply (frule iterates_imp_wfrec_replacement, assumption+)
    1.77 +apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    1.78 +                 relativize2_def iterates_MH_abs 
    1.79 +                 iterates_nat_def recursor_def transrec_def 
    1.80 +                 eclose_sing_Ord_eq nat_into_M
    1.81 +         trans_wfrec_closed [of _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.82 +done
    1.83  
    1.84  
    1.85  constdefs
    1.86 @@ -127,60 +152,43 @@
    1.87          \<exists>n1[M]. \<exists>AX[M]. 
    1.88           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
    1.89  
    1.90 -  list_functor_case :: "[i=>o,i,i,i,i] => o"
    1.91 -    --{*Abbreviation for the definition of lists below*}
    1.92 -    "list_functor_case(M,A,g,x,y) == 
    1.93 -        is_nat_case(M, 0, 
    1.94 -             \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & is_list_functor(M,A,gm,u),
    1.95 -             x, y)"
    1.96 -
    1.97  lemma (in M_axioms) list_functor_abs [simp]: 
    1.98       "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
    1.99  by (simp add: is_list_functor_def singleton_0 nat_into_M)
   1.100  
   1.101 -lemma (in M_axioms) list_functor_case_abs: 
   1.102 -     "[| M(A); M(n); M(y); M(g) |] 
   1.103 -      ==> list_functor_case(M,A,g,n,y) <-> 
   1.104 -          y = nat_case(0, \<lambda>m. {0} + A * g`m, n)"
   1.105 -by (simp add: list_functor_case_def nat_into_M)
   1.106 -
   1.107  
   1.108  locale M_datatypes = M_wfrank +
   1.109 -  assumes list_replacement1: 
   1.110 -       "[|M(A); n \<in> nat|] ==> 
   1.111 -	strong_replacement(M, 
   1.112 -	  \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
   1.113 -		 pair(M,x,y,z) & successor(M,n,sucn) & 
   1.114 -		 membership(M,sucn,memr) &
   1.115 -		 M_is_recfun(M, \<lambda>n f z. list_functor_case(M,A,f,n,z), 
   1.116 -                             memr, x, g) &
   1.117 -                 list_functor_case(M,A,g,x,y))"
   1.118 -(*THEY NEED RELATIVIZATION*)
   1.119 -      and list_replacement2: 
   1.120 -           "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
   1.121 + assumes list_replacement1: 
   1.122 +   "M(A) ==> \<exists>zero[M]. empty(M,zero) & 
   1.123 +		       iterates_replacement(M, is_list_functor(M,A), zero)"
   1.124 +  and list_replacement2: 
   1.125 +   "M(A) ==> 
   1.126 +    \<exists>zero[M]. empty(M,zero) & 
   1.127 +	      strong_replacement(M, 
   1.128 +         \<lambda>n y. n\<in>nat & 
   1.129 +               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.130 +               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), zero), 
   1.131 +                        msn, n, y)))"
   1.132  
   1.133 -
   1.134 -
   1.135 -lemma (in M_datatypes) list_replacement1':
   1.136 -  "[|M(A); n \<in> nat|]
   1.137 -   ==> strong_replacement
   1.138 -	  (M, \<lambda>x z. \<exists>y[M]. z = \<langle>x,y\<rangle> &
   1.139 -               (\<exists>g[M]. is_recfun (Memrel(succ(n)), x,
   1.140 -		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
   1.141 - 	       y = nat_case(0, \<lambda>m. {0} + A * g ` m, x)))"
   1.142 -apply (insert list_replacement1 [of A n], simp add: nat_into_M)
   1.143 -apply (simp add: nat_into_M list_functor_case_abs
   1.144 -                 is_recfun_abs [of "\<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n)"])
   1.145 +lemma (in M_datatypes) list_replacement1': 
   1.146 +   "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
   1.147 +apply (insert list_replacement1, simp) 
   1.148  done
   1.149  
   1.150  lemma (in M_datatypes) list_replacement2': 
   1.151 -  "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
   1.152 -by (insert list_replacement2, simp add: nat_into_M) 
   1.153 -
   1.154 +  "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
   1.155 +apply (insert list_replacement2 [of A]) 
   1.156 +apply (rule strong_replacement_cong [THEN iffD1])  
   1.157 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
   1.158 +apply (simp_all add: list_replacement1' relativize1_def) 
   1.159 +done
   1.160  
   1.161  lemma (in M_datatypes) list_closed [intro,simp]:
   1.162       "M(A) ==> M(list(A))"
   1.163 -by (simp add: list_eq_Union list_replacement1' list_replacement2')
   1.164 +apply (insert list_replacement1)
   1.165 +by  (simp add: RepFun_closed2 list_eq_Union 
   1.166 +               list_replacement2' relativize1_def
   1.167 +               iterates_closed [of "is_list_functor(M,A)"])
   1.168  
   1.169  
   1.170  end
     2.1 --- a/src/ZF/Constructible/Relative.thy	Fri Jul 12 11:24:40 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Jul 12 16:41:39 2002 +0200
     2.3 @@ -179,6 +179,16 @@
     2.4         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
     2.5         (is_quasinat(M,k) | z=0)"
     2.6  
     2.7 +  relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
     2.8 +    "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
     2.9 +
    2.10 +  relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
    2.11 +    "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
    2.12 +
    2.13 +  relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    2.14 +    "relativize3(M,is_f,f) == 
    2.15 +       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
    2.16 +
    2.17  
    2.18  subsection {*The relativized ZF axioms*}
    2.19  constdefs
    2.20 @@ -584,7 +594,7 @@
    2.21    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
    2.22    even for f : M -> M.
    2.23  *)
    2.24 -lemma (in M_triv_axioms) RepFun_closed [intro,simp]:
    2.25 +lemma (in M_triv_axioms) RepFun_closed:
    2.26       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
    2.27        ==> M(RepFun(A,f))"
    2.28  apply (simp add: RepFun_def) 
    2.29 @@ -592,10 +602,23 @@
    2.30  apply (auto dest: transM  simp add: univalent_def) 
    2.31  done
    2.32  
    2.33 +lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
    2.34 +by simp
    2.35 +
    2.36 +text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
    2.37 +      makes relativization easier.*}
    2.38 +lemma (in M_triv_axioms) RepFun_closed2:
    2.39 +     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
    2.40 +      ==> M(RepFun(A, %x. f(x)))"
    2.41 +apply (simp add: RepFun_def)
    2.42 +apply (frule strong_replacement_closed, assumption)
    2.43 +apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
    2.44 +done
    2.45 +
    2.46  lemma (in M_triv_axioms) lam_closed [intro,simp]:
    2.47       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
    2.48        ==> M(\<lambda>x\<in>A. b(x))"
    2.49 -by (simp add: lam_def, blast dest: transM) 
    2.50 +by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
    2.51  
    2.52  lemma (in M_triv_axioms) image_abs [simp]: 
    2.53       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
    2.54 @@ -635,19 +658,18 @@
    2.55  by (auto simp add: is_quasinat_def quasinat_def)
    2.56  
    2.57  lemma (in M_triv_axioms) nat_case_abs [simp]: 
    2.58 -  assumes b_abs: "!!x y. M(x) --> M(y) --> (is_b(x,y) <-> y = b(x))"
    2.59 -  shows
    2.60 -     "[| M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    2.61 +     "[| relativize1(M,is_b,b); M(k); M(z) |] 
    2.62 +      ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    2.63  apply (case_tac "quasinat(k)") 
    2.64   prefer 2 
    2.65   apply (simp add: is_nat_case_def non_nat_case) 
    2.66   apply (force simp add: quasinat_def) 
    2.67  apply (simp add: quasinat_def is_nat_case_def)
    2.68  apply (elim disjE exE) 
    2.69 - apply (simp_all add: b_abs) 
    2.70 + apply (simp_all add: relativize1_def) 
    2.71  done
    2.72  
    2.73 -(*Needed?  surely better to replace by nat_case?*)
    2.74 +(*Needed?  surely better to replace is_nat_case by nat_case?*)
    2.75  lemma (in M_triv_axioms) is_nat_case_cong [cong]:
    2.76       "[| a = a'; k = k';  z = z';  M(z');
    2.77         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
    2.78 @@ -980,8 +1002,7 @@
    2.79  
    2.80  lemma (in M_axioms) apply_abs [simp]: 
    2.81       "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
    2.82 -apply (simp add: fun_apply_def apply_def)
    2.83 -apply (blast intro: elim:); 
    2.84 +apply (simp add: fun_apply_def apply_def, blast) 
    2.85  done
    2.86  
    2.87  lemma (in M_axioms) typed_function_abs [simp]: 
     3.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Jul 12 11:24:40 2002 +0200
     3.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Jul 12 16:41:39 2002 +0200
     3.3 @@ -261,7 +261,7 @@
     3.4        separation
     3.5  	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
     3.6  apply (insert wfrank_separation [of r])
     3.7 -apply (simp add: is_recfun_abs [of "%x. range"])
     3.8 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
     3.9  done
    3.10  
    3.11  lemma (in M_wfrank) wfrank_strong_replacement':
    3.12 @@ -270,7 +270,7 @@
    3.13  		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
    3.14  		  y = range(f))"
    3.15  apply (insert wfrank_strong_replacement [of r])
    3.16 -apply (simp add: is_recfun_abs [of "%x. range"])
    3.17 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
    3.18  done
    3.19  
    3.20  lemma (in M_wfrank) Ord_wfrank_separation':
    3.21 @@ -278,7 +278,7 @@
    3.22        separation (M, \<lambda>x. 
    3.23           ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
    3.24  apply (insert Ord_wfrank_separation [of r])
    3.25 -apply (simp add: is_recfun_abs [of "%x. range"])
    3.26 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
    3.27  done
    3.28  
    3.29  text{*This function, defined using replacement, is a rank function for
    3.30 @@ -524,19 +524,26 @@
    3.31        before we can replace @{term "r^+"} by @{term r}. *}
    3.32  theorem (in M_trancl) trans_wfrec_relativize:
    3.33    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
    3.34 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    3.35 -                pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); 
    3.36 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    3.37       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    3.38     ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
    3.39 -by (simp cong: is_recfun_cong
    3.40 -         add: wfrec_relativize trancl_eq_r
    3.41 -               is_recfun_restrict_idem domain_restrict_idem)
    3.42 +apply (frule wfrec_replacement', assumption+) 
    3.43 +apply (simp cong: is_recfun_cong
    3.44 +           add: wfrec_relativize trancl_eq_r
    3.45 +                is_recfun_restrict_idem domain_restrict_idem)
    3.46 +done
    3.47  
    3.48 +theorem (in M_trancl) trans_wfrec_abs:
    3.49 +  "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
    3.50 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    3.51 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    3.52 +   ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" 
    3.53 +apply (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
    3.54 +done
    3.55  
    3.56  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
    3.57    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
    3.58 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    3.59 -                pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); 
    3.60 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    3.61       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    3.62     ==> y = <x, wfrec(r, x, H)> <-> 
    3.63         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    3.64 @@ -566,8 +573,8 @@
    3.65  
    3.66  text{*Eliminates one instance of replacement.*}
    3.67  lemma (in M_wfrank) wfrec_replacement_iff:
    3.68 -     "strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
    3.69 -                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
    3.70 +     "strong_replacement(M, \<lambda>x z. 
    3.71 +          \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <->
    3.72        strong_replacement(M, 
    3.73             \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    3.74  apply simp 
    3.75 @@ -577,11 +584,10 @@
    3.76  text{*Useful version for transitive relations*}
    3.77  theorem (in M_wfrank) trans_wfrec_closed:
    3.78       "[|wf(r); trans(r); relation(r); M(r); M(a);
    3.79 -        strong_replacement(M, 
    3.80 -             \<lambda>x z. \<exists>y[M]. \<exists>g[M].
    3.81 -                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    3.82 +       wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    3.83          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    3.84        ==> M(wfrec(r,a,H))"
    3.85 +apply (frule wfrec_replacement', assumption+) 
    3.86  apply (frule wfrec_replacement_iff [THEN iffD1]) 
    3.87  apply (rule wfrec_closed_lemma, assumption+) 
    3.88  apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
    3.89 @@ -621,15 +627,16 @@
    3.90  text{*Full version not assuming transitivity, but maybe not very useful.*}
    3.91  theorem (in M_wfrank) wfrec_closed:
    3.92       "[|wf(r); M(r); M(a);
    3.93 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
    3.94 -          pair(M,x,y,z) & 
    3.95 -          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
    3.96 -          y = H(x, restrict(g, r -`` {x}))); 
    3.97 +        wfrec_replacement(M,MH,r^+);  
    3.98 +        relativize2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
    3.99          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   3.100        ==> M(wfrec(r,a,H))"
   3.101 -apply (frule wfrec_replacement_iff [THEN iffD1]) 
   3.102 -apply (rule wfrec_closed_lemma, assumption+) 
   3.103 -apply (simp_all add: eq_pair_wfrec_iff) 
   3.104 +apply (frule wfrec_replacement' 
   3.105 +               [of MH "r^+" "\<lambda>x f. H(x, restrict(f, r -`` {x}))"])
   3.106 +   prefer 4
   3.107 +   apply (frule wfrec_replacement_iff [THEN iffD1]) 
   3.108 +   apply (rule wfrec_closed_lemma, assumption+) 
   3.109 +     apply (simp_all add: eq_pair_wfrec_iff func.function_restrictI) 
   3.110  done
   3.111  
   3.112  end
     4.1 --- a/src/ZF/Constructible/WFrec.thy	Fri Jul 12 11:24:40 2002 +0200
     4.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Jul 12 16:41:39 2002 +0200
     4.3 @@ -275,7 +275,7 @@
     4.4  done
     4.5  
     4.6  constdefs
     4.7 - M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
     4.8 +  M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
     4.9     "M_is_recfun(M,MH,r,a,f) == 
    4.10       \<forall>z[M]. z \<in> f <-> 
    4.11              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
    4.12 @@ -283,11 +283,20 @@
    4.13                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
    4.14                 xa \<in> r & MH(x, f_r_sx, y))"
    4.15  
    4.16 +  is_wfrec :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    4.17 +   "is_wfrec(M,MH,r,a,z) == 
    4.18 +      \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)"
    4.19 +
    4.20 +  wfrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
    4.21 +   "wfrec_replacement(M,MH,r) ==
    4.22 +        strong_replacement(M, 
    4.23 +             \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & is_wfrec(M,MH,r,x,y))"
    4.24 +
    4.25  lemma (in M_axioms) is_recfun_abs:
    4.26       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
    4.27 -         \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] 
    4.28 +         relativize2(M,MH,H) |] 
    4.29        ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
    4.30 -apply (simp add: M_is_recfun_def is_recfun_relativize)
    4.31 +apply (simp add: M_is_recfun_def relativize2_def is_recfun_relativize)
    4.32  apply (rule rall_cong)
    4.33  apply (blast dest: transM)
    4.34  done
    4.35 @@ -298,7 +307,33 @@
    4.36        ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
    4.37  by (simp add: M_is_recfun_def) 
    4.38  
    4.39 +lemma (in M_axioms) is_wfrec_abs:
    4.40 +     "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
    4.41 +         relativize2(M,MH,H);  M(r); M(a); M(z) |]
    4.42 +      ==> is_wfrec(M,MH,r,a,z) <-> 
    4.43 +          (\<exists>g[M]. is_recfun(r,a,H,g) & z = H(a,g))"
    4.44 +by (simp add: is_wfrec_def relativize2_def is_recfun_abs)
    4.45  
    4.46 +text{*Relating @{term wfrec_replacement} to native constructs*}
    4.47 +lemma (in M_axioms) wfrec_replacement':
    4.48 +  "[|wfrec_replacement(M,MH,r);
    4.49 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)); 
    4.50 +     relativize2(M,MH,H);  M(r)|] 
    4.51 +   ==> strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    4.52 +                pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
    4.53 +apply (rotate_tac 1) 
    4.54 +apply (simp add: wfrec_replacement_def is_wfrec_abs) 
    4.55 +done
    4.56 +
    4.57 +lemma wfrec_replacement_cong [cong]:
    4.58 +     "[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z);
    4.59 +         r=r' |] 
    4.60 +      ==> wfrec_replacement(M, %x y. MH(x,y), r) <-> 
    4.61 +          wfrec_replacement(M, %x y. MH'(x,y), r')" 
    4.62 +by (simp add: is_wfrec_def wfrec_replacement_def) 
    4.63 +
    4.64 +
    4.65 +(*FIXME: update to use new techniques!!*)
    4.66  constdefs
    4.67   (*This expresses ordinal addition in the language of ZF.  It also 
    4.68     provides an abbreviation that can be used in the instance of strong
    4.69 @@ -367,7 +402,7 @@
    4.70  	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
    4.71  apply (frule lt_Ord) 
    4.72  apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
    4.73 -             is_recfun_abs [of "%x g. i Un g``x"]
    4.74 +             relativize2_def is_recfun_abs [of "%x g. i Un g``x"]
    4.75               image_closed is_recfun_iff_equation  
    4.76               Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
    4.77  apply (simp add: lt_def) 
    4.78 @@ -382,7 +417,7 @@
    4.79  		  (\<exists>g[M]. is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
    4.80  		  y = i Un g``x))" 
    4.81  apply (insert oadd_strong_replacement [of i j]) 
    4.82 -apply (simp add: is_oadd_fun_def is_recfun_abs [of "%x g. i Un g``x"])  
    4.83 +apply (simp add: is_oadd_fun_def relativize2_def is_recfun_abs [of "%x g. i Un g``x"])  
    4.84  done
    4.85  
    4.86