src/ZF/Constructible/WF_absolute.thy
changeset 13353 1800e7134d2e
parent 13352 3cd767f8d78b
child 13363 c26eeb000470
     1.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Jul 12 11:24:40 2002 +0200
     1.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Jul 12 16:41:39 2002 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4        separation
     1.5  	   (M, \<lambda>x. ~ (\<exists>f[M]. is_recfun(r^+, x, %x f. range(f), f)))"
     1.6  apply (insert wfrank_separation [of r])
     1.7 -apply (simp add: is_recfun_abs [of "%x. range"])
     1.8 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
     1.9  done
    1.10  
    1.11  lemma (in M_wfrank) wfrank_strong_replacement':
    1.12 @@ -270,7 +270,7 @@
    1.13  		  pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) &
    1.14  		  y = range(f))"
    1.15  apply (insert wfrank_strong_replacement [of r])
    1.16 -apply (simp add: is_recfun_abs [of "%x. range"])
    1.17 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
    1.18  done
    1.19  
    1.20  lemma (in M_wfrank) Ord_wfrank_separation':
    1.21 @@ -278,7 +278,7 @@
    1.22        separation (M, \<lambda>x. 
    1.23           ~ (\<forall>f[M]. is_recfun(r^+, x, \<lambda>x. range, f) --> Ord(range(f))))" 
    1.24  apply (insert Ord_wfrank_separation [of r])
    1.25 -apply (simp add: is_recfun_abs [of "%x. range"])
    1.26 +apply (simp add: relativize2_def is_recfun_abs [of "%x. range"])
    1.27  done
    1.28  
    1.29  text{*This function, defined using replacement, is a rank function for
    1.30 @@ -524,19 +524,26 @@
    1.31        before we can replace @{term "r^+"} by @{term r}. *}
    1.32  theorem (in M_trancl) trans_wfrec_relativize:
    1.33    "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);
    1.34 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    1.35 -                pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); 
    1.36 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    1.37       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.38     ==> wfrec(r,a,H) = z <-> (\<exists>f[M]. is_recfun(r,a,H,f) & z = H(a,f))" 
    1.39 -by (simp cong: is_recfun_cong
    1.40 -         add: wfrec_relativize trancl_eq_r
    1.41 -               is_recfun_restrict_idem domain_restrict_idem)
    1.42 +apply (frule wfrec_replacement', assumption+) 
    1.43 +apply (simp cong: is_recfun_cong
    1.44 +           add: wfrec_relativize trancl_eq_r
    1.45 +                is_recfun_restrict_idem domain_restrict_idem)
    1.46 +done
    1.47  
    1.48 +theorem (in M_trancl) trans_wfrec_abs:
    1.49 +  "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
    1.50 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    1.51 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.52 +   ==> is_wfrec(M,MH,r,a,z) <-> z=wfrec(r,a,H)" 
    1.53 +apply (simp add: trans_wfrec_relativize [THEN iff_sym] is_wfrec_abs, blast) 
    1.54 +done
    1.55  
    1.56  lemma (in M_trancl) trans_eq_pair_wfrec_iff:
    1.57    "[|wf(r);  trans(r); relation(r); M(r);  M(y); 
    1.58 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. 
    1.59 -                pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))); 
    1.60 +     wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    1.61       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.62     ==> y = <x, wfrec(r, x, H)> <-> 
    1.63         (\<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    1.64 @@ -566,8 +573,8 @@
    1.65  
    1.66  text{*Eliminates one instance of replacement.*}
    1.67  lemma (in M_wfrank) wfrec_replacement_iff:
    1.68 -     "strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M]. 
    1.69 -                pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <->
    1.70 +     "strong_replacement(M, \<lambda>x z. 
    1.71 +          \<exists>y[M]. pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g))) <->
    1.72        strong_replacement(M, 
    1.73             \<lambda>x y. \<exists>f[M]. is_recfun(r,x,H,f) & y = <x, H(x,f)>)"
    1.74  apply simp 
    1.75 @@ -577,11 +584,10 @@
    1.76  text{*Useful version for transitive relations*}
    1.77  theorem (in M_wfrank) trans_wfrec_closed:
    1.78       "[|wf(r); trans(r); relation(r); M(r); M(a);
    1.79 -        strong_replacement(M, 
    1.80 -             \<lambda>x z. \<exists>y[M]. \<exists>g[M].
    1.81 -                    pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
    1.82 +       wfrec_replacement(M,MH,r);  relativize2(M,MH,H);
    1.83          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
    1.84        ==> M(wfrec(r,a,H))"
    1.85 +apply (frule wfrec_replacement', assumption+) 
    1.86  apply (frule wfrec_replacement_iff [THEN iffD1]) 
    1.87  apply (rule wfrec_closed_lemma, assumption+) 
    1.88  apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
    1.89 @@ -621,15 +627,16 @@
    1.90  text{*Full version not assuming transitivity, but maybe not very useful.*}
    1.91  theorem (in M_wfrank) wfrec_closed:
    1.92       "[|wf(r); M(r); M(a);
    1.93 -     strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
    1.94 -          pair(M,x,y,z) & 
    1.95 -          is_recfun(r^+, x, \<lambda>x f. H(x, restrict(f, r -`` {x})), g) & 
    1.96 -          y = H(x, restrict(g, r -`` {x}))); 
    1.97 +        wfrec_replacement(M,MH,r^+);  
    1.98 +        relativize2(M,MH, \<lambda>x f. H(x, restrict(f, r -`` {x})));
    1.99          \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |] 
   1.100        ==> M(wfrec(r,a,H))"
   1.101 -apply (frule wfrec_replacement_iff [THEN iffD1]) 
   1.102 -apply (rule wfrec_closed_lemma, assumption+) 
   1.103 -apply (simp_all add: eq_pair_wfrec_iff) 
   1.104 +apply (frule wfrec_replacement' 
   1.105 +               [of MH "r^+" "\<lambda>x f. H(x, restrict(f, r -`` {x}))"])
   1.106 +   prefer 4
   1.107 +   apply (frule wfrec_replacement_iff [THEN iffD1]) 
   1.108 +   apply (rule wfrec_closed_lemma, assumption+) 
   1.109 +     apply (simp_all add: eq_pair_wfrec_iff func.function_restrictI) 
   1.110  done
   1.111  
   1.112  end