--- a/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 16:29:36 2002 +0200
@@ -101,17 +101,14 @@
iterates_replacement :: "[i=>o, [i,i]=>o, i] => o"
"iterates_replacement(M,isF,v) ==
- \<forall>n[M]. n\<in>nat -->
+ \<forall>n[M]. n\<in>nat -->
wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
lemma (in M_axioms) iterates_MH_abs:
"[| relativize1(M,isF,F); M(n); M(g); M(z) |]
==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
-apply (simp add: iterates_MH_def)
-apply (rule nat_case_abs)
-apply (simp_all add: relativize1_def)
-done
-
+by (simp add: nat_case_abs [of _ "\<lambda>m. F(g ` m)"]
+ relativize1_def iterates_MH_def)
lemma (in M_axioms) iterates_imp_wfrec_replacement:
"[|relativize1(M,isF,F); n \<in> nat; iterates_replacement(M,isF,v)|]
@@ -159,28 +156,20 @@
locale M_datatypes = M_wfrank +
assumes list_replacement1:
- "M(A) ==> \<exists>zero[M]. empty(M,zero) &
- iterates_replacement(M, is_list_functor(M,A), zero)"
+ "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
and list_replacement2:
- "M(A) ==>
- \<exists>zero[M]. empty(M,zero) &
- strong_replacement(M,
+ "M(A) ==> 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_list_functor(M,A), zero),
+ is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0),
msn, n, y)))"
-lemma (in M_datatypes) list_replacement1':
- "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
-apply (insert list_replacement1, simp)
-done
-
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))"
apply (insert list_replacement2 [of A])
apply (rule strong_replacement_cong [THEN iffD1])
apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
-apply (simp_all add: list_replacement1' relativize1_def)
+apply (simp_all add: list_replacement1 relativize1_def)
done
lemma (in M_datatypes) list_closed [intro,simp]:
--- a/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:29:36 2002 +0200
@@ -66,7 +66,8 @@
apply (simp_all add: Replace_iff univalent_def, blast)
done
-subsection{*Instantiation of the locale @{text M_triv_axioms}*}
+subsection{*Instantiating the locale @{text M_triv_axioms}*}
+text{*No instances of Separation yet.*}
lemma Lset_mono_le: "mono_le_subset(Lset)"
by (simp add: mono_le_subset_def le_imp_subset Lset_mono)
@@ -90,57 +91,57 @@
fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);
-fun trivaxL th =
+fun triv_axioms_L th =
kill_flex_triv_prems
([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat]
MRS (inst "M" "L" th));
-bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));
-bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));
-bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));
-bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));
-bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));
-bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));
-bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));
-bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));
-bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));
-bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));
-bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));
-bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));
-bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));
-bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));
-bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));
-bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));
-bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));
-bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));
-bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));
-bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));
-bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));
-bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));
-bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));
-bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));
-bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));
-bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));
-bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));
-bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));
-bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));
-bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));
-bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));
-bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));
-bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));
-bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));
-bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));
-bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));
-bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));
-bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));
-bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));
-bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));
-bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));
-bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));
-bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));
-bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
-bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));
-bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));
+bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs"));
+bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs"));
+bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs"));
+bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs"));
+bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv"));
+bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI"));
+bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs"));
+bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs"));
+bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs"));
+bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff"));
+bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff"));
+bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs"));
+bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff"));
+bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M"));
+bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs"));
+bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs"));
+bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs"));
+bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs"));
+bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs"));
+bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed"));
+bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed"));
+bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed"));
+bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs"));
+bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff"));
+bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed"));
+bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI"));
+bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed"));
+bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed"));
+bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed"));
+bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs"));
+bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow"));
+bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow"));
+bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M"));
+bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed"));
+bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff"));
+bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff"));
+bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed"));
+bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs"));
+bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs"));
+bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs"));
+bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs"));
+bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs"));
+bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs"));
+bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs"));
+bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs"));
*}
declare ball_abs [simp]
@@ -563,6 +564,39 @@
done
+subsubsection{*The Number 1, Internalized*}
+
+(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
+constdefs number1_fm :: "i=>i"
+ "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
+
+lemma number1_type [TC]:
+ "x \<in> nat ==> number1_fm(x) \<in> formula"
+by (simp add: number1_fm_def)
+
+lemma arity_number1_fm [simp]:
+ "x \<in> nat ==> arity(number1_fm(x)) = succ(x)"
+by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_number1_fm [simp]:
+ "[| x \<in> nat; env \<in> list(A)|]
+ ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))"
+by (simp add: number1_fm_def number1_def)
+
+lemma number1_iff_sats:
+ "[| nth(i,env) = x; nth(j,env) = y;
+ i \<in> nat; env \<in> list(A)|]
+ ==> number1(**A, x) <-> sats(A, number1_fm(i), env)"
+by simp
+
+theorem number1_reflection:
+ "REFLECTS[\<lambda>x. number1(L,f(x)),
+ \<lambda>i x. number1(**Lset(i),f(x))]"
+apply (simp only: number1_def setclass_simps)
+apply (intro FOL_reflections empty_reflection successor_reflection)
+done
+
+
subsubsection{*Big Union, Internalized*}
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
@@ -1076,7 +1110,8 @@
by simp
lemmas function_reflections =
- empty_reflection upair_reflection pair_reflection union_reflection
+ empty_reflection number1_reflection
+ upair_reflection pair_reflection union_reflection
big_union_reflection cons_reflection successor_reflection
fun_apply_reflection subset_reflection
transitive_set_reflection membership_reflection
@@ -1085,7 +1120,8 @@
is_relation_reflection is_function_reflection
lemmas function_iff_sats =
- empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats
+ empty_iff_sats number1_iff_sats
+ upair_iff_sats pair_iff_sats union_iff_sats
cons_iff_sats successor_iff_sats
fun_apply_iff_sats Memrel_iff_sats
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
--- a/src/ZF/Constructible/Rec_Separation.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy Tue Jul 16 16:29:36 2002 +0200
@@ -1,10 +1,13 @@
-header{*Separation for the Absoluteness of Recursion*}
+header{*Separation for Facts About Recursion*}
-theory Rec_Separation = Separation:
+theory Rec_Separation = Separation + Datatype_absolute:
text{*This theory proves all instances needed for locales @{text
"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
+lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
+by simp
+
subsection{*The Locale @{text "M_trancl"}*}
subsubsection{*Separation for Reflexive/Transitive Closure*}
@@ -194,6 +197,40 @@
apply (simp_all add: succ_Un_distrib [symmetric])
done
+
+subsubsection{*Instantiating the locale @{text M_trancl}*}
+ML
+{*
+val rtrancl_separation = thm "rtrancl_separation";
+val wellfounded_trancl_separation = thm "wellfounded_trancl_separation";
+
+
+val m_trancl = [rtrancl_separation, wellfounded_trancl_separation];
+
+fun trancl_L th =
+ kill_flex_triv_prems (m_trancl MRS (axioms_L th));
+
+bind_thm ("iterates_abs", trancl_L (thm "M_trancl.iterates_abs"));
+bind_thm ("rtran_closure_rtrancl", trancl_L (thm "M_trancl.rtran_closure_rtrancl"));
+bind_thm ("rtrancl_closed", trancl_L (thm "M_trancl.rtrancl_closed"));
+bind_thm ("rtrancl_abs", trancl_L (thm "M_trancl.rtrancl_abs"));
+bind_thm ("trancl_closed", trancl_L (thm "M_trancl.trancl_closed"));
+bind_thm ("trancl_abs", trancl_L (thm "M_trancl.trancl_abs"));
+bind_thm ("wellfounded_on_trancl", trancl_L (thm "M_trancl.wellfounded_on_trancl"));
+bind_thm ("wellfounded_trancl", trancl_L (thm "M_trancl.wellfounded_trancl"));
+bind_thm ("wfrec_relativize", trancl_L (thm "M_trancl.wfrec_relativize"));
+bind_thm ("trans_wfrec_relativize", trancl_L (thm "M_trancl.trans_wfrec_relativize"));
+bind_thm ("trans_wfrec_abs", trancl_L (thm "M_trancl.trans_wfrec_abs"));
+bind_thm ("trans_eq_pair_wfrec_iff", trancl_L (thm "M_trancl.trans_eq_pair_wfrec_iff"));
+bind_thm ("eq_pair_wfrec_iff", trancl_L (thm "M_trancl.eq_pair_wfrec_iff"));
+*}
+
+declare rtrancl_closed [intro,simp]
+declare rtrancl_abs [simp]
+declare trancl_closed [intro,simp]
+declare trancl_abs [simp]
+
+
subsection{*Well-Founded Recursion!*}
(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
@@ -275,7 +312,22 @@
restriction_reflection MH_reflection)
done
-subsection{*Separation for @{term "wfrank"}*}
+text{*Currently, @{text sats}-theorems for higher-order operators don't seem
+useful. Reflection theorems do work, though. This one avoids the repetition
+of the @{text MH}-term.*}
+theorem is_wfrec_reflection:
+ assumes MH_reflection:
+ "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
+ \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
+ shows "REFLECTS[\<lambda>x. is_wfrec(L, MH(L), f(x), g(x), h(x)),
+ \<lambda>i x. is_wfrec(**Lset(i), MH(**Lset(i)), 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"}*}
lemma wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
@@ -305,7 +357,7 @@
done
-subsection{*Replacement for @{term "wfrank"}*}
+subsubsection{*Replacement for @{term "wfrank"}*}
lemma wfrank_replacement_Reflects:
"REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
@@ -347,7 +399,7 @@
done
-subsection{*Separation for @{term "wfrank"}*}
+subsubsection{*Separation for Proving @{text Ord_wfrank_range}*}
lemma Ord_wfrank_Reflects:
"REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
@@ -387,4 +439,438 @@
done
+subsubsection{*Instantiating the locale @{text M_wfrank}*}
+ML
+{*
+val wfrank_separation = thm "wfrank_separation";
+val wfrank_strong_replacement = thm "wfrank_strong_replacement";
+val Ord_wfrank_separation = thm "Ord_wfrank_separation";
+
+val m_wfrank =
+ [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation];
+
+fun wfrank_L th =
+ kill_flex_triv_prems (m_wfrank MRS (trancl_L th));
+
+
+
+bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed"));
+bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank"));
+bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank"));
+bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range"));
+bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank"));
+bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank"));
+bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank"));
+bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type"));
+bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank"));
+bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq"));
+bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt"));
+bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage"));
+bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf"));
+bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on"));
+bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs"));
+bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs"));
+bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff"));
+bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed"));
+bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed"));
+*}
+
+declare iterates_closed [intro,simp]
+declare Ord_wfrank_range [rule_format]
+declare wf_abs [simp]
+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 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))" *)
+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}*}
+
+(* 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, 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(1,0))))),
+ Or(quasinat_fm(k), empty_fm(z))))"
+
+lemma is_nat_case_type [TC]:
+ "[| is_b(1,0) \<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 arity_is_nat_case_fm [simp]:
+ "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(is_nat_case_fm(x,is_b,y,z)) =
+ succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)"
+apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")
+apply typecheck
+(*FIXME: could nat_diff_split work?*)
+apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
+ succ_Un_distrib [symmetric] Un_ac
+ split: split_nat_case)
+done
+
+lemma sats_is_nat_case_fm:
+ assumes is_b_iff_sats:
+ "!!a b. [| a \<in> A; b \<in> A|]
+ ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, 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 b. [| a \<in> A; b \<in> A|]
+ ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, 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, i]=>i"
+ "iterates_MH_fm(isF,v,n,g,z) ==
+ is_nat_case_fm(v,
+ \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0),
+ Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))),
+ n, z)"
+
+lemma iterates_MH_type [TC]:
+ "[| p(1,0) \<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 arity_iterates_MH_fm [simp]:
+ "[| p(1,0) \<in> formula;
+ v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
+ ==> arity(iterates_MH_fm(p,v,x,y,z)) =
+ succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
+apply (subgoal_tac "arity(p(1,0)) \<in> nat")
+apply typecheck
+apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
+ split: split_nat_case, clarify)
+apply (rename_tac i j)
+apply (drule eq_succ_imp_eq_m1, simp)
+apply (drule eq_succ_imp_eq_m1, simp)
+apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
+done
+
+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(1,0), 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))"
+by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
+ is_F_iff_sats [symmetric])
+
+lemma iterates_MH_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(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
+ 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)"
+apply (rule iff_sym)
+apply (rule iff_trans)
+apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
+done
+
+theorem iterates_MH_reflection:
+ assumes p_reflection:
+ "!!f g h. REFLECTS[\<lambda>x. p(L, f(x), g(x)),
+ \<lambda>i x. p(**Lset(i), f(x), g(x))]"
+ shows "REFLECTS[\<lambda>x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)),
+ \<lambda>i x. iterates_MH(**Lset(i), p(**Lset(i)), 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}*}
+
+
+lemma list_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_list_functor(L,A), 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_list_functor(**Lset(i), A), 0), memsn, u, y))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection
+ iterates_MH_reflection list_functor_reflection)
+
+lemma list_replacement1:
+ "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 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,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
+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 (rule DPowI2)
+apply (rename_tac v)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,A,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 list_functor_iff_sats quasinat_iff_sats | simp)+
+apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
+done
+
+
+lemma list_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_list_functor(L, A), 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_list_functor(**Lset(i), A), 0),
+ msn, u, x))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection
+ iterates_MH_reflection list_functor_reflection)
+
+
+lemma list_replacement2:
+ "L(A) ==> 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_list_functor(L,A), 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="{A,B,z,0,nat}" in subset_LsetE)
+apply (blast intro: L_nat)
+apply (rule ReflectsE [OF list_replacement2_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption)
+apply (erule reflection_imp_L_separation)
+ apply (simp_all add: lt_Ord2)
+apply (rule DPowI2)
+apply (rename_tac v)
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,A,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 list_functor_iff_sats quasinat_iff_sats | simp)+
+apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
+done
+
+
+
end
--- a/src/ZF/Constructible/Relative.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Jul 16 16:29:36 2002 +0200
@@ -28,6 +28,15 @@
successor :: "[i=>o,i,i] => o"
"successor(M,a,z) == is_cons(M,a,a,z)"
+ number1 :: "[i=>o,i] => o"
+ "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
+
+ number2 :: "[i=>o,i] => o"
+ "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
+
+ number3 :: "[i=>o,i] => o"
+ "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
+
powerset :: "[i=>o,i,i] => o"
"powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
@@ -161,15 +170,6 @@
--{*omega is a limit ordinal none of whose elements are limit*}
"omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
- number1 :: "[i=>o,i] => o"
- "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))"
-
- number2 :: "[i=>o,i] => o"
- "number2(M,a) == (\<exists>x[M]. number1(M,x) & successor(M,x,a))"
-
- number3 :: "[i=>o,i] => o"
- "number3(M,a) == (\<exists>x[M]. number2(M,x) & successor(M,x,a))"
-
is_quasinat :: "[i=>o,i] => o"
"is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
@@ -177,7 +177,7 @@
"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) | z=0)"
+ (is_quasinat(M,k) | empty(M,z))"
relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
"relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
@@ -669,8 +669,10 @@
apply (simp_all add: relativize1_def)
done
-(*Needed? surely better to replace is_nat_case by nat_case?*)
-lemma (in M_triv_axioms) is_nat_case_cong [cong]:
+(*NOT for the simplifier. The assumption M(z') is apparently necessary, but
+ causes the error "Failed congruence proof!" It may be better to replace
+ is_nat_case by nat_case before attempting congruence reasoning.*)
+lemma (in M_triv_axioms) is_nat_case_cong:
"[| a = a'; k = k'; z = z'; M(z');
!!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
--- a/src/ZF/Constructible/Separation.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy Tue Jul 16 16:29:36 2002 +0200
@@ -457,6 +457,10 @@
done
+subsection{*Instantiating the locale @{text M_axioms}*}
+text{*Separation (and Strong Replacement) for basic set-theoretic constructions
+such as intersection, Cartesian Product and image.*}
+
ML
{*
val Inter_separation = thm "Inter_separation";
@@ -481,119 +485,119 @@
well_ord_iso_separation, obase_separation,
obase_equals_separation, omap_replacement, is_recfun_separation]
-fun axiomsL th =
- kill_flex_triv_prems (m_axioms MRS (trivaxL th));
+fun axioms_L th =
+ kill_flex_triv_prems (m_axioms MRS (triv_axioms_L th));
-bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff"));
-bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed"));
-bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed"));
-bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff"));
-bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed"));
-bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs"));
-bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed"));
-bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs"));
-bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed"));
-bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs"));
-bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed"));
-bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs"));
-bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed"));
-bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs"));
-bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed"));
-bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs"));
-bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
-bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
-bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
-bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
-bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
-bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
-bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs"));
-bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff"));
-bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed"));
-bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs"));
-bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function"));
-bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs"));
-bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff"));
-bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed"));
-bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs"));
-bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed"));
-bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed"));
-bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed"));
-bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs"));
-bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2"));
-bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ"));
-bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed"));
+bind_thm ("cartprod_iff", axioms_L (thm "M_axioms.cartprod_iff"));
+bind_thm ("cartprod_closed", axioms_L (thm "M_axioms.cartprod_closed"));
+bind_thm ("sum_closed", axioms_L (thm "M_axioms.sum_closed"));
+bind_thm ("M_converse_iff", axioms_L (thm "M_axioms.M_converse_iff"));
+bind_thm ("converse_closed", axioms_L (thm "M_axioms.converse_closed"));
+bind_thm ("converse_abs", axioms_L (thm "M_axioms.converse_abs"));
+bind_thm ("image_closed", axioms_L (thm "M_axioms.image_closed"));
+bind_thm ("vimage_abs", axioms_L (thm "M_axioms.vimage_abs"));
+bind_thm ("vimage_closed", axioms_L (thm "M_axioms.vimage_closed"));
+bind_thm ("domain_abs", axioms_L (thm "M_axioms.domain_abs"));
+bind_thm ("domain_closed", axioms_L (thm "M_axioms.domain_closed"));
+bind_thm ("range_abs", axioms_L (thm "M_axioms.range_abs"));
+bind_thm ("range_closed", axioms_L (thm "M_axioms.range_closed"));
+bind_thm ("field_abs", axioms_L (thm "M_axioms.field_abs"));
+bind_thm ("field_closed", axioms_L (thm "M_axioms.field_closed"));
+bind_thm ("relation_abs", axioms_L (thm "M_axioms.relation_abs"));
+bind_thm ("function_abs", axioms_L (thm "M_axioms.function_abs"));
+bind_thm ("apply_closed", axioms_L (thm "M_axioms.apply_closed"));
+bind_thm ("apply_abs", axioms_L (thm "M_axioms.apply_abs"));
+bind_thm ("typed_function_abs", axioms_L (thm "M_axioms.typed_function_abs"));
+bind_thm ("injection_abs", axioms_L (thm "M_axioms.injection_abs"));
+bind_thm ("surjection_abs", axioms_L (thm "M_axioms.surjection_abs"));
+bind_thm ("bijection_abs", axioms_L (thm "M_axioms.bijection_abs"));
+bind_thm ("M_comp_iff", axioms_L (thm "M_axioms.M_comp_iff"));
+bind_thm ("comp_closed", axioms_L (thm "M_axioms.comp_closed"));
+bind_thm ("composition_abs", axioms_L (thm "M_axioms.composition_abs"));
+bind_thm ("restriction_is_function", axioms_L (thm "M_axioms.restriction_is_function"));
+bind_thm ("restriction_abs", axioms_L (thm "M_axioms.restriction_abs"));
+bind_thm ("M_restrict_iff", axioms_L (thm "M_axioms.M_restrict_iff"));
+bind_thm ("restrict_closed", axioms_L (thm "M_axioms.restrict_closed"));
+bind_thm ("Inter_abs", axioms_L (thm "M_axioms.Inter_abs"));
+bind_thm ("Inter_closed", axioms_L (thm "M_axioms.Inter_closed"));
+bind_thm ("Int_closed", axioms_L (thm "M_axioms.Int_closed"));
+bind_thm ("finite_fun_closed", axioms_L (thm "M_axioms.finite_fun_closed"));
+bind_thm ("is_funspace_abs", axioms_L (thm "M_axioms.is_funspace_abs"));
+bind_thm ("succ_fun_eq2", axioms_L (thm "M_axioms.succ_fun_eq2"));
+bind_thm ("funspace_succ", axioms_L (thm "M_axioms.funspace_succ"));
+bind_thm ("finite_funspace_closed", axioms_L (thm "M_axioms.finite_funspace_closed"));
*}
ML
{*
-bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal"));
-bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut"));
-bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional"));
-bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize"));
-bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict"));
-bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun"));
-bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep"));
-bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun"));
-bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun"));
-bind_thm ("is_recfun_abs", axiomsL (thm "M_axioms.is_recfun_abs"));
-bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs"));
-bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs"));
-bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs"));
-bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on"));
-bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear"));
-bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on"));
-bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on"));
-bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A"));
-bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded"));
-bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded"));
-bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
-bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
-bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct"));
-bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct"));
-bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2"));
-bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized"));
-bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized"));
-bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized"));
-bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized"));
-bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized"));
-bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs"));
-bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs"));
+bind_thm ("is_recfun_equal", axioms_L (thm "M_axioms.is_recfun_equal"));
+bind_thm ("is_recfun_cut", axioms_L (thm "M_axioms.is_recfun_cut"));
+bind_thm ("is_recfun_functional", axioms_L (thm "M_axioms.is_recfun_functional"));
+bind_thm ("is_recfun_relativize", axioms_L (thm "M_axioms.is_recfun_relativize"));
+bind_thm ("is_recfun_restrict", axioms_L (thm "M_axioms.is_recfun_restrict"));
+bind_thm ("univalent_is_recfun", axioms_L (thm "M_axioms.univalent_is_recfun"));
+bind_thm ("exists_is_recfun_indstep", axioms_L (thm "M_axioms.exists_is_recfun_indstep"));
+bind_thm ("wellfounded_exists_is_recfun", axioms_L (thm "M_axioms.wellfounded_exists_is_recfun"));
+bind_thm ("wf_exists_is_recfun", axioms_L (thm "M_axioms.wf_exists_is_recfun"));
+bind_thm ("is_recfun_abs", axioms_L (thm "M_axioms.is_recfun_abs"));
+bind_thm ("irreflexive_abs", axioms_L (thm "M_axioms.irreflexive_abs"));
+bind_thm ("transitive_rel_abs", axioms_L (thm "M_axioms.transitive_rel_abs"));
+bind_thm ("linear_rel_abs", axioms_L (thm "M_axioms.linear_rel_abs"));
+bind_thm ("wellordered_is_trans_on", axioms_L (thm "M_axioms.wellordered_is_trans_on"));
+bind_thm ("wellordered_is_linear", axioms_L (thm "M_axioms.wellordered_is_linear"));
+bind_thm ("wellordered_is_wellfounded_on", axioms_L (thm "M_axioms.wellordered_is_wellfounded_on"));
+bind_thm ("wellfounded_imp_wellfounded_on", axioms_L (thm "M_axioms.wellfounded_imp_wellfounded_on"));
+bind_thm ("wellfounded_on_subset_A", axioms_L (thm "M_axioms.wellfounded_on_subset_A"));
+bind_thm ("wellfounded_on_iff_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_iff_wellfounded"));
+bind_thm ("wellfounded_on_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_imp_wellfounded"));
+bind_thm ("wellfounded_on_field_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_field_imp_wellfounded"));
+bind_thm ("wellfounded_iff_wellfounded_on_field", axioms_L (thm "M_axioms.wellfounded_iff_wellfounded_on_field"));
+bind_thm ("wellfounded_induct", axioms_L (thm "M_axioms.wellfounded_induct"));
+bind_thm ("wellfounded_on_induct", axioms_L (thm "M_axioms.wellfounded_on_induct"));
+bind_thm ("wellfounded_on_induct2", axioms_L (thm "M_axioms.wellfounded_on_induct2"));
+bind_thm ("linear_imp_relativized", axioms_L (thm "M_axioms.linear_imp_relativized"));
+bind_thm ("trans_on_imp_relativized", axioms_L (thm "M_axioms.trans_on_imp_relativized"));
+bind_thm ("wf_on_imp_relativized", axioms_L (thm "M_axioms.wf_on_imp_relativized"));
+bind_thm ("wf_imp_relativized", axioms_L (thm "M_axioms.wf_imp_relativized"));
+bind_thm ("well_ord_imp_relativized", axioms_L (thm "M_axioms.well_ord_imp_relativized"));
+bind_thm ("order_isomorphism_abs", axioms_L (thm "M_axioms.order_isomorphism_abs"));
+bind_thm ("pred_set_abs", axioms_L (thm "M_axioms.pred_set_abs"));
*}
ML
{*
-bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed"));
-bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs"));
-bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff"));
-bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed"));
-bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD"));
-bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq"));
-bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym"));
-bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym"));
-bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt"));
-bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff"));
-bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff"));
-bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique"));
-bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord"));
-bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff"));
-bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range"));
-bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype"));
-bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap"));
-bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset"));
-bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype"));
-bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij"));
-bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso"));
-bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred"));
-bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso"));
-bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals"));
-bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
-bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists"));
-bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists"));
-bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists"));
-bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype"));
-bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists"));
-bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord"));
-bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs"));
+bind_thm ("pred_closed", axioms_L (thm "M_axioms.pred_closed"));
+bind_thm ("membership_abs", axioms_L (thm "M_axioms.membership_abs"));
+bind_thm ("M_Memrel_iff", axioms_L (thm "M_axioms.M_Memrel_iff"));
+bind_thm ("Memrel_closed", axioms_L (thm "M_axioms.Memrel_closed"));
+bind_thm ("wellordered_iso_predD", axioms_L (thm "M_axioms.wellordered_iso_predD"));
+bind_thm ("wellordered_iso_pred_eq", axioms_L (thm "M_axioms.wellordered_iso_pred_eq"));
+bind_thm ("wellfounded_on_asym", axioms_L (thm "M_axioms.wellfounded_on_asym"));
+bind_thm ("wellordered_asym", axioms_L (thm "M_axioms.wellordered_asym"));
+bind_thm ("ord_iso_pred_imp_lt", axioms_L (thm "M_axioms.ord_iso_pred_imp_lt"));
+bind_thm ("obase_iff", axioms_L (thm "M_axioms.obase_iff"));
+bind_thm ("omap_iff", axioms_L (thm "M_axioms.omap_iff"));
+bind_thm ("omap_unique", axioms_L (thm "M_axioms.omap_unique"));
+bind_thm ("omap_yields_Ord", axioms_L (thm "M_axioms.omap_yields_Ord"));
+bind_thm ("otype_iff", axioms_L (thm "M_axioms.otype_iff"));
+bind_thm ("otype_eq_range", axioms_L (thm "M_axioms.otype_eq_range"));
+bind_thm ("Ord_otype", axioms_L (thm "M_axioms.Ord_otype"));
+bind_thm ("domain_omap", axioms_L (thm "M_axioms.domain_omap"));
+bind_thm ("omap_subset", axioms_L (thm "M_axioms.omap_subset"));
+bind_thm ("omap_funtype", axioms_L (thm "M_axioms.omap_funtype"));
+bind_thm ("wellordered_omap_bij", axioms_L (thm "M_axioms.wellordered_omap_bij"));
+bind_thm ("omap_ord_iso", axioms_L (thm "M_axioms.omap_ord_iso"));
+bind_thm ("Ord_omap_image_pred", axioms_L (thm "M_axioms.Ord_omap_image_pred"));
+bind_thm ("restrict_omap_ord_iso", axioms_L (thm "M_axioms.restrict_omap_ord_iso"));
+bind_thm ("obase_equals", axioms_L (thm "M_axioms.obase_equals"));
+bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
+bind_thm ("obase_exists", axioms_L (thm "M_axioms.obase_exists"));
+bind_thm ("omap_exists", axioms_L (thm "M_axioms.omap_exists"));
+bind_thm ("otype_exists", axioms_L (thm "M_axioms.otype_exists"));
+bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype"));
+bind_thm ("ordertype_exists", axioms_L (thm "M_axioms.ordertype_exists"));
+bind_thm ("relativized_imp_well_ord", axioms_L (thm "M_axioms.relativized_imp_well_ord"));
+bind_thm ("well_ord_abs", axioms_L (thm "M_axioms.well_ord_abs"));
*}
declare cartprod_closed [intro,simp]
--- a/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 16:28:49 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 16:29:36 2002 +0200
@@ -611,19 +611,6 @@
apply (simp add: wfrec_relativize, blast)
done
-lemma (in M_wfrank) wfrec_closed_lemma [rule_format]:
- "[|wf(r); M(r);
- strong_replacement(M, \<lambda>x y. y = \<langle>x, wfrec(r, x, H)\<rangle>);
- \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g)) |]
- ==> M(a) --> M(wfrec(r,a,H))"
-apply (rule_tac a=a in wf_induct, assumption+)
-apply (subst wfrec, assumption, clarify)
-apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)"
- in rspec [THEN rspec])
-apply (simp_all add: function_lam)
-apply (blast intro: dest: pair_components_in_M )
-done
-
text{*Full version not assuming transitivity, but maybe not very useful.*}
theorem (in M_wfrank) wfrec_closed:
"[|wf(r); M(r); M(a);