--- a/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 17 15:48:54 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 17 16:41:32 2002 +0200
@@ -106,45 +106,6 @@
-subsection {*lists without univ*}
-
-lemmas datatype_univs = Inl_in_univ Inr_in_univ
- Pair_in_univ nat_into_univ A_into_univ
-
-lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
-apply (rule bnd_monoI)
- apply (intro subset_refl zero_subset_univ A_subset_univ
- sum_subset_univ Sigma_subset_univ)
-apply (rule subset_refl sum_mono Sigma_mono | assumption)+
-done
-
-lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
-by (intro sum_contin prod_contin id_contin const_contin)
-
-text{*Re-expresses lists using sum and product*}
-lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
-apply (simp add: list_def)
-apply (rule equalityI)
- apply (rule lfp_lowerbound)
- prefer 2 apply (rule lfp_subset)
- apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
- apply (simp add: Nil_def Cons_def)
- apply blast
-txt{*Opposite inclusion*}
-apply (rule lfp_lowerbound)
- prefer 2 apply (rule lfp_subset)
-apply (clarify, subst lfp_unfold [OF list.bnd_mono])
-apply (simp add: Nil_def Cons_def)
-apply (blast intro: datatype_univs
- dest: lfp_subset [THEN subsetD])
-done
-
-text{*Re-expresses lists using "iterates", no univ.*}
-lemma list_eq_Union:
- "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
-by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
-
-
subsection {*Absoluteness for "Iterates"*}
constdefs
@@ -198,6 +159,45 @@
done
+subsection {*lists without univ*}
+
+lemmas datatype_univs = Inl_in_univ Inr_in_univ
+ Pair_in_univ nat_into_univ A_into_univ
+
+lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
+apply (rule bnd_monoI)
+ apply (intro subset_refl zero_subset_univ A_subset_univ
+ sum_subset_univ Sigma_subset_univ)
+apply (rule subset_refl sum_mono Sigma_mono | assumption)+
+done
+
+lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
+by (intro sum_contin prod_contin id_contin const_contin)
+
+text{*Re-expresses lists using sum and product*}
+lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
+apply (simp add: list_def)
+apply (rule equalityI)
+ apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset)
+ apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
+ apply (simp add: Nil_def Cons_def)
+ apply blast
+txt{*Opposite inclusion*}
+apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset)
+apply (clarify, subst lfp_unfold [OF list.bnd_mono])
+apply (simp add: Nil_def Cons_def)
+apply (blast intro: datatype_univs
+ dest: lfp_subset [THEN subsetD])
+done
+
+text{*Re-expresses lists using "iterates", no univ.*}
+lemma list_eq_Union:
+ "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
+by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
+
+
constdefs
is_list_functor :: "[i=>o,i,i,i] => o"
"is_list_functor(M,A,X,Z) ==
@@ -209,6 +209,65 @@
by (simp add: is_list_functor_def singleton_0 nat_into_M)
+subsection {*formulas without univ*}
+
+lemma formula_fun_bnd_mono:
+ "bnd_mono(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+apply (rule bnd_monoI)
+ apply (intro subset_refl zero_subset_univ A_subset_univ
+ sum_subset_univ Sigma_subset_univ nat_subset_univ)
+apply (rule subset_refl sum_mono Sigma_mono | assumption)+
+done
+
+lemma formula_fun_contin:
+ "contin(\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+by (intro sum_contin prod_contin id_contin const_contin)
+
+
+text{*Re-expresses formulas using sum and product*}
+lemma formula_eq_lfp2:
+ "formula = lfp(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+apply (simp add: formula_def)
+apply (rule equalityI)
+ apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset)
+ apply (clarify, subst lfp_unfold [OF formula_fun_bnd_mono])
+ apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)
+ apply blast
+txt{*Opposite inclusion*}
+apply (rule lfp_lowerbound)
+ prefer 2 apply (rule lfp_subset, clarify)
+apply (subst lfp_unfold [OF formula.bnd_mono, simplified])
+apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)
+apply (elim sumE SigmaE, simp_all)
+apply (blast intro: datatype_univs dest: lfp_subset [THEN subsetD])+
+done
+
+text{*Re-expresses formulas using "iterates", no univ.*}
+lemma formula_eq_Union:
+ "formula =
+ (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))) ^ n (0))"
+by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono
+ formula_fun_contin)
+
+
+constdefs
+ is_formula_functor :: "[i=>o,i,i] => o"
+ "is_formula_functor(M,X,Z) ==
+ \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. \<exists>X4[M].
+ 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,X,X3,X4) &
+ is_sum(M,natnatsum,X4,Z)"
+
+lemma (in M_axioms) formula_functor_abs [simp]:
+ "[| M(X); M(Z) |]
+ ==> is_formula_functor(M,X,Z) <->
+ Z = ((nat*nat) + (nat*nat)) + (X + (X*X + X))"
+by (simp add: is_formula_functor_def)
+
+
+subsection{*@{term M} Contains the List and Formula Datatypes*}
locale (open) M_datatypes = M_wfrank +
assumes list_replacement1:
"M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
@@ -218,6 +277,14 @@
(\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0),
msn, n, y)))"
+ and formula_replacement1:
+ "iterates_replacement(M, is_formula_functor(M), 0)"
+ and formula_replacement2:
+ "strong_replacement(M,
+ \<lambda>n y. n\<in>nat &
+ (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
+ is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0),
+ msn, n, y)))"
lemma (in M_datatypes) list_replacement2':
"M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
@@ -235,4 +302,20 @@
iterates_closed [of "is_list_functor(M,A)"])
+lemma (in M_datatypes) formula_replacement2':
+ "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
+apply (insert formula_replacement2)
+apply (rule strong_replacement_cong [THEN iffD1])
+apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
+apply (simp_all add: formula_replacement1 relativize1_def)
+done
+
+lemma (in M_datatypes) formula_closed [intro,simp]:
+ "M(formula)"
+apply (insert formula_replacement1)
+apply (simp add: RepFun_closed2 formula_eq_Union
+ formula_replacement2' relativize1_def
+ iterates_closed [of "is_formula_functor(M)"])
+done
+
end
--- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 17 15:48:54 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Wed Jul 17 16:41:32 2002 +0200
@@ -562,46 +562,6 @@
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 Operator @{term quasinat}*}
(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
@@ -785,6 +745,49 @@
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:
"REFLECTS
[\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
@@ -809,7 +812,8 @@
apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
- apply (simp_all add: lt_Ord2)
+ apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (elim conjE)
apply (rule DPow_LsetI)
apply (rename_tac v)
apply (rule bex_iff_sats conj_iff_sats)+
@@ -818,7 +822,6 @@
txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
done
@@ -864,4 +867,133 @@
apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
done
+
+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]. \<exists>X4[M].
+ 5 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,X,X3,X4) &
+ is_sum(M,natnatsum,X4,Z)" *)
+ "formula_functor_fm(X,Z) ==
+ Exists(Exists(Exists(Exists(Exists(Exists(
+ And(omega_fm(5),
+ And(cartprod_fm(5,5,4),
+ And(sum_fm(4,4,3),
+ And(cartprod_fm(X#+6,X#+6,2),
+ And(sum_fm(2,X#+6,1),
+ And(sum_fm(X#+6,1,0), sum_fm(3,0,Z#+6)))))))))))))"
+
+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:
+ "REFLECTS
+ [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+ is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+ is_wfrec(**Lset(i),
+ iterates_MH(**Lset(i),
+ is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection
+ iterates_MH_reflection formula_functor_reflection)
+
+lemma formula_replacement1:
+ "iterates_replacement(L, is_formula_functor(L), 0)"
+apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
+apply (rule strong_replacementI)
+apply (rule rallI)
+apply (rename_tac B)
+apply (rule separation_CollectI)
+apply (insert nonempty)
+apply (subgoal_tac "L(Memrel(succ(n)))")
+apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
+apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+ apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (rule DPow_LsetI)
+apply (rename_tac v)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
+apply (rule sep_rules | simp)+
+txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
+apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
+apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+
+txt{*SLOW: like 40 seconds!*}
+done
+
+lemma formula_replacement2_Reflects:
+ "REFLECTS
+ [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
+ (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
+ is_wfrec (L, iterates_MH (L, is_formula_functor(L), 0),
+ msn, u, x)),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
+ (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i).
+ successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
+ is_wfrec (**Lset(i),
+ iterates_MH (**Lset(i), is_formula_functor(**Lset(i)), 0),
+ msn, u, x))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection
+ iterates_MH_reflection formula_functor_reflection)
+
+
+lemma formula_replacement2:
+ "strong_replacement(L,
+ \<lambda>n y. n\<in>nat &
+ (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
+ is_wfrec(L, iterates_MH(L,is_formula_functor(L), 0),
+ msn, n, y)))"
+apply (rule strong_replacementI)
+apply (rule rallI)
+apply (rename_tac B)
+apply (rule separation_CollectI)
+apply (insert nonempty)
+apply (rule_tac A="{B,z,0,nat}" in subset_LsetE)
+apply (blast intro: L_nat)
+apply (rule ReflectsE [OF formula_replacement2_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 (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
+apply (rule sep_rules | simp)+
+apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
+apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+
+done
+
+text{*NB The proofs for type @{term formula} are virtually identical to those
+for @{term "list(A)"}. It was a cut-and-paste job! *}
+
end