# HG changeset patch # User paulson # Date 1029440186 -7200 # Node ID d93f41fe35d21ef3dada355185028c89dc03f716 # Parent da43ebc02f176fab1de66dac674917aa3cdcfc3e Relativization and absoluteness for DPow!! diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/Constructible/DPow_absolute.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Constructible/DPow_absolute.thy Thu Aug 15 21:36:26 2002 +0200 @@ -0,0 +1,319 @@ +(* Title: ZF/Constructible/DPow_absolute.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge +*) + +header {*Absoluteness for the Definable Powerset Function*} + + +theory DPow_absolute = Satisfies_absolute: + + +subsection{*Preliminary Internalizations*} + +subsubsection{*The Operator @{term is_formula_rec}*} + +text{*The three arguments of @{term p} are always 2, 1, 0. It is buried + within 11 quantifiers!!*} + +(* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" + "is_formula_rec(M,MH,p,z) == + \dp[M]. \i[M]. \f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & + 2 1 0 + successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" +*) + +constdefs formula_rec_fm :: "[i, i, i]=>i" + "formula_rec_fm(mh,p,z) == + Exists(Exists(Exists( + And(finite_ordinal_fm(2), + And(depth_fm(p#+3,2), + And(succ_fm(2,1), + And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))" + +lemma is_formula_rec_type [TC]: + "[| p \ formula; x \ nat; z \ nat |] + ==> formula_rec_fm(p,x,z) \ formula" +by (simp add: formula_rec_fm_def) + +lemma sats_formula_rec_fm: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A; a7\A; a8\A; a9\A; a10\A|] + ==> MH(a2, a1, a0) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, + Cons(a4,Cons(a5,Cons(a6,Cons(a7, + Cons(a8,Cons(a9,Cons(a10,env))))))))))))" + shows + "[|x \ nat; z \ nat; env \ list(A)|] + ==> sats(A, formula_rec_fm(p,x,z), env) <-> + is_formula_rec(**A, MH, nth(x,env), nth(z,env))" +by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def + MH_iff_sats [THEN iff_sym]) + +lemma formula_rec_iff_sats: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A; a7\A; a8\A; a9\A; a10\A|] + ==> MH(a2, a1, a0) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, + Cons(a4,Cons(a5,Cons(a6,Cons(a7, + Cons(a8,Cons(a9,Cons(a10,env))))))))))))" + shows + "[|nth(i,env) = x; nth(k,env) = z; + i \ nat; k \ nat; env \ list(A)|] + ==> is_formula_rec(**A, MH, x, z) <-> sats(A, formula_rec_fm(p,i,k), env)" +by (simp add: sats_formula_rec_fm [OF MH_iff_sats]) + +theorem formula_rec_reflection: + assumes MH_reflection: + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" + shows "REFLECTS[\x. is_formula_rec(L, MH(L,x), f(x), h(x)), + \i x. is_formula_rec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]" +apply (simp (no_asm_use) only: is_formula_rec_def setclass_simps) +apply (intro FOL_reflections function_reflections fun_plus_reflections + depth_reflection is_transrec_reflection MH_reflection) +done + + +subsubsection{*The Operator @{term is_satisfies}*} + +(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *) +constdefs satisfies_fm :: "[i,i,i]=>i" + "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))" + +lemma is_satisfies_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> satisfies_fm(x,y,z) \ formula" +by (simp add: satisfies_fm_def) + +lemma sats_satisfies_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, satisfies_fm(x,y,z), env) <-> + is_satisfies(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm + sats_formula_rec_fm) + +lemma satisfies_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> is_satisfies(**A, x, y, z) <-> sats(A, satisfies_fm(i,j,k), env)" +by (simp add: sats_satisfies_fm) + +theorem satisfies_reflection: + "REFLECTS[\x. is_satisfies(L,f(x),g(x),h(x)), + \i x. is_satisfies(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: is_satisfies_def setclass_simps) +apply (intro formula_rec_reflection satisfies_MH_reflection) +done + + +subsection {*Relativization of the Operator @{term DPow'}*} + +lemma DPow'_eq: + "DPow'(A) = Replace(list(A) * formula, + %ep z. \env \ list(A). \p \ formula. + ep = & z = {x\A. sats(A, p, Cons(x,env))})" +apply (simp add: DPow'_def, blast) +done + + +constdefs + is_DPow_body :: "[i=>o,i,i,i,i] => o" + "is_DPow_body(M,A,env,p,x) == + \n1[M]. \e[M]. \sp[M]. + is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> + fun_apply(M, sp, e, n1) --> number1(M, n1)" + +lemma (in M_satisfies) DPow_body_abs: + "[| M(A); env \ list(A); p \ formula; M(x) |] + ==> is_DPow_body(M,A,env,p,x) <-> sats(A, p, Cons(x,env))" +apply (subgoal_tac "M(env)") + apply (simp add: is_DPow_body_def satisfies_closed satisfies_abs) +apply (blast dest: transM) +done + +lemma (in M_satisfies) Collect_DPow_body_abs: + "[| M(A); env \ list(A); p \ formula |] + ==> Collect(A, is_DPow_body(M,A,env,p)) = + {x \ A. sats(A, p, Cons(x,env))}" +by (simp add: DPow_body_abs transM [of _ A]) + + +subsubsection{*The Operator @{term is_DPow_body}, Internalized*} + +(* is_DPow_body(M,A,env,p,x) == + \n1[M]. \e[M]. \sp[M]. + is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> + fun_apply(M, sp, e, n1) --> number1(M, n1) *) + +constdefs DPow_body_fm :: "[i,i,i,i]=>i" + "DPow_body_fm(A,env,p,x) == + Forall(Forall(Forall( + Implies(satisfies_fm(A#+3,p#+3,0), + Implies(Cons_fm(x#+3,env#+3,1), + Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))" + +lemma is_DPow_body_type [TC]: + "[| A \ nat; x \ nat; y \ nat; z \ nat |] + ==> DPow_body_fm(A,x,y,z) \ formula" +by (simp add: DPow_body_fm_def) + +lemma sats_DPow_body_fm [simp]: + "[| u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, DPow_body_fm(u,x,y,z), env) <-> + is_DPow_body(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))" +by (simp add: DPow_body_fm_def is_DPow_body_def) + +lemma DPow_body_iff_sats: + "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz; + u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> is_DPow_body(**A,nu,nx,ny,nz) <-> + sats(A, DPow_body_fm(u,x,y,z), env)" +by simp + +theorem DPow_body_reflection: + "REFLECTS[\x. is_DPow_body(L,f(x),g(x),h(x),g'(x)), + \i x. is_DPow_body(**Lset(i),f(x),g(x),h(x),g'(x))]" +apply (unfold is_DPow_body_def) +apply (intro FOL_reflections function_reflections extra_reflections + satisfies_reflection) +done + + +subsection{*Additional Constraints on the Class Model @{term M}*} + +locale M_DPow = M_satisfies + + assumes sep: + "[| M(A); env \ list(A); p \ formula |] + ==> separation(M, \x. is_DPow_body(M,A,env,p,x))" + and rep: + "M(A) + ==> strong_replacement (M, + \ep z. \env[M]. \p[M]. mem_formula(M,p) & mem_list(M,A,env) & + pair(M,env,p,ep) & + is_Collect(M, A, \x. is_DPow_body(M,A,env,p,x), z))" + +lemma (in M_DPow) sep': + "[| M(A); env \ list(A); p \ formula |] + ==> separation(M, \x. sats(A, p, Cons(x,env)))" +by (insert sep [of A env p], simp add: DPow_body_abs) + +lemma (in M_DPow) rep': + "M(A) + ==> strong_replacement (M, + \ep z. \env\list(A). \p\formula. + ep = & z = {x \ A . sats(A, p, Cons(x, env))})" +by (insert rep [of A], simp add: Collect_DPow_body_abs) + + +lemma univalent_pair_eq: + "univalent (M, A, \xy z. \x\B. \y\C. xy = \x,y\ \ z = f(x,y))" +by (simp add: univalent_def, blast) + +lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))" +apply (simp add: DPow'_eq) +apply (fast intro: rep' sep' univalent_pair_eq) +done + +text{*Relativization of the Operator @{term DPow'}*} +constdefs + is_DPow' :: "[i=>o,i,i] => o" + "is_DPow'(M,A,Z) == + \X[M]. X \ Z <-> + subset(M,X,A) & + (\env[M]. \p[M]. mem_formula(M,p) & mem_list(M,A,env) & + is_Collect(M, A, is_DPow_body(M,A,env,p), X))" + +lemma (in M_DPow) DPow'_abs: + "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) <-> Z = DPow'(A)" +apply (rule iffI) + prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs) +apply (rule M_equalityI) +apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs, assumption) +apply (erule DPow'_closed) +done + + +subsection{*Instantiating the Locale @{text M_DPow}*} + +subsubsection{*The Instance of Separation*} + +lemma DPow_separation: + "[| L(A); env \ list(A); p \ formula |] + ==> separation(L, \x. is_DPow_body(L,A,env,p,x))" +apply (subgoal_tac "L(env) & L(p)") + prefer 2 apply (blast intro: transL) +apply (rule separation_CollectI) +apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF DPow_body_reflection], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPow_LsetI) +apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats) +apply (rule sep_rules | simp)+ +done + + + +subsubsection{*The Instance of Replacement*} + +lemma DPow_replacement_Reflects: + "REFLECTS [\x. \u[L]. u \ B & + (\env[L]. \p[L]. + mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) & + is_Collect (L, A, is_DPow_body(L,A,env,p), x)), + \i x. \u \ Lset(i). u \ B & + (\env \ Lset(i). \p \ Lset(i). + mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) & + pair(**Lset(i),env,p,u) & + is_Collect (**Lset(i), A, is_DPow_body(**Lset(i),A,env,p), x))]" +apply (unfold is_Collect_def) +apply (intro FOL_reflections function_reflections mem_formula_reflection + mem_list_reflection DPow_body_reflection) +done + +lemma DPow_replacement: + "L(A) + ==> strong_replacement (L, + \ep z. \env[L]. \p[L]. mem_formula(L,p) & mem_list(L,A,env) & + pair(L,env,p,ep) & + is_Collect(L, A, \x. is_DPow_body(L,A,env,p,x), z))" +apply (rule strong_replacementI) +apply (rule rallI) +apply (rename_tac B) +apply (rule separation_CollectI) +apply (rule_tac A="{A,B,z}" in subset_LsetE, blast) +apply (rule ReflectsE [OF DPow_replacement_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPow_LsetI) +apply (rename_tac v) +apply (unfold is_Collect_def) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[u,v,A,B]" in mem_iff_sats) +apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats + DPow_body_iff_sats | simp)+ +done + + +subsubsection{*Actually Instantiating the Locale*} + +lemma M_DPow_axioms_L: "M_DPow_axioms(L)" + apply (rule M_DPow_axioms.intro) + apply (assumption | rule DPow_separation DPow_replacement)+ + done + +theorem M_DPow_L: "PROP M_DPow(L)" + apply (rule M_DPow.intro) + apply (rule M_satisfies.axioms [OF M_satisfies_L])+ + apply (rule M_DPow_axioms_L) + done + +lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L] + and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L] + +end diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/Constructible/Internalize.thy --- a/src/ZF/Constructible/Internalize.thy Wed Aug 14 14:33:26 2002 +0200 +++ b/src/ZF/Constructible/Internalize.thy Thu Aug 15 21:36:26 2002 +0200 @@ -556,4 +556,879 @@ Member_iff_sats Equal_iff_sats Nand_iff_sats Forall_iff_sats is_and_iff_sats is_or_iff_sats is_not_iff_sats + +subsection{*Well-Founded Recursion!*} + + +text{*Alternative definition, minimizing nesting of quantifiers around MH*} +lemma M_is_recfun_iff: + "M_is_recfun(M,MH,r,a,f) <-> + (\z[M]. z \ f <-> + (\x[M]. \f_r_sx[M]. \y[M]. + MH(x, f_r_sx, y) & pair(M,x,y,z) & + (\xa[M]. \sx[M]. \r_sx[M]. + 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)))" +apply (simp add: M_is_recfun_def) +apply (rule rall_cong, blast) +done + + +(* 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 <-> + 2 1 0 +new def (\x[M]. \f_r_sx[M]. \y[M]. + MH(x, f_r_sx, y) & pair(M,x,y,z) & + (\xa[M]. \sx[M]. \r_sx[M]. + 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)" +*) + +text{*The three arguments of @{term p} are always 2, 1, 0 and z*} +constdefs is_recfun_fm :: "[i, i, i, i]=>i" + "is_recfun_fm(p,r,a,f) == + Forall(Iff(Member(0,succ(f)), + Exists(Exists(Exists( + And(p, + And(pair_fm(2,0,3), + Exists(Exists(Exists( + And(pair_fm(5,a#+7,2), + And(upair_fm(5,5,1), + And(pre_image_fm(r#+7,1,0), + And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))" + +lemma is_recfun_type [TC]: + "[| p \ formula; x \ nat; y \ nat; z \ nat |] + ==> is_recfun_fm(p,x,y,z) \ formula" +by (simp add: is_recfun_fm_def) + + +lemma sats_is_recfun_fm: + assumes MH_iff_sats: + "!!a0 a1 a2 a3. + [|a0\A; a1\A; a2\A; a3\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,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, MH, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym]) + +lemma is_recfun_iff_sats: + assumes MH_iff_sats: + "!!a0 a1 a2 a3. + [|a0\A; a1\A; a2\A; a3\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))" + shows + "[| 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, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" +by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) + +text{*The additional variable in the premise, namely @{term f'}, is essential. +It lets @{term MH} depend upon @{term x}, which seems often necessary. +The same thing occurs in @{text is_wfrec_reflection}.*} +theorem is_recfun_reflection: + assumes MH_reflection: + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" + shows "REFLECTS[\x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), + \i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), 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) +done + +subsubsection{*The Operator @{term is_wfrec}*} + +text{*The three arguments of @{term p} are always 2, 1, 0*} + +(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o" + "is_wfrec(M,MH,r,a,z) == + \f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *) +constdefs is_wfrec_fm :: "[i, i, i, i]=>i" + "is_wfrec_fm(p,r,a,z) == + Exists(And(is_recfun_fm(p, succ(r), succ(a), 0), + Exists(Exists(Exists(Exists( + And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))" + +text{*We call @{term p} with arguments a, f, z by equating them with + the corresponding quantified variables with de Bruijn indices 2, 1, 0.*} + +text{*There's an additional existential quantifier to ensure that the + environments in both calls to MH have the same length.*} + +lemma is_wfrec_type [TC]: + "[| p \ formula; x \ nat; y \ nat; z \ nat |] + ==> is_wfrec_fm(p,x,y,z) \ formula" +by (simp add: is_wfrec_fm_def) + +lemma sats_is_wfrec_fm: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4. + [|a0\A; a1\A; a2\A; a3\A; a4\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" + shows + "[|x \ nat; y < length(env); z < length(env); env \ list(A)|] + ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> + is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))" +apply (frule_tac x=z in lt_length_in_nat, assumption) +apply (frule lt_length_in_nat, assumption) +apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) +done + + +lemma is_wfrec_iff_sats: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4. + [|a0\A; a1\A; a2\A; a3\A; a4\A|] + ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" + shows + "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j < length(env); k < length(env); env \ list(A)|] + ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" +by (simp add: sats_is_wfrec_fm [OF MH_iff_sats]) + +theorem is_wfrec_reflection: + assumes MH_reflection: + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" + shows "REFLECTS[\x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), + \i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]" +apply (simp (no_asm_use) only: is_wfrec_def setclass_simps) +apply (intro FOL_reflections MH_reflection is_recfun_reflection) +done + + +subsection{*For Datatypes*} + +subsubsection{*Binary Products, Internalized*} + +constdefs cartprod_fm :: "[i,i,i]=>i" +(* "cartprod(M,A,B,z) == + \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\B & pair(M,x,y,u)))" *) + "cartprod_fm(A,B,z) == + Forall(Iff(Member(0,succ(z)), + Exists(And(Member(0,succ(succ(A))), + Exists(And(Member(0,succ(succ(succ(B)))), + pair_fm(1,0,2)))))))" + +lemma cartprod_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> cartprod_fm(x,y,z) \ formula" +by (simp add: cartprod_fm_def) + +lemma arity_cartprod_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(cartprod_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_cartprod_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, cartprod_fm(x,y,z), env) <-> + cartprod(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: cartprod_fm_def cartprod_def) + +lemma cartprod_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)" +by (simp add: sats_cartprod_fm) + +theorem cartprod_reflection: + "REFLECTS[\x. cartprod(L,f(x),g(x),h(x)), + \i x. cartprod(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: cartprod_def setclass_simps) +apply (intro FOL_reflections pair_reflection) +done + + +subsubsection{*Binary Sums, Internalized*} + +(* "is_sum(M,A,B,Z) == + \A0[M]. \n1[M]. \s1[M]. \B1[M]. + 3 2 1 0 + number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & + cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" *) +constdefs sum_fm :: "[i,i,i]=>i" + "sum_fm(A,B,Z) == + Exists(Exists(Exists(Exists( + And(number1_fm(2), + And(cartprod_fm(2,A#+4,3), + And(upair_fm(2,2,1), + And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))" + +lemma sum_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> sum_fm(x,y,z) \ formula" +by (simp add: sum_fm_def) + +lemma arity_sum_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(sum_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_sum_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, sum_fm(x,y,z), env) <-> + is_sum(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: sum_fm_def is_sum_def) + +lemma sum_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)" +by simp + +theorem sum_reflection: + "REFLECTS[\x. is_sum(L,f(x),g(x),h(x)), + \i x. is_sum(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: is_sum_def setclass_simps) +apply (intro FOL_reflections function_reflections cartprod_reflection) +done + + +subsubsection{*The Operator @{term quasinat}*} + +(* "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" *) +constdefs quasinat_fm :: "i=>i" + "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))" + +lemma quasinat_type [TC]: + "x \ nat ==> quasinat_fm(x) \ formula" +by (simp add: quasinat_fm_def) + +lemma arity_quasinat_fm [simp]: + "x \ nat ==> arity(quasinat_fm(x)) = succ(x)" +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_quasinat_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))" +by (simp add: quasinat_fm_def is_quasinat_def) + +lemma quasinat_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)" +by simp + +theorem quasinat_reflection: + "REFLECTS[\x. is_quasinat(L,f(x)), + \i x. is_quasinat(**Lset(i),f(x))]" +apply (simp only: is_quasinat_def setclass_simps) +apply (intro FOL_reflections function_reflections) +done + + +subsubsection{*The Operator @{term is_nat_case}*} +text{*I could not get it to work with the more natural assumption that + @{term is_b} takes two arguments. Instead it must be a formula where 1 and 0 + stand for @{term m} and @{term b}, respectively.*} + +(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" + "is_nat_case(M, a, is_b, k, z) == + (empty(M,k) --> z=a) & + (\m[M]. successor(M,m,k) --> is_b(m,z)) & + (is_quasinat(M,k) | empty(M,z))" *) +text{*The formula @{term is_b} has free variables 1 and 0.*} +constdefs is_nat_case_fm :: "[i, i, i, i]=>i" + "is_nat_case_fm(a,is_b,k,z) == + And(Implies(empty_fm(k), Equal(z,a)), + And(Forall(Implies(succ_fm(0,succ(k)), + Forall(Implies(Equal(0,succ(succ(z))), is_b)))), + Or(quasinat_fm(k), empty_fm(z))))" + +lemma is_nat_case_type [TC]: + "[| is_b \ formula; + x \ nat; y \ nat; z \ nat |] + ==> is_nat_case_fm(x,is_b,y,z) \ formula" +by (simp add: is_nat_case_fm_def) + +lemma sats_is_nat_case_fm: + assumes is_b_iff_sats: + "!!a. a \ A ==> is_b(a,nth(z, env)) <-> + sats(A, p, Cons(nth(z,env), Cons(a, env)))" + shows + "[|x \ nat; y \ nat; z < length(env); env \ list(A)|] + ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> + is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))" +apply (frule lt_length_in_nat, assumption) +apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym]) +done + +lemma is_nat_case_iff_sats: + "[| (!!a. a \ A ==> is_b(a,z) <-> + sats(A, p, Cons(z, Cons(a,env)))); + nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k < length(env); env \ list(A)|] + ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" +by (simp add: sats_is_nat_case_fm [of A is_b]) + + +text{*The second argument of @{term is_b} gives it direct access to @{term x}, + which is essential for handling free variable references. Without this + argument, we cannot prove reflection for @{term iterates_MH}.*} +theorem is_nat_case_reflection: + assumes is_b_reflection: + "!!h f g. REFLECTS[\x. is_b(L, h(x), f(x), g(x)), + \i x. is_b(**Lset(i), h(x), f(x), g(x))]" + shows "REFLECTS[\x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), + \i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]" +apply (simp (no_asm_use) only: is_nat_case_def setclass_simps) +apply (intro FOL_reflections function_reflections + restriction_reflection is_b_reflection quasinat_reflection) +done + + +subsection{*The Operator @{term iterates_MH}, Needed for Iteration*} + +(* iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o" + "iterates_MH(M,isF,v,n,g,z) == + is_nat_case(M, v, \m u. \gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), + n, z)" *) +constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i" + "iterates_MH_fm(isF,v,n,g,z) == + is_nat_case_fm(v, + Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), + Forall(Implies(Equal(0,2), isF)))), + n, z)" + +lemma iterates_MH_type [TC]: + "[| p \ formula; + v \ nat; x \ nat; y \ nat; z \ nat |] + ==> iterates_MH_fm(p,v,x,y,z) \ formula" +by (simp add: iterates_MH_fm_def) + +lemma sats_iterates_MH_fm: + assumes is_F_iff_sats: + "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] + ==> is_F(a,b) <-> + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))" + shows + "[|v \ nat; x \ nat; y \ nat; z < length(env); env \ list(A)|] + ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> + iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))" +apply (frule lt_length_in_nat, assumption) +apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm + is_F_iff_sats [symmetric]) +apply (rule is_nat_case_cong) +apply (simp_all add: setclass_def) +done + +lemma iterates_MH_iff_sats: + assumes is_F_iff_sats: + "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] + ==> is_F(a,b) <-> + sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))" + shows + "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i' \ nat; i \ nat; j \ nat; k < length(env); env \ list(A)|] + ==> iterates_MH(**A, is_F, v, x, y, z) <-> + sats(A, iterates_MH_fm(p,i',i,j,k), env)" +by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) + +text{*The second argument of @{term p} gives it direct access to @{term x}, + which is essential for handling free variable references. Without this + argument, we cannot prove reflection for @{term list_N}.*} +theorem iterates_MH_reflection: + assumes p_reflection: + "!!f g h. REFLECTS[\x. p(L, h(x), f(x), g(x)), + \i x. p(**Lset(i), h(x), f(x), g(x))]" + shows "REFLECTS[\x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)), + \i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]" +apply (simp (no_asm_use) only: iterates_MH_def) +txt{*Must be careful: simplifying with @{text setclass_simps} above would + change @{text "\gm[**Lset(i)]"} into @{text "\gm \ Lset(i)"}, when + it would no longer match rule @{text is_nat_case_reflection}. *} +apply (rule is_nat_case_reflection) +apply (simp (no_asm_use) only: setclass_simps) +apply (intro FOL_reflections function_reflections is_nat_case_reflection + restriction_reflection p_reflection) +done + + + +subsubsection{*The Formula @{term is_eclose_n}, Internalized*} + +(* is_eclose_n(M,A,n,Z) == + \sn[M]. \msn[M]. + 1 0 + successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z) *) + +constdefs eclose_n_fm :: "[i,i,i]=>i" + "eclose_n_fm(A,n,Z) == + Exists(Exists( + And(succ_fm(n#+2,1), + And(Memrel_fm(1,0), + is_wfrec_fm(iterates_MH_fm(big_union_fm(1,0), + A#+7, 2, 1, 0), + 0, n#+2, Z#+2)))))" + +lemma eclose_n_fm_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> eclose_n_fm(x,y,z) \ formula" +by (simp add: eclose_n_fm_def) + +lemma sats_eclose_n_fm [simp]: + "[| x \ nat; y < length(env); z < length(env); env \ list(A)|] + ==> sats(A, eclose_n_fm(x,y,z), env) <-> + is_eclose_n(**A, nth(x,env), nth(y,env), nth(z,env))" +apply (frule_tac x=z in lt_length_in_nat, assumption) +apply (frule_tac x=y in lt_length_in_nat, assumption) +apply (simp add: eclose_n_fm_def is_eclose_n_def sats_is_wfrec_fm + sats_iterates_MH_fm) +done + +lemma eclose_n_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j < length(env); k < length(env); env \ list(A)|] + ==> is_eclose_n(**A, x, y, z) <-> sats(A, eclose_n_fm(i,j,k), env)" +by (simp add: sats_eclose_n_fm) + +theorem eclose_n_reflection: + "REFLECTS[\x. is_eclose_n(L, f(x), g(x), h(x)), + \i x. is_eclose_n(**Lset(i), f(x), g(x), h(x))]" +apply (simp only: is_eclose_n_def setclass_simps) +apply (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection) +done + + +subsubsection{*Membership in @{term "eclose(A)"}*} + +(* mem_eclose(M,A,l) == + \n[M]. \eclosen[M]. + finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \ eclosen *) +constdefs mem_eclose_fm :: "[i,i]=>i" + "mem_eclose_fm(x,y) == + Exists(Exists( + And(finite_ordinal_fm(1), + And(eclose_n_fm(x#+2,1,0), Member(y#+2,0)))))" + +lemma mem_eclose_type [TC]: + "[| x \ nat; y \ nat |] ==> mem_eclose_fm(x,y) \ formula" +by (simp add: mem_eclose_fm_def) + +lemma sats_mem_eclose_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, mem_eclose_fm(x,y), env) <-> mem_eclose(**A, nth(x,env), nth(y,env))" +by (simp add: mem_eclose_fm_def mem_eclose_def) + +lemma mem_eclose_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> mem_eclose(**A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)" +by simp + +theorem mem_eclose_reflection: + "REFLECTS[\x. mem_eclose(L,f(x),g(x)), + \i x. mem_eclose(**Lset(i),f(x),g(x))]" +apply (simp only: mem_eclose_def setclass_simps) +apply (intro FOL_reflections finite_ordinal_reflection eclose_n_reflection) +done + + +subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*} + +(* is_eclose(M,A,Z) == \l[M]. l \ Z <-> mem_eclose(M,A,l) *) +constdefs is_eclose_fm :: "[i,i]=>i" + "is_eclose_fm(A,Z) == + Forall(Iff(Member(0,succ(Z)), mem_eclose_fm(succ(A),0)))" + +lemma is_eclose_type [TC]: + "[| x \ nat; y \ nat |] ==> is_eclose_fm(x,y) \ formula" +by (simp add: is_eclose_fm_def) + +lemma sats_is_eclose_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, is_eclose_fm(x,y), env) <-> is_eclose(**A, nth(x,env), nth(y,env))" +by (simp add: is_eclose_fm_def is_eclose_def) + +lemma is_eclose_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> is_eclose(**A, x, y) <-> sats(A, is_eclose_fm(i,j), env)" +by simp + +theorem is_eclose_reflection: + "REFLECTS[\x. is_eclose(L,f(x),g(x)), + \i x. is_eclose(**Lset(i),f(x),g(x))]" +apply (simp only: is_eclose_def setclass_simps) +apply (intro FOL_reflections mem_eclose_reflection) +done + + +subsubsection{*The List Functor, Internalized*} + +constdefs list_functor_fm :: "[i,i,i]=>i" +(* "is_list_functor(M,A,X,Z) == + \n1[M]. \AX[M]. + number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *) + "list_functor_fm(A,X,Z) == + Exists(Exists( + And(number1_fm(1), + And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))" + +lemma list_functor_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> list_functor_fm(x,y,z) \ formula" +by (simp add: list_functor_fm_def) + +lemma arity_list_functor_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(list_functor_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_list_functor_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, list_functor_fm(x,y,z), env) <-> + is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: list_functor_fm_def is_list_functor_def) + +lemma list_functor_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)" +by simp + +theorem list_functor_reflection: + "REFLECTS[\x. is_list_functor(L,f(x),g(x),h(x)), + \i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: is_list_functor_def setclass_simps) +apply (intro FOL_reflections number1_reflection + cartprod_reflection sum_reflection) +done + + +subsubsection{*The Formula @{term is_list_N}, Internalized*} + +(* "is_list_N(M,A,n,Z) == + \zero[M]. \sn[M]. \msn[M]. + empty(M,zero) & + successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *) + +constdefs list_N_fm :: "[i,i,i]=>i" + "list_N_fm(A,n,Z) == + Exists(Exists(Exists( + And(empty_fm(2), + And(succ_fm(n#+3,1), + And(Memrel_fm(1,0), + is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0), + 7,2,1,0), + 0, n#+3, Z#+3)))))))" + +lemma list_N_fm_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> list_N_fm(x,y,z) \ formula" +by (simp add: list_N_fm_def) + +lemma sats_list_N_fm [simp]: + "[| x \ nat; y < length(env); z < length(env); env \ list(A)|] + ==> sats(A, list_N_fm(x,y,z), env) <-> + is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))" +apply (frule_tac x=z in lt_length_in_nat, assumption) +apply (frule_tac x=y in lt_length_in_nat, assumption) +apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm + sats_iterates_MH_fm) +done + +lemma list_N_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j < length(env); k < length(env); env \ list(A)|] + ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)" +by (simp add: sats_list_N_fm) + +theorem list_N_reflection: + "REFLECTS[\x. is_list_N(L, f(x), g(x), h(x)), + \i x. is_list_N(**Lset(i), f(x), g(x), h(x))]" +apply (simp only: is_list_N_def setclass_simps) +apply (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection list_functor_reflection) +done + + + +subsubsection{*The Predicate ``Is A List''*} + +(* mem_list(M,A,l) == + \n[M]. \listn[M]. + finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \ listn *) +constdefs mem_list_fm :: "[i,i]=>i" + "mem_list_fm(x,y) == + Exists(Exists( + And(finite_ordinal_fm(1), + And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))" + +lemma mem_list_type [TC]: + "[| x \ nat; y \ nat |] ==> mem_list_fm(x,y) \ formula" +by (simp add: mem_list_fm_def) + +lemma sats_mem_list_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))" +by (simp add: mem_list_fm_def mem_list_def) + +lemma mem_list_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)" +by simp + +theorem mem_list_reflection: + "REFLECTS[\x. mem_list(L,f(x),g(x)), + \i x. mem_list(**Lset(i),f(x),g(x))]" +apply (simp only: mem_list_def setclass_simps) +apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection) +done + + +subsubsection{*The Predicate ``Is @{term "list(A)"}''*} + +(* is_list(M,A,Z) == \l[M]. l \ Z <-> mem_list(M,A,l) *) +constdefs is_list_fm :: "[i,i]=>i" + "is_list_fm(A,Z) == + Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))" + +lemma is_list_type [TC]: + "[| x \ nat; y \ nat |] ==> is_list_fm(x,y) \ formula" +by (simp add: is_list_fm_def) + +lemma sats_is_list_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))" +by (simp add: is_list_fm_def is_list_def) + +lemma is_list_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)" +by simp + +theorem is_list_reflection: + "REFLECTS[\x. is_list(L,f(x),g(x)), + \i x. is_list(**Lset(i),f(x),g(x))]" +apply (simp only: is_list_def setclass_simps) +apply (intro FOL_reflections mem_list_reflection) +done + + +subsubsection{*The Formula Functor, Internalized*} + +constdefs formula_functor_fm :: "[i,i]=>i" +(* "is_formula_functor(M,X,Z) == + \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. + 4 3 2 1 0 + omega(M,nat') & cartprod(M,nat',nat',natnat) & + is_sum(M,natnat,natnat,natnatsum) & + cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & + is_sum(M,natnatsum,X3,Z)" *) + "formula_functor_fm(X,Z) == + Exists(Exists(Exists(Exists(Exists( + And(omega_fm(4), + And(cartprod_fm(4,4,3), + And(sum_fm(3,3,2), + And(cartprod_fm(X#+5,X#+5,1), + And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))" + +lemma formula_functor_type [TC]: + "[| x \ nat; y \ nat |] ==> formula_functor_fm(x,y) \ formula" +by (simp add: formula_functor_fm_def) + +lemma sats_formula_functor_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, formula_functor_fm(x,y), env) <-> + is_formula_functor(**A, nth(x,env), nth(y,env))" +by (simp add: formula_functor_fm_def is_formula_functor_def) + +lemma formula_functor_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)" +by simp + +theorem formula_functor_reflection: + "REFLECTS[\x. is_formula_functor(L,f(x),g(x)), + \i x. is_formula_functor(**Lset(i),f(x),g(x))]" +apply (simp only: is_formula_functor_def setclass_simps) +apply (intro FOL_reflections omega_reflection + cartprod_reflection sum_reflection) +done + + +subsubsection{*The Formula @{term is_formula_N}, Internalized*} + +(* "is_formula_N(M,n,Z) == + \zero[M]. \sn[M]. \msn[M]. + 2 1 0 + empty(M,zero) & + successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *) +constdefs formula_N_fm :: "[i,i]=>i" + "formula_N_fm(n,Z) == + Exists(Exists(Exists( + And(empty_fm(2), + And(succ_fm(n#+3,1), + And(Memrel_fm(1,0), + is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0), + 0, n#+3, Z#+3)))))))" + +lemma formula_N_fm_type [TC]: + "[| x \ nat; y \ nat |] ==> formula_N_fm(x,y) \ formula" +by (simp add: formula_N_fm_def) + +lemma sats_formula_N_fm [simp]: + "[| x < length(env); y < length(env); env \ list(A)|] + ==> sats(A, formula_N_fm(x,y), env) <-> + is_formula_N(**A, nth(x,env), nth(y,env))" +apply (frule_tac x=y in lt_length_in_nat, assumption) +apply (frule lt_length_in_nat, assumption) +apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm) +done + +lemma formula_N_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i < length(env); j < length(env); env \ list(A)|] + ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)" +by (simp add: sats_formula_N_fm) + +theorem formula_N_reflection: + "REFLECTS[\x. is_formula_N(L, f(x), g(x)), + \i x. is_formula_N(**Lset(i), f(x), g(x))]" +apply (simp only: is_formula_N_def setclass_simps) +apply (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection formula_functor_reflection) +done + + + +subsubsection{*The Predicate ``Is A Formula''*} + +(* mem_formula(M,p) == + \n[M]. \formn[M]. + finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \ formn *) +constdefs mem_formula_fm :: "i=>i" + "mem_formula_fm(x) == + Exists(Exists( + And(finite_ordinal_fm(1), + And(formula_N_fm(1,0), Member(x#+2,0)))))" + +lemma mem_formula_type [TC]: + "x \ nat ==> mem_formula_fm(x) \ formula" +by (simp add: mem_formula_fm_def) + +lemma sats_mem_formula_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))" +by (simp add: mem_formula_fm_def mem_formula_def) + +lemma mem_formula_iff_sats: + "[| nth(i,env) = x; i \ nat; env \ list(A)|] + ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)" +by simp + +theorem mem_formula_reflection: + "REFLECTS[\x. mem_formula(L,f(x)), + \i x. mem_formula(**Lset(i),f(x))]" +apply (simp only: mem_formula_def setclass_simps) +apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection) +done + + + +subsubsection{*The Predicate ``Is @{term "formula"}''*} + +(* is_formula(M,Z) == \p[M]. p \ Z <-> mem_formula(M,p) *) +constdefs is_formula_fm :: "i=>i" + "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))" + +lemma is_formula_type [TC]: + "x \ nat ==> is_formula_fm(x) \ formula" +by (simp add: is_formula_fm_def) + +lemma sats_is_formula_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))" +by (simp add: is_formula_fm_def is_formula_def) + +lemma is_formula_iff_sats: + "[| nth(i,env) = x; i \ nat; env \ list(A)|] + ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)" +by simp + +theorem is_formula_reflection: + "REFLECTS[\x. is_formula(L,f(x)), + \i x. is_formula(**Lset(i),f(x))]" +apply (simp only: is_formula_def setclass_simps) +apply (intro FOL_reflections mem_formula_reflection) +done + + +subsubsection{*The Operator @{term is_transrec}*} + +text{*The three arguments of @{term p} are always 2, 1, 0. It is buried + within eight quantifiers! + We call @{term p} with arguments a, f, z by equating them with + the corresponding quantified variables with de Bruijn indices 2, 1, 0.*} + +(* is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o" + "is_transrec(M,MH,a,z) == + \sa[M]. \esa[M]. \mesa[M]. + 2 1 0 + upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) & + is_wfrec(M,MH,mesa,a,z)" *) +constdefs is_transrec_fm :: "[i, i, i]=>i" + "is_transrec_fm(p,a,z) == + Exists(Exists(Exists( + And(upair_fm(a#+3,a#+3,2), + And(is_eclose_fm(2,1), + And(Memrel_fm(1,0), is_wfrec_fm(p,0,a#+3,z#+3)))))))" + + +lemma is_transrec_type [TC]: + "[| p \ formula; x \ nat; z \ nat |] + ==> is_transrec_fm(p,x,z) \ formula" +by (simp add: is_transrec_fm_def) + +lemma sats_is_transrec_fm: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6 a7. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A; a7\A|] + ==> MH(a2, a1, a0) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, + Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))" + shows + "[|x < length(env); z < length(env); env \ list(A)|] + ==> sats(A, is_transrec_fm(p,x,z), env) <-> + is_transrec(**A, MH, nth(x,env), nth(z,env))" +apply (frule_tac x=z in lt_length_in_nat, assumption) +apply (frule_tac x=x in lt_length_in_nat, assumption) +apply (simp add: is_transrec_fm_def sats_is_wfrec_fm is_transrec_def MH_iff_sats [THEN iff_sym]) +done + + +lemma is_transrec_iff_sats: + assumes MH_iff_sats: + "!!a0 a1 a2 a3 a4 a5 a6 a7. + [|a0\A; a1\A; a2\A; a3\A; a4\A; a5\A; a6\A; a7\A|] + ==> MH(a2, a1, a0) <-> + sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3, + Cons(a4,Cons(a5,Cons(a6,Cons(a7,env)))))))))" + shows + "[|nth(i,env) = x; nth(k,env) = z; + i < length(env); k < length(env); env \ list(A)|] + ==> is_transrec(**A, MH, x, z) <-> sats(A, is_transrec_fm(p,i,k), env)" +by (simp add: sats_is_transrec_fm [OF MH_iff_sats]) + +theorem is_transrec_reflection: + assumes MH_reflection: + "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), + \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" + shows "REFLECTS[\x. is_transrec(L, MH(L,x), f(x), h(x)), + \i x. is_transrec(**Lset(i), MH(**Lset(i),x), f(x), h(x))]" +apply (simp (no_asm_use) only: is_transrec_def setclass_simps) +apply (intro FOL_reflections function_reflections MH_reflection + is_wfrec_reflection is_eclose_reflection) +done + end diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Wed Aug 14 14:33:26 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Thu Aug 15 21:36:26 2002 +0200 @@ -8,4 +8,4 @@ Build using isatool usedir -d pdf ZF Constructible *) -use_thy "Satisfies_absolute"; +use_thy "DPow_absolute"; diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Aug 14 14:33:26 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Thu Aug 15 21:36:26 2002 +0200 @@ -234,151 +234,6 @@ declare trancl_abs [simp] -subsection{*Well-Founded Recursion!*} - - -text{*Alternative definition, minimizing nesting of quantifiers around MH*} -lemma M_is_recfun_iff: - "M_is_recfun(M,MH,r,a,f) <-> - (\z[M]. z \ f <-> - (\x[M]. \f_r_sx[M]. \y[M]. - MH(x, f_r_sx, y) & pair(M,x,y,z) & - (\xa[M]. \sx[M]. \r_sx[M]. - 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)))" -apply (simp add: M_is_recfun_def) -apply (rule rall_cong, blast) -done - - -(* 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 <-> - 2 1 0 -new def (\x[M]. \f_r_sx[M]. \y[M]. - MH(x, f_r_sx, y) & pair(M,x,y,z) & - (\xa[M]. \sx[M]. \r_sx[M]. - 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)" -*) - -text{*The three arguments of @{term p} are always 2, 1, 0 and z*} -constdefs is_recfun_fm :: "[i, i, i, i]=>i" - "is_recfun_fm(p,r,a,f) == - Forall(Iff(Member(0,succ(f)), - Exists(Exists(Exists( - And(p, - And(pair_fm(2,0,3), - Exists(Exists(Exists( - And(pair_fm(5,a#+7,2), - And(upair_fm(5,5,1), - And(pre_image_fm(r#+7,1,0), - And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))" - -lemma is_recfun_type [TC]: - "[| p \ formula; x \ nat; y \ nat; z \ nat |] - ==> is_recfun_fm(p,x,y,z) \ formula" -by (simp add: is_recfun_fm_def) - - -lemma sats_is_recfun_fm: - assumes MH_iff_sats: - "!!a0 a1 a2 a3. - [|a0\A; a1\A; a2\A; a3\A|] - ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,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, MH, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym]) - -lemma is_recfun_iff_sats: - assumes MH_iff_sats: - "!!a0 a1 a2 a3. - [|a0\A; a1\A; a2\A; a3\A|] - ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))" - shows - "[| 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, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" -by (simp add: sats_is_recfun_fm [OF MH_iff_sats]) - -text{*The additional variable in the premise, namely @{term f'}, is essential. -It lets @{term MH} depend upon @{term x}, which seems often necessary. -The same thing occurs in @{text is_wfrec_reflection}.*} -theorem is_recfun_reflection: - assumes MH_reflection: - "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), - \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" - shows "REFLECTS[\x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)), - \i x. M_is_recfun(**Lset(i), MH(**Lset(i),x), 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) -done - -subsubsection{*The Operator @{term is_wfrec}*} - -text{*The three arguments of @{term p} are always 2, 1, 0*} - -(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o" - "is_wfrec(M,MH,r,a,z) == - \f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *) -constdefs is_wfrec_fm :: "[i, i, i, i]=>i" - "is_wfrec_fm(p,r,a,z) == - Exists(And(is_recfun_fm(p, succ(r), succ(a), 0), - Exists(Exists(Exists(Exists( - And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))" - -text{*We call @{term p} with arguments a, f, z by equating them with - the corresponding quantified variables with de Bruijn indices 2, 1, 0.*} - -text{*There's an additional existential quantifier to ensure that the - environments in both calls to MH have the same length.*} - -lemma is_wfrec_type [TC]: - "[| p \ formula; x \ nat; y \ nat; z \ nat |] - ==> is_wfrec_fm(p,x,y,z) \ formula" -by (simp add: is_wfrec_fm_def) - -lemma sats_is_wfrec_fm: - assumes MH_iff_sats: - "!!a0 a1 a2 a3 a4. - [|a0\A; a1\A; a2\A; a3\A; a4\A|] - ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" - shows - "[|x \ nat; y < length(env); z < length(env); env \ list(A)|] - ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> - is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))" -apply (frule_tac x=z in lt_length_in_nat, assumption) -apply (frule lt_length_in_nat, assumption) -apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) -done - - -lemma is_wfrec_iff_sats: - assumes MH_iff_sats: - "!!a0 a1 a2 a3 a4. - [|a0\A; a1\A; a2\A; a3\A; a4\A|] - ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" - shows - "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j < length(env); k < length(env); env \ list(A)|] - ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" -by (simp add: sats_is_wfrec_fm [OF MH_iff_sats]) - -theorem is_wfrec_reflection: - assumes MH_reflection: - "!!f' f g h. REFLECTS[\x. MH(L, f'(x), f(x), g(x), h(x)), - \i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]" - shows "REFLECTS[\x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)), - \i x. is_wfrec(**Lset(i), MH(**Lset(i),x), f(x), g(x), h(x))]" -apply (simp (no_asm_use) only: is_wfrec_def setclass_simps) -apply (intro FOL_reflections MH_reflection is_recfun_reflection) -done - subsection{*The Locale @{text "M_wfrank"}*} subsubsection{*Separation for @{term "wfrank"}*} @@ -531,297 +386,8 @@ declare wf_on_abs [simp] -subsection{*For Datatypes*} - -subsubsection{*Binary Products, Internalized*} - -constdefs cartprod_fm :: "[i,i,i]=>i" -(* "cartprod(M,A,B,z) == - \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\B & pair(M,x,y,u)))" *) - "cartprod_fm(A,B,z) == - Forall(Iff(Member(0,succ(z)), - Exists(And(Member(0,succ(succ(A))), - Exists(And(Member(0,succ(succ(succ(B)))), - pair_fm(1,0,2)))))))" - -lemma cartprod_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> cartprod_fm(x,y,z) \ formula" -by (simp add: cartprod_fm_def) - -lemma arity_cartprod_fm [simp]: - "[| x \ nat; y \ nat; z \ nat |] - ==> arity(cartprod_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" -by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) - -lemma sats_cartprod_fm [simp]: - "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, cartprod_fm(x,y,z), env) <-> - cartprod(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: cartprod_fm_def cartprod_def) - -lemma cartprod_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)" -by (simp add: sats_cartprod_fm) - -theorem cartprod_reflection: - "REFLECTS[\x. cartprod(L,f(x),g(x),h(x)), - \i x. cartprod(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: cartprod_def setclass_simps) -apply (intro FOL_reflections pair_reflection) -done - - -subsubsection{*Binary Sums, Internalized*} - -(* "is_sum(M,A,B,Z) == - \A0[M]. \n1[M]. \s1[M]. \B1[M]. - 3 2 1 0 - number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & - cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" *) -constdefs sum_fm :: "[i,i,i]=>i" - "sum_fm(A,B,Z) == - Exists(Exists(Exists(Exists( - And(number1_fm(2), - And(cartprod_fm(2,A#+4,3), - And(upair_fm(2,2,1), - And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))" - -lemma sum_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> sum_fm(x,y,z) \ formula" -by (simp add: sum_fm_def) - -lemma arity_sum_fm [simp]: - "[| x \ nat; y \ nat; z \ nat |] - ==> arity(sum_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" -by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) - -lemma sats_sum_fm [simp]: - "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, sum_fm(x,y,z), env) <-> - is_sum(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: sum_fm_def is_sum_def) - -lemma sum_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)" -by simp - -theorem sum_reflection: - "REFLECTS[\x. is_sum(L,f(x),g(x),h(x)), - \i x. is_sum(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_sum_def setclass_simps) -apply (intro FOL_reflections function_reflections cartprod_reflection) -done - - -subsubsection{*The Operator @{term quasinat}*} - -(* "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" *) -constdefs quasinat_fm :: "i=>i" - "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))" - -lemma quasinat_type [TC]: - "x \ nat ==> quasinat_fm(x) \ formula" -by (simp add: quasinat_fm_def) - -lemma arity_quasinat_fm [simp]: - "x \ nat ==> arity(quasinat_fm(x)) = succ(x)" -by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) - -lemma sats_quasinat_fm [simp]: - "[| x \ nat; env \ list(A)|] - ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))" -by (simp add: quasinat_fm_def is_quasinat_def) - -lemma quasinat_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; - i \ nat; env \ list(A)|] - ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)" -by simp - -theorem quasinat_reflection: - "REFLECTS[\x. is_quasinat(L,f(x)), - \i x. is_quasinat(**Lset(i),f(x))]" -apply (simp only: is_quasinat_def setclass_simps) -apply (intro FOL_reflections function_reflections) -done - - -subsubsection{*The Operator @{term is_nat_case}*} -text{*I could not get it to work with the more natural assumption that - @{term is_b} takes two arguments. Instead it must be a formula where 1 and 0 - stand for @{term m} and @{term b}, respectively.*} - -(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" - "is_nat_case(M, a, is_b, k, z) == - (empty(M,k) --> z=a) & - (\m[M]. successor(M,m,k) --> is_b(m,z)) & - (is_quasinat(M,k) | empty(M,z))" *) -text{*The formula @{term is_b} has free variables 1 and 0.*} -constdefs is_nat_case_fm :: "[i, i, i, i]=>i" - "is_nat_case_fm(a,is_b,k,z) == - And(Implies(empty_fm(k), Equal(z,a)), - And(Forall(Implies(succ_fm(0,succ(k)), - Forall(Implies(Equal(0,succ(succ(z))), is_b)))), - Or(quasinat_fm(k), empty_fm(z))))" - -lemma is_nat_case_type [TC]: - "[| is_b \ formula; - x \ nat; y \ nat; z \ nat |] - ==> is_nat_case_fm(x,is_b,y,z) \ formula" -by (simp add: is_nat_case_fm_def) - -lemma sats_is_nat_case_fm: - assumes is_b_iff_sats: - "!!a. a \ A ==> is_b(a,nth(z, env)) <-> - sats(A, p, Cons(nth(z,env), Cons(a, env)))" - shows - "[|x \ nat; y \ nat; z < length(env); env \ list(A)|] - ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> - is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))" -apply (frule lt_length_in_nat, assumption) -apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym]) -done - -lemma is_nat_case_iff_sats: - "[| (!!a. a \ A ==> is_b(a,z) <-> - sats(A, p, Cons(z, Cons(a,env)))); - nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k < length(env); env \ list(A)|] - ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" -by (simp add: sats_is_nat_case_fm [of A is_b]) - - -text{*The second argument of @{term is_b} gives it direct access to @{term x}, - which is essential for handling free variable references. Without this - argument, we cannot prove reflection for @{term iterates_MH}.*} -theorem is_nat_case_reflection: - assumes is_b_reflection: - "!!h f g. REFLECTS[\x. is_b(L, h(x), f(x), g(x)), - \i x. is_b(**Lset(i), h(x), f(x), g(x))]" - shows "REFLECTS[\x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), - \i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]" -apply (simp (no_asm_use) only: is_nat_case_def setclass_simps) -apply (intro FOL_reflections function_reflections - restriction_reflection is_b_reflection quasinat_reflection) -done - - - -subsection{*The Operator @{term iterates_MH}, Needed for Iteration*} - -(* iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o" - "iterates_MH(M,isF,v,n,g,z) == - is_nat_case(M, v, \m u. \gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), - n, z)" *) -constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i" - "iterates_MH_fm(isF,v,n,g,z) == - is_nat_case_fm(v, - Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), - Forall(Implies(Equal(0,2), isF)))), - n, z)" - -lemma iterates_MH_type [TC]: - "[| p \ formula; - v \ nat; x \ nat; y \ nat; z \ nat |] - ==> iterates_MH_fm(p,v,x,y,z) \ formula" -by (simp add: iterates_MH_fm_def) - -lemma sats_iterates_MH_fm: - assumes is_F_iff_sats: - "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] - ==> is_F(a,b) <-> - sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))" - shows - "[|v \ nat; x \ nat; y \ nat; z < length(env); env \ list(A)|] - ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> - iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))" -apply (frule lt_length_in_nat, assumption) -apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm - is_F_iff_sats [symmetric]) -apply (rule is_nat_case_cong) -apply (simp_all add: setclass_def) -done - -lemma iterates_MH_iff_sats: - assumes is_F_iff_sats: - "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] - ==> is_F(a,b) <-> - sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))" - shows - "[| nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i' \ nat; i \ nat; j \ nat; k < length(env); env \ list(A)|] - ==> iterates_MH(**A, is_F, v, x, y, z) <-> - sats(A, iterates_MH_fm(p,i',i,j,k), env)" -by (simp add: sats_iterates_MH_fm [OF is_F_iff_sats]) - -text{*The second argument of @{term p} gives it direct access to @{term x}, - which is essential for handling free variable references. Without this - argument, we cannot prove reflection for @{term list_N}.*} -theorem iterates_MH_reflection: - assumes p_reflection: - "!!f g h. REFLECTS[\x. p(L, h(x), f(x), g(x)), - \i x. p(**Lset(i), h(x), f(x), g(x))]" - shows "REFLECTS[\x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)), - \i x. iterates_MH(**Lset(i), p(**Lset(i),x), e(x), f(x), g(x), h(x))]" -apply (simp (no_asm_use) only: iterates_MH_def) -txt{*Must be careful: simplifying with @{text setclass_simps} above would - change @{text "\gm[**Lset(i)]"} into @{text "\gm \ Lset(i)"}, when - it would no longer match rule @{text is_nat_case_reflection}. *} -apply (rule is_nat_case_reflection) -apply (simp (no_asm_use) only: setclass_simps) -apply (intro FOL_reflections function_reflections is_nat_case_reflection - restriction_reflection p_reflection) -done - - - subsection{*@{term L} is Closed Under the Operator @{term list}*} -subsubsection{*The List Functor, Internalized*} - -constdefs list_functor_fm :: "[i,i,i]=>i" -(* "is_list_functor(M,A,X,Z) == - \n1[M]. \AX[M]. - number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *) - "list_functor_fm(A,X,Z) == - Exists(Exists( - And(number1_fm(1), - And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))" - -lemma list_functor_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> list_functor_fm(x,y,z) \ formula" -by (simp add: list_functor_fm_def) - -lemma arity_list_functor_fm [simp]: - "[| x \ nat; y \ nat; z \ nat |] - ==> arity(list_functor_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" -by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) - -lemma sats_list_functor_fm [simp]: - "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, list_functor_fm(x,y,z), env) <-> - is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: list_functor_fm_def is_list_functor_def) - -lemma list_functor_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)" -by simp - -theorem list_functor_reflection: - "REFLECTS[\x. is_list_functor(L,f(x),g(x),h(x)), - \i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: is_list_functor_def setclass_simps) -apply (intro FOL_reflections number1_reflection - cartprod_reflection sum_reflection) -done - - subsubsection{*Instances of Replacement for Lists*} lemma list_replacement1_Reflects: @@ -904,48 +470,6 @@ subsection{*@{term L} is Closed Under the Operator @{term formula}*} -subsubsection{*The Formula Functor, Internalized*} - -constdefs formula_functor_fm :: "[i,i]=>i" -(* "is_formula_functor(M,X,Z) == - \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. - 4 3 2 1 0 - omega(M,nat') & cartprod(M,nat',nat',natnat) & - is_sum(M,natnat,natnat,natnatsum) & - cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & - is_sum(M,natnatsum,X3,Z)" *) - "formula_functor_fm(X,Z) == - Exists(Exists(Exists(Exists(Exists( - And(omega_fm(4), - And(cartprod_fm(4,4,3), - And(sum_fm(3,3,2), - And(cartprod_fm(X#+5,X#+5,1), - And(sum_fm(1,X#+5,0), sum_fm(2,0,Z#+5)))))))))))" - -lemma formula_functor_type [TC]: - "[| x \ nat; y \ nat |] ==> formula_functor_fm(x,y) \ formula" -by (simp add: formula_functor_fm_def) - -lemma sats_formula_functor_fm [simp]: - "[| x \ nat; y \ nat; env \ list(A)|] - ==> sats(A, formula_functor_fm(x,y), env) <-> - is_formula_functor(**A, nth(x,env), nth(y,env))" -by (simp add: formula_functor_fm_def is_formula_functor_def) - -lemma formula_functor_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; - i \ nat; j \ nat; env \ list(A)|] - ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)" -by simp - -theorem formula_functor_reflection: - "REFLECTS[\x. is_formula_functor(L,f(x),g(x)), - \i x. is_formula_functor(**Lset(i),f(x),g(x))]" -apply (simp only: is_formula_functor_def setclass_simps) -apply (intro FOL_reflections omega_reflection - cartprod_reflection sum_reflection) -done - subsubsection{*Instances of Replacement for Formulas*} lemma formula_replacement1_Reflects: diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Wed Aug 14 14:33:26 2002 +0200 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Thu Aug 15 21:36:26 2002 +0200 @@ -10,226 +10,6 @@ -subsubsection{*The Formula @{term is_list_N}, Internalized*} - -(* "is_list_N(M,A,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)" *) - -constdefs list_N_fm :: "[i,i,i]=>i" - "list_N_fm(A,n,Z) == - Exists(Exists(Exists( - And(empty_fm(2), - And(succ_fm(n#+3,1), - And(Memrel_fm(1,0), - is_wfrec_fm(iterates_MH_fm(list_functor_fm(A#+9#+3,1,0), - 7,2,1,0), - 0, n#+3, Z#+3)))))))" - -lemma list_N_fm_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> list_N_fm(x,y,z) \ formula" -by (simp add: list_N_fm_def) - -lemma sats_list_N_fm [simp]: - "[| x \ nat; y < length(env); z < length(env); env \ list(A)|] - ==> sats(A, list_N_fm(x,y,z), env) <-> - is_list_N(**A, nth(x,env), nth(y,env), nth(z,env))" -apply (frule_tac x=z in lt_length_in_nat, assumption) -apply (frule_tac x=y in lt_length_in_nat, assumption) -apply (simp add: list_N_fm_def is_list_N_def sats_is_wfrec_fm - sats_iterates_MH_fm) -done - -lemma list_N_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j < length(env); k < length(env); env \ list(A)|] - ==> is_list_N(**A, x, y, z) <-> sats(A, list_N_fm(i,j,k), env)" -by (simp add: sats_list_N_fm) - -theorem list_N_reflection: - "REFLECTS[\x. is_list_N(L, f(x), g(x), h(x)), - \i x. is_list_N(**Lset(i), f(x), g(x), h(x))]" -apply (simp only: is_list_N_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection list_functor_reflection) -done - - - -subsubsection{*The Predicate ``Is A List''*} - -(* mem_list(M,A,l) == - \n[M]. \listn[M]. - finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \ listn *) -constdefs mem_list_fm :: "[i,i]=>i" - "mem_list_fm(x,y) == - Exists(Exists( - And(finite_ordinal_fm(1), - And(list_N_fm(x#+2,1,0), Member(y#+2,0)))))" - -lemma mem_list_type [TC]: - "[| x \ nat; y \ nat |] ==> mem_list_fm(x,y) \ formula" -by (simp add: mem_list_fm_def) - -lemma sats_mem_list_fm [simp]: - "[| x \ nat; y \ nat; env \ list(A)|] - ==> sats(A, mem_list_fm(x,y), env) <-> mem_list(**A, nth(x,env), nth(y,env))" -by (simp add: mem_list_fm_def mem_list_def) - -lemma mem_list_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; - i \ nat; j \ nat; env \ list(A)|] - ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)" -by simp - -theorem mem_list_reflection: - "REFLECTS[\x. mem_list(L,f(x),g(x)), - \i x. mem_list(**Lset(i),f(x),g(x))]" -apply (simp only: mem_list_def setclass_simps) -apply (intro FOL_reflections finite_ordinal_reflection list_N_reflection) -done - - -subsubsection{*The Predicate ``Is @{term "list(A)"}''*} - -(* is_list(M,A,Z) == \l[M]. l \ Z <-> mem_list(M,A,l) *) -constdefs is_list_fm :: "[i,i]=>i" - "is_list_fm(A,Z) == - Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))" - -lemma is_list_type [TC]: - "[| x \ nat; y \ nat |] ==> is_list_fm(x,y) \ formula" -by (simp add: is_list_fm_def) - -lemma sats_is_list_fm [simp]: - "[| x \ nat; y \ nat; env \ list(A)|] - ==> sats(A, is_list_fm(x,y), env) <-> is_list(**A, nth(x,env), nth(y,env))" -by (simp add: is_list_fm_def is_list_def) - -lemma is_list_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; - i \ nat; j \ nat; env \ list(A)|] - ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)" -by simp - -theorem is_list_reflection: - "REFLECTS[\x. is_list(L,f(x),g(x)), - \i x. is_list(**Lset(i),f(x),g(x))]" -apply (simp only: is_list_def setclass_simps) -apply (intro FOL_reflections mem_list_reflection) -done - - -subsubsection{*The Formula @{term is_formula_N}, Internalized*} - -(* "is_formula_N(M,n,Z) == - \zero[M]. \sn[M]. \msn[M]. - 2 1 0 - empty(M,zero) & - successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)" *) -constdefs formula_N_fm :: "[i,i]=>i" - "formula_N_fm(n,Z) == - Exists(Exists(Exists( - And(empty_fm(2), - And(succ_fm(n#+3,1), - And(Memrel_fm(1,0), - is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0),7,2,1,0), - 0, n#+3, Z#+3)))))))" - -lemma formula_N_fm_type [TC]: - "[| x \ nat; y \ nat |] ==> formula_N_fm(x,y) \ formula" -by (simp add: formula_N_fm_def) - -lemma sats_formula_N_fm [simp]: - "[| x < length(env); y < length(env); env \ list(A)|] - ==> sats(A, formula_N_fm(x,y), env) <-> - is_formula_N(**A, nth(x,env), nth(y,env))" -apply (frule_tac x=y in lt_length_in_nat, assumption) -apply (frule lt_length_in_nat, assumption) -apply (simp add: formula_N_fm_def is_formula_N_def sats_is_wfrec_fm sats_iterates_MH_fm) -done - -lemma formula_N_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; - i < length(env); j < length(env); env \ list(A)|] - ==> is_formula_N(**A, x, y) <-> sats(A, formula_N_fm(i,j), env)" -by (simp add: sats_formula_N_fm) - -theorem formula_N_reflection: - "REFLECTS[\x. is_formula_N(L, f(x), g(x)), - \i x. is_formula_N(**Lset(i), f(x), g(x))]" -apply (simp only: is_formula_N_def setclass_simps) -apply (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection formula_functor_reflection) -done - - - -subsubsection{*The Predicate ``Is A Formula''*} - -(* mem_formula(M,p) == - \n[M]. \formn[M]. - finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \ formn *) -constdefs mem_formula_fm :: "i=>i" - "mem_formula_fm(x) == - Exists(Exists( - And(finite_ordinal_fm(1), - And(formula_N_fm(1,0), Member(x#+2,0)))))" - -lemma mem_formula_type [TC]: - "x \ nat ==> mem_formula_fm(x) \ formula" -by (simp add: mem_formula_fm_def) - -lemma sats_mem_formula_fm [simp]: - "[| x \ nat; env \ list(A)|] - ==> sats(A, mem_formula_fm(x), env) <-> mem_formula(**A, nth(x,env))" -by (simp add: mem_formula_fm_def mem_formula_def) - -lemma mem_formula_iff_sats: - "[| nth(i,env) = x; i \ nat; env \ list(A)|] - ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)" -by simp - -theorem mem_formula_reflection: - "REFLECTS[\x. mem_formula(L,f(x)), - \i x. mem_formula(**Lset(i),f(x))]" -apply (simp only: mem_formula_def setclass_simps) -apply (intro FOL_reflections finite_ordinal_reflection formula_N_reflection) -done - - - -subsubsection{*The Predicate ``Is @{term "formula"}''*} - -(* is_formula(M,Z) == \p[M]. p \ Z <-> mem_formula(M,p) *) -constdefs is_formula_fm :: "i=>i" - "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))" - -lemma is_formula_type [TC]: - "x \ nat ==> is_formula_fm(x) \ formula" -by (simp add: is_formula_fm_def) - -lemma sats_is_formula_fm [simp]: - "[| x \ nat; env \ list(A)|] - ==> sats(A, is_formula_fm(x), env) <-> is_formula(**A, nth(x,env))" -by (simp add: is_formula_fm_def is_formula_def) - -lemma is_formula_iff_sats: - "[| nth(i,env) = x; i \ nat; env \ list(A)|] - ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)" -by simp - -theorem is_formula_reflection: - "REFLECTS[\x. is_formula(L,f(x)), - \i x. is_formula(**Lset(i),f(x))]" -apply (simp only: is_formula_def setclass_simps) -apply (intro FOL_reflections mem_formula_reflection) -done - - subsubsection{*The Formula @{term is_depth}, Internalized*} (* "is_depth(M,p,n) == @@ -404,10 +184,10 @@ \u. d(u, h ` succ(depth(u)) ` u))" is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o" - --{* predicate to relative the functional @{term formula_rec}*} + --{* predicate to relativize the functional @{term formula_rec}*} "is_formula_rec(M,MH,p,z) == - \i[M]. \f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) & - is_transrec(M,MH,i,f)" + \dp[M]. \i[M]. \f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & + successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)" text{*Unfold @{term formula_rec} to @{term formula_rec_case}*} lemma (in M_triv_axioms) formula_rec_eq2: @@ -503,7 +283,7 @@ "[| p \ formula; M(z)|] ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed] - transrec_abs [OF fr_replace MH_rel2] + transrec_abs [OF fr_replace MH_rel2] depth_type fr_transrec_closed formula_rec_lam_closed eq_commute) @@ -598,15 +378,7 @@ z)" is_satisfies :: "[i=>o,i,i,i]=>o" - "is_satisfies(M,A) == - is_formula_rec (M, \u f z. - \fml[M]. - is_formula(M,fml) \ - is_lambda - (M, fml, - is_formula_case - (M, satisfies_is_a(M,A), satisfies_is_b(M,A), - satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)), z))" + "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))" text{*This lemma relates the fragments defined above to the original primitive @@ -837,7 +609,7 @@ "[|M(A); M(z); p \ formula|] ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)" by (simp only: M_formula_rec.formula_rec_abs [OF M_formula_rec_M] - satisfies_eq is_satisfies_def) + satisfies_eq is_satisfies_def satisfies_MH_def) subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*} diff -r da43ebc02f17 -r d93f41fe35d2 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed Aug 14 14:33:26 2002 +0200 +++ b/src/ZF/IsaMakefile Thu Aug 15 21:36:26 2002 +0200 @@ -78,7 +78,7 @@ ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz $(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML \ - Constructible/Datatype_absolute.thy\ + Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\ Constructible/Formula.thy Constructible/Internalize.thy \ Constructible/Relative.thy \ Constructible/L_axioms.thy Constructible/Wellorderings.thy \