src/ZF/Constructible/Rec_Separation.thy
changeset 13352 3cd767f8d78b
parent 13348 374d05460db4
child 13363 c26eeb000470
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 11 17:56:28 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Jul 12 11:24:40 2002 +0200
     1.3 @@ -196,8 +196,8 @@
     1.4  
     1.5  subsection{*Well-Founded Recursion!*}
     1.6  
     1.7 -(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o"
     1.8 -   "M_is_recfun(M,r,a,MH,f) == 
     1.9 +(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    1.10 +   "M_is_recfun(M,MH,r,a,f) == 
    1.11       \<forall>z[M]. z \<in> f <-> 
    1.12              5      4       3       2       1           0
    1.13              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
    1.14 @@ -252,7 +252,7 @@
    1.15    shows 
    1.16        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.17         ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> 
    1.18 -           M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))"
    1.19 +           M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
    1.20  by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
    1.21  
    1.22  lemma is_recfun_iff_sats:
    1.23 @@ -261,15 +261,15 @@
    1.24                          sats(A, p(x,y,z), env));
    1.25        nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.26        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.27 -   ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
    1.28 +   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
    1.29  by (simp add: sats_is_recfun_fm [of A MH])
    1.30  
    1.31  theorem is_recfun_reflection:
    1.32    assumes MH_reflection:
    1.33      "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
    1.34                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
    1.35 -  shows "REFLECTS[\<lambda>x. M_is_recfun(L, f(x), g(x), MH(L), h(x)), 
    1.36 -               \<lambda>i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]"
    1.37 +  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), 
    1.38 +               \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
    1.39  apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
    1.40  apply (intro FOL_reflections function_reflections 
    1.41               restriction_reflection MH_reflection)  
    1.42 @@ -279,15 +279,17 @@
    1.43  
    1.44  lemma wfrank_Reflects:
    1.45   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.46 -              ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)),
    1.47 +              ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
    1.48        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
    1.49 -         ~ (\<exists>f \<in> Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]"
    1.50 +         ~ (\<exists>f \<in> Lset(i). 
    1.51 +            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), 
    1.52 +                        rplus, x, f))]"
    1.53  by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)  
    1.54  
    1.55  lemma wfrank_separation:
    1.56       "L(r) ==>
    1.57        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.58 -         ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))"
    1.59 +         ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    1.60  apply (rule separation_CollectI) 
    1.61  apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
    1.62  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
    1.63 @@ -309,12 +311,12 @@
    1.64   "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
    1.65          (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.66           (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
    1.67 -                        M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
    1.68 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    1.69                          is_range(L,f,y))),
    1.70   \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & 
    1.71        (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
    1.72         (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  & 
    1.73 -         M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) &
    1.74 +         M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
    1.75           is_range(**Lset(i),f,y)))]"
    1.76  by (intro FOL_reflections function_reflections fun_plus_reflections
    1.77               is_recfun_reflection tran_closure_reflection)
    1.78 @@ -325,7 +327,7 @@
    1.79        strong_replacement(L, \<lambda>x z. 
    1.80           \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    1.81           (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
    1.82 -                        M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
    1.83 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    1.84                          is_range(L,f,y)))"
    1.85  apply (rule strong_replacementI) 
    1.86  apply (rule rallI)
    1.87 @@ -351,12 +353,13 @@
    1.88   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
    1.89            ~ (\<forall>f[L]. \<forall>rangef[L]. 
    1.90               is_range(L,f,rangef) -->
    1.91 -             M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
    1.92 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
    1.93               ordinal(L,rangef)),
    1.94        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> 
    1.95            ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). 
    1.96               is_range(**Lset(i),f,rangef) -->
    1.97 -             M_is_recfun(**Lset(i), rplus, x, \<lambda>x f y. is_range(**Lset(i),f,y), f) -->
    1.98 +             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), 
    1.99 +                         rplus, x, f) -->
   1.100               ordinal(**Lset(i),rangef))]"
   1.101  by (intro FOL_reflections function_reflections is_recfun_reflection 
   1.102            tran_closure_reflection ordinal_reflection)
   1.103 @@ -367,7 +370,7 @@
   1.104           \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   1.105            ~ (\<forall>f[L]. \<forall>rangef[L]. 
   1.106               is_range(L,f,rangef) -->
   1.107 -             M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
   1.108 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   1.109               ordinal(L,rangef)))" 
   1.110  apply (rule separation_CollectI) 
   1.111  apply (rule_tac A="{r,z}" in subset_LsetE, blast )