# HG changeset patch # User paulson # Date 1026387804 -7200 # Node ID 374d05460db4e206ed4e0c35f9f704fe6c556359 # Parent 867f876589e7aa9ded54b929110def8791d7d793 Separation/Replacement up to M_wfrank! diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 10:48:30 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 13:43:24 2002 +0200 @@ -121,7 +121,6 @@ wf_Memrel trans_Memrel relation_Memrel nat_case_closed) - locale M_datatypes = M_wfrank + (*THEY NEED RELATIVIZATION*) assumes list_replacement1: @@ -133,7 +132,7 @@ is_recfun (memr, x, \n f. nat_case(0, \m. {0} + A \ f`m, n), g) & y = nat_case(0, \m. {0} + A \ g`m, x))" - and list_replacement2': + and list_replacement2: "M(A) ==> strong_replacement(M, \x y. y = (\X. {0} + A \ X)^x (0))" @@ -146,6 +145,10 @@ z = nat_case(0, \m. {0} + A \ g ` m, x)))" by (insert list_replacement1, simp add: nat_into_M) +lemma (in M_datatypes) list_replacement2': + "M(A) ==> strong_replacement(M, \x y. y = (\X. {0} + A \ X)^x (0))" +by (insert list_replacement2, simp add: nat_into_M) + lemma (in M_datatypes) list_closed [intro,simp]: "M(A) ==> M(list(A))" diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Thu Jul 11 10:48:30 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Thu Jul 11 13:43:24 2002 +0200 @@ -884,6 +884,46 @@ done +subsubsection{*Pre-Image under a Relation, Internalized*} + +(* "pre_image(M,r,A,z) == + \x[M]. x \ z <-> (\w[M]. w\r & (\y[M]. y\A & pair(M,x,y,w)))" *) +constdefs pre_image_fm :: "[i,i,i]=>i" + "pre_image_fm(r,A,z) == + Forall(Iff(Member(0,succ(z)), + Exists(And(Member(0,succ(succ(r))), + Exists(And(Member(0,succ(succ(succ(A)))), + pair_fm(2,0,1)))))))" + +lemma pre_image_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> pre_image_fm(x,y,z) \ formula" +by (simp add: pre_image_fm_def) + +lemma arity_pre_image_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(pre_image_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_pre_image_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, pre_image_fm(x,y,z), env) <-> + pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: pre_image_fm_def Relative.pre_image_def) + +lemma pre_image_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)" +by (simp add: sats_pre_image_fm) + +theorem pre_image_reflection: + "REFLECTS[\x. pre_image(L,f(x),g(x),h(x)), + \i x. pre_image(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: Relative.pre_image_def setclass_simps) +apply (intro FOL_reflections pair_reflection) +done + + subsubsection{*The Concept of Relation, Internalized*} (* "is_relation(M,r) == @@ -1000,7 +1040,7 @@ fun_apply_reflection subset_reflection transitive_set_reflection membership_reflection pred_set_reflection domain_reflection range_reflection field_reflection - image_reflection + image_reflection pre_image_reflection is_relation_reflection is_function_reflection lemmas function_iff_sats = @@ -1008,7 +1048,7 @@ cons_iff_sats successor_iff_sats fun_apply_iff_sats Memrel_iff_sats pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats - image_iff_sats + image_iff_sats pre_image_iff_sats relation_iff_sats function_iff_sats @@ -1189,6 +1229,46 @@ done +subsubsection{*Restriction of a Relation, Internalized*} + + +(* "restriction(M,r,A,z) == + \x[M]. x \ z <-> (x \ r & (\u[M]. u\A & (\v[M]. pair(M,u,v,x))))" *) +constdefs restriction_fm :: "[i,i,i]=>i" + "restriction_fm(r,A,z) == + Forall(Iff(Member(0,succ(z)), + And(Member(0,succ(r)), + Exists(And(Member(0,succ(succ(A))), + Exists(pair_fm(1,0,2)))))))" + +lemma restriction_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> restriction_fm(x,y,z) \ formula" +by (simp add: restriction_fm_def) + +lemma arity_restriction_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(restriction_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_restriction_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, restriction_fm(x,y,z), env) <-> + restriction(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: restriction_fm_def restriction_def) + +lemma restriction_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)" +by simp + +theorem restriction_reflection: + "REFLECTS[\x. restriction(L,f(x),g(x),h(x)), + \i x. restriction(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: restriction_def setclass_simps) +apply (intro FOL_reflections pair_reflection) +done + subsubsection{*Order-Isomorphisms, Internalized*} (* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" @@ -1327,12 +1407,14 @@ lemmas fun_plus_reflections = typed_function_reflection composition_reflection injection_reflection surjection_reflection - bijection_reflection order_isomorphism_reflection + bijection_reflection restriction_reflection + order_isomorphism_reflection ordinal_reflection limit_ordinal_reflection omega_reflection lemmas fun_plus_iff_sats = typed_function_iff_sats composition_iff_sats - injection_iff_sats surjection_iff_sats bijection_iff_sats + injection_iff_sats surjection_iff_sats + bijection_iff_sats restriction_iff_sats order_isomorphism_iff_sats ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/Rec_Separation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Constructible/Rec_Separation.thy Thu Jul 11 13:43:24 2002 +0200 @@ -0,0 +1,387 @@ +header{*Separation for the Absoluteness of Recursion*} + +theory Rec_Separation = Separation: + +text{*This theory proves all instances needed for locales @{text +"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*} + +subsection{*The Locale @{text "M_trancl"}*} + +subsubsection{*Separation for Reflexive/Transitive Closure*} + +text{*First, The Defining Formula*} + +(* "rtran_closure_mem(M,A,r,p) == + \nnat[M]. \n[M]. \n'[M]. + omega(M,nnat) & n\nnat & successor(M,n,n') & + (\f[M]. typed_function(M,n',A,f) & + (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & + fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & + (\j[M]. j\n --> + (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. + fun_apply(M,f,j,fj) & successor(M,j,sj) & + fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r)))"*) +constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" + "rtran_closure_mem_fm(A,r,p) == + Exists(Exists(Exists( + And(omega_fm(2), + And(Member(1,2), + And(succ_fm(1,0), + Exists(And(typed_function_fm(1, A#+4, 0), + And(Exists(Exists(Exists( + And(pair_fm(2,1,p#+7), + And(empty_fm(0), + And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), + Forall(Implies(Member(0,3), + Exists(Exists(Exists(Exists( + And(fun_apply_fm(5,4,3), + And(succ_fm(4,2), + And(fun_apply_fm(5,2,1), + And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" + + +lemma rtran_closure_mem_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> rtran_closure_mem_fm(x,y,z) \ formula" +by (simp add: rtran_closure_mem_fm_def) + +lemma arity_rtran_closure_mem_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_rtran_closure_mem_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> + rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) + +lemma rtran_closure_mem_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" +by (simp add: sats_rtran_closure_mem_fm) + +theorem rtran_closure_mem_reflection: + "REFLECTS[\x. rtran_closure_mem(L,f(x),g(x),h(x)), + \i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: rtran_closure_mem_def setclass_simps) +apply (intro FOL_reflections function_reflections fun_plus_reflections) +done + +text{*Separation for @{term "rtrancl(r)"}.*} +lemma rtrancl_separation: + "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" +apply (rule separation_CollectI) +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPowI2) +apply (rename_tac u) +apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats) +apply (rule sep_rules | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + +subsubsection{*Reflexive/Transitive Closure, Internalized*} + +(* "rtran_closure(M,r,s) == + \A[M]. is_field(M,r,A) --> + (\p[M]. p \ s <-> rtran_closure_mem(M,A,r,p))" *) +constdefs rtran_closure_fm :: "[i,i]=>i" + "rtran_closure_fm(r,s) == + Forall(Implies(field_fm(succ(r),0), + Forall(Iff(Member(0,succ(succ(s))), + rtran_closure_mem_fm(1,succ(succ(r)),0)))))" + +lemma rtran_closure_type [TC]: + "[| x \ nat; y \ nat |] ==> rtran_closure_fm(x,y) \ formula" +by (simp add: rtran_closure_fm_def) + +lemma arity_rtran_closure_fm [simp]: + "[| x \ nat; y \ nat |] + ==> arity(rtran_closure_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_rtran_closure_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, rtran_closure_fm(x,y), env) <-> + rtran_closure(**A, nth(x,env), nth(y,env))" +by (simp add: rtran_closure_fm_def rtran_closure_def) + +lemma rtran_closure_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" +by simp + +theorem rtran_closure_reflection: + "REFLECTS[\x. rtran_closure(L,f(x),g(x)), + \i x. rtran_closure(**Lset(i),f(x),g(x))]" +apply (simp only: rtran_closure_def setclass_simps) +apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) +done + + +subsubsection{*Transitive Closure of a Relation, Internalized*} + +(* "tran_closure(M,r,t) == + \s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) +constdefs tran_closure_fm :: "[i,i]=>i" + "tran_closure_fm(r,s) == + Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" + +lemma tran_closure_type [TC]: + "[| x \ nat; y \ nat |] ==> tran_closure_fm(x,y) \ formula" +by (simp add: tran_closure_fm_def) + +lemma arity_tran_closure_fm [simp]: + "[| x \ nat; y \ nat |] + ==> arity(tran_closure_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_tran_closure_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, tran_closure_fm(x,y), env) <-> + tran_closure(**A, nth(x,env), nth(y,env))" +by (simp add: tran_closure_fm_def tran_closure_def) + +lemma tran_closure_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" +by simp + +theorem tran_closure_reflection: + "REFLECTS[\x. tran_closure(L,f(x),g(x)), + \i x. tran_closure(**Lset(i),f(x),g(x))]" +apply (simp only: tran_closure_def setclass_simps) +apply (intro FOL_reflections function_reflections + rtran_closure_reflection composition_reflection) +done + + +subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} + +lemma wellfounded_trancl_reflects: + "REFLECTS[\x. \w[L]. \wx[L]. \rp[L]. + w \ Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \ rp, + \i x. \w \ Lset(i). \wx \ Lset(i). \rp \ Lset(i). + w \ Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) & + wx \ rp]" +by (intro FOL_reflections function_reflections fun_plus_reflections + tran_closure_reflection) + + +lemma wellfounded_trancl_separation: + "[| L(r); L(Z) |] ==> + separation (L, \x. + \w[L]. \wx[L]. \rp[L]. + w \ Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \ rp)" +apply (rule separation_CollectI) +apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPowI2) +apply (rename_tac u) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) +apply (rule sep_rules tran_closure_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + +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) == + \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]. + pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & + pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & + xa \ r & MH(x, f_r_sx, y))" +*) + +constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i" + "is_recfun_fm(p,r,a,f) == + Forall(Iff(Member(0,succ(f)), + Exists(Exists(Exists(Exists(Exists(Exists( + And(pair_fm(5,4,6), + And(pair_fm(5,a#+7,3), + And(upair_fm(5,5,2), + And(pre_image_fm(r#+7,2,1), + And(restriction_fm(f#+7,1,0), + And(Member(3,r#+7), p(5,0,4)))))))))))))))" + + +lemma is_recfun_type_0: + "[| !!x y z. [| x \ nat; y \ nat; z \ nat |] ==> p(x,y,z) \ formula; + x \ nat; y \ nat; z \ nat |] + ==> is_recfun_fm(p,x,y,z) \ formula" +apply (unfold is_recfun_fm_def) +(*FIXME: FIND OUT why simp loops!*) +apply typecheck +by simp + +lemma is_recfun_type [TC]: + "[| p(5,0,4) \ formula; + x \ nat; y \ nat; z \ nat |] + ==> is_recfun_fm(p,x,y,z) \ formula" +by (simp add: is_recfun_fm_def) + +lemma arity_is_recfun_fm [simp]: + "[| arity(p(5,0,4)) le 8; x \ nat; y \ nat; z \ nat |] + ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \ succ(y) \ succ(z)" +apply (frule lt_nat_in_nat, simp) +apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] ) +apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1]) +apply (rule le_imp_subset) +apply (erule le_trans, simp) +apply (simp add: succ_Un_distrib [symmetric] Un_ac) +done + +lemma sats_is_recfun_fm: + assumes MH_iff_sats: + "!!x y z env. + [| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)" + 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))" +by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym]) + +lemma is_recfun_iff_sats: + "[| (!!x y z env. [| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> + 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)" +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))]" +apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps) +apply (intro FOL_reflections function_reflections + restriction_reflection MH_reflection) +done + +subsection{*Separation for @{term "wfrank"}*} + +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)), + \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))]" +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)))" +apply (rule separation_CollectI) +apply (rule_tac A="{r,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF wfrank_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2, clarify) +apply (rule DPowI2) +apply (rename_tac u) +apply (rule ball_iff_sats imp_iff_sats)+ +apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) +apply (rule sep_rules is_recfun_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + +subsection{*Replacement for @{term "wfrank"}*} + +lemma wfrank_replacement_Reflects: + "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) & + 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) & + is_range(**Lset(i),f,y)))]" +by (intro FOL_reflections function_reflections fun_plus_reflections + is_recfun_reflection tran_closure_reflection) + + +lemma wfrank_strong_replacement: + "L(r) ==> + 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) & + is_range(L,f,y)))" +apply (rule strong_replacementI) +apply (rule rallI) +apply (rename_tac B) +apply (rule separation_CollectI) +apply (rule_tac A="{B,r,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPowI2) +apply (rename_tac u) +apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + +subsection{*Separation for @{term "wfrank"}*} + +lemma Ord_wfrank_Reflects: + "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) --> + 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) --> + ordinal(**Lset(i),rangef))]" +by (intro FOL_reflections function_reflections is_recfun_reflection + tran_closure_reflection ordinal_reflection) + +lemma Ord_wfrank_separation: + "L(r) ==> + separation (L, \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) --> + ordinal(L,rangef)))" +apply (rule separation_CollectI) +apply (rule_tac A="{r,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2, clarify) +apply (rule DPowI2) +apply (rename_tac u) +apply (rule ball_iff_sats imp_iff_sats)+ +apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) +apply (rule sep_rules is_recfun_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + +end diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Thu Jul 11 10:48:30 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Thu Jul 11 13:43:24 2002 +0200 @@ -532,7 +532,7 @@ done text{*Probably the premise and conclusion are equivalent*} -lemma (in M_triv_axioms) strong_replacementI [OF rallI]: +lemma (in M_triv_axioms) strong_replacementI [rule_format]: "[| \A[M]. separation(M, %u. \x[M]. x\A & P(x,u)) |] ==> strong_replacement(M,P)" apply (simp add: strong_replacement_def, clarify) diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 10:48:30 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 13:43:24 2002 +0200 @@ -232,21 +232,30 @@ rank function.*} -(*NEEDS RELATIVIZATION*) locale M_wfrank = M_trancl + assumes wfrank_separation: "M(r) ==> separation (M, \x. - ~ (\f[M]. M_is_recfun(M, r^+, x, %mm x f y. y = range(f), f)))" - and wfrank_strong_replacement': + \rplus[M]. tran_closure(M,r,rplus) --> + ~ (\f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))" + and wfrank_strong_replacement: "M(r) ==> - strong_replacement(M, \x z. \y[M]. \f[M]. - pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & - y = range(f))" + strong_replacement(M, \x z. + \rplus[M]. tran_closure(M,r,rplus) --> + (\y[M]. \f[M]. pair(M,x,y,z) & + M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) & + is_range(M,f,y)))" and Ord_wfrank_separation: "M(r) ==> - separation (M, \x. ~ (\f. M(f) \ - is_recfun(r^+, x, \x. range, f) \ Ord(range(f))))" + separation (M, \x. + \rplus[M]. tran_closure(M,r,rplus) --> + ~ (\f[M]. \rangef[M]. + is_range(M,f,rangef) --> + M_is_recfun(M, rplus, x, \x f y. is_range(M,f,y), f) --> + ordinal(M,rangef)))" + +text{*Proving that the relativized instances of Separation or Replacement +agree with the "real" ones.*} lemma (in M_wfrank) wfrank_separation': "M(r) ==> @@ -256,6 +265,23 @@ apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym]) done +lemma (in M_wfrank) wfrank_strong_replacement': + "M(r) ==> + strong_replacement(M, \x z. \y[M]. \f[M]. + pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & + y = range(f))" +apply (insert wfrank_strong_replacement [of r]) +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym]) +done + +lemma (in M_wfrank) Ord_wfrank_separation': + "M(r) ==> + separation (M, \x. + ~ (\f[M]. is_recfun(r^+, x, \x. range, f) --> Ord(range(f))))" +apply (insert Ord_wfrank_separation [of r]) +apply (simp add: is_recfun_iff_M [of concl: _ _ "%x. range", THEN iff_sym]) +done + text{*This function, defined using replacement, is a rank function for well-founded relations within the class M.*} constdefs @@ -290,11 +316,11 @@ lemma (in M_wfrank) Ord_wfrank_range [rule_format]: "[| wellfounded(M,r); a\A; M(r); M(A) |] - ==> \f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" + ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" apply (drule wellfounded_trancl, assumption) apply (rule wellfounded_induct, assumption+) apply simp - apply (blast intro: Ord_wfrank_separation, clarify) + apply (blast intro: Ord_wfrank_separation', clarify) txt{*The reasoning in both cases is that we get @{term y} such that @{term "\y, x\ \ r^+"}. We find that @{term "f`y = restrict(f, r^+ -`` {y})"}. *} @@ -314,7 +340,8 @@ apply (simp add: trans_trancl trancl_subset_times)+ apply (drule spec [THEN mp], assumption) apply (subgoal_tac "M(restrict(f, r^+ -`` {y}))") - apply (drule_tac x="restrict(f, r^+ -`` {y})" in spec) + apply (drule_tac x="restrict(f, r^+ -`` {y})" in rspec) +apply assumption apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) apply (blast dest: pair_components_in_M) done diff -r 867f876589e7 -r 374d05460db4 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Thu Jul 11 10:48:30 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Thu Jul 11 13:43:24 2002 +0200 @@ -275,17 +275,17 @@ done constdefs - M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o" + M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o" "M_is_recfun(M,r,a,MH,f) == \z[M]. z \ f <-> (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & - xa \ r & MH(M, x, f_r_sx, y))" + xa \ r & MH(x, f_r_sx, y))" lemma (in M_axioms) is_recfun_iff_M: "[| M(r); M(a); M(f); \x[M]. \g[M]. function(g) --> M(H(x,g)); - \x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==> + \x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] ==> is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)" apply (simp add: M_is_recfun_def is_recfun_relativize) apply (rule rall_cong) @@ -294,7 +294,7 @@ lemma M_is_recfun_cong [cong]: "[| r = r'; a = a'; f = f'; - !!x g y. [| M(x); M(g); M(y) |] ==> MH(M,x,g,y) <-> MH'(M,x,g,y) |] + !!x g y. [| M(x); M(g); M(y) |] ==> MH(x,g,y) <-> MH'(x,g,y) |] ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')" by (simp add: M_is_recfun_def) @@ -309,7 +309,7 @@ (\sj msj. M(sj) --> M(msj) --> successor(M,j,sj) --> membership(M,sj,msj) --> M_is_recfun(M, msj, x, - %M x g y. \gx. M(gx) & image(M,g,x,gx) & union(M,i,gx,y), + %x g y. \gx[M]. image(M,g,x,gx) & union(M,i,gx,y), f))" is_oadd :: "[i=>o,i,i,i] => o"