diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Fri Jul 12 11:24:40 2002 +0200 @@ -196,8 +196,8 @@ subsection{*Well-Founded Recursion!*} -(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o" - "M_is_recfun(M,r,a,MH,f) == +(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" + "M_is_recfun(M,MH,r,a,f) == \z[M]. z \ f <-> 5 4 3 2 1 0 (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. @@ -252,7 +252,7 @@ shows "[|x \ nat; y \ nat; z \ nat; env \ list(A)|] ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> - M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))" + M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))" by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym]) lemma is_recfun_iff_sats: @@ -261,15 +261,15 @@ sats(A, p(x,y,z), env)); nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" + ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" by (simp add: sats_is_recfun_fm [of A MH]) theorem is_recfun_reflection: assumes MH_reflection: "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), \i x. MH(**Lset(i), f(x), g(x), h(x))]" - shows "REFLECTS[\x. M_is_recfun(L, f(x), g(x), MH(L), h(x)), - \i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]" + shows "REFLECTS[\x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), + \i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]" apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps) apply (intro FOL_reflections function_reflections restriction_reflection MH_reflection) @@ -279,15 +279,17 @@ lemma wfrank_Reflects: "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)), + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> - ~ (\f \ Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]" + ~ (\f \ Lset(i). + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), + rplus, x, f))]" by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) lemma wfrank_separation: "L(r) ==> separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))" + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" apply (rule separation_CollectI) apply (rule_tac A="{r,z}" in subset_LsetE, blast ) apply (rule ReflectsE [OF wfrank_Reflects], assumption) @@ -309,12 +311,12 @@ "REFLECTS[\z. \x[L]. x \ A & (\rplus[L]. tran_closure(L,r,rplus) --> (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & is_range(L,f,y))), \i z. \x \ Lset(i). x \ A & (\rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> (\y \ Lset(i). \f \ Lset(i). pair(**Lset(i),x,y,z) & - M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) & + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & is_range(**Lset(i),f,y)))]" by (intro FOL_reflections function_reflections fun_plus_reflections is_recfun_reflection tran_closure_reflection) @@ -325,7 +327,7 @@ strong_replacement(L, \x z. \rplus[L]. tran_closure(L,r,rplus) --> (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & is_range(L,f,y)))" apply (rule strong_replacementI) apply (rule rallI) @@ -351,12 +353,13 @@ "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> ~ (\f[L]. \rangef[L]. is_range(L,f,rangef) --> - M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> ordinal(L,rangef)), \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> ~ (\f \ Lset(i). \rangef \ Lset(i). is_range(**Lset(i),f,rangef) --> - M_is_recfun(**Lset(i), rplus, x, \x f y. is_range(**Lset(i),f,y), f) --> + M_is_recfun(**Lset(i), \x f y. is_range(**Lset(i),f,y), + rplus, x, f) --> ordinal(**Lset(i),rangef))]" by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection ordinal_reflection) @@ -367,7 +370,7 @@ \rplus[L]. tran_closure(L,r,rplus) --> ~ (\f[L]. \rangef[L]. is_range(L,f,rangef) --> - M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> ordinal(L,rangef)))" apply (rule separation_CollectI) apply (rule_tac A="{r,z}" in subset_LsetE, blast )