--- /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) ==
+ \<exists>dp[M]. \<exists>i[M]. \<exists>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 \<in> formula; x \<in> nat; z \<in> nat |]
+ ==> formula_rec_fm(p,x,z) \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>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 \<in> nat; z \<in> nat; env \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>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 \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
+ \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+ shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)),
+ \<lambda>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
+by (simp add: satisfies_fm_def)
+
+lemma sats_satisfies_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
+ \<lambda>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. \<exists>env \<in> list(A). \<exists>p \<in> formula.
+ ep = <env,p> & z = {x\<in>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) ==
+ \<forall>n1[M]. \<forall>e[M]. \<forall>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 \<in> list(A); p \<in> 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 \<in> list(A); p \<in> formula |]
+ ==> Collect(A, is_DPow_body(M,A,env,p)) =
+ {x \<in> 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) ==
+ \<forall>n1[M]. \<forall>e[M]. \<forall>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 \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> DPow_body_fm(A,x,y,z) \<in> formula"
+by (simp add: DPow_body_fm_def)
+
+lemma sats_DPow_body_fm [simp]:
+ "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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[\<lambda>x. is_DPow_body(L,f(x),g(x),h(x),g'(x)),
+ \<lambda>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 \<in> list(A); p \<in> formula |]
+ ==> separation(M, \<lambda>x. is_DPow_body(M,A,env,p,x))"
+ and rep:
+ "M(A)
+ ==> strong_replacement (M,
+ \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
+ pair(M,env,p,ep) &
+ is_Collect(M, A, \<lambda>x. is_DPow_body(M,A,env,p,x), z))"
+
+lemma (in M_DPow) sep':
+ "[| M(A); env \<in> list(A); p \<in> formula |]
+ ==> separation(M, \<lambda>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,
+ \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
+ ep = <env,p> & z = {x \<in> 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, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> 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) ==
+ \<forall>X[M]. X \<in> Z <->
+ subset(M,X,A) &
+ (\<exists>env[M]. \<exists>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 \<in> list(A); p \<in> formula |]
+ ==> separation(L, \<lambda>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 [\<lambda>x. \<exists>u[L]. u \<in> B &
+ (\<exists>env[L]. \<exists>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)),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
+ (\<exists>env \<in> Lset(i). \<exists>p \<in> 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,
+ \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
+ pair(L,env,p,ep) &
+ is_Collect(L, A, \<lambda>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
--- 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) <->
+ (\<forall>z[M]. z \<in> f <->
+ (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
+ MH(x, f_r_sx, y) & pair(M,x,y,z) &
+ (\<exists>xa[M]. \<exists>sx[M]. \<exists>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 \<in> 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) ==
+ \<forall>z[M]. z \<in> f <->
+ 2 1 0
+new def (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
+ MH(x, f_r_sx, y) & pair(M,x,y,z) &
+ (\<exists>xa[M]. \<exists>sx[M]. \<exists>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 \<in> 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 \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> is_recfun_fm(p,x,y,z) \<in> formula"
+by (simp add: is_recfun_fm_def)
+
+
+lemma sats_is_recfun_fm:
+ assumes MH_iff_sats:
+ "!!a0 a1 a2 a3.
+ [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
+ ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
+ shows
+ "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
+ \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+ shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
+ \<lambda>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) ==
+ \<exists>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 \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> is_wfrec_fm(p,x,y,z) \<in> formula"
+by (simp add: is_wfrec_fm_def)
+
+lemma sats_is_wfrec_fm:
+ assumes MH_iff_sats:
+ "!!a0 a1 a2 a3 a4.
+ [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
+ ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
+ shows
+ "[|x \<in> nat; y < length(env); z < length(env); env \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>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 \<in> nat; j < length(env); k < length(env); env \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
+ \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+ shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
+ \<lambda>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) ==
+ \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
+by (simp add: cartprod_fm_def)
+
+lemma arity_cartprod_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_cartprod_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
+ \<lambda>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) ==
+ \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
+by (simp add: sum_fm_def)
+
+lemma arity_sum_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_sum_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+ ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
+by simp
+
+theorem sum_reflection:
+ "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
+ \<lambda>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) | (\<exists>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 \<in> nat ==> quasinat_fm(x) \<in> formula"
+by (simp add: quasinat_fm_def)
+
+lemma arity_quasinat_fm [simp]:
+ "x \<in> 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 \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
+ ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
+by simp
+
+theorem quasinat_reflection:
+ "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
+ \<lambda>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) &
+ (\<forall>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 \<in> formula;
+ x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
+by (simp add: is_nat_case_fm_def)
+
+lemma sats_is_nat_case_fm:
+ assumes is_b_iff_sats:
+ "!!a. a \<in> A ==> is_b(a,nth(z, env)) <->
+ sats(A, p, Cons(nth(z,env), Cons(a, env)))"
+ shows
+ "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> 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 \<in> 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 \<in> nat; j \<in> nat; k < length(env); env \<in> 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[\<lambda>x. is_b(L, h(x), f(x), g(x)),
+ \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
+ shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
+ \<lambda>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, \<lambda>m u. \<exists>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 \<in> formula;
+ v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
+by (simp add: iterates_MH_fm_def)
+
+lemma sats_iterates_MH_fm:
+ assumes is_F_iff_sats:
+ "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
+ ==> is_F(a,b) <->
+ sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
+ shows
+ "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> 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 \<in> A; b \<in> A; c \<in> A; d \<in> 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' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> 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[\<lambda>x. p(L, h(x), f(x), g(x)),
+ \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
+ shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
+ \<lambda>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 "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> 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) ==
+ \<exists>sn[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> eclose_n_fm(x,y,z) \<in> formula"
+by (simp add: eclose_n_fm_def)
+
+lemma sats_eclose_n_fm [simp]:
+ "[| x \<in> nat; y < length(env); z < length(env); env \<in> 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 \<in> nat; j < length(env); k < length(env); env \<in> 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[\<lambda>x. is_eclose_n(L, f(x), g(x), h(x)),
+ \<lambda>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) ==
+ \<exists>n[M]. \<exists>eclosen[M].
+ finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> 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 \<in> nat; y \<in> nat |] ==> mem_eclose_fm(x,y) \<in> formula"
+by (simp add: mem_eclose_fm_def)
+
+lemma sats_mem_eclose_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> mem_eclose(**A, x, y) <-> sats(A, mem_eclose_fm(i,j), env)"
+by simp
+
+theorem mem_eclose_reflection:
+ "REFLECTS[\<lambda>x. mem_eclose(L,f(x),g(x)),
+ \<lambda>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) == \<forall>l[M]. l \<in> 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 \<in> nat; y \<in> nat |] ==> is_eclose_fm(x,y) \<in> formula"
+by (simp add: is_eclose_fm_def)
+
+lemma sats_is_eclose_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> is_eclose(**A, x, y) <-> sats(A, is_eclose_fm(i,j), env)"
+by simp
+
+theorem is_eclose_reflection:
+ "REFLECTS[\<lambda>x. is_eclose(L,f(x),g(x)),
+ \<lambda>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) ==
+ \<exists>n1[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
+by (simp add: list_functor_fm_def)
+
+lemma arity_list_functor_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_list_functor_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
+ \<lambda>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) ==
+ \<exists>zero[M]. \<exists>sn[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
+by (simp add: list_N_fm_def)
+
+lemma sats_list_N_fm [simp]:
+ "[| x \<in> nat; y < length(env); z < length(env); env \<in> 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 \<in> nat; j < length(env); k < length(env); env \<in> 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[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
+ \<lambda>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) ==
+ \<exists>n[M]. \<exists>listn[M].
+ finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> 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 \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
+by (simp add: mem_list_fm_def)
+
+lemma sats_mem_list_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
+by simp
+
+theorem mem_list_reflection:
+ "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
+ \<lambda>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) == \<forall>l[M]. l \<in> 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 \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
+by (simp add: is_list_fm_def)
+
+lemma sats_is_list_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
+by simp
+
+theorem is_list_reflection:
+ "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
+ \<lambda>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) ==
+ \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>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 \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
+by (simp add: formula_functor_fm_def)
+
+lemma sats_formula_functor_fm [simp]:
+ "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
+ ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
+by simp
+
+theorem formula_functor_reflection:
+ "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
+ \<lambda>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) ==
+ \<exists>zero[M]. \<exists>sn[M]. \<exists>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 \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
+by (simp add: formula_N_fm_def)
+
+lemma sats_formula_N_fm [simp]:
+ "[| x < length(env); y < length(env); env \<in> 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 \<in> 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[\<lambda>x. is_formula_N(L, f(x), g(x)),
+ \<lambda>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) ==
+ \<exists>n[M]. \<exists>formn[M].
+ finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> 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 \<in> nat ==> mem_formula_fm(x) \<in> formula"
+by (simp add: mem_formula_fm_def)
+
+lemma sats_mem_formula_fm [simp]:
+ "[| x \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
+ ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
+by simp
+
+theorem mem_formula_reflection:
+ "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
+ \<lambda>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) == \<forall>p[M]. p \<in> 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 \<in> nat ==> is_formula_fm(x) \<in> formula"
+by (simp add: is_formula_fm_def)
+
+lemma sats_is_formula_fm [simp]:
+ "[| x \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
+ ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
+by simp
+
+theorem is_formula_reflection:
+ "REFLECTS[\<lambda>x. is_formula(L,f(x)),
+ \<lambda>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) ==
+ \<exists>sa[M]. \<exists>esa[M]. \<exists>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 \<in> formula; x \<in> nat; z \<in> nat |]
+ ==> is_transrec_fm(p,x,z) \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>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 \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>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 \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
+ \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
+ shows "REFLECTS[\<lambda>x. is_transrec(L, MH(L,x), f(x), h(x)),
+ \<lambda>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
--- 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";
--- 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) <->
- (\<forall>z[M]. z \<in> f <->
- (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
- MH(x, f_r_sx, y) & pair(M,x,y,z) &
- (\<exists>xa[M]. \<exists>sx[M]. \<exists>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 \<in> 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) ==
- \<forall>z[M]. z \<in> f <->
- 2 1 0
-new def (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M].
- MH(x, f_r_sx, y) & pair(M,x,y,z) &
- (\<exists>xa[M]. \<exists>sx[M]. \<exists>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 \<in> 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 \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> is_recfun_fm(p,x,y,z) \<in> formula"
-by (simp add: is_recfun_fm_def)
-
-
-lemma sats_is_recfun_fm:
- assumes MH_iff_sats:
- "!!a0 a1 a2 a3.
- [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|]
- ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
- shows
- "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
- \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
- shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L,x), f(x), g(x), h(x)),
- \<lambda>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) ==
- \<exists>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 \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> is_wfrec_fm(p,x,y,z) \<in> formula"
-by (simp add: is_wfrec_fm_def)
-
-lemma sats_is_wfrec_fm:
- assumes MH_iff_sats:
- "!!a0 a1 a2 a3 a4.
- [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|]
- ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
- shows
- "[|x \<in> nat; y < length(env); z < length(env); env \<in> 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\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>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 \<in> nat; j < length(env); k < length(env); env \<in> 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[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)),
- \<lambda>i x. MH(**Lset(i), f'(x), f(x), g(x), h(x))]"
- shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L,x), f(x), g(x), h(x)),
- \<lambda>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) ==
- \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> cartprod_fm(x,y,z) \<in> formula"
-by (simp add: cartprod_fm_def)
-
-lemma arity_cartprod_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> arity(cartprod_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac)
-
-lemma sats_cartprod_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. cartprod(L,f(x),g(x),h(x)),
- \<lambda>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) ==
- \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> sum_fm(x,y,z) \<in> formula"
-by (simp add: sum_fm_def)
-
-lemma arity_sum_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> arity(sum_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac)
-
-lemma sats_sum_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
- ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)"
-by simp
-
-theorem sum_reflection:
- "REFLECTS[\<lambda>x. is_sum(L,f(x),g(x),h(x)),
- \<lambda>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) | (\<exists>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 \<in> nat ==> quasinat_fm(x) \<in> formula"
-by (simp add: quasinat_fm_def)
-
-lemma arity_quasinat_fm [simp]:
- "x \<in> 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 \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
- ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)"
-by simp
-
-theorem quasinat_reflection:
- "REFLECTS[\<lambda>x. is_quasinat(L,f(x)),
- \<lambda>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) &
- (\<forall>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 \<in> formula;
- x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
-by (simp add: is_nat_case_fm_def)
-
-lemma sats_is_nat_case_fm:
- assumes is_b_iff_sats:
- "!!a. a \<in> A ==> is_b(a,nth(z, env)) <->
- sats(A, p, Cons(nth(z,env), Cons(a, env)))"
- shows
- "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> 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 \<in> 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 \<in> nat; j \<in> nat; k < length(env); env \<in> 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[\<lambda>x. is_b(L, h(x), f(x), g(x)),
- \<lambda>i x. is_b(**Lset(i), h(x), f(x), g(x))]"
- shows "REFLECTS[\<lambda>x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)),
- \<lambda>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, \<lambda>m u. \<exists>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 \<in> formula;
- v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
-by (simp add: iterates_MH_fm_def)
-
-lemma sats_iterates_MH_fm:
- assumes is_F_iff_sats:
- "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
- ==> is_F(a,b) <->
- sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
- shows
- "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> 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 \<in> A; b \<in> A; c \<in> A; d \<in> 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' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> 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[\<lambda>x. p(L, h(x), f(x), g(x)),
- \<lambda>i x. p(**Lset(i), h(x), f(x), g(x))]"
- shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L,x), e(x), f(x), g(x), h(x)),
- \<lambda>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 "\<exists>gm[**Lset(i)]"} into @{text "\<exists>gm \<in> 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) ==
- \<exists>n1[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
-by (simp add: list_functor_fm_def)
-
-lemma arity_list_functor_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat |]
- ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac)
-
-lemma sats_list_functor_fm [simp]:
- "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; k \<in> nat; env \<in> 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[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)),
- \<lambda>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) ==
- \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>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 \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
-by (simp add: formula_functor_fm_def)
-
-lemma sats_formula_functor_fm [simp]:
- "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
-by simp
-
-theorem formula_functor_reflection:
- "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)),
- \<lambda>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:
--- 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) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>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 \<in> nat; y \<in> nat; z \<in> nat |] ==> list_N_fm(x,y,z) \<in> formula"
-by (simp add: list_N_fm_def)
-
-lemma sats_list_N_fm [simp]:
- "[| x \<in> nat; y < length(env); z < length(env); env \<in> 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 \<in> nat; j < length(env); k < length(env); env \<in> 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[\<lambda>x. is_list_N(L, f(x), g(x), h(x)),
- \<lambda>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) ==
- \<exists>n[M]. \<exists>listn[M].
- finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> 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 \<in> nat; y \<in> nat |] ==> mem_list_fm(x,y) \<in> formula"
-by (simp add: mem_list_fm_def)
-
-lemma sats_mem_list_fm [simp]:
- "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> mem_list(**A, x, y) <-> sats(A, mem_list_fm(i,j), env)"
-by simp
-
-theorem mem_list_reflection:
- "REFLECTS[\<lambda>x. mem_list(L,f(x),g(x)),
- \<lambda>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) == \<forall>l[M]. l \<in> 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 \<in> nat; y \<in> nat |] ==> is_list_fm(x,y) \<in> formula"
-by (simp add: is_list_fm_def)
-
-lemma sats_is_list_fm [simp]:
- "[| x \<in> nat; y \<in> nat; env \<in> 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 \<in> nat; j \<in> nat; env \<in> list(A)|]
- ==> is_list(**A, x, y) <-> sats(A, is_list_fm(i,j), env)"
-by simp
-
-theorem is_list_reflection:
- "REFLECTS[\<lambda>x. is_list(L,f(x),g(x)),
- \<lambda>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) ==
- \<exists>zero[M]. \<exists>sn[M]. \<exists>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 \<in> nat; y \<in> nat |] ==> formula_N_fm(x,y) \<in> formula"
-by (simp add: formula_N_fm_def)
-
-lemma sats_formula_N_fm [simp]:
- "[| x < length(env); y < length(env); env \<in> 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 \<in> 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[\<lambda>x. is_formula_N(L, f(x), g(x)),
- \<lambda>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) ==
- \<exists>n[M]. \<exists>formn[M].
- finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> 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 \<in> nat ==> mem_formula_fm(x) \<in> formula"
-by (simp add: mem_formula_fm_def)
-
-lemma sats_mem_formula_fm [simp]:
- "[| x \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
- ==> mem_formula(**A, x) <-> sats(A, mem_formula_fm(i), env)"
-by simp
-
-theorem mem_formula_reflection:
- "REFLECTS[\<lambda>x. mem_formula(L,f(x)),
- \<lambda>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) == \<forall>p[M]. p \<in> 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 \<in> nat ==> is_formula_fm(x) \<in> formula"
-by (simp add: is_formula_fm_def)
-
-lemma sats_is_formula_fm [simp]:
- "[| x \<in> nat; env \<in> 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 \<in> nat; env \<in> list(A)|]
- ==> is_formula(**A, x) <-> sats(A, is_formula_fm(i), env)"
-by simp
-
-theorem is_formula_reflection:
- "REFLECTS[\<lambda>x. is_formula(L,f(x)),
- \<lambda>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 @@
\<lambda>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) ==
- \<exists>i[M]. \<exists>f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) &
- is_transrec(M,MH,i,f)"
+ \<exists>dp[M]. \<exists>i[M]. \<exists>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 \<in> 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, \<lambda>u f z.
- \<forall>fml[M].
- is_formula(M,fml) \<longrightarrow>
- 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 \<in> 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"}*}
--- 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 \