diff --git a/thys/Independence_CH/Definitions_Main.thy b/thys/Independence_CH/Definitions_Main.thy --- a/thys/Independence_CH/Definitions_Main.thy +++ b/thys/Independence_CH/Definitions_Main.thy @@ -1,640 +1,640 @@ section\Main definitions of the development\label{sec:main-definitions}\ theory Definitions_Main imports Absolute_Versions begin text\This theory gathers the main definitions of the \<^session>\Transitive_Models\ session and the present one. It might be considered as the bare minimum reading requisite to trust that our development indeed formalizes the theory of forcing. This should be mathematically clear since this is the only known method for obtaining proper extensions of ctms while preserving the ordinals. The main theorem of this session and all of its relevant definitions appear in Section~\ref{sec:def-main-forcing}. The reader trusting all the libraries on which our development is based, might jump directly to Section~\ref{sec:relative-arith}, which treats relative cardinal arithmetic as implemented in \<^session>\Transitive_Models\. But in case one wants to dive deeper, the following sections treat some basic concepts of the ZF logic (Section~\ref{sec:def-main-ZF}) and in the ZF-Constructible library (Section~\ref{sec:def-main-relative}) on which our definitions are built. \ declare [[show_question_marks=false]] subsection\ZF\label{sec:def-main-ZF}\ text\For the basic logic ZF we restrict ourselves to just a few concepts.\ thm bij_def[unfolded inj_def surj_def] text\@{thm [display] bij_def[unfolded inj_def surj_def]}\ (* bij(A, B) \ {f \ A \ B . \w\A. \x\A. f ` w = f ` x \ w = x} \ {f \ A \ B . \y\B. \x\A. f ` x = y} *) thm eqpoll_def text\@{thm [display] eqpoll_def}\ (* A \ B \ \f. f \ bij(A, B) *) thm Transset_def text\@{thm [display] Transset_def}\ (* Transset(i) \ \x\i. x \ i *) thm Ord_def text\@{thm [display] Ord_def}\ (* Ord(i) \ Transset(i) \ (\x\i. Transset(x)) *) thm lt_def le_iff text\@{thm [display] lt_def le_iff}\ (* i < j \ i \ j \ Ord(j) i \ j \ i < j \ i = j \ Ord(j) *) text\With the concepts of empty set and successor in place,\ lemma empty_def': "\x. x \ 0" by simp lemma succ_def': "succ(i) = i \ {i}" by blast text\we can define the set of natural numbers \<^term>\\\. In the sources, it is defined as a fixpoint, but here we just write its characterization as the first limit ordinal.\ thm Limit_nat[unfolded Limit_def] nat_le_Limit[unfolded Limit_def] text\@{thm [display] Limit_nat[unfolded Limit_def] nat_le_Limit[unfolded Limit_def]}\ (* Ord(\) \ 0 < \ \ (\y. y < \ \ succ(y) < \) Ord(i) \ 0 < i \ (\y. y < i \ succ(y) < i) \ \ \ i *) text\Then, addition and predecessor on \<^term>\\\ are inductively characterized as follows:\ thm add_0_right add_succ_right pred_0 pred_succ_eq text\@{thm [display] add_succ_right add_0_right pred_0 pred_succ_eq}\ (* m \ \ \ m +\<^sub>\ 0 = m m +\<^sub>\ succ(n) = succ(m +\<^sub>\ n) pred(0) = 0 pred(succ(y)) = y *) text\Lists on a set \<^term>\A\ can be characterized by being recursively generated from the empty list \<^term>\[]\ and the operation \<^term>\Cons\ that adds a new element to the left end; the induction theorem for them shows that the characterization is “complete”.\ thm Nil Cons list.induct text\@{thm [display] Nil Cons list.induct }\ (* [] \ list(A) a \ A \ l \ list(A) \ Cons(a, l) \ list(A) x \ list(A) \ P([]) \ (\a l. a \ A \ l \ list(A) \ P(l) \ P(Cons(a, l))) \ P(x) *) text\Length, concatenation, and \<^term>\n\th element of lists are recursively characterized as follows.\ thm length.simps app.simps nth_0 nth_Cons text\@{thm [display] length.simps app.simps nth_0 nth_Cons}\ (* length([]) = 0 length(Cons(a, l)) = succ(length(l)) [] @ ys = ys Cons(a, l) @ ys = Cons(a, l @ ys) nth(0, Cons(a, l)) = a n \ \ \ nth(succ(n), Cons(a, l)) = nth(n, l) *) text\We have the usual Haskell-like notation for iterated applications of \<^term>\Cons\:\ lemma Cons_app: "[a,b,c] = Cons(a,Cons(b,Cons(c,[])))" .. text\Relative quantifiers restrict the range of the bound variable to a class \<^term>\M\ of type \<^typ>\i\o\; that is, a truth-valued function with set arguments.\ lemma "\x[M]. P(x) \ \x. M(x) \ P(x)" "\x[M]. P(x) \ \x. M(x) \ P(x)" unfolding rall_def rex_def . text\Finally, a set can be viewed (“cast”) as a class using the following function of type \<^typ>\i\(i\o)\.\ thm setclass_iff text\@{thm [display] setclass_iff}\ (* (##A)(x) \ x \ A *) subsection\Relative concepts\label{sec:def-main-relative}\ text\A list of relative concepts (mostly from the ZF-Constructible library) follows next.\ thm big_union_def text\@{thm [display] big_union_def}\ (* big_union(M, A, z) \ \x[M]. x \ z \ (\y[M]. y \ A \ x \ y) *) thm upair_def text\@{thm [display] upair_def}\ (* upair(M, a, b, z) \ a \ z \ b \ z \ (\x[M]. x \ z \ x = a \ x = b) *) thm pair_def text\@{thm [display] pair_def}\ (* pair(M, a, b, z) \ \x[M]. upair(M, a, a, x) \ (\y[M]. upair(M, a, b, y) \ upair(M, x, y, z)) *) thm successor_def[unfolded is_cons_def union_def] text\@{thm [display] successor_def[unfolded is_cons_def union_def]}\ (* successor(M, a, z) \ \x[M]. upair(M, a, a, x) \ (\xa[M]. xa \ z \ xa \ x \ xa \ a) *) thm empty_def text\@{thm [display] empty_def}\ (* empty(M, z) \ \x[M]. x \ z *) thm transitive_set_def[unfolded subset_def] text\@{thm [display] transitive_set_def[unfolded subset_def]}\ (* transitive_set(M, a) \ \x[M]. x \ a \ (\xa[M]. xa \ x \ xa \ a) *) thm ordinal_def text\@{thm [display] ordinal_def}\ (* ordinal(M, a) \ transitive_set(M, a) \ (\x[M]. x \ a \ transitive_set(M, x)) *) thm image_def text\@{thm [display] image_def}\ (* image(M, r, A, z) \ \y[M]. y \ z \ (\w[M]. w \ r \ (\x[M]. x \ A \ pair(M, x, y, w))) *) thm fun_apply_def text\@{thm [display] fun_apply_def}\ (* fun_apply(M, f, x, y) \ \xs[M]. \fxs[M]. upair(M, x, x, xs) \ image(M, f, xs, fxs) \ big_union(M, fxs, y) *) thm is_function_def text\@{thm [display] is_function_def}\ (* is_function(M, r) \ \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. pair(M, x, y, p) \ pair(M, x, y', p') \ p \ r \ p' \ r \ y = y' *) thm is_relation_def text\@{thm [display] is_relation_def}\ (* is_relation(M, r) \ \z[M]. z \ r \ (\x[M]. \y[M]. pair(M, x, y, z)) *) thm is_domain_def text\@{thm [display] is_domain_def}\ (* is_domain(M, r, z) \ \x[M]. x \ z \ (\w[M]. w \ r \ (\y[M]. pair(M, x, y, w))) *) thm typed_function_def text\@{thm [display] typed_function_def}\ (* typed_function(M, A, B, r) \ is_function(M, r) \ is_relation(M, r) \ is_domain(M, r, A) \ (\u[M]. u \ r \ (\x[M]. \y[M]. pair(M, x, y, u) \ y \ B)) *) thm is_function_space_def[unfolded is_funspace_def] function_space_rel_def surjection_def text\@{thm [display] is_function_space_def[unfolded is_funspace_def] function_space_rel_def surjection_def}\ (* is_function_space(M, A, B, fs) \ M(fs) \ (\f[M]. f \ fs \ typed_function(M, A, B, f)) A \\<^bsup>M\<^esup> B \ THE d. is_function_space(M, A, B, d) surjection(M, A, B, f) \ typed_function(M, A, B, f) \ (\y[M]. y \ B \ (\x[M]. x \ A \ is_apply(M, f, x, y))) *) text\Relative version of the $\ZFC$ axioms\ thm extensionality_def text\@{thm [display] extensionality_def}\ (* extensionality(M) \ \x[M]. \y[M]. (\z[M]. z \ x \ z \ y) \ x = y *) thm foundation_ax_def text\@{thm [display] foundation_ax_def}\ (* foundation_ax(M) \ \x[M]. (\y[M]. y \ x) \ (\y[M]. y \ x \ \ (\z[M]. z \ x \ z \ y)) *) thm upair_ax_def text\@{thm [display] upair_ax_def}\ (* upair_ax(M) \ \x[M]. \y[M]. \z[M]. upair(M, x, y, z) *) thm Union_ax_def text\@{thm [display] Union_ax_def}\ (* Union_ax(M) \ \x[M]. \z[M]. \xa[M]. xa \ z \ (\y[M]. y \ x \ xa \ y) *) thm power_ax_def[unfolded powerset_def subset_def] text\@{thm [display] power_ax_def[unfolded powerset_def subset_def]}\ (* power_ax(M) \ \x[M]. \z[M]. \xa[M]. xa \ z \ (\xb[M]. xb \ xa \ xb \ x) *) thm infinity_ax_def text\@{thm [display] infinity_ax_def}\ (* infinity_ax(M) \ \I[M]. (\z[M]. empty(M, z) \ z \ I) \ (\y[M]. y \ I \ (\sy[M]. successor(M, y, sy) \ sy \ I)) *) thm choice_ax_def text\@{thm [display] choice_ax_def}\ (* choice_ax(M) \ \x[M]. \a[M]. \f[M]. ordinal(M, a) \ surjection(M, a, x, f) *) thm separation_def text\@{thm [display] separation_def}\ (* separation(M, P) \ \z[M]. \y[M]. \x[M]. x \ y \ x \ z \ P(x) *) thm univalent_def text\@{thm [display] univalent_def}\ (* univalent(M, A, P) \ \x[M]. x \ A \ (\y[M]. \z[M]. P(x, y) \ P(x, z) \ y = z) *) thm strong_replacement_def text\@{thm [display] strong_replacement_def}\ (* strong_replacement(M, P) \ \A[M]. univalent(M, A, P) \ (\Y[M]. \b[M]. b \ Y \ (\x[M]. x \ A \ P(x, b))) *) text\Internalized formulas\ text\“Codes” for formulas (as sets) are constructed from natural numbers using \<^term>\Member\, \<^term>\Equal\, \<^term>\Nand\, and \<^term>\Forall\.\ thm Member Equal Nand Forall formula.induct text\@{thm [display] Member Equal Nand Forall formula.induct}\ (* x \ \ \ y \ \ \ \x \ y\ \ formula x \ \ \ y \ \ \ \x = y\ \ formula p \ formula \ q \ formula \ \\(p \ q)\ \ formula p \ formula \ (\p) \ formula x \ formula \ (\x y. x \ \ \ y \ \ \ P(\x \ y\)) \ (\x y. x \ \ \ y \ \ \ P(\x = y\)) \ (\p q. p \ formula \ P(p) \ q \ formula \ P(q) \ P(\\(p \ q)\)) \ (\p. p \ formula \ P(p) \ P((\p))) \ P(x) *) text\Definitions for the other connectives and the internal existential quantifier are also provided. For instance, negation:\ thm Neg_def text\@{thm [display] Neg_def}\ (* \\p\ \ \\(p \ p)\ *) thm arity.simps text\@{thm [display] arity.simps}\ (* arity(\x \ y\) = succ(x) \ succ(y) arity(\x = y\) = succ(x) \ succ(y) arity(\\(p \ q)\) = arity(p) \ arity(q) arity((\p)) = pred(arity(p)) *) text\We have the satisfaction relation between $\in$-models and first order formulas (given a “environment” list representing the assignment of free variables),\ thm mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff text\@{thm [display] mem_iff_sats equal_iff_sats sats_Nand_iff sats_Forall_iff}\ (* nth(i, env) = x \ nth(j, env) = y \ env \ list(A) \ x \ y \ A, env \ \i \ j\ nth(i, env) = x \ nth(j, env) = y \ env \ list(A) \ x = y \ A, env \ \i = j\ env \ list(A) \ (A, env \ \\(p \ q)\) \ \ ((A, env \ p) \ (A, env \ q)) env \ list(A) \ (A, env \ (\\p\)) \ (\x\A. A, Cons(x, env) \ p)*) text\as well as the satisfaction of an arbitrary set of sentences.\ thm satT_def text\@{thm [display] satT_def}\ (* A \ \ \ \\\\. A, [] \ \ *) text\The internalized (viz. as elements of the set \<^term>\formula\) version of the axioms follow next.\ thm ZF_union_iff_sats ZF_power_iff_sats ZF_pairing_iff_sats ZF_foundation_iff_sats ZF_extensionality_iff_sats ZF_infinity_iff_sats sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff ZF_choice_iff_sats text\@{thm [display] ZF_union_iff_sats ZF_power_iff_sats ZF_pairing_iff_sats ZF_foundation_iff_sats ZF_extensionality_iff_sats ZF_infinity_iff_sats sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff ZF_choice_iff_sats}\ (* Union_ax(##A) \ A, [] \ \Union Ax\ power_ax(##A) \ A, [] \ \Powerset Ax\ upair_ax(##A) \ A, [] \ \Pairing\ foundation_ax(##A) \ A, [] \ \Foundation\ extensionality(##A) \ A, [] \ \Extensionality\ infinity_ax(##A) \ A, [] \ \Infinity\ \ \ formula \ (M, [] \ \Separation(\)\) \ (\env\list(M). arity(\) \ 1 +\<^sub>\ length(env) \ separation(##M, \x. M, [x] @ env \ \)) \ \ formula \ (M, [] \ \Replacement(\)\) \ (\env. replacement_assm(M, env, \)) choice_ax(##A) \ A, [] \ \AC\ *) text\Above, we use the following:\ thm replacement_assm_def text\@{thm [display] replacement_assm_def}\ (* replacement_assm(M, env, \) \ \ \ formula \ env \ list(M) \ arity(\) \ 2 +\<^sub>\ length(env) \ strong_replacement(##M, \x y. M, [x, y] @ env \ \ *) text\Finally, the axiom sets are defined as follows.\ thm ZF_fin_def ZF_schemes_def Zermelo_fms_def ZC_def ZF_def ZFC_def text\@{thm [display] ZF_fin_def ZF_schemes_def Zermelo_fms_def ZC_def ZF_def ZFC_def}\ (* ZF_fin \ {\Extensionality\, \Foundation\, \Pairing\, \Union Ax\, \Infinity\, \Powerset Ax\} ZF_schemes \ {\Separation(p)\ . p \ formula} \ {\Replacement(p)\ . p \ formula} \Z\ \ ZF_fin \ {\Separation(p)\ . p \ formula} ZC \ \Z\ \ {\AC\} ZF \ ZF_schemes \ ZF_fin ZFC \ ZF \ {\AC\} *) subsection\Relativization of infinitary arithmetic\label{sec:relative-arith}\ text\In order to state the defining property of the relative equipotence relation, we work under the assumptions of the locale \<^term>\M_cardinals\. They comprise a finite set of instances of Separation and Replacement to prove closure properties of the transitive class \<^term>\M\.\ lemma (in M_cardinals) eqpoll_def': assumes "M(A)" "M(B)" shows "A \\<^bsup>M\<^esup> B \ (\f[M]. f \ bij(A,B))" using assms unfolding eqpoll_rel_def by auto text\Below, $\mu$ denotes the minimum operator on the ordinals.\ lemma cardinalities_defs: fixes M::"i\o" shows "|A|\<^bsup>M\<^esup> \ \ i. M(i) \ i \\<^bsup>M\<^esup> A" "Card\<^bsup>M\<^esup>(\) \ \ = |\|\<^bsup>M\<^esup>" "\\<^bsup>\\,M\<^esup> \ |\ \\<^bsup>M\<^esup> \|\<^bsup>M\<^esup>" "(\\<^sup>+)\<^bsup>M\<^esup> \ \ x. M(x) \ Card\<^bsup>M\<^esup>(x) \ \ < x" unfolding cardinal_rel_def cexp_rel_def csucc_rel_def Card_rel_def . context M_aleph begin text\Analogous to the previous Lemma @{thm [source] eqpoll_def'}, we are now under the assumptions of the locale \<^term>\M_aleph\. The axiom instances included are sufficient to state and prove the defining properties of the relativized \<^term>\Aleph\ function (in particular, the required ability to perform transfinite recursions).\ thm Aleph_rel_zero Aleph_rel_succ Aleph_rel_limit text\@{thm [display] Aleph_rel_zero Aleph_rel_succ Aleph_rel_limit}\ (* \\<^bsub>0\<^esub>\<^bsup>M\<^esup> = \ Ord(\) \ M(\) \ \\<^bsub>succ(\)\<^esub>\<^bsup>M\<^esup> = (\\<^bsub>\\<^esub>\<^bsup>M\<^esup>\<^sup>+)\<^bsup>M\<^esup> Limit(\) \ M(\) \ \\<^bsub>\\<^esub>\<^bsup>M\<^esup> = (\j\\. \\<^bsub>j\<^esub>\<^bsup>M\<^esup>) *) end \ \\<^locale>\M_aleph\\ lemma ContHyp_rel_def': fixes N::"i\o" shows "CH\<^bsup>N\<^esup> \ \\<^bsub>1\<^esub>\<^bsup>N\<^esup> = 2\<^bsup>\\\<^bsub>0\<^esub>\<^bsup>N\<^esup>,N\<^esup>" unfolding ContHyp_rel_def . text\Under appropriate hypotheses (this time, from the locale \<^term>\M_ZF_library\), \<^term>\CH\<^bsup>M\<^esup>\ is equivalent to its fully relational version \<^term>\is_ContHyp\. As a sanity check, we see that if the transitive class is indeed \<^term>\\\, we recover the original $\CH$.\ thm M_ZF_library.is_ContHyp_iff is_ContHyp_iff_CH[unfolded ContHyp_def] text\@{thm [display] M_ZF_library.is_ContHyp_iff is_ContHyp_iff_CH[unfolded ContHyp_def]}\ (* M_ZF_library(M) \ is_ContHyp(M) \ CH\<^bsup>M\<^esup> is_ContHyp(\) \ \\<^bsub>1\<^esub> = 2\<^bsup>\\\<^bsub>0\<^esub>\<^esup> *) text\In turn, the fully relational version evaluated on a nonempty transitive \<^term>\A\ is equivalent to the satisfaction of the first-order formula \<^term>\\CH\\.\ thm is_ContHyp_iff_sats text\@{thm [display] is_ContHyp_iff_sats}\ (* env \ list(A) \ 0 \ A \ is_ContHyp(##A) \ A, env \ \CH\ *) subsection\Forcing \label{sec:def-main-forcing}\ text\Our first milestone was to obtain a proper extension using forcing. Its original proof didn't required the previous developments involving the relativization of material on cardinal arithmetic. Now it is derived from a stronger result, namely @{thm [source] extensions_of_ctms} below.\ thm extensions_of_ctms_ZF text\@{thm [display] extensions_of_ctms_ZF}\ (* M \ \ \ Transset(M) \ M \ ZF \ \N. M \ N \ N \ \ \ Transset(N) \ N \ ZF \ M \ N \ (\\. Ord(\) \ \ \ M \ \ \ N) \ ((M, [] \ \AC\) \ N \ ZFC) *) text\We can finally state our main results, namely, the existence of models for $\ZFC + \CH$ and $\ZFC + \neg\CH$ under the assumption of a ctm of $\ZFC$.\ thm ctm_ZFC_imp_ctm_not_CH text\@{thm [display] ctm_ZFC_imp_ctm_not_CH}\ (* M \ \ \ Transset(M) \ M \ ZFC \ \N. M \ N \ N \ \ \ Transset(N) \ N \ ZFC \ {\\\CH\\} \ (\\. Ord(\) \ \ \ M \ \ \ N) *) thm ctm_ZFC_imp_ctm_CH text\@{thm [display] ctm_ZFC_imp_ctm_CH}\ (* M \ \ \ Transset(M) \ M \ ZFC \ \N. M \ N \ N \ \ \ Transset(N) \ N \ ZFC \ {\CH\} \ (\\. Ord(\) \ \ \ M \ \ \ N) *) text\These results can be strengthened by enumerating six finite sets of replacement instances which are sufficient to develop forcing and for the construction of the aforementioned models: \<^term>\instances1_fms\ through \<^term>\instances3_fms\, \<^term>\instances_ground_fms\, and \<^term>\instances_ground_notCH_fms\, which are then collected into the $31$-element set \<^term>\overhead_notCH\. For example, we have:\ thm instances1_fms_def text\@{thm [display] instances1_fms_def}\ (* instances1_fms \ -{ eclose_repl1_intf_fm, eclose_repl2_intf_fm, - wfrec_rank_fm, trans_repl_HVFrom_fm } +{ eclose_closed_fm, eclose_abs_fm, + wfrec_rank_fm, transrec_VFrom_fm } *) thm overhead_def overhead_notCH_def text\@{thm [display] overhead_def overhead_notCH_def overhead_CH_def}\ (* overhead \ instances1_fms \ instances_ground_fms overhead_notCH \ overhead \ instances2_fms \ instances3_fms \ instances_ground_notCH_fms *) text\One further instance is needed to force $\CH$, with a total count of $32$ instances:\ thm overhead_CH_def text\@{thm [display] overhead_CH_def}\ (* - overhead_CH \ overhead_notCH \ {replacement_dcwit_repl_body_fm} + overhead_CH \ overhead_notCH \ {dc_abs_fm} *) thm extensions_of_ctms text\@{thm [display] extensions_of_ctms}\ (* M \ \ \ Transset(M) \ M \ \Z\ \ {\Replacement(p)\ . p \ overhead} \ \ \ formula \ M \ {\Replacement(ground_repl_fm(\))\ . \ \ \} \ \N. M \ N \ N \ \ \ Transset(N) \ M \ N \ (\\. Ord(\) \ \ \ M \ \ \ N) \ ((M, [] \ \AC\) \ N, [] \ \AC\) \ N \ \Z\ \ {\Replacement(\)\ . \ \ \} *) thm ctm_of_not_CH text\@{thm [display] ctm_of_not_CH}\ (* M \ \ \ Transset(M) \ M \ ZC \ {\Replacement(p)\ . p \ overhead_notCH} \ \ \ formula \ M \ {\Replacement(ground_repl_fm(\))\ . \ \ \} \ \N. M \ N \ N \ \ \ Transset(N) \ N \ ZC \ {\\\CH\\} \ {\Replacement(\)\ . \ \ \} \ (\\. Ord(\) \ \ \ M \ \ \ N) *) thm ctm_of_CH text\@{thm [display] ctm_of_CH}\ (* M \ \ \ Transset(M) \ M \ ZC \ {\Replacement(p)\ . p \ overhead_CH} \ \ \ formula \ M \ {\Replacement(ground_repl_fm(\))\ . \ \ \} \ \N. M \ N \ N \ \ \ Transset(N) \ N \ ZC \ {\CH\} \ {\Replacement(\)\ . \ \ \} \ (\\. Ord(\) \ \ \ M \ \ \ N) *) text\In the above three statements, the function \<^term>\ground_repl_fm\ takes an element \<^term>\\\ of \<^term>\formula\ and returns the replacement instance in the ground model that produces the \<^term>\\\-replacement instance in the generic extension. The next result is stated in the context \<^locale>\G_generic1\, which assumes the existence of a generic filter.\ context G_generic1 begin thm sats_ground_repl_fm_imp_sats_ZF_replacement_fm text\@{thm [display] sats_ground_repl_fm_imp_sats_ZF_replacement_fm}\ (* \ \ formula \ M, [] \ \Replacement(ground_repl_fm(\))\ \ M[G], [] \ \Replacement(\)\ *) end \ \\<^locale>\G_generic1\\ end \ No newline at end of file diff --git a/thys/Independence_CH/Fm_Definitions.thy b/thys/Independence_CH/Fm_Definitions.thy --- a/thys/Independence_CH/Fm_Definitions.thy +++ b/thys/Independence_CH/Fm_Definitions.thy @@ -1,1011 +1,1011 @@ section\Concepts involved in instances of Replacement\ theory Fm_Definitions imports Transitive_Models.Renaming_Auto Transitive_Models.Aleph_Relative FrecR_Arities begin (* Really, I have no idea why is this needed again. At the end of the imported theories, notation works just fine. *) no_notation Aleph (\\_\ [90] 90) text\In this theory we put every concept that should be synthesized in a formula to have an instance of replacement. The automatic synthesis of a concept /foo/ requires that every concept used to define /foo/ is already synthesized. We try to use our meta-programs to synthesize concepts: given the absolute concept /foo/ we relativize in relational form obtaining /is\_foo/ and the we synthesize the formula /is\_foo\_fm/. The meta-program that synthesizes formulas also produce satisfactions lemmas. Having one file to collect every formula needed for replacements breaks the reading flow: we need to introduce the concept in this theory in order to use the meta-programs; moreover there are some concepts for which we prove here the satisfaction lemmas manually, while for others we prove them on its theory. \ declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del] FOL_arities[simp del] synthesize "setdiff" from_definition "setdiff" assuming "nonempty" arity_theorem for "setdiff_fm" synthesize "is_converse" from_definition assuming "nonempty" arity_theorem for "is_converse_fm" relationalize "first_rel" "is_first" external synthesize "first_fm" from_definition "is_first" assuming "nonempty" relationalize "minimum_rel" "is_minimum" external definition is_minimum' where "is_minimum'(M,R,X,u) \ (M(u) \ u \ X \ (\v[M]. \a[M]. (v \ X \ v \ u \ a \ R) \ pair(M, u, v, a))) \ (\x[M]. (M(x) \ x \ X \ (\v[M]. \a[M]. (v \ X \ v \ x \ a \ R) \ pair(M, x, v, a))) \ (\y[M]. M(y) \ y \ X \ (\v[M]. \a[M]. (v \ X \ v \ y \ a \ R) \ pair(M, y, v, a)) \ y = x)) \ \ (\x[M]. (M(x) \ x \ X \ (\v[M]. \a[M]. (v \ X \ v \ x \ a \ R) \ pair(M, x, v, a))) \ (\y[M]. M(y) \ y \ X \ (\v[M]. \a[M]. (v \ X \ v \ y \ a \ R) \ pair(M, y, v, a)) \ y = x)) \ empty(M, u)" synthesize "minimum" from_definition "is_minimum'" assuming "nonempty" arity_theorem for "minimum_fm" lemma is_lambda_iff_sats[iff_sats]: assumes is_F_iff_sats: "!!a0 a1 a2. [|a0\Aa; a1\Aa; a2\Aa|] ==> is_F(a1, a0) \ sats(Aa, is_F_fm, Cons(a0,Cons(a1,Cons(a2,env))))" shows "nth(A, env) = Ab \ nth(r, env) = ra \ A \ nat \ r \ nat \ env \ list(Aa) \ is_lambda(##Aa, Ab, is_F, ra) \ Aa, env \ lambda_fm(is_F_fm,A, r)" using sats_lambda_fm[OF assms, of A r] by simp \ \same as @{thm [source] sats_is_wfrec_fm}, but changing length assumptions to \<^term>\0\ being in the model\ lemma sats_is_wfrec_fm': assumes MH_iff_sats: "!!a0 a1 a2 a3 a4. [|a0\A; a1\A; a2\A; a3\A; a4\A|] ==> MH(a2, a1, a0) \ sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" shows "[|x \ nat; y \ nat; z \ nat; env \ list(A); 0 \ A|] ==> sats(A, is_wfrec_fm(p,x,y,z), env) \ is_wfrec(##A, MH, nth(x,env), nth(y,env), nth(z,env))" using MH_iff_sats [THEN iff_sym] nth_closed sats_is_recfun_fm by (simp add: is_wfrec_fm_def is_wfrec_def) blast lemma is_wfrec_iff_sats'[iff_sats]: assumes MH_iff_sats: "!!a0 a1 a2 a3 a4. [|a0\Aa; a1\Aa; a2\Aa; a3\Aa; a4\Aa|] ==> MH(a2, a1, a0) \ sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" "nth(x, env) = xx" "nth(y, env) = yy" "nth(z, env) = zz" "x \ nat" "y \ nat" "z \ nat" "env \ list(Aa)" "0 \ Aa" shows "is_wfrec(##Aa, MH, xx, yy, zz) \ Aa, env \ is_wfrec_fm(p,x,y,z)" using assms(2-4) sats_is_wfrec_fm'[OF assms(1,5-9)] by simp lemma is_wfrec_on_iff_sats[iff_sats]: assumes MH_iff_sats: "!!a0 a1 a2 a3 a4. [|a0\Aa; a1\Aa; a2\Aa; a3\Aa; a4\Aa|] ==> MH(a2, a1, a0) \ sats(Aa, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))" shows "nth(x, env) = xx \ nth(y, env) = yy \ nth(z, env) = zz \ x \ nat \ y \ nat \ z \ nat \ env \ list(Aa) \ 0 \ Aa \ is_wfrec_on(##Aa, MH, aa,xx, yy, zz) \ Aa, env \ is_wfrec_fm(p,x,y,z)" using assms sats_is_wfrec_fm'[OF assms] unfolding is_wfrec_on_def by simp text\Formulas for particular replacement instances\ text\Now we introduce some definitions used in the definition of check; which is defined by well-founded recursion using replacement in the recursive call.\ \ \The well-founded relation for defining check.\ definition rcheck :: "i \ i" where "rcheck(x) \ Memrel(eclose({x}))^+" relativize "rcheck" "is_rcheck" synthesize "is_rcheck" from_definition arity_theorem for "is_rcheck_fm" \ \The function used for the replacement.\ definition PHcheck :: "[i\o,i,i,i,i] \ o" where "PHcheck(M,o,f,y,p) \ M(p) \ (\fy[M]. fun_apply(M,f,y,fy) \ pair(M,fy,o,p))" synthesize "PHcheck" from_definition assuming "nonempty" arity_theorem for "PHcheck_fm" \ \The recursive call for check. We could use the meta-program relationalize for this; but it makes some proofs more involved.\ definition is_Hcheck :: "[i\o,i,i,i,i] \ o" where "is_Hcheck(M,o,z,f,hc) \ is_Replace(M,z,PHcheck(M,o,f),hc)" synthesize "is_Hcheck" from_definition assuming "nonempty" lemma arity_is_Hcheck_fm: assumes "m\nat" "n\nat" "p\nat" "o\nat" shows "arity(is_Hcheck_fm(m,n,p,o)) = succ(o) \ succ(n) \ succ(p) \ succ(m) " unfolding is_Hcheck_fm_def using assms arity_Replace_fm[rule_format,OF PHcheck_fm_type _ _ _ arity_PHcheck_fm] pred_Un_distrib Un_assoc Un_nat_type by simp \ \The relational version of check is hand-made because our automatic tool does not handle \<^term>\wfrec\.\ definition is_check :: "[i\o,i,i,i] \ o" where "is_check(M,o,x,z) \ \rch[M]. is_rcheck(M,x,rch) \ is_wfrec(M,is_Hcheck(M,o),rch,x,z)" \ \Finally, we internalize the formula.\ definition check_fm :: "[i,i,i] \ i" where "check_fm(o,x,z) \ Exists(And(is_rcheck_fm(1+\<^sub>\x,0), is_wfrec_fm(is_Hcheck_fm(6+\<^sub>\o,2,1,0),0,1+\<^sub>\x,1+\<^sub>\z)))" lemma check_fm_type[TC]: "x\nat \ o\nat \ z\nat \ check_fm(x,o,z) \ formula" by (simp add:check_fm_def) lemma sats_check_fm : assumes "o\nat" "x\nat" "z\nat" "env\list(M)" "0\M" shows "(M , env \ check_fm(o,x,z)) \ is_check(##M,nth(o,env),nth(x,env),nth(z,env))" proof - have sats_is_Hcheck_fm: "\a0 a1 a2 a3 a4 a6. \ a0\M; a1\M; a2\M; a3\M; a4\M;a6 \M\ \ is_Hcheck(##M,a6,a2, a1, a0) \ (M , [a0,a1,a2,a3,a4,r,a6]@env \ is_Hcheck_fm(6,2,1,0))" if "r\M" for r using that assms by simp then have "(M , [r]@env \ is_wfrec_fm(is_Hcheck_fm(6+\<^sub>\o,2,1,0),0,1+\<^sub>\x,1+\<^sub>\z)) \ is_wfrec(##M,is_Hcheck(##M,nth(o,env)),r,nth(x,env),nth(z,env))" if "r\M" for r using that assms is_wfrec_iff_sats'[symmetric] by simp then show ?thesis unfolding is_check_def check_fm_def using assms is_rcheck_iff_sats[symmetric] by simp qed lemma iff_sats_check_fm[iff_sats] : assumes "nth(o, env) = oa" "nth(x, env) = xa" "nth(z, env) = za" "o \ nat" "x \ nat" "z \ nat" "env \ list(A)" "0 \ A" shows "is_check(##A, oa,xa, za) \ A, env \ check_fm(o,x,z)" using assms sats_check_fm[symmetric] by auto lemma arity_check_fm[arity]: assumes "m\nat" "n\nat" "o\nat" shows "arity(check_fm(m,n,o)) = succ(o) \ succ(n) \ succ(m) " unfolding check_fm_def using assms arity_is_wfrec_fm[rule_format,OF _ _ _ _ _ arity_is_Hcheck_fm] pred_Un_distrib Un_assoc arity_tran_closure_fm by (auto simp add:arity) notation check_fm (\\_\<^sup>v_ is _\\) \ \The pair of elements belongs to some set. The intended set is the preorder.\ definition is_leq :: "[i\o,i,i,i] \ o" where "is_leq(A,l,q,p) \ \qp[A]. (pair(A,q,p,qp) \ qp\l)" synthesize "is_leq" from_definition assuming "nonempty" arity_theorem for "is_leq_fm" abbreviation fm_leq :: "[i,i,i] \ i" (\\_\\<^bsup>_\<^esup>_\\) where "fm_leq(A,l,B) \ is_leq_fm(l,A,B)" subsection\Formulas used to prove some generic instances.\ definition \_repl :: "i\i" where "\_repl(l) \ rsum({\0, 1\, \1, 0\}, id(l), 2, 3, l)" lemma f_type : "{\0, 1\, \1, 0\} \ 2 \ 3" using Pi_iff unfolding function_def by auto \ \thm\Internalize.sum_type\ clashes with thm\Renaming.sum_type\.\ hide_fact Internalize.sum_type lemma ren_type : assumes "l\nat" shows "\_repl(l) : 2+\<^sub>\l \ 3+\<^sub>\l" using sum_type[of 2 3 l l "{\0, 1\, \1, 0\}" "id(l)"] f_type assms id_type unfolding \_repl_def by auto definition Lambda_in_M_fm where [simp]:"Lambda_in_M_fm(\,len) \ \(\\\pair_fm(1, 0, 2) \ ren(\) ` (2 +\<^sub>\ len) ` (3 +\<^sub>\ len) ` \_repl(len) \\) \ \0 \ len +\<^sub>\ 2\\" lemma Lambda_in_M_fm_type[TC]: "\\formula \ len\nat \ Lambda_in_M_fm(\,len) \formula" using ren_tc[of \ "2+\<^sub>\len" "3+\<^sub>\len" "\_repl(len)"] ren_type unfolding Lambda_in_M_fm_def by simp definition \_pair_repl :: "i\i" where "\_pair_repl(l) \ rsum({\0, 0\, \1, 1\, \2, 3\}, id(l), 3, 4, l)" definition LambdaPair_in_M_fm where "LambdaPair_in_M_fm(\,len) \ \(\\\pair_fm(1, 0, 2) \ ren((\\(\\\\fst(2) is 0\ \ \\snd(2) is 1\ \ ren(\) ` (3 +\<^sub>\ len) ` (4 +\<^sub>\ len) ` \_pair_repl(len) \\\)\)) ` (2 +\<^sub>\ len) ` (3 +\<^sub>\ len) ` \_repl(len) \\) \ \0 \ len +\<^sub>\ 2\\ " lemma f_type' : "{\0,0 \, \1, 1\, \2, 3\} \ 3 \ 4" using Pi_iff unfolding function_def by auto lemma ren_type' : assumes "l\nat" shows "\_pair_repl(l) : 3+\<^sub>\l \ 4+\<^sub>\l" using sum_type[of 3 4 l l "{\0, 0\, \1, 1\, \2, 3\}" "id(l)"] f_type' assms id_type unfolding \_pair_repl_def by auto lemma LambdaPair_in_M_fm_type[TC]: "\\formula \ len\nat \ LambdaPair_in_M_fm(\,len) \formula" using ren_tc[OF _ _ _ ren_type',of \ "len"] Lambda_in_M_fm_type unfolding LambdaPair_in_M_fm_def by simp subsection\The relation \<^term>\frecrel\\ definition frecrelP :: "[i\o,i] \ o" where "frecrelP(M,xy) \ (\x[M]. \y[M]. pair(M,x,y,xy) \ is_frecR(M,x,y))" synthesize "frecrelP" from_definition arity_theorem for "frecrelP_fm" definition is_frecrel :: "[i\o,i,i] \ o" where "is_frecrel(M,A,r) \ \A2[M]. cartprod(M,A,A,A2) \ is_Collect(M,A2, frecrelP(M) ,r)" synthesize "frecrel" from_definition "is_frecrel" arity_theorem for "frecrel_fm" definition names_below :: "i \ i \ i" where "names_below(P,x) \ 2\ecloseN(x)\ecloseN(x)\P" lemma names_belowsD: assumes "x \ names_below(P,z)" obtains f n1 n2 p where "x = \f,n1,n2,p\" "f\2" "n1\ecloseN(z)" "n2\ecloseN(z)" "p\P" using assms unfolding names_below_def by auto synthesize "number2" from_definition lemma number2_iff : "(A)(c) \ number2(A,c) \ (\b[A]. \a[A]. successor(A, b, c) \ successor(A, a, b) \ empty(A, a))" unfolding number2_def number1_def by auto arity_theorem for "number2_fm" reldb_add "ecloseN" "is_ecloseN" relativize "names_below" "is_names_below" synthesize "is_names_below" from_definition arity_theorem for "is_names_below_fm" definition is_tuple :: "[i\o,i,i,i,i,i] \ o" where "is_tuple(M,z,t1,t2,p,t) \ \t1t2p[M]. \t2p[M]. pair(M,t2,p,t2p) \ pair(M,t1,t2p,t1t2p) \ pair(M,z,t1t2p,t)" synthesize "is_tuple" from_definition arity_theorem for "is_tuple_fm" subsection\Definition of Forces\ subsubsection\Definition of \<^term>\forces\ for equality and membership\ text\$p\forces \tau = \theta$ if for every $q\leqslant p$ both $q\forces \sigma \in \tau$ and $q\forces \sigma \in \theta$ hold for all $\sigma \in \dom(\tau)\cup \dom(\theta)$.\ definition eq_case :: "[i,i,i,i,i,i] \ o" where "eq_case(\,\,p,P,leq,f) \ \\. \ \ domain(\) \ domain(\) \ (\q. q\P \ \q,p\\leq \ (f`\1,\,\,q\=1 \ f`\1,\,\,q\ =1))" relativize "eq_case" "is_eq_case" synthesize "eq_case" from_definition "is_eq_case" text\$p\forces \tau \in \theta$ if for every $v\leqslant p$ there exist $q$, $r$, and $\sigma$ such that $v\leqslant q$, $q\leqslant r$, $\langle \sigma,r\rangle \in \tau$, and $q\forces \pi = \sigma$.\ definition mem_case :: "[i,i,i,i,i,i] \ o" where "mem_case(\,\,p,P,leq,f) \ \v\P. \v,p\\leq \ (\q. \\. \r. r\P \ q\P \ \q,v\\leq \ \\,r\ \ \ \ \q,r\\leq \ f`\0,\,\,q\ = 1)" relativize "mem_case" "is_mem_case" synthesize "mem_case" from_definition "is_mem_case" arity_theorem intermediate for "eq_case_fm" lemma arity_eq_case_fm[arity]: assumes "n1\nat" "n2\nat" "p\nat" "P\nat" "leq\nat" "f\nat" shows "arity(eq_case_fm(n1,n2,p,P,leq,f)) = succ(n1) \ succ(n2) \ succ(p) \ succ(P) \ succ(leq) \ succ(f)" using assms arity_eq_case_fm' by auto arity_theorem intermediate for "mem_case_fm" lemma arity_mem_case_fm[arity] : assumes "n1\nat" "n2\nat" "p\nat" "P\nat" "leq\nat" "f\nat" shows "arity(mem_case_fm(n1,n2,p,P,leq,f)) = succ(n1) \ succ(n2) \ succ(p) \ succ(P) \ succ(leq) \ succ(f)" using assms arity_mem_case_fm' by auto definition Hfrc :: "[i,i,i,i] \ o" where "Hfrc(P,leq,fnnc,f) \ \ft. \\. \\. \p. p\P \ fnnc = \ft,\,\,p\ \ ( ft = 0 \ eq_case(\,\,p,P,leq,f) \ ft = 1 \ mem_case(\,\,p,P,leq,f))" relativize "Hfrc" "is_Hfrc" synthesize "Hfrc" from_definition "is_Hfrc" definition is_Hfrc_at :: "[i\o,i,i,i,i,i] \ o" where "is_Hfrc_at(M,P,leq,fnnc,f,b) \ (empty(M,b) \ \ is_Hfrc(M,P,leq,fnnc,f)) \ (number1(M,b) \ is_Hfrc(M,P,leq,fnnc,f))" synthesize "Hfrc_at" from_definition "is_Hfrc_at" arity_theorem intermediate for "Hfrc_fm" lemma arity_Hfrc_fm[arity] : assumes "P\nat" "leq\nat" "fnnc\nat" "f\nat" shows "arity(Hfrc_fm(P,leq,fnnc,f)) = succ(P) \ succ(leq) \ succ(fnnc) \ succ(f)" using assms arity_Hfrc_fm' by auto arity_theorem for "Hfrc_at_fm" subsubsection\The well-founded relation \<^term>\forcerel\\ definition forcerel :: "i \ i \ i" where "forcerel(P,x) \ frecrel(names_below(P,x))^+" definition is_forcerel :: "[i\o,i,i,i] \ o" where "is_forcerel(M,P,x,z) \ \r[M]. \nb[M]. tran_closure(M,r,z) \ (is_names_below(M,P,x,nb) \ is_frecrel(M,nb,r))" synthesize "is_forcerel" from_definition arity_theorem for "is_forcerel_fm" subsection\\<^term>\frc_at\, forcing for atomic formulas\ definition frc_at :: "[i,i,i] \ i" where "frc_at(P,leq,fnnc) \ wfrec(frecrel(names_below(P,fnnc)),fnnc, \x f. bool_of_o(Hfrc(P,leq,x,f)))" \ \The relational form is defined manually because it uses \<^term>\wfrec\.\ definition is_frc_at :: "[i\o,i,i,i,i] \ o" where "is_frc_at(M,P,leq,x,z) \ \r[M]. is_forcerel(M,P,x,r) \ is_wfrec(M,is_Hfrc_at(M,P,leq),r,x,z)" definition frc_at_fm :: "[i,i,i,i] \ i" where "frc_at_fm(p,l,x,z) \ Exists(And(is_forcerel_fm(succ(p),succ(x),0), is_wfrec_fm(Hfrc_at_fm(6+\<^sub>\p,6+\<^sub>\l,2,1,0),0,succ(x),succ(z))))" lemma frc_at_fm_type [TC] : "\p\nat;l\nat;x\nat;z\nat\ \ frc_at_fm(p,l,x,z)\formula" unfolding frc_at_fm_def by simp lemma arity_frc_at_fm[arity] : assumes "p\nat" "l\nat" "x\nat" "z\nat" shows "arity(frc_at_fm(p,l,x,z)) = succ(p) \ succ(l) \ succ(x) \ succ(z)" proof - let ?\ = "Hfrc_at_fm(6 +\<^sub>\ p, 6 +\<^sub>\ l, 2, 1, 0)" note assms moreover from this have "arity(?\) = (7+\<^sub>\p) \ (7+\<^sub>\l)" "?\ \ formula" using arity_Hfrc_at_fm ord_simp_union by auto moreover from calculation have "arity(is_wfrec_fm(?\, 0, succ(x), succ(z))) = 2+\<^sub>\p \ (2+\<^sub>\l) \ (2+\<^sub>\x) \ (2+\<^sub>\z)" using arity_is_wfrec_fm[OF \?\\_\ _ _ _ _ \arity(?\) = _\] pred_Un_distrib pred_succ_eq union_abs1 by auto moreover from assms have "arity(is_forcerel_fm(succ(p),succ(x),0)) = 2+\<^sub>\p \ (2+\<^sub>\x)" using arity_is_forcerel_fm ord_simp_union by auto ultimately show ?thesis unfolding frc_at_fm_def using arity_is_forcerel_fm pred_Un_distrib by (auto simp:FOL_arities) qed lemma sats_frc_at_fm : assumes "p\nat" "l\nat" "i\nat" "j\nat" "env\list(A)" "i < length(env)" "j < length(env)" shows "(A , env \ frc_at_fm(p,l,i,j)) \ is_frc_at(##A,nth(p,env),nth(l,env),nth(i,env),nth(j,env))" proof - { fix r pp ll assume "r\A" have "is_Hfrc_at(##A,nth(p,env),nth(l,env),a2, a1, a0) \ (A, [a0,a1,a2,a3,a4,r]@env \ Hfrc_at_fm(6+\<^sub>\p,6+\<^sub>\l,2,1,0))" if "a0\A" "a1\A" "a2\A" "a3\A" "a4\A" for a0 a1 a2 a3 a4 using that assms \r\A\ Hfrc_at_iff_sats[of "6+\<^sub>\p" "6+\<^sub>\l" 2 1 0 "[a0,a1,a2,a3,a4,r]@env" A] by simp with \r\A\ have "(A,[r]@env \ is_wfrec_fm(Hfrc_at_fm(6+\<^sub>\p, 6+\<^sub>\l,2,1,0),0, i+\<^sub>\1, j+\<^sub>\1)) \ is_wfrec(##A, is_Hfrc_at(##A, nth(p,env), nth(l,env)), r,nth(i, env), nth(j, env))" using assms sats_is_wfrec_fm by simp } moreover have "(A, Cons(r, env) \ is_forcerel_fm(succ(p), succ(i), 0)) \ is_forcerel(##A,nth(p,env),nth(i,env),r)" if "r\A" for r using assms sats_is_forcerel_fm that by simp ultimately show ?thesis unfolding is_frc_at_def frc_at_fm_def using assms by simp qed lemma frc_at_fm_iff_sats: assumes "nth(i,env) = w" "nth(j,env) = x" "nth(k,env) = y" "nth(l,env) = z" "i \ nat" "j \ nat" "k \ nat" "l\nat" "env \ list(A)" "k (A , env \ frc_at_fm(i,j,k,l))" using assms sats_frc_at_fm by simp declare frc_at_fm_iff_sats [iff_sats] definition forces_eq' :: "[i,i,i,i,i] \ o" where "forces_eq'(P,l,p,t1,t2) \ frc_at(P,l,\0,t1,t2,p\) = 1" definition forces_mem' :: "[i,i,i,i,i] \ o" where "forces_mem'(P,l,p,t1,t2) \ frc_at(P,l,\1,t1,t2,p\) = 1" definition forces_neq' :: "[i,i,i,i,i] \ o" where "forces_neq'(P,l,p,t1,t2) \ \ (\q\P. \q,p\\l \ forces_eq'(P,l,q,t1,t2))" definition forces_nmem' :: "[i,i,i,i,i] \ o" where "forces_nmem'(P,l,p,t1,t2) \ \ (\q\P. \q,p\\l \ forces_mem'(P,l,q,t1,t2))" \ \The following definitions are explicitly defined to avoid the expansion of concepts.\ definition is_forces_eq' :: "[i\o,i,i,i,i,i] \ o" where "is_forces_eq'(M,P,l,p,t1,t2) \ \o[M]. \z[M]. \t[M]. number1(M,o) \ empty(M,z) \ is_tuple(M,z,t1,t2,p,t) \ is_frc_at(M,P,l,t,o)" definition is_forces_mem' :: "[i\o,i,i,i,i,i] \ o" where "is_forces_mem'(M,P,l,p,t1,t2) \ \o[M]. \t[M]. number1(M,o) \ is_tuple(M,o,t1,t2,p,t) \ is_frc_at(M,P,l,t,o)" definition is_forces_neq' :: "[i\o,i,i,i,i,i] \ o" where "is_forces_neq'(M,P,l,p,t1,t2) \ \ (\q[M]. q\P \ (\qp[M]. pair(M,q,p,qp) \ qp\l \ is_forces_eq'(M,P,l,q,t1,t2)))" definition is_forces_nmem' :: "[i\o,i,i,i,i,i] \ o" where "is_forces_nmem'(M,P,l,p,t1,t2) \ \ (\q[M]. \qp[M]. q\P \ pair(M,q,p,qp) \ qp\l \ is_forces_mem'(M,P,l,q,t1,t2))" synthesize "forces_eq" from_definition "is_forces_eq'" synthesize "forces_mem" from_definition "is_forces_mem'" synthesize "forces_neq" from_definition "is_forces_neq'" assuming "nonempty" synthesize "forces_nmem" from_definition "is_forces_nmem'" assuming "nonempty" context notes Un_assoc[simp] Un_trasposition_aux2[simp] begin arity_theorem for "forces_eq_fm" arity_theorem for "forces_mem_fm" arity_theorem for "forces_neq_fm" arity_theorem for "forces_nmem_fm" end subsection\Forcing for general formulas\ definition ren_forces_nand :: "i\i" where "ren_forces_nand(\) \ Exists(And(Equal(0,1),iterates(\p. incr_bv(p)`1 , 2, \)))" lemma ren_forces_nand_type[TC] : "\\formula \ ren_forces_nand(\) \formula" unfolding ren_forces_nand_def by simp lemma arity_ren_forces_nand : assumes "\\formula" shows "arity(ren_forces_nand(\)) \ succ(arity(\))" proof - consider (lt) "1)" | (ge) "\ 1 < arity(\)" by auto then show ?thesis proof cases case lt with \\\_\ have "2 < succ(arity(\))" "2)+\<^sub>\2" using succ_ltI by auto with \\\_\ have "arity(iterates(\p. incr_bv(p)`1,2,\)) = 2+\<^sub>\arity(\)" using arity_incr_bv_lemma lt by auto with \\\_\ show ?thesis unfolding ren_forces_nand_def using lt pred_Un_distrib union_abs1 Un_assoc[symmetric] Un_le_compat by (simp add:FOL_arities) next case ge with \\\_\ have "arity(\) \ 1" "pred(arity(\)) \ 1" using not_lt_iff_le le_trans[OF le_pred] by simp_all with \\\_\ have "arity(iterates(\p. incr_bv(p)`1,2,\)) = (arity(\))" using arity_incr_bv_lemma ge by simp with \arity(\) \ 1\ \\\_\ \pred(_) \ 1\ show ?thesis unfolding ren_forces_nand_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2 by (simp add:FOL_arities) qed qed lemma sats_ren_forces_nand: "[q,P,leq,o,p] @ env \ list(M) \ \\formula \ (M, [q,p,P,leq,o] @ env \ ren_forces_nand(\)) \ (M, [q,P,leq,o] @ env \ \)" unfolding ren_forces_nand_def using sats_incr_bv_iff [of _ _ M _ "[q]"] by simp definition ren_forces_forall :: "i\i" where "ren_forces_forall(\) \ Exists(Exists(Exists(Exists(Exists( And(Equal(0,6),And(Equal(1,7),And(Equal(2,8),And(Equal(3,9), And(Equal(4,5),iterates(\p. incr_bv(p)`5 , 5, \)))))))))))" lemma arity_ren_forces_all : assumes "\\formula" shows "arity(ren_forces_forall(\)) = 5 \ arity(\)" proof - consider (lt) "5)" | (ge) "\ 5 < arity(\)" by auto then show ?thesis proof cases case lt with \\\_\ have "5 < succ(arity(\))" "5)+\<^sub>\2" "5)+\<^sub>\3" "5)+\<^sub>\4" using succ_ltI by auto with \\\_\ have "arity(iterates(\p. incr_bv(p)`5,5,\)) = 5+\<^sub>\arity(\)" using arity_incr_bv_lemma lt by simp with \\\_\ show ?thesis unfolding ren_forces_forall_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2 by (simp add:FOL_arities) next case ge with \\\_\ have "arity(\) \ 5" "pred^5(arity(\)) \ 5" using not_lt_iff_le le_trans[OF le_pred] by simp_all with \\\_\ have "arity(iterates(\p. incr_bv(p)`5,5,\)) = arity(\)" using arity_incr_bv_lemma ge by simp with \arity(\) \ 5\ \\\_\ \pred^5(_) \ 5\ show ?thesis unfolding ren_forces_forall_def using pred_Un_distrib union_abs1 Un_assoc[symmetric] union_abs2 by (simp add:FOL_arities) qed qed lemma ren_forces_forall_type[TC] : "\\formula \ ren_forces_forall(\) \formula" unfolding ren_forces_forall_def by simp lemma sats_ren_forces_forall : "[x,P,leq,o,p] @ env \ list(M) \ \\formula \ (M, [x,p,P,leq,o] @ env \ ren_forces_forall(\)) \ (M, [p,P,leq,o,x] @ env \ \)" unfolding ren_forces_forall_def using sats_incr_bv_iff [of _ _ M _ "[p,P,leq,o,x]"] by simp subsubsection\The primitive recursion\ consts forces' :: "i\i" primrec "forces'(Member(x,y)) = forces_mem_fm(1,2,0,x+\<^sub>\4,y+\<^sub>\4)" "forces'(Equal(x,y)) = forces_eq_fm(1,2,0,x+\<^sub>\4,y+\<^sub>\4)" "forces'(Nand(p,q)) = Neg(Exists(And(Member(0,2),And(is_leq_fm(3,0,1),And(ren_forces_nand(forces'(p)), ren_forces_nand(forces'(q)))))))" "forces'(Forall(p)) = Forall(ren_forces_forall(forces'(p)))" definition forces :: "i\i" where "forces(\) \ And(Member(0,1),forces'(\))" lemma forces'_type [TC]: "\\formula \ forces'(\) \ formula" by (induct \ set:formula; simp) lemma forces_type[TC] : "\\formula \ forces(\) \ formula" unfolding forces_def by simp subsection\The arity of \<^term>\forces\\ lemma arity_forces_at: assumes "x \ nat" "y \ nat" shows "arity(forces(Member(x, y))) = (succ(x) \ succ(y)) +\<^sub>\ 4" "arity(forces(Equal(x, y))) = (succ(x) \ succ(y)) +\<^sub>\ 4" unfolding forces_def using assms arity_forces_mem_fm arity_forces_eq_fm succ_Un_distrib ord_simp_union by (auto simp:FOL_arities,(rule_tac le_anti_sym,simp_all,(rule_tac not_le_anti_sym,simp_all))+) lemma arity_forces': assumes "\\formula" shows "arity(forces'(\)) \ arity(\) +\<^sub>\ 4" using assms proof (induct set:formula) case (Member x y) then show ?case using arity_forces_mem_fm succ_Un_distrib ord_simp_union leI not_le_iff_lt by simp next case (Equal x y) then show ?case using arity_forces_eq_fm succ_Un_distrib ord_simp_union leI not_le_iff_lt by simp next case (Nand \ \) let ?\' = "ren_forces_nand(forces'(\))" let ?\' = "ren_forces_nand(forces'(\))" have "arity(is_leq_fm(3, 0, 1)) = 4" using arity_is_leq_fm succ_Un_distrib ord_simp_union by simp have "3 \ (4+\<^sub>\arity(\)) \ (4+\<^sub>\arity(\))" (is "_ \ ?rhs") using ord_simp_union by simp from \\\_\ Nand have "pred(arity(?\')) \ ?rhs" "pred(arity(?\')) \ ?rhs" proof - from \\\_\ \\\_\ have A:"pred(arity(?\')) \ arity(forces'(\))" "pred(arity(?\')) \ arity(forces'(\))" using pred_mono[OF _ arity_ren_forces_nand] pred_succ_eq by simp_all from Nand have "3 \ arity(forces'(\)) \ arity(\) +\<^sub>\ 4" "3 \ arity(forces'(\)) \ arity(\) +\<^sub>\ 4" using Un_le by simp_all with Nand show "pred(arity(?\')) \ ?rhs" "pred(arity(?\')) \ ?rhs" using le_trans[OF A(1)] le_trans[OF A(2)] le_Un_iff by simp_all qed with Nand \_=4\ show ?case using pred_Un_distrib Un_assoc[symmetric] succ_Un_distrib union_abs1 Un_leI3[OF \3 \ ?rhs\] by (simp add:FOL_arities) next case (Forall \) let ?\' = "ren_forces_forall(forces'(\))" show ?case proof (cases "arity(\) = 0") case True with Forall show ?thesis proof - from Forall True have "arity(forces'(\)) \ 5" using le_trans[of _ 4 5] by auto with \\\_\ have "arity(?\') \ 5" using arity_ren_forces_all[OF forces'_type[OF \\\_\]] union_abs2 by auto with Forall True show ?thesis using pred_mono[OF _ \arity(?\') \ 5\] by simp qed next case False with Forall show ?thesis proof - from Forall False have "arity(?\') = 5 \ arity(forces'(\))" "arity(forces'(\)) \ 5 +\<^sub>\ arity(\)" "4 \ 3+\<^sub>\arity(\)" using Ord_0_lt arity_ren_forces_all le_trans[OF _ add_le_mono[of 4 5, OF _ le_refl]] by auto with \\\_\ have "5 \ arity(forces'(\)) \ 5+\<^sub>\arity(\)" using ord_simp_union by auto with \\\_\ \arity(?\') = 5 \ _\ show ?thesis using pred_Un_distrib succ_pred_eq[OF _ \arity(\)\0\] pred_mono[OF _ Forall(2)] Un_le[OF \4\3+\<^sub>\arity(\)\] by simp qed qed qed lemma arity_forces : assumes "\\formula" shows "arity(forces(\)) \ 4+\<^sub>\arity(\)" unfolding forces_def using assms arity_forces' le_trans ord_simp_union FOL_arities by auto lemma arity_forces_le : assumes "\\formula" "n\nat" "arity(\) \ n" shows "arity(forces(\)) \ 4+\<^sub>\n" using assms le_trans[OF _ add_le_mono[OF le_refl[of 5] \arity(\)\_\]] arity_forces by auto definition rename_split_fm where "rename_split_fm(\) \ (\\(\\(\\(\\(\\(\\\\snd(9) is 0\ \ \\fst(9) is 4\ \ \\1=11\ \ \\2=12\ \ \\3=13\ \ \\5=7\ \ (\p. incr_bv(p)`6)^8(forces(\)) \\\\\\\)\)\)\)\)\)" lemma rename_split_fm_type[TC]: "\\formula \ rename_split_fm(\)\formula" unfolding rename_split_fm_def by simp schematic_goal arity_rename_split_fm: "\\formula \ arity(rename_split_fm(\)) = ?m" using arity_forces[of \] forces_type unfolding rename_split_fm_def by (simp add:arity Un_assoc[symmetric] union_abs1) lemma arity_rename_split_fm_le: assumes "\\formula" shows "arity(rename_split_fm(\)) \ 8 \ (6 +\<^sub>\ arity(\))" proof - from assms have arity_forces_6: "\ 1 < arity(\) \ 6 \ n \ arity(forces(\)) \ n" for n using le_trans lt_trans[of _ 5 n] not_lt_iff_le[of 1 "arity(\)"] by (auto intro!:le_trans[OF arity_forces]) have pred1_arity_forces: "\ 1 < arity(\) \ pred^n(arity(forces(\))) \ 8" if "n\nat" for n using that pred_le[of 7] le_succ[THEN [2] le_trans] arity_forces_6 by (induct rule:nat_induct) auto have arity_forces_le_succ6: "pred^n(arity(forces(\))) \ succ(succ(succ(succ(succ(succ(arity(\)))))))" if "n\nat" for n using that assms arity_forces[of \, THEN le_trans, OF _ le_succ, THEN le_trans, OF _ _ le_succ] le_trans[OF pred_le[OF _ le_succ]] by (induct rule:nat_induct) auto note trivial_arities = arity_forces_6 arity_forces_le_succ6[of 1, simplified] arity_forces_le_succ6[of 2, simplified] arity_forces_le_succ6[of 3, simplified] arity_forces_le_succ6[of 4, simplified] arity_forces_le_succ6[of 5, simplified] arity_forces_le_succ6[of 6, simplified] pred1_arity_forces[of 1, simplified] pred1_arity_forces[of 2, simplified] pred1_arity_forces[of 3, simplified] pred1_arity_forces[of 4, simplified] pred1_arity_forces[of 5, simplified] pred1_arity_forces[of 6, simplified] show ?thesis using assms arity_forces[of \] arity_forces[of \, THEN le_trans, OF _ le_succ] arity_forces[of \, THEN le_trans, OF _ le_succ, THEN le_trans, OF _ _ le_succ] unfolding rename_split_fm_def by (simp add:arity Un_assoc[symmetric] union_abs1 arity_forces[of \] forces_type) ((subst arity_incr_bv_lemma; auto simp: arity ord_simp_union forces_type trivial_arities)+) qed definition body_ground_repl_fm where "body_ground_repl_fm(\) \ (\\(\\\is_Vset_fm(2, 0) \ \\1 \ 0\ \ rename_split_fm(\) \\\)\)" lemma body_ground_repl_fm_type[TC]: "\\formula \ body_ground_repl_fm(\)\formula" unfolding body_ground_repl_fm_def by simp lemma arity_body_ground_repl_fm_le: notes le_trans[trans] assumes "\\formula" shows "arity(body_ground_repl_fm(\)) \ 6 \ (arity(\) +\<^sub>\ 4)" proof - from \\\formula\ have ineq: "n \ pred(pred(arity(rename_split_fm(\)))) \ m \ pred(pred(8 \ (arity(\) +\<^sub>\6 )))" if "n \ m" "n\nat" "m\nat" for n m using that arity_rename_split_fm_le[of \, THEN [2] pred_mono, THEN [2] pred_mono, THEN [2] Un_mono[THEN subset_imp_le, OF _ le_imp_subset]] le_imp_subset by auto moreover have eq1: "pred(pred(pred(4 \ 2 \ pred(pred(pred( pred(pred(pred(pred(pred(9 \ 1 \ 3 \ 2))))))))))) = 1" by (auto simp:pred_Un_distrib) ultimately have "pred(pred(pred(4 \ 2 \ pred(pred(pred( pred(pred(pred(pred(pred(9 \ 1 \ 3 \ 2))))))))))) \ pred(pred(arity(rename_split_fm(\)))) \ 1 \ pred(pred(8 \ (arity(\) +\<^sub>\6 )))" by auto also from \\\formula\ have "1 \ pred(pred(8 \ (arity(\) +\<^sub>\6 ))) \ 6 \ (4+\<^sub>\arity(\))" by (auto simp:pred_Un_distrib Un_assoc[symmetric] ord_simp_union) finally show ?thesis using \\\formula\ unfolding body_ground_repl_fm_def by (simp add:arity pred_Un_distrib, subst arity_transrec_fm[of "is_HVfrom_fm(8,2,1,0)" 3 1]) (simp add:arity pred_Un_distrib,simp_all, auto simp add:eq1 arity_is_HVfrom_fm[of 8 2 1 0]) qed definition ground_repl_fm where "ground_repl_fm(\) \ least_fm(body_ground_repl_fm(\), 1)" lemma ground_repl_fm_type[TC]: "\\formula \ ground_repl_fm(\) \ formula" unfolding ground_repl_fm_def by simp lemma arity_ground_repl_fm: assumes "\\formula" shows "arity(ground_repl_fm(\)) \ 5 \ (3 +\<^sub>\ arity(\))" proof - from assms have "pred(arity(body_ground_repl_fm(\))) \ 5 \ (3 +\<^sub>\ arity(\))" using arity_body_ground_repl_fm_le pred_mono succ_Un_distrib by (rule_tac pred_le) auto with assms have "2 \ pred(arity(body_ground_repl_fm(\))) \ 5 \ (3 +\<^sub>\ arity(\))" using Un_le le_Un_iff by auto then show ?thesis using assms arity_forces arity_body_ground_repl_fm_le unfolding least_fm_def ground_repl_fm_def apply (auto simp add:arity Un_assoc[symmetric]) apply (simp add: pred_Un Un_assoc, simp add: Un_assoc[symmetric] union_abs1 pred_Un) by(simp only: Un_commute, subst Un_commute, simp add:ord_simp_union,force) qed synthesize "is_ordermap" from_definition assuming "nonempty" synthesize "is_ordertype" from_definition assuming "nonempty" synthesize "is_order_body" from_definition assuming "nonempty" arity_theorem for "is_order_body_fm" definition omap_wfrec_body where "omap_wfrec_body(A,r) \ (\\\image_fm(2, 0, 1) \ pred_set_fm(9+\<^sub>\A, 3,9+\<^sub>\r, 0) \\)" lemma type_omap_wfrec_body_fm :"A\nat \ r\nat \ omap_wfrec_body(A,r)\formula" unfolding omap_wfrec_body_def by simp lemma arity_omap_wfrec_aux : "A\nat \ r\nat \ arity(omap_wfrec_body(A,r)) = (9+\<^sub>\A) \ (9+\<^sub>\r)" unfolding omap_wfrec_body_def using arity_image_fm arity_pred_set_fm pred_Un_distrib union_abs2[of 3] union_abs1 by (simp add:FOL_arities, auto simp add:Un_assoc[symmetric] union_abs1) lemma arity_omap_wfrec: "A\nat \ r\nat \ arity(is_wfrec_fm(omap_wfrec_body(A,r),r+\<^sub>\3, 1, 0)) = (4+\<^sub>\A) \ (4+\<^sub>\r)" using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_omap_wfrec_aux,of A r "3+\<^sub>\r" 1 0] pred_Un_distrib union_abs1 union_abs2 type_omap_wfrec_body_fm by auto lemma arity_isordermap: "A\nat \ r\nat \d\nat\ arity(is_ordermap_fm(A,r,d)) = succ(d) \ (succ(A) \ succ(r))" unfolding is_ordermap_fm_def using arity_lambda_fm[where i="(4+\<^sub>\A) \ (4+\<^sub>\r)",OF _ _ _ _ arity_omap_wfrec, unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1 by auto lemma arity_is_ordertype: "A\nat \ r\nat \d\nat\ arity(is_ordertype_fm(A,r,d)) = succ(d) \ (succ(A) \ succ(r))" unfolding is_ordertype_fm_def using arity_isordermap arity_image_fm pred_Un_distrib FOL_arities by auto lemma arity_is_order_body: "arity(is_order_body_fm(0,1)) = 2" using arity_is_order_body_fm arity_is_ordertype ord_simp_union by (simp add:FOL_arities) definition H_order_pred where "H_order_pred(A,r) \ \x f . f `` Order.pred(A, x, r)" relationalize "H_order_pred" "is_H_order_pred" synthesize "is_H_order_pred" from_definition assuming "nonempty" definition order_pred_wfrec_body where "order_pred_wfrec_body(M,A,r,z,x) \ \y[M]. pair(M, x, y, z) \ (\f[M]. (\z[M]. z \ f \ (\xa[M]. \y[M]. \xaa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M, xa, y, z) \ pair(M, xa, x, xaa) \ upair(M, xa, xa, sx) \ pre_image(M, r, sx, r_sx) \ restriction(M, f, r_sx, f_r_sx) \ xaa \ r \ (\a[M]. image(M, f_r_sx, a, y) \ pred_set(M, A, xa, r, a)))) \ (\a[M]. image(M, f, a, y) \ pred_set(M, A, x, r, a)))" synthesize "order_pred_wfrec_body" from_definition arity_theorem for "order_pred_wfrec_body_fm" -definition replacement_is_order_body_fm where "replacement_is_order_body_fm \ (\\\is_order_body_fm(1, 0) \ \\1,0\ is 2 \\\)" -definition wfrec_replacement_order_pred_fm where "wfrec_replacement_order_pred_fm \ order_pred_wfrec_body_fm(3,2,1,0)" +definition ordtype_replacement_fm where "ordtype_replacement_fm \ (\\\is_order_body_fm(1, 0) \ \\1,0\ is 2 \\\)" +definition wfrec_ordertype_fm where "wfrec_ordertype_fm \ order_pred_wfrec_body_fm(3,2,1,0)" definition replacement_is_aleph_fm where "replacement_is_aleph_fm \ \\0 is ordinal\ \ \\(0) is 1\\" definition funspace_succ_rep_intf where "funspace_succ_rep_intf \ \p z n. \f b. p = & z = {cons(, f)}" relativize functional "funspace_succ_rep_intf" "funspace_succ_rep_intf_rel" \ \The definition obtained next uses \<^term>\is_cons\ instead of \<^term>\upair\ as in Paulson's \<^file>\~~/src/ZF/Constructible/Relative.thy\.\ relationalize "funspace_succ_rep_intf_rel" "is_funspace_succ_rep_intf" synthesize "is_funspace_succ_rep_intf" from_definition arity_theorem for "is_funspace_succ_rep_intf_fm" definition wfrec_Hfrc_at_fm where "wfrec_Hfrc_at_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(Hfrc_at_fm(8, 9, 2, 1, 0), 5, 1, 0) \\)" definition list_repl1_intf_fm where "list_repl1_intf_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(iterates_MH_fm(list_functor_fm(13, 1, 0), 10, 2, 1, 0), 3, 1, 0) \\)" definition list_repl2_intf_fm where "list_repl2_intf_fm \ \\0 \ 4\ \ is_iterates_fm(list_functor_fm(13, 1, 0), 3, 0, 1) \" definition formula_repl2_intf_fm where "formula_repl2_intf_fm \ \\0 \ 3\ \ is_iterates_fm(formula_functor_fm(1, 0), 2, 0, 1) \" -definition eclose_repl2_intf_fm where "eclose_repl2_intf_fm \ \\0 \ 3\ \ is_iterates_fm(\\1 is 0\, 2, 0, 1) \" +definition eclose_abs_fm where "eclose_abs_fm \ \\0 \ 3\ \ is_iterates_fm(\\1 is 0\, 2, 0, 1) \" definition powapply_repl_fm where "powapply_repl_fm \ is_Powapply_fm(2,0,1)" definition wfrec_rank_fm where "wfrec_rank_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(is_Hrank_fm(2, 1, 0), 3, 1, 0) \\)" -definition trans_repl_HVFrom_fm where "trans_repl_HVFrom_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(is_HVfrom_fm(8, 2, 1, 0), 4, 1, 0) \\)" +definition transrec_VFrom_fm where "transrec_VFrom_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(is_HVfrom_fm(8, 2, 1, 0), 4, 1, 0) \\)" definition wfrec_Hcheck_fm where "wfrec_Hcheck_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(is_Hcheck_fm(8, 2, 1, 0), 4, 1, 0) \\) " definition repl_PHcheck_fm where "repl_PHcheck_fm \ PHcheck_fm(2,3,0,1)" definition tl_repl_intf_fm where "tl_repl_intf_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(iterates_MH_fm(tl_fm(1,0), 9, 2, 1, 0), 3, 1, 0) \\)" definition formula_repl1_intf_fm where "formula_repl1_intf_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(iterates_MH_fm(formula_functor_fm(1,0), 9, 2, 1, 0), 3, 1, 0) \\)" -definition eclose_repl1_intf_fm where "eclose_repl1_intf_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(iterates_MH_fm(\\1 is 0\, 9, 2, 1, 0), 3, 1, 0) \\)" +definition eclose_closed_fm where "eclose_closed_fm \ (\\\pair_fm(1, 0, 2) \ is_wfrec_fm(iterates_MH_fm(\\1 is 0\, 9, 2, 1, 0), 3, 1, 0) \\)" definition replacement_assm where "replacement_assm(M,env,\) \ \ \ formula \ env \ list(M) \ arity(\) \ 2 +\<^sub>\ length(env) \ strong_replacement(##M,\x y. (M , [x,y]@env \ \))" definition ground_replacement_assm where "ground_replacement_assm(M,env,\) \ replacement_assm(M,env,ground_repl_fm(\))" end \ No newline at end of file diff --git a/thys/Independence_CH/Interface.thy b/thys/Independence_CH/Interface.thy --- a/thys/Independence_CH/Interface.thy +++ b/thys/Independence_CH/Interface.thy @@ -1,1498 +1,1498 @@ section\Interface between set models and Constructibility\ text\This theory provides an interface between Paulson's relativization results and set models of ZFC. In particular, it is used to prove that the locale \<^term>\forcing_data\ is a sublocale of all relevant locales in \<^session>\ZF-Constructible\ (\<^term>\M_trivial\, \<^term>\M_basic\, \<^term>\M_eclose\, etc). In order to interpret the locales in \<^session>\ZF-Constructible\ we introduce new locales, each stronger than the previous one, assuming only the instances of Replacement needed to interpret the subsequent locales of that session. From the start we assume Separation for every internalized formula (with one parameter, but this is not a problem since we can use pairing).\ theory Interface imports Fm_Definitions Transitive_Models.Cardinal_AC_Relative begin locale M_Z_basic = fixes M assumes upair_ax: "upair_ax(##M)" and Union_ax: "Union_ax(##M)" and power_ax: "power_ax(##M)" and extensionality:"extensionality(##M)" and foundation_ax: "foundation_ax(##M)" and infinity_ax: "infinity_ax(##M)" and separation_ax: "\ \ formula \ env \ list(M) \ arity(\) \ 1 +\<^sub>\ length(env) \ separation(##M,\x. (M, [x] @ env \ \))" locale M_transset = fixes M assumes trans_M: "Transset(M)" locale M_Z_trans = M_Z_basic + M_transset locale M_ZF1 = M_Z_basic + assumes replacement_ax1: - "replacement_assm(M,env,eclose_repl1_intf_fm)" - "replacement_assm(M,env,eclose_repl2_intf_fm)" + "replacement_assm(M,env,eclose_closed_fm)" + "replacement_assm(M,env,eclose_abs_fm)" "replacement_assm(M,env,wfrec_rank_fm)" - "replacement_assm(M,env,trans_repl_HVFrom_fm)" + "replacement_assm(M,env,transrec_VFrom_fm)" definition instances1_fms where "instances1_fms \ - { eclose_repl1_intf_fm, - eclose_repl2_intf_fm, + { eclose_closed_fm, + eclose_abs_fm, wfrec_rank_fm, - trans_repl_HVFrom_fm + transrec_VFrom_fm }" text\This set has 4 internalized formulas.\ lemmas replacement_instances1_defs = list_repl1_intf_fm_def list_repl2_intf_fm_def formula_repl1_intf_fm_def formula_repl2_intf_fm_def - eclose_repl1_intf_fm_def eclose_repl2_intf_fm_def - wfrec_rank_fm_def trans_repl_HVFrom_fm_def tl_repl_intf_fm_def + eclose_closed_fm_def eclose_abs_fm_def + wfrec_rank_fm_def transrec_VFrom_fm_def tl_repl_intf_fm_def lemma instances1_fms_type[TC]: "instances1_fms \ formula" using Lambda_in_M_fm_type unfolding replacement_instances1_defs instances1_fms_def by simp declare (in M_ZF1) replacement_instances1_defs[simp] locale M_ZF1_trans = M_ZF1 + M_Z_trans context M_Z_trans begin lemmas transitivity = Transset_intf[OF trans_M] subsection\Interface with \<^term>\M_trivial\\ lemma zero_in_M: "0 \ M" proof - obtain z where "empty(##M,z)" "z\M" using empty_intf[OF infinity_ax] by auto moreover from this have "z=0" using transitivity empty_def by auto ultimately show ?thesis by simp qed lemma separation_in_ctm : assumes "\ \ formula" "env\list(M)" "arity(\) \ 1 +\<^sub>\ length(env)" and satsQ: "\x. x\M \ (M, [x]@env \ \) \ Q(x)" shows "separation(##M,Q)" using assms separation_ax satsQ transitivity separation_cong[of "##M" "\y. (M, [y]@env \ \)" "Q"] by simp end \ \\<^locale>\M_Z_trans\\ locale M_ZC_basic = M_Z_basic + M_AC "##M" locale M_ZFC1 = M_ZF1 + M_ZC_basic locale M_ZFC1_trans = M_ZF1_trans + M_ZFC1 sublocale M_Z_trans \ M_trans "##M" using transitivity zero_in_M exI[of "\x. x\M"] by unfold_locales simp_all sublocale M_Z_trans \ M_trivial "##M" using upair_ax Union_ax by unfold_locales subsection\Interface with \<^term>\M_basic\\ definition Intersection where "Intersection(N,B,x) \ (\y[N]. y\B \ x\y)" synthesize "Intersection" from_definition "Intersection" assuming "nonempty" arity_theorem for "Intersection_fm" definition CartProd where "CartProd(N,B,C,z) \ (\x[N]. x\B \ (\y[N]. y\C \ pair(N,x,y,z)))" synthesize "CartProd" from_definition "CartProd" assuming "nonempty" arity_theorem for "CartProd_fm" definition ImageSep where "ImageSep(N,B,r,y) \ (\p[N]. p\r \ (\x[N]. x\B \ pair(N,x,y,p)))" synthesize "ImageSep" from_definition assuming "nonempty" arity_theorem for "ImageSep_fm" definition Converse where "Converse(N,R,z) \ \p[N]. p\R \ (\x[N].\y[N]. pair(N,x,y,p) \ pair(N,y,x,z))" synthesize "Converse" from_definition "Converse" assuming "nonempty" arity_theorem for "Converse_fm" definition Restrict where "Restrict(N,A,z) \ \x[N]. x\A \ (\y[N]. pair(N,x,y,z))" synthesize "Restrict" from_definition "Restrict" assuming "nonempty" arity_theorem for "Restrict_fm" definition Comp where "Comp(N,R,S,xz) \ \x[N]. \y[N]. \z[N]. \xy[N]. \yz[N]. pair(N,x,z,xz) \ pair(N,x,y,xy) \ pair(N,y,z,yz) \ xy\S \ yz\R" synthesize "Comp" from_definition "Comp" assuming "nonempty" arity_theorem for "Comp_fm" definition Pred where "Pred(N,R,X,y) \ \p[N]. p\R \ pair(N,y,X,p)" synthesize "Pred" from_definition "Pred" assuming "nonempty" arity_theorem for "Pred_fm" definition is_Memrel where "is_Memrel(N,z) \ \x[N]. \y[N]. pair(N,x,y,z) \ x \ y" synthesize "is_Memrel" from_definition "is_Memrel" assuming "nonempty" arity_theorem for "is_Memrel_fm" definition RecFun where "RecFun(N,r,f,g,a,b,x) \ \xa[N]. \xb[N]. pair(N,x,a,xa) \ xa \ r \ pair(N,x,b,xb) \ xb \ r \ (\fx[N]. \gx[N]. fun_apply(N,f,x,fx) \ fun_apply(N,g,x,gx) \ fx \ gx)" synthesize "RecFun" from_definition "RecFun" assuming "nonempty" arity_theorem for "RecFun_fm" arity_theorem for "rtran_closure_mem_fm" synthesize "wellfounded_trancl" from_definition assuming "nonempty" arity_theorem for "wellfounded_trancl_fm" context M_Z_trans begin lemma inter_sep_intf : assumes "A\M" shows "separation(##M,\x . \y\M . y\A \ x\y)" using assms separation_in_ctm[of "Intersection_fm(1,0)" "[A]" "Intersection(##M,A)"] Intersection_iff_sats[of 1 "[_,A]" A 0 _ M] arity_Intersection_fm Intersection_fm_type ord_simp_union zero_in_M unfolding Intersection_def by simp lemma diff_sep_intf : assumes "B\M" shows "separation(##M,\x . x\B)" using assms separation_in_ctm[of "Neg(Member(0,1))" "[B]" "\x . x\B"] ord_simp_union by simp lemma cartprod_sep_intf : assumes "A\M" and "B\M" shows "separation(##M,\z. \x\M. x\A \ (\y\M. y\B \ pair(##M,x,y,z)))" using assms separation_in_ctm[of "CartProd_fm(1,2,0)" "[A,B]" "CartProd(##M,A,B)"] CartProd_iff_sats[of 1 "[_,A,B]" A 2 B 0 _ M] arity_CartProd_fm CartProd_fm_type ord_simp_union zero_in_M unfolding CartProd_def by simp lemma image_sep_intf : assumes "A\M" and "B\M" shows "separation(##M, \y. \p\M. p\B \ (\x\M. x\A \ pair(##M,x,y,p)))" using assms separation_in_ctm[of "ImageSep_fm(1,2,0)" "[A,B]" "ImageSep(##M,A,B)"] ImageSep_iff_sats[of 1 "[_,A,B]" _ 2 _ 0 _ M] arity_ImageSep_fm ImageSep_fm_type ord_simp_union zero_in_M unfolding ImageSep_def by simp lemma converse_sep_intf : assumes "R\M" shows "separation(##M,\z. \p\M. p\R \ (\x\M.\y\M. pair(##M,x,y,p) \ pair(##M,y,x,z)))" using assms separation_in_ctm[of "Converse_fm(1,0)" "[R]" "Converse(##M,R)"] Converse_iff_sats[of 1 "[_,R]" _ 0 _ M] arity_Converse_fm Converse_fm_type ord_simp_union zero_in_M unfolding Converse_def by simp lemma restrict_sep_intf : assumes "A\M" shows "separation(##M,\z. \x\M. x\A \ (\y\M. pair(##M,x,y,z)))" using assms separation_in_ctm[of "Restrict_fm(1,0)" "[A]" "Restrict(##M,A)"] Restrict_iff_sats[of 1 "[_,A]" _ 0 _ M] arity_Restrict_fm Restrict_fm_type ord_simp_union zero_in_M unfolding Restrict_def by simp lemma comp_sep_intf : assumes "R\M" and "S\M" shows "separation(##M,\xz. \x\M. \y\M. \z\M. \xy\M. \yz\M. pair(##M,x,z,xz) \ pair(##M,x,y,xy) \ pair(##M,y,z,yz) \ xy\S \ yz\R)" using assms separation_in_ctm[of "Comp_fm(1,2,0)" "[R,S]" "Comp(##M,R,S)"] Comp_iff_sats[of 1 "[_,R,S]" _ 2 _ 0 _ M] arity_Comp_fm Comp_fm_type ord_simp_union zero_in_M unfolding Comp_def by simp lemma pred_sep_intf: assumes "R\M" and "X\M" shows "separation(##M, \y. \p\M. p\R \ pair(##M,y,X,p))" using assms separation_in_ctm[of "Pred_fm(1,2,0)" "[R,X]" "Pred(##M,R,X)"] Pred_iff_sats[of 1 "[_,R,X]" _ 2 _ 0 _ M] arity_Pred_fm Pred_fm_type ord_simp_union zero_in_M unfolding Pred_def by simp lemma memrel_sep_intf: "separation(##M, \z. \x\M. \y\M. pair(##M,x,y,z) \ x \ y)" using separation_in_ctm[of "is_Memrel_fm(0)" "[]" "is_Memrel(##M)"] is_Memrel_iff_sats[of 0 "[_]" _ M] arity_is_Memrel_fm is_Memrel_fm_type ord_simp_union zero_in_M unfolding is_Memrel_def by simp lemma is_recfun_sep_intf : assumes "r\M" "f\M" "g\M" "a\M" "b\M" shows "separation(##M,\x. \xa\M. \xb\M. pair(##M,x,a,xa) \ xa \ r \ pair(##M,x,b,xb) \ xb \ r \ (\fx\M. \gx\M. fun_apply(##M,f,x,fx) \ fun_apply(##M,g,x,gx) \ fx \ gx))" using assms separation_in_ctm[of "RecFun_fm(1,2,3,4,5,0)" "[r,f,g,a,b]" "RecFun(##M,r,f,g,a,b)"] RecFun_iff_sats[of 1 "[_,r,f,g,a,b]" _ 2 _ 3 _ 4 _ 5 _ 0 _ M] arity_RecFun_fm RecFun_fm_type ord_simp_union zero_in_M unfolding RecFun_def by simp lemmas M_basic_sep_instances = inter_sep_intf diff_sep_intf cartprod_sep_intf image_sep_intf converse_sep_intf restrict_sep_intf pred_sep_intf memrel_sep_intf comp_sep_intf is_recfun_sep_intf end \ \\<^locale>\M_Z_trans\\ sublocale M_Z_trans \ M_basic_no_repl "##M" using power_ax M_basic_sep_instances by unfold_locales simp_all lemma Replace_eq_Collect: assumes "\x y y'. x\A \ P(x,y) \ P(x,y') \ y=y'" "{y . x \ A, P(x, y)} \ B" shows "{y . x \ A, P(x, y)} = {y\B . \x\A. P(x,y)}" using assms by blast context M_Z_trans begin lemma Pow_inter_M_closed: assumes "A \ M" shows "Pow(A) \ M \ M" proof - have "{a \ Pow(A) . a \ M} = Pow(A) \ M" by auto then show ?thesis using power_ax powerset_abs assms unfolding power_ax_def by auto qed lemma Pow'_inter_M_closed: assumes "A \ M" shows "{a \ Pow(A) . a \ M} \ M" using power_ax powerset_abs assms unfolding power_ax_def by auto end \ \\<^locale>\M_Z_trans\\ context M_basic_no_repl begin lemma Replace_funspace_succ_rep_intf_sub: assumes "M(A)" "M(n)" shows "{z . p \ A, funspace_succ_rep_intf_rel(M,p,z,n)} \ Pow\<^bsup>M\<^esup>(Pow\<^bsup>M\<^esup>(\domain(A) \ ({n} \ range(A)) \ (\({n} \ range(A)))))" unfolding funspace_succ_rep_intf_rel_def using assms mem_Pow_rel_abs by clarsimp (auto simp: cartprod_def) lemma funspace_succ_rep_intf_uniq: assumes "funspace_succ_rep_intf_rel(M,p,z,n)" "funspace_succ_rep_intf_rel(M,p,z',n)" shows "z = z'" using assms unfolding funspace_succ_rep_intf_rel_def by auto lemma Replace_funspace_succ_rep_intf_eq: assumes "M(A)" "M(n)" shows "{z . p \ A, funspace_succ_rep_intf_rel(M,p,z,n)} = {z \ Pow\<^bsup>M\<^esup>(Pow\<^bsup>M\<^esup>(\domain(A) \ ({n} \ range(A)) \ (\({n} \ range(A))))) . \p\A. funspace_succ_rep_intf_rel(M,p,z,n)}" using assms Replace_eq_Collect[OF funspace_succ_rep_intf_uniq, of A, OF _ _ Replace_funspace_succ_rep_intf_sub[of A n], of "\x y z. x" "\x y z. n"] by (intro equalityI) (auto dest:transM simp:funspace_succ_rep_intf_rel_def) end \ \\<^locale>\M_basic_no_repl\\ definition fsri where "fsri(N,A,B) \ \z. \p\A. \f[N]. \b[N]. p = \f, b\ \ z = {cons(\B, b\, f)}" relationalize "fsri" "is_fsri" synthesize "is_fsri" from_definition assuming "nonempty" arity_theorem for "is_fsri_fm" context M_Z_trans begin lemma separation_fsri: "(##M)(A) \ (##M)(B) \ separation(##M, is_fsri(##M,A,B))" using separation_in_ctm[where env="[A,B]" and \="is_fsri_fm(1,2,0)"] zero_in_M is_fsri_iff_sats[symmetric] arity_is_fsri_fm is_fsri_fm_type by (simp_all add: ord_simp_union) lemma separation_funspace_succ_rep_intf_rel: "(##M)(A) \ (##M)(B) \ separation(##M, \z. \p\A. funspace_succ_rep_intf_rel(##M,p,z,B))" using separation_fsri zero_in_M by (rule_tac separation_cong[THEN iffD1, of _ "is_fsri(##M,A,B)"]) (auto simp flip:setclass_iff dest:transM simp:is_fsri_def funspace_succ_rep_intf_rel_def, force) lemma Replace_funspace_succ_rep_intf_in_M: assumes "A \ M" "n \ M" shows "{z . p \ A, funspace_succ_rep_intf_rel(##M,p,z,n)} \ M" proof - have "(##M)({z \ Pow\<^bsup>M\<^esup>(Pow\<^bsup>M\<^esup>(\domain(A) \ ({n} \ range(A)) \ (\({n} \ range(A))))) . \p\A. funspace_succ_rep_intf_rel(##M,p,z,n)})" using assms separation_funspace_succ_rep_intf_rel by (intro separation_closed) (auto simp flip:setclass_iff) with assms show ?thesis using Replace_funspace_succ_rep_intf_eq by auto qed lemma funspace_succ_rep_intf: assumes "n\M" shows "strong_replacement(##M, \p z. \f\M. \b\M. \nb\M. \cnbf\M. pair(##M,f,b,p) \ pair(##M,n,b,nb) \ is_cons(##M,nb,f,cnbf) \ upair(##M,cnbf,cnbf,z))" using assms pair_in_M_iff[simplified] cons_closed[simplified] unfolding strong_replacement_def univalent_def apply (clarsimp, rename_tac A) apply (rule_tac x="{z . p \ A, funspace_succ_rep_intf_rel(##M,p,z,n)}" in bexI) apply (auto simp:funspace_succ_rep_intf_rel_def Replace_funspace_succ_rep_intf_in_M[unfolded funspace_succ_rep_intf_rel_def, simplified]) done end \ \\<^locale>\M_Z_trans\\ sublocale M_Z_trans \ M_basic "##M" using power_ax M_basic_sep_instances funspace_succ_rep_intf by unfold_locales auto subsection\Interface with \<^term>\M_trancl\\ context M_ZF1_trans begin lemma rtrancl_separation_intf: assumes "r\M" "A\M" shows "separation (##M, rtran_closure_mem(##M,A,r))" using assms separation_in_ctm[of "rtran_closure_mem_fm(1,2,0)" "[A,r]" "rtran_closure_mem(##M,A,r)"] arity_rtran_closure_mem_fm ord_simp_union zero_in_M by simp lemma wftrancl_separation_intf: assumes "r\M" and "Z\M" shows "separation (##M, wellfounded_trancl(##M,Z,r))" using assms separation_in_ctm[of "wellfounded_trancl_fm(1,2,0)" "[Z,r]" "wellfounded_trancl(##M,Z,r)"] arity_wellfounded_trancl_fm ord_simp_union zero_in_M by simp text\To prove \<^term>\nat \ M\ we get an infinite set \<^term>\I\ from \<^term>\infinity_ax\ closed under \<^term>\0\ and \<^term>\succ\; that shows \<^term>\nat\I\. Then we can separate \<^term>\I\ with the predicate \<^term>\\x. x\nat\.\ lemma finite_sep_intf: "separation(##M, \x. x\nat)" proof - have "(\v\M. separation(##M,\x. (M, [x,v] \ finite_ordinal_fm(0))))" using separation_ax arity_finite_ordinal_fm by simp then have "(\v\M. separation(##M,finite_ordinal(##M)))" unfolding separation_def by simp then have "separation(##M,finite_ordinal(##M))" using separation_in_ctm zero_in_M by auto then show ?thesis unfolding separation_def by simp qed lemma nat_subset_I: "\I\M. nat \ I" proof - have "nat \ I" if "I\M" and "0\I" and "\x. x\I \ succ(x)\I" for I using that by (rule_tac subsetI,induct_tac x,simp_all) moreover obtain I where "I\M" "0\I" "\x. x\I \ succ(x)\I" using infinity_ax transitivity unfolding infinity_ax_def by auto ultimately show ?thesis by auto qed lemma nat_in_M: "nat \ M" proof - have "{x\B . x\A}=A" if "A\B" for A B using that by auto moreover obtain I where "I\M" "nat\I" using nat_subset_I by auto moreover from this have "{x\I . x\nat} \ M" using finite_sep_intf separation_closed[of "\x . x\nat"] by simp ultimately show ?thesis by simp qed end \ \\<^locale>\M_ZF1_trans\\ sublocale M_ZF1_trans \ M_trancl "##M" using rtrancl_separation_intf wftrancl_separation_intf nat_in_M wellfounded_trancl_def by unfold_locales auto subsection\Interface with \<^term>\M_eclose\\ lemma repl_sats: assumes sat:"\x z. x\M \ z\M \ (M, Cons(x,Cons(z,env)) \ \) \ P(x,z)" shows "strong_replacement(##M,\x z. (M, Cons(x,Cons(z,env)) \ \)) \ strong_replacement(##M,P)" by (rule strong_replacement_cong,simp add:sat) arity_theorem for "list_functor_fm" arity_theorem for "formula_functor_fm" arity_theorem for "Inl_fm" arity_theorem for "Inr_fm" arity_theorem for "Nil_fm" arity_theorem for "Cons_fm" arity_theorem for "quasilist_fm" arity_theorem for "tl_fm" arity_theorem for "big_union_fm" context M_ZF1_trans begin text\This lemma obtains \<^term>\iterates_replacement\ for predicates without parameters.\ lemma iterates_repl_intf : assumes "v\M" and isfm:"is_F_fm \ formula" and arty:"arity(is_F_fm)=2" and satsf: "\a b env'. \ a\M ; b\M ; env'\list(M) \ \ is_F(a,b) \ (M, [b,a]@env' \ is_F_fm)" and is_F_fm_replacement: "\env. (\\\\\1,0\ is 2\ \ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) \\) \ formula \ env \ list(M) \ arity((\\\\\1,0\ is 2\ \ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) \\)) \ 2 +\<^sub>\ length(env) \ strong_replacement(##M,\x y. M, [x,y] @ env \ (\\\\\1,0\ is 2\ \ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) \\))" shows "iterates_replacement(##M,is_F,v)" proof - let ?f="(\\\\\1,0\ is 2\ \ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) \\)" have "arity(?f) = 4" "?f\formula" using arity_iterates_MH_fm[where isF=is_F_fm and i=2] arity_wfrec_replacement_fm[where i=10] isfm arty ord_simp_union by simp_all { fix n assume "n\nat" then have "Memrel(succ(n))\M" using nat_into_M Memrel_closed by simp moreover { fix a0 a1 a2 a3 a4 y x z assume "[a0,a1,a2,a3,a4,y,x,z]\list(M)" moreover note \v\M\ \Memrel(succ(n))\M\ moreover from calculation have "(M, [b,a,c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v] \ is_F_fm) \ is_F(a,b)" if "a\M" "b\M" "c\M" "d\M" for a b c d using that satsf[of a b "[c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]"] by simp moreover from calculation have "(M, [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v] \ iterates_MH_fm(is_F_fm,9,2,1,0)) \ iterates_MH(##M,is_F,v,a2, a1, a0)" using sats_iterates_MH_fm[of M "is_F" "is_F_fm"] by simp } moreover from calculation have "(M, [y,x,z,Memrel(succ(n)),v] \ is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0)) \ is_wfrec(##M, iterates_MH(##M,is_F,v),Memrel(succ(n)), x, y)" if "y\M" "x\M" "z\M" for y x z using that sats_is_wfrec_fm \v\M\ by simp moreover from calculation have "(M, [x,z,Memrel(succ(n)),v] \ ?f) \ (\y\M. pair(##M,x,y,z) \ is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))" if "x\M" "z\M" for x z using that \v\M\ by (simp del:pair_abs) moreover note \arity(?f) = 4\ \?f\formula\ moreover from calculation \v\_\ have "strong_replacement(##M,\x z. (M, [x,z,Memrel(succ(n)),v] \ ?f))" using is_F_fm_replacement by simp ultimately have "strong_replacement(##M,\x z. \y\M. pair(##M,x,y,z) \ is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))" using repl_sats[of M ?f "[Memrel(succ(n)),v]"] by (simp del:pair_abs) } then show ?thesis unfolding iterates_replacement_def wfrec_replacement_def by simp qed lemma eclose_repl1_intf: assumes "A\M" shows "iterates_replacement(##M, big_union(##M), A)" using assms arity_big_union_fm iterates_repl_intf[where is_F_fm="big_union_fm(1,0)"] replacement_ax1(1)[unfolded replacement_assm_def] ord_simp_union by simp lemma eclose_repl2_intf: assumes "A\M" shows "strong_replacement(##M,\n y. n\nat \ is_iterates(##M, big_union(##M), A, n, y))" proof - let ?f = "And(Member(0,3),is_iterates_fm(big_union_fm(1,0),2,0,1))" note nat_in_M \A\M\ moreover from this have "big_union(##M,a,b) \ (M, [b,a,c,d,e,f,g,h,i,j,k,n,y,A,nat] \ big_union_fm(1,0))" if "a\M" "b\M" "c\M" "d\M" "e\M" "f\M""g\M""h\M""i\M""j\M" "k\M" "n\M" "y\M" for a b c d e f g h i j k n y using that by simp moreover from calculation have "(M, [n,y,A,nat] \ is_iterates_fm(big_union_fm(1,0),2,0,1)) \ is_iterates(##M, big_union(##M), A, n , y)" if "n\M" "y\M" for n y using that sats_is_iterates_fm[of M "big_union(##M)"] by simp moreover from calculation have "(M, [n,y,A,nat] \ ?f) \ n\nat \ is_iterates(##M, big_union(##M), A, n, y)" if "n\M" "y\M" for n y using that by simp moreover have "arity(?f) = 4" using arity_is_iterates_fm[where p="big_union_fm(1,0)" and i=2] arity_big_union_fm arity_And ord_simp_union by simp ultimately show ?thesis using repl_sats[of M ?f "[A,nat]"] replacement_ax1(2)[unfolded replacement_assm_def] by simp qed end \ \\<^locale>\M_ZF1_trans\\ sublocale M_ZF1_trans \ M_eclose "##M" using eclose_repl1_intf eclose_repl2_intf by unfold_locales auto text\Interface with \<^locale>\M_eclose\.\ schematic_goal sats_is_Vset_fm_auto: assumes "i\nat" "v\nat" "env\list(A)" "0\A" "i < length(env)" "v < length(env)" shows "is_Vset(##A,nth(i, env),nth(v, env)) \ (A, env \ ?ivs_fm(i,v))" unfolding is_Vset_def is_Vfrom_def by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+) synthesize "is_Vset" from_schematic "sats_is_Vset_fm_auto" arity_theorem for "is_Vset_fm" declare is_Hrank_fm_def[fm_definitions add] context M_ZF1_trans begin lemma wfrec_rank : assumes "X\M" shows "wfrec_replacement(##M,is_Hrank(##M),rrank(X))" proof - let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)))" note assms zero_in_M moreover from this have "is_Hrank(##M,a2, a1, a0) \ (M, [a0,a1,a2,a3,a4,y,x,z,rrank(X)] \ is_Hrank_fm(2,1,0))" if "a4\M" "a3\M" "a2\M" "a1\M" "a0\M" "y\M" "x\M" "z\M" for a4 a3 a2 a1 a0 y x z using that rrank_in_M is_Hrank_iff_sats by simp moreover from calculation have "(M, [y,x,z,rrank(X)] \ is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)) \ is_wfrec(##M, is_Hrank(##M) ,rrank(X), x, y)" if "y\M" "x\M" "z\M" for y x z using that rrank_in_M sats_is_wfrec_fm by simp moreover from calculation have "(M, [x,z,rrank(X)] \ ?f) \ (\y\M. pair(##M,x,y,z) \ is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))" if "x\M" "z\M" for x z using that rrank_in_M by (simp del:pair_abs) moreover have "arity(?f) = 3" using arity_wfrec_replacement_fm[where p="is_Hrank_fm(2,1,0)" and i=3,simplified] arity_is_Hrank_fm[of 2 1 0,simplified] ord_simp_union by simp moreover from calculation have "strong_replacement(##M,\x z. (M, [x,z,rrank(X)] \ ?f))" using replacement_ax1(3)[unfolded replacement_assm_def] rrank_in_M by simp ultimately show ?thesis using repl_sats[of M ?f "[rrank(X)]"] unfolding wfrec_replacement_def by (simp del:pair_abs) qed lemma trans_repl_HVFrom : assumes "A\M" "i\M" shows "transrec_replacement(##M,is_HVfrom(##M,A),i)" proof - let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)))" note facts = assms zero_in_M moreover have "\sa\M. \esa\M. \mesa\M. upair(##M,a,a,sa) \ is_eclose(##M,sa,esa) \ membership(##M,esa,mesa)" if "a\M" for a using that upair_ax eclose_closed Memrel_closed unfolding upair_ax_def by (simp del:upair_abs) moreover { fix mesa assume "mesa\M" moreover note facts moreover from calculation have "is_HVfrom(##M,A,a2, a1, a0) \ (M, [a0,a1,a2,a3,a4,y,x,z,A,mesa] \ is_HVfrom_fm(8,2,1,0))" if "a4\M" "a3\M" "a2\M" "a1\M" "a0\M" "y\M" "x\M" "z\M" for a4 a3 a2 a1 a0 y x z using that sats_is_HVfrom_fm by simp moreover from calculation have "(M, [y,x,z,A,mesa] \ is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)) \ is_wfrec(##M, is_HVfrom(##M,A),mesa, x, y)" if "y\M" "x\M" "z\M" for y x z using that sats_is_wfrec_fm by simp moreover from calculation have "(M, [x,z,A,mesa] \ ?f) \ (\y\M. pair(##M,x,y,z) \ is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))" if "x\M" "z\M" for x z using that by (simp del:pair_abs) moreover have "arity(?f) = 4" using arity_wfrec_replacement_fm[where p="is_HVfrom_fm(8,2,1,0)" and i=9] arity_is_HVfrom_fm ord_simp_union by simp moreover from calculation have "strong_replacement(##M,\x z. (M, [x,z,A,mesa] \ ?f))" using replacement_ax1(4)[unfolded replacement_assm_def] by simp ultimately have "wfrec_replacement(##M,is_HVfrom(##M,A),mesa)" using repl_sats[of M ?f "[A,mesa]"] unfolding wfrec_replacement_def by (simp del:pair_abs) } ultimately show ?thesis unfolding transrec_replacement_def by simp qed end \ \\<^locale>\M_ZF1_trans\\ subsection\Interface for proving Collects and Replace in M.\ context M_ZF1_trans begin lemma Collect_in_M : assumes "\ \ formula" "env\list(M)" "arity(\) \ 1 +\<^sub>\ length(env)" "A\M" and satsQ: "\x. x\M \ (M, [x]@env \ \) \ Q(x)" shows "{y\A . Q(y)}\M" proof - have "separation(##M,\x. (M, [x] @ env \ \))" using assms separation_ax by simp then show ?thesis using \A\M\ satsQ transitivity separation_closed separation_cong[of "##M" "\y. (M, [y]@env \ \)" "Q"] by simp qed \ \This version has a weaker assumption.\ lemma separation_in_M : assumes "\ \ formula" "env\list(M)" "arity(\) \ 1 +\<^sub>\ length(env)" "A\M" and satsQ: "\x. x\A \ (M, [x]@env \ \) \ Q(x)" shows "{y\A . Q(y)} \ M" proof - let ?\' = "And(\,Member(0,length(env)+\<^sub>\1))" note assms moreover have "arity(?\') \ 1 +\<^sub>\ length(env@[A])" using assms Un_le le_trans[of "arity(\)" "1+\<^sub>\length(env)" "2+\<^sub>\length(env)"] by (force simp:FOL_arities) moreover from calculation have "?\'\formula" "nth(length(env), env @ [A]) = A" using nth_append by auto moreover from calculation have "\ x . x \ M \ (M, [x]@env@[A] \ ?\') \ Q(x) \ x\A" using arity_sats_iff[of _ "[A]" _ "[_]@env"] by auto ultimately show ?thesis using Collect_in_M[of ?\' "env@[A]" _ "\x . Q(x) \ x\A", OF _ _ _ \A\M\] by auto qed end \ \\<^locale>\M_ZF1_trans\\ context M_Z_trans begin lemma strong_replacement_in_ctm: assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 2 +\<^sub>\ length(env)" and fsats: "\x y. x\M \ y\M \ (M,[x,y]@env \ \) \ y = f(x)" and fclosed: "\x. x\M \ f(x) \ M" and phi_replacement:"replacement_assm(M,env,\)" and "env\list(M)" shows "strong_replacement(##M, \x y . y = f(x))" using assms strong_replacement_cong[of "##M" "\x y. M,[x,y]@env\\" "\x y. y = f(x)"] unfolding replacement_assm_def by auto lemma strong_replacement_rel_in_ctm : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 2 +\<^sub>\ length(env)" and fsats: "\x y. x\M \ y\M \ (M,[x,y]@env \ \) \ f(x,y)" and phi_replacement:"replacement_assm(M,env,\)" and "env\list(M)" shows "strong_replacement(##M, f)" using assms strong_replacement_cong[of "##M" "\x y. M,[x,y]@env\\" "f"] unfolding replacement_assm_def by auto lemma Replace_in_M : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 2 +\<^sub>\ length(env)" and fsats: "\x y. x\A \ y\M \ (M,[x,y]@env \ \) \ y = f(x)" and fclosed: "\x. x\A \ f(x) \ M" and "A\M" "env\list(M)" and phi'_replacement:"replacement_assm(M,env@[A], \\ \ \0 \ length(env) +\<^sub>\ 2\\ )" shows "{f(x) . x\A}\M" proof - let ?\' = "And(\,Member(0,length(env)+\<^sub>\2))" note assms moreover from this have "arity(?\') \ 2 +\<^sub>\ length(env@[A])" using Un_le le_trans[of "arity(\)" "2+\<^sub>\(length(env))" "3+\<^sub>\length(env)"] by (force simp:FOL_arities) moreover from calculation have "?\'\formula" "nth(length(env), env @ [A]) = A" using nth_append by auto moreover from calculation have "\ x y. x \ M \ y\M \ (M,[x,y]@env@[A]\?\') \ y=f(x) \x\A" using arity_sats_iff[of _ "[A]" _ "[_,_]@env"] by auto moreover from calculation have "strong_replacement(##M, \x y. M,[x,y]@env@[A] \ ?\')" using phi'_replacement assms(1-6) unfolding replacement_assm_def by simp ultimately have 4:"strong_replacement(##M, \x y. y = f(x) \ x\A)" using strong_replacement_cong[of "##M" "\x y. M,[x,y]@env@[A]\?\'" "\x y. y = f(x) \ x\A"] by simp then have "{y . x\A , y = f(x)} \ M" using \A\M\ strong_replacement_closed[OF 4,of A] fclosed by simp moreover have "{f(x). x\A} = { y . x\A , y = f(x)}" by auto ultimately show ?thesis by simp qed lemma Replace_relativized_in_M : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 2 +\<^sub>\ length(env)" and fsats: "\x y. x\A \ y\M \ (M,[x,y]@env \ \) \ is_f(x,y)" and fabs: "\x y. x\A \ y\M \ is_f(x,y) \ y = f(x)" and fclosed: "\x. x\A \ f(x) \ M" and "A\M" "env\list(M)" and phi'_replacement:"replacement_assm(M,env@[A], \\ \ \0 \ length(env) +\<^sub>\ 2\\ )" shows "{f(x) . x\A}\M" using assms Replace_in_M[of \] by auto lemma ren_action : assumes "env\list(M)" "x\M" "y\M" "z\M" shows "\ i . i < 2+\<^sub>\length(env) \ nth(i,[x,z]@env) = nth(\_repl(length(env))`i,[z,x,y]@env)" proof - let ?f="{\0, 1\, \1, 0\}" have 1:"(\j. j < length(env) \ nth(j, env) = nth(id(length(env)) ` j, env))" using assms ltD by simp have 2:"nth(j, [x,z]) = nth(?f ` j, [z,x,y])" if "j<2" for j proof - consider "j=0" | "j=1" using ltD[OF \j<2\] by auto then show ?thesis proof(cases) case 1 then show ?thesis using apply_equality f_type by simp next case 2 then show ?thesis using apply_equality f_type by simp qed qed show ?thesis using sum_action[OF _ _ _ _ f_type id_type _ _ _ _ _ _ _ 2 1,simplified] assms unfolding \_repl_def by simp qed lemma Lambda_in_M : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 2 +\<^sub>\ length(env)" and fsats: "\x y. x\A \ y\M \ (M,[x,y]@env \ \) \ is_f(x,y)" and fabs: "\x y. x\A \ y\M \ is_f(x,y) \ y = f(x)" and fclosed: "\x. x\A \ f(x) \ M" and "A\M" "env\list(M)" and phi'_replacement2: "replacement_assm(M,env@[A],Lambda_in_M_fm(\,length(env)))" shows "(\x\A . f(x)) \M" unfolding lam_def proof - let ?ren="\_repl(length(env))" let ?j="2+\<^sub>\length(env)" let ?k="3+\<^sub>\length(env)" let ?\="ren(\)`?j`?k`?ren" let ?\'="Exists(And(pair_fm(1,0,2),?\))" let ?p="\x y. \z\M. pair(##M,x,z,y) \ is_f(x,z)" have "?\'\formula" "?\\formula" using \env\_\ length_type f_fm ren_type ren_tc[of \ "2+\<^sub>\length(env)" "3+\<^sub>\length(env)" ?ren] by simp_all moreover from this have "arity(?\)\3+\<^sub>\(length(env))" "arity(?\)\nat" using assms arity_ren[OF f_fm _ _ ren_type,of "length(env)"] by simp_all then have "arity(?\') \ 2+\<^sub>\(length(env))" using Un_le pred_Un_distrib assms pred_le by (simp add:arity) moreover from this calculation have "x\A \ y\M \ (M,[x,y]@env \ ?\') \ ?p(x,y)" for x y using \env\_\ length_type[OF \env\_\] assms transitivity[OF _ \A\M\] sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type f_ar ren_action[rule_format,of _ x y],of _ M ] by auto moreover have "x\A \ y\M \ ?p(x,y) \ y = " for x y using assms transitivity[OF _ \A\_\] fclosed by simp moreover have "\ x . x\A \ \ M" using transitivity[OF _ \A\M\] pair_in_M_iff fclosed by simp ultimately show "{\x,f(x)\ . x\A } \ M" using Replace_in_M[of ?\' env A] phi'_replacement2 \A\M\ \env\_\ by simp qed lemma ren_action' : assumes "env\list(M)" "x\M" "y\M" "z\M" "u\M" shows "\ i . i < 3+\<^sub>\length(env) \ nth(i,[x,z,u]@env) = nth(\_pair_repl(length(env))`i,[x,z,y,u]@env)" proof - let ?f="{\0, 0\, \1, 1\, \2,3\}" have 1:"(\j. j < length(env) \ nth(j, env) = nth(id(length(env)) ` j, env))" using assms ltD by simp have 2:"nth(j, [x,z,u]) = nth(?f ` j, [x,z,y,u])" if "j<3" for j proof - consider "j=0" | "j=1" | "j=2" using ltD[OF \j<3\] by auto then show ?thesis proof(cases) case 1 then show ?thesis using apply_equality f_type' by simp next case 2 then show ?thesis using apply_equality f_type' by simp next case 3 then show ?thesis using apply_equality f_type' by simp qed qed show ?thesis using sum_action[OF _ _ _ _ f_type' id_type _ _ _ _ _ _ _ 2 1,simplified] assms unfolding \_pair_repl_def by simp qed lemma LambdaPair_in_M : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 3 +\<^sub>\ length(env)" and fsats: "\x z r. x\M \ z\M \ r\M \ (M,[x,z,r]@env \ \) \ is_f(x,z,r)" and fabs: "\x z r. x\M \ z\M \ r\M \ is_f(x,z,r) \ r = f(x,z)" and fclosed: "\x z. x\M \ z\M \ f(x,z) \ M" and "A\M" "env\list(M)" and phi'_replacement3: "replacement_assm(M,env@[A],LambdaPair_in_M_fm(\,length(env)))" shows "(\x\A . f(fst(x),snd(x))) \M" proof - let ?ren="\_pair_repl(length(env))" let ?j="3+\<^sub>\length(env)" let ?k="4+\<^sub>\length(env)" let ?\="ren(\)`?j`?k`?ren" let ?\'="Exists(Exists(And(fst_fm(2,0),(And(snd_fm(2,1),?\)))))" let ?p="\x y. is_f(fst(x),snd(x),y)" have "?\'\formula" "?\\formula" using \env\_\ length_type f_fm ren_type' ren_tc[of \ ?j ?k ?ren] by simp_all moreover from this have "arity(?\)\4+\<^sub>\(length(env))" "arity(?\)\nat" using assms arity_ren[OF f_fm _ _ ren_type',of "length(env)"] by simp_all moreover from calculation have 1:"arity(?\') \ 2+\<^sub>\(length(env))" "?\'\formula" using Un_le pred_Un_distrib assms pred_le by (simp_all add:arity) moreover from this calculation have 2:"x\A \ y\M \ (M,[x,y]@env \ ?\') \ ?p(x,y)" for x y using sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type' f_ar ren_action'[rule_format,of _ "fst(x)" x "snd(x)" y],simplified] \env\_\ length_type[OF \env\_\] transitivity[OF _ \A\M\] fst_snd_closed pair_in_M_iff fsats[of "fst(x)" "snd(x)" y,symmetric] fst_abs snd_abs by auto moreover from assms have 3:"x\A \ y\M \ ?p(x,y) \ y = f(fst(x),snd(x))" for x y using fclosed fst_snd_closed pair_in_M_iff fabs transitivity by auto moreover have 4:"\ x . x\A \ \ M" "\ x . x\A \ f(fst(x),snd(x)) \ M" using transitivity[OF _ \A\M\] pair_in_M_iff fclosed fst_snd_closed by simp_all ultimately show ?thesis using Lambda_in_M[unfolded Lambda_in_M_fm_def, of ?\', OF _ _ _ _ _ _ _ phi'_replacement3[unfolded LambdaPair_in_M_fm_def]] \env\_\ \A\_\ by simp qed lemma (in M_ZF1_trans) lam_replacement2_in_ctm : assumes f_fm: "\ \ formula" and f_ar: "arity(\)\ 3 +\<^sub>\ length(env)" and fsats: "\x z r. x\M \ z\M \ r\M \ (M,[x,z,r]@env \ \) \ is_f(x,z,r)" and fabs: "\x z r. x\M \ z\M \ r\M \ is_f(x,z,r) \ r = f(x,z)" and fclosed: "\x z. x\M \ z\M \ f(x,z) \ M" and "env\list(M)" and phi'_replacement3: "\A. A\M \ replacement_assm(M,env@[A],LambdaPair_in_M_fm(\,length(env)))" shows "lam_replacement(##M , \x . f(fst(x),snd(x)))" using LambdaPair_in_M fabs f_ar ord_simp_union transitivity assms fst_snd_closed by (rule_tac lam_replacement_iff_lam_closed[THEN iffD2],simp_all) simple_rename "ren_U" src "[z1,x_P, x_leq, x_o, x_t, z2_c]" tgt "[z2_c,z1,z,x_P, x_leq, x_o, x_t]" simple_rename "ren_V" src "[fz,x_P, x_leq, x_o,x_f, x_t, gz]" tgt "[gz,fz,z,x_P, x_leq, x_o,x_f, x_t]" simple_rename "ren_V3" src "[fz,x_P, x_leq, x_o,x_f, gz, hz]" tgt "[hz,gz,fz,z,x_P, x_leq, x_o,x_f]" lemma separation_sat_after_function_1: assumes "[a,b,c,d]\list(M)" and "\\formula" and "arity(\) \ 6" and f_fm: "f_fm \ formula" and f_ar: "arity(f_fm) \ 6" and fsats: "\ fx x. fx\M \ x\M \ (M,[fx,x]@[a, b, c, d] \ f_fm) \ fx=f(x)" and fclosed: "\x . x\M \ f(x) \ M" and g_fm: "g_fm \ formula" and g_ar: "arity(g_fm) \ 7" and gsats: "\ gx fx x. gx\M \ fx\M \ x\M \ (M,[gx,fx,x]@[a, b, c, d] \ g_fm) \ gx=g(x)" and gclosed: "\x . x\M \ g(x) \ M" shows "separation(##M, \r. M, [f(r), a, b, c, d, g(r)] \ \)" proof - note types = assms(1-4) let ?\="ren(\)`6`7`ren_U_fn" let ?\'="Exists(And(f_fm,Exists(And(g_fm,?\))))" let ?\="\z.[f(z), a, b, c, d, g(z)]" let ?env="[a, b, c, d]" let ?\="\z.[g(z),f(z),z]@?env" note types moreover from this have "arity(\) \ 7" "?\\formula" using ord_simp_union ren_tc ren_U_thm(2)[folded ren_U_fn_def] le_trans[of "arity(\)" 6] by simp_all moreover from calculation have "arity(?\) \ 7" "?\'\formula" using arity_ren ren_U_thm(2)[folded ren_U_fn_def] f_fm g_fm by simp_all moreover from calculation f_ar g_ar f_fm g_fm have "arity(?\') \ 5" using ord_simp_union pred_le arity_type by (simp add:arity) moreover from calculation fclosed gclosed have 0:"(M, [f(z), a, b, c, d, g(z)] \ \) \ (M,?\(z)\ ?\)" if "(##M)(z)" for z using sats_iff_sats_ren[of \ 6 7 _ _ "?\(z)"] ren_U_thm(1)[where A=M,folded ren_U_fn_def] ren_U_thm(2)[folded ren_U_fn_def] that by simp moreover from calculation have 1:"(M,?\(z)\ ?\) \ M,[z]@?env\?\'" if "(##M)(z)" for z using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z] fclosed gclosed f_fm g_fm proof(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp,(auto)[1]) assume "M, [z] @ [a, b, c, d] \ (\\\f_fm \ (\\\g_fm \ ren(\) ` 6 ` 7 ` ren_U_fn\\)\\)" then have "\xa\M. (M, [xa, z, a, b, c, d] \ f_fm) \ (\x\M. (M, [x, xa, z, a, b, c, d] \ g_fm) \ (M, [x, xa, z, a, b, c, d] \ ren(\) ` 6 ` 7 ` ren_U_fn))" using that calculation by auto then obtain xa x where "x\M" "xa\M" "M, [xa, z, a, b, c, d] \ f_fm" "(M, [x, xa, z, a, b, c, d] \ g_fm)" "(M, [x, xa, z, a, b, c, d] \ ren(\) ` 6 ` 7 ` ren_U_fn)" using that calculation by auto moreover from this have "xa=f(z)" "x=g(z)" using fsats[of xa] gsats[of x xa] that by simp_all ultimately show "M, [g(z), f(z), z] @ [a, b, c, d] \ ren(\) ` 6 ` 7 ` ren_U_fn" by auto qed moreover from calculation have "separation(##M, \z. (M,[z]@?env \ ?\'))" using separation_ax by simp_all ultimately show ?thesis by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force) qed lemma separation_sat_after_function3: assumes "[a, b, c, d]\list(M)" and "\\formula" and "arity(\) \ 7" and f_fm: "f_fm \ formula" and f_ar: "arity(f_fm) \ 6" and fsats: "\ fx x. fx\M \ x\M \ (M,[fx,x]@[a, b, c, d] \ f_fm) \ fx=f(x)" and fclosed: "\x . x\M \ f(x) \ M" and g_fm: "g_fm \ formula" and g_ar: "arity(g_fm) \ 7" and gsats: "\ gx fx x. gx\M \ fx\M \ x\M \ (M,[gx,fx,x]@[a, b, c, d] \ g_fm) \ gx=g(x)" and gclosed: "\x . x\M \ g(x) \ M" and h_fm: "h_fm \ formula" and h_ar: "arity(h_fm) \ 8" and hsats: "\ hx gx fx x. hx\M \ gx\M \ fx\M \ x\M \ (M,[hx,gx,fx,x]@[a, b, c, d] \ h_fm) \ hx=h(x)" and hclosed: "\x . x\M \ h(x) \ M" shows "separation(##M, \r. M, [f(r), a, b, c, d, g(r), h(r)] \ \)" proof - note types = assms(1-3) let ?\="\" let ?\="ren(?\)`7`8`ren_V3_fn" let ?\'="Exists(And(f_fm,Exists(And(g_fm,Exists(And(h_fm,?\))))))" let ?\="\z.[f(z), a, b, c, d,g(z), h(z)]" let ?env="[a, b, c, d]" let ?\="\z.[h(z),g(z),f(z),z]@?env" note types moreover from this have "?\\formula" by simp moreover from calculation have "arity(?\) \ 9" "?\\formula" using ord_simp_union ren_tc ren_V3_thm(2)[folded ren_V3_fn_def] le_trans[of "arity(\)" 7] by simp_all moreover from calculation have "arity(?\) \ 8" "?\'\formula" using arity_ren ren_V3_thm(2)[folded ren_V3_fn_def] f_fm g_fm h_fm by (simp_all) moreover from this f_ar g_ar f_fm g_fm h_fm h_ar \?\'\_\ have "arity(?\') \ 5" using ord_simp_union arity_type nat_into_Ord by (simp add:arity,(rule_tac pred_le,simp,rule_tac Un_le,simp)+,simp_all add: \?\\_\) moreover from calculation fclosed gclosed hclosed have 0:"(M, ?\(z) \ ?\) \ (M,?\(z)\ ?\)" if "(##M)(z)" for z using sats_iff_sats_ren[of ?\ 7 8 "?\(z)" M "?\(z)"] ren_V3_thm(1)[where A=M,folded ren_V3_fn_def,simplified] ren_V3_thm(2)[folded ren_V3_fn_def] that by simp moreover from calculation have 1:"(M,?\(z)\ ?\) \ M,[z]@?env\?\'" if "(##M)(z)" for z using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z] hsats[of "h(z)" "g(z)" "f(z)" z] fclosed gclosed hclosed f_fm g_fm h_fm apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp) apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="g(z)"],simp) apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="h(z)"],simp,rule_tac conjI,simp,simp) proof - assume "M, [z] @ [a, b, c, d] \ (\\\f_fm \ (\\\g_fm \ (\\\h_fm \ ren(\) ` 7 ` 8 ` ren_V3_fn\\)\\)\\)" with calculation that have "\x\M. (M, [x, z, a, b, c, d] \ f_fm) \ (\xa\M. (M, [xa, x, z, a, b, c, d] \ g_fm) \ (\xb\M. (M, [xb, xa, x, z, a, b, c, d] \ h_fm) \ (M, [xb, xa, x, z, a, b, c, d] \ ren(\) ` 7 ` 8 ` ren_V3_fn)))" by auto with calculation obtain x where "x\M" "(M, [x, z, a, b, c, d] \ f_fm)" "(\xa\M. (M, [xa, x, z, a, b, c, d] \ g_fm) \ (\xb\M. (M, [xb, xa, x, z, a, b, c, d] \ h_fm) \ (M, [xb, xa, x, z, a, b, c, d] \ ren(\) ` 7 ` 8 ` ren_V3_fn)))" by force moreover from this have "x=f(z)" using fsats[of x] that by simp moreover from calculation obtain xa where "xa\M" "(M, [xa, x, z, a, b, c, d] \ g_fm)" "(\xb\M. (M, [xb, xa, x, z, a, b, c, d] \ h_fm) \ (M, [xb, xa, x, z, a, b, c, d] \ ren(\) ` 7 ` 8 ` ren_V3_fn))" by auto moreover from calculation have "xa=g(z)" using gsats[of xa x] that by simp moreover from calculation obtain xb where "xb\M" "(M, [xb, xa, x, z, a, b, c, d] \ h_fm)" "(M, [xb, xa, x, z, a, b, c, d] \ ren(\) ` 7 ` 8 ` ren_V3_fn)" by auto moreover from calculation have "xb=h(z)" using hsats[of xb xa x] that by simp ultimately show "M, [h(z), g(z), f(z), z] @ [a, b, c, d] \ ren(\) ` 7 ` 8 ` ren_V3_fn" by auto qed moreover from calculation \?\'\_\ have "separation(##M, \z. (M,[z]@?env \ ?\'))" using separation_ax by simp ultimately show ?thesis by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force) qed lemma separation_sat_after_function: assumes "[a, b, c, d, \]\list(M)" and "\\formula" and "arity(\) \ 7" and f_fm: "f_fm \ formula" and f_ar: "arity(f_fm) \ 7" and fsats: "\ fx x. fx\M \ x\M \ (M,[fx,x]@[a, b, c, d, \] \ f_fm) \ fx=f(x)" and fclosed: "\x . x\M \ f(x) \ M" and g_fm: "g_fm \ formula" and g_ar: "arity(g_fm) \ 8" and gsats: "\ gx fx x. gx\M \ fx\M \ x\M \ (M,[gx,fx,x]@[a, b, c, d, \] \ g_fm) \ gx=g(x)" and gclosed: "\x . x\M \ g(x) \ M" shows "separation(##M, \r. M, [f(r), a, b, c, d, \, g(r)] \ \)" proof - note types = assms(1-3) let ?\="\" let ?\="ren(?\)`7`8`ren_V_fn" let ?\'="Exists(And(f_fm,Exists(And(g_fm,?\))))" let ?\="\z.[f(z), a, b, c, d, \, g(z)]" let ?env="[a, b, c, d, \]" let ?\="\z.[g(z),f(z),z]@?env" note types moreover from this have "?\\formula" by simp moreover from calculation have "arity(?\) \ 8" "?\\formula" using ord_simp_union ren_tc ren_V_thm(2)[folded ren_V_fn_def] le_trans[of "arity(\)" 7] by simp_all moreover from calculation have "arity(?\) \ 8" "?\'\formula" using arity_ren ren_V_thm(2)[folded ren_V_fn_def] f_fm g_fm by (simp_all) moreover from calculation f_ar g_ar f_fm g_fm have "arity(?\') \ 6" using ord_simp_union pred_le arity_type by (simp add:arity) moreover from calculation fclosed gclosed have 0:"(M, ?\(z) \ ?\) \ (M,?\(z)\ ?\)" if "(##M)(z)" for z using sats_iff_sats_ren[of ?\ 7 8 "?\(z)" _ "?\(z)"] ren_V_thm(1)[where A=M,folded ren_V_fn_def] ren_V_thm(2)[folded ren_V_fn_def] that by simp moreover from calculation have 1:"(M,?\(z)\ ?\) \ M,[z]@?env\?\'" if "(##M)(z)" for z using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z] fclosed gclosed f_fm g_fm apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp) apply(auto)[1] proof - assume "M, [z] @ [a, b, c, d, \] \ (\\\f_fm \ (\\\g_fm \ ren(\) ` 7 ` 8 ` ren_V_fn\\)\\)" then have "\xa\M. (M, [xa, z, a, b, c, d, \] \ f_fm) \ (\x\M. (M, [x, xa, z, a, b, c, d, \] \ g_fm) \ (M, [x, xa, z, a, b, c, d, \] \ ren(\) ` 7 ` 8 ` ren_V_fn))" using that calculation by auto then obtain xa where "xa\M" "M, [xa, z, a, b, c, d, \] \ f_fm" "(\x\M. (M, [x, xa, z, a, b, c, d, \] \ g_fm) \ (M, [x, xa, z, a, b, c, d, \] \ ren(\) ` 7 ` 8 ` ren_V_fn))" by auto moreover from this have "xa=f(z)" using fsats[of xa] that by simp moreover from calculation obtain x where "x\M" "M, [x, xa, z, a, b, c, d, \] \ g_fm" "M, [x, xa, z, a, b, c, d, \] \ ren(\) ` 7 ` 8 ` ren_V_fn" by auto moreover from calculation have "x=g(z)" using gsats[of x xa] that by simp ultimately show "M, [g(z), f(z), z] @ [a, b, c, d, \] \ ren(\) ` 7 ` 8 ` ren_V_fn" by auto qed moreover from calculation have "separation(##M, \z. (M,[z]@?env \ ?\'))" using separation_ax by simp_all ultimately show ?thesis by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force) qed end definition separation_assm_fm :: "[i,i,i] \ i" where "separation_assm_fm(A,x,f_fm) \ (\\ (\\ \\0 \ A +\<^sub>\ 2\ \ \\\0,1\ is x+\<^sub>\ 2 \ \ f_fm \\\)\)" lemma separation_assm_fm_type[TC]: "A \ \ \ y \ \ \ f_fm \ formula \ separation_assm_fm(A, y,f_fm) \ formula" unfolding separation_assm_fm_def by simp lemma arity_separation_assm_fm : "A \ \ \ x \ \ \ f_fm \ formula \ arity(separation_assm_fm(A, x, f_fm)) = succ(A) \ succ(x) \ pred(pred(arity(f_fm)))" using pred_Un_distrib unfolding separation_assm_fm_def by (auto simp add:arity) definition separation_assm_bin_fm where "separation_assm_bin_fm(A,y,f_fm) \ (\\(\\(\\(\\(\(\\3 \ A +\<^sub>\ 4\ \ \\3,2\ is y +\<^sub>\ 4\\ ) \ \f_fm \ \ \fst(3) is 0 \ \ \snd(3) is 1\\\\ ) \)\)\)\) " lemma separation_assm_bin_fm_type[TC]: "A \ \ \ y \ \ \ f_fm \ formula \ separation_assm_bin_fm(A, y,f_fm) \ formula" unfolding separation_assm_bin_fm_def by simp lemma arity_separation_assm_bin_fm : "A \ \ \ x \ \ \ f_fm \ formula \ arity(separation_assm_bin_fm(A, x, f_fm)) = succ(A) \ succ(x) \ (pred^4(arity(f_fm)))" using pred_Un_distrib unfolding separation_assm_bin_fm_def by (auto simp add:arity) context M_Z_trans begin lemma separation_assm_sats : assumes f_fm: "\ \ formula" and f_ar: "arity(\) = 2" and fsats: "\env x y. env\list(M) \ x\M \ y\M \ (M,[x,y]@env \ \) \ is_f(x,y)" and fabs: "\x y. x\M \ y\M \ is_f(x,y) \ y = f(x)" and fclosed: "\x. x\M \ f(x) \ M" and "A\M" shows "separation(##M, \y. \x \ M . x\A \ y = \x, f(x)\)" proof - let ?\'="separation_assm_fm(1,0,\)" let ?p="\y. \x\M . x\A \ y = \x, f(x)\" from f_fm have "?\'\formula" by simp moreover from this f_ar f_fm have "arity(?\') = 2" using arity_separation_assm_fm[of 1 0 \] ord_simp_union by simp moreover from \A\M\ calculation have "separation(##M,\y . M,[y,A] \ ?\')" using separation_ax by auto moreover have "y\M \ (M,[y,A] \ ?\') \ ?p(y)" for y using assms transitivity[OF _ \A\M\] unfolding separation_assm_fm_def by auto ultimately show ?thesis by(rule_tac separation_cong[THEN iffD1],auto) qed lemma separation_assm_bin_sats : assumes f_fm: "\ \ formula" and f_ar: "arity(\) = 3" and fsats: "\env x z y. env\list(M) \ x\M \ z\M \ y\M \ (M,[x,z,y]@env \ \) \ is_f(x,z,y)" and fabs: "\x z y. x\M \ z\M \ y\M \ is_f(x,z,y) \ y = f(x,z)" and fclosed: "\x z . x\M \ z\M \ f(x,z) \ M" and "A\M" shows "separation(##M, \y. \x \ M . x\A \ y = \x, f(fst(x),snd(x))\)" proof - let ?\'="separation_assm_bin_fm(1,0,\)" let ?p="\y. \x\M . x\A \ y = \x, f(fst(x),snd(x))\" from f_fm have "?\'\formula" by simp moreover from this f_ar f_fm have "arity(?\') = 2" using arity_separation_assm_bin_fm[of 1 0 \] ord_simp_union by simp moreover from \A\M\ calculation have "separation(##M,\y . M,[y,A] \ ?\')" using separation_ax by auto moreover have "y\M \ (M,[y,A] \ ?\') \ ?p(y)" for y using assms transitivity[OF _ \A\M\] pair_in_M_iff fst_abs snd_abs fst_closed snd_closed unfolding separation_assm_bin_fm_def by auto ultimately show ?thesis by(rule_tac separation_cong[THEN iffD1],auto) qed lemma separation_Union: "A\M \ separation(##M, \y. \x \ M . x\A \ y = \x, Union(x)\)" using separation_assm_sats[of "big_union_fm(0,1)"] arity_big_union_fm ord_simp_union Union_closed[simplified] by simp lemma lam_replacement_Union: "lam_replacement(##M, Union)" using lam_replacement_Union' separation_Union transM by simp lemma separation_fst: "A\M \ separation(##M, \y. \x \ M . x\A \ y = \x, fst(x)\)" using separation_assm_sats[of "fst_fm(0,1)"] arity_fst_fm ord_simp_union fst_closed fst_abs by simp lemma lam_replacement_fst: "lam_replacement(##M, fst)" using lam_replacement_fst' separation_fst transM by simp lemma separation_snd: "A\M \ separation(##M, \y. \x \ M . x\A \ y = \x, snd(x)\)" using separation_assm_sats[of "snd_fm(0,1)"] arity_snd_fm ord_simp_union snd_closed[simplified] snd_abs by simp lemma lam_replacement_snd: "lam_replacement(##M, snd)" using lam_replacement_snd' separation_snd transM by simp text\Binary lambda-replacements\ lemma separation_Image: "A\M \ separation(##M, \y. \x\M. x \ A \ y = \x, fst(x) `` snd(x)\)" using arity_image_fm ord_simp_union nonempty image_closed image_abs by (rule_tac separation_assm_bin_sats[of "image_fm(0,1,2)"],auto) lemma lam_replacement_Image: "lam_replacement(##M, \x . fst(x) `` snd(x))" using lam_replacement_Image' separation_Image by simp lemma separation_middle_del: "A\M \ separation(##M, \y. \x\M. x \ A \ y = \x, middle_del(fst(x), snd(x))\)" using arity_is_middle_del_fm ord_simp_union nonempty fst_abs snd_abs fst_closed snd_closed pair_in_M_iff by (rule_tac separation_assm_bin_sats[of "is_middle_del_fm(0,1,2)"], auto simp:is_middle_del_def middle_del_def) lemma lam_replacement_middle_del: "lam_replacement(##M, \r . middle_del(fst(r),snd(r)))" using lam_replacement_middle_del' separation_middle_del by simp lemma separation_prodRepl: "A\M \ separation(##M, \y. \x\M. x \ A \ y = \x, prodRepl(fst(x), snd(x))\)" using arity_is_prodRepl_fm ord_simp_union nonempty fst_abs snd_abs fst_closed snd_closed pair_in_M_iff by (rule_tac separation_assm_bin_sats[of "is_prodRepl_fm(0,1,2)"], auto simp:is_prodRepl_def prodRepl_def) lemma lam_replacement_prodRepl: "lam_replacement(##M, \r . prodRepl(fst(r),snd(r)))" using lam_replacement_prodRepl' separation_prodRepl by simp end \ \\<^locale>\M_Z_trans\\ context M_trivial begin lemma first_closed: "M(B) \ M(r) \ first(u,r,B) \ M(u)" using transM[OF first_is_elem] by simp is_iff_rel for "first" unfolding is_first_def first_rel_def by auto is_iff_rel for "minimum" unfolding is_minimum_def minimum_rel_def using is_first_iff The_abs nonempty by force end \ \\<^locale>\M_trivial\\ context M_Z_trans begin lemma (in M_basic) is_minimum_equivalence : "M(R) \ M(X) \ M(u) \ is_minimum(M,R,X,u) \ is_minimum'(M,R,X,u)" unfolding is_minimum_def is_minimum'_def is_The_def is_first_def by simp lemma separation_minimum: "A\M \ separation(##M, \y. \x\M. x \ A \ y = \x, minimum(fst(x), snd(x))\)" using arity_minimum_fm ord_simp_union is_minimum_iff minimum_abs is_minimum_equivalence nonempty minimum_closed minimum_abs by (rule_tac separation_assm_bin_sats[of "minimum_fm(0,1,2)"], auto) lemma lam_replacement_minimum: "lam_replacement(##M, \x . minimum(fst(x),snd(x)))" using lam_replacement_minimum' separation_minimum by simp end \ \\<^locale>\M_Z_trans\\ end \ No newline at end of file diff --git a/thys/Independence_CH/Names.thy b/thys/Independence_CH/Names.thy --- a/thys/Independence_CH/Names.thy +++ b/thys/Independence_CH/Names.thy @@ -1,637 +1,641 @@ section\Names and generic extensions\ theory Names imports Forcing_Data FrecR_Arities ZF_Trans_Interpretations begin definition Hv :: "[i,i,i]\i" where "Hv(G,x,f) \ { z . y\ domain(x), (\p\G. \y,p\ \ x) \ z=f`y}" text\The funcion \<^term>\val\ interprets a name in \<^term>\M\ according to a (generic) filter \<^term>\G\. Note the definition in terms of the well-founded recursor.\ definition val :: "[i,i]\i" where "val(G,\) \ wfrec(edrel(eclose({\})), \ ,Hv(G))" definition GenExt :: "[i,i]\i" ("_[_]" [71,1]) where "M[G] \ {val(G,\). \ \ M}" lemma map_val_in_MG: assumes "env\list(M)" shows "map(val(G),env)\list(M[G])" unfolding GenExt_def using assms map_type2 by simp subsection\Values and check-names\ context forcing_data1 begin lemma name_components_in_M: assumes "\\,p\\\" "\ \ M" shows "\\M" "p\M" using assms transitivity pair_in_M_iff by auto definition Hcheck :: "[i,i] \ i" where "Hcheck(z,f) \ { \f`y,\\ . y \ z}" definition check :: "i \ i" where "check(x) \ transrec(x , Hcheck)" lemma checkD: "check(x) = wfrec(Memrel(eclose({x})), x, Hcheck)" unfolding check_def transrec_def .. lemma Hcheck_trancl:"Hcheck(y, restrict(f,Memrel(eclose({x}))-``{y})) = Hcheck(y, restrict(f,(Memrel(eclose({x}))^+)-``{y}))" unfolding Hcheck_def using restrict_trans_eq by simp lemma check_trancl: "check(x) = wfrec(rcheck(x), x, Hcheck)" using checkD wf_eq_trancl Hcheck_trancl unfolding rcheck_def by simp lemma rcheck_in_M : "x \ M \ rcheck(x) \ M" unfolding rcheck_def by (simp flip: setclass_iff) lemma rcheck_subset_M : "x \ M \ field(rcheck(x)) \ eclose({x})" unfolding rcheck_def using field_Memrel field_trancl by auto lemma aux_def_check: "x \ y \ wfrec(Memrel(eclose({y})), x, Hcheck) = wfrec(Memrel(eclose({x})), x, Hcheck)" by (rule wfrec_eclose_eq,auto simp add: arg_into_eclose eclose_sing) lemma def_check : "check(y) = { \check(w),\\ . w \ y}" proof - let ?r="\y. Memrel(eclose({y}))" have wfr: "\w . wf(?r(w))" using wf_Memrel .. then have "check(y)= Hcheck( y, \x\?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))" using wfrec[of "?r(y)" y "Hcheck"] checkD by simp also have " ... = Hcheck( y, \x\y. wfrec(?r(y), x, Hcheck))" using under_Memrel_eclose arg_into_eclose by simp also have " ... = Hcheck( y, \x\y. check(x))" using aux_def_check checkD by simp finally show ?thesis using Hcheck_def by simp qed lemma def_checkS : fixes n assumes "n \ nat" shows "check(succ(n)) = check(n) \ {\check(n),\\}" proof - have "check(succ(n)) = {\check(i),\\ . i \ succ(n)} " using def_check by blast also have "... = {\check(i),\\ . i \ n} \ {\check(n),\\}" by blast also have "... = check(n) \ {\check(n),\\}" using def_check[of n,symmetric] by simp finally show ?thesis . qed lemma field_Memrel2 : assumes "x \ M" shows "field(Memrel(eclose({x}))) \ M" proof - have "field(Memrel(eclose({x}))) \ eclose({x})" "eclose({x}) \ M" using Ordinal.Memrel_type field_rel_subset assms eclose_least[OF trans_M] by auto then show ?thesis using subset_trans by simp qed lemma aux_def_val: assumes "z \ domain(x)" shows "wfrec(edrel(eclose({x})),z,Hv(G)) = wfrec(edrel(eclose({z})),z,Hv(G))" proof - let ?r="\x . edrel(eclose({x}))" have "z\eclose({z})" using arg_in_eclose_sing . moreover have "relation(?r(x))" using relation_edrel . moreover have "wf(?r(x))" using wf_edrel . moreover from assms have "tr_down(?r(x),z) \ eclose({z})" using tr_edrel_subset by simp ultimately have "wfrec(?r(x),z,Hv(G)) = wfrec[eclose({z})](?r(x),z,Hv(G))" using wfrec_restr by simp also from \z\domain(x)\ have "... = wfrec(?r(z),z,Hv(G))" using restrict_edrel_eq wfrec_restr_eq by simp finally show ?thesis . qed text\The next lemma provides the usual recursive expresion for the definition of \<^term>\val\.\ lemma def_val: "val(G,x) = {z . t\domain(x) , (\p\G . \t,p\\x) \ z=val(G,t)}" proof - let ?r="\\ . edrel(eclose({\}))" let ?f="\z\?r(x)-``{x}. wfrec(?r(x),z,Hv(G))" have "\\. wf(?r(\))" using wf_edrel by simp with wfrec [of _ x] have "val(G,x) = Hv(G,x,?f)" using val_def by simp also have " ... = Hv(G,x,\z\domain(x). wfrec(?r(x),z,Hv(G)))" using dom_under_edrel_eclose by simp also have " ... = Hv(G,x,\z\domain(x). val(G,z))" using aux_def_val val_def by simp finally show ?thesis using Hv_def by simp qed lemma val_mono : "x\y \ val(G,x) \ val(G,y)" by (subst (1 2) def_val, force) text\Check-names are the canonical names for elements of the ground model. Here we show that this is the case.\ lemma val_check : "\ \ G \ \ \ \ \ val(G,check(y)) = y" proof (induct rule:eps_induct) case (1 y) then show ?case proof - have "check(y) = { \check(w), \\ . w \ y}" (is "_ = ?C") using def_check . then have "val(G,check(y)) = val(G, {\check(w), \\ . w \ y})" by simp also have " ... = {z . t\domain(?C) , (\p\G . \t, p\\?C ) \ z=val(G,t) }" using def_val by blast also have " ... = {z . t\domain(?C) , (\w\y. t=check(w)) \ z=val(G,t) }" using 1 by simp also have " ... = {val(G,check(w)) . w\y }" by force finally show "val(G,check(y)) = y" using 1 by simp qed qed lemma val_of_name : "val(G,{x\A\\. Q(x)}) = {z . t\A , (\p\\ . Q(\t,p\) \ p \ G) \ z=val(G,t)}" proof - let ?n="{x\A\\. Q(x)}" and ?r="\\ . edrel(eclose({\}))" let ?f="\z\?r(?n)-``{?n}. val(G,z)" have wfR : "wf(?r(\))" for \ by (simp add: wf_edrel) have "domain(?n) \ A" by auto { fix t assume H:"t \ domain({x \ A \ \ . Q(x)})" then have "?f ` t = (if t \ ?r(?n)-``{?n} then val(G,t) else 0)" by simp moreover have "... = val(G,t)" using dom_under_edrel_eclose H if_P by auto } then have Eq1: "t \ domain({x \ A \ \ . Q(x)}) \ val(G,t) = ?f` t" for t by simp have "val(G,?n) = {z . t\domain(?n), (\p \ G . \t,p\ \ ?n) \ z=val(G,t)}" by (subst def_val,simp) also have "... = {z . t\domain(?n), (\p\\ . \t,p\\?n \ p\G) \ z=?f`t}" unfolding Hv_def by (auto simp add:Eq1) also have "... = {z . t\domain(?n), (\p\\ . \t,p\\?n \ p\G) \ z=(if t\?r(?n)-``{?n} then val(G,t) else 0)}" by (simp) also have "... = { z . t\domain(?n), (\p\\ . \t,p\\?n \ p\G) \ z=val(G,t)}" proof - have "domain(?n) \ ?r(?n)-``{?n}" using dom_under_edrel_eclose by simp then have "\t\domain(?n). (if t\?r(?n)-``{?n} then val(G,t) else 0) = val(G,t)" by auto then show "{ z . t\domain(?n), (\p\\ . \t,p\\?n \ p\G) \ z=(if t\?r(?n)-``{?n} then val(G,t) else 0)} = { z . t\domain(?n), (\p\\ . \t,p\\?n \ p\G) \ z=val(G,t)}" by auto qed also have " ... = { z . t\A, (\p\\ . \t,p\\?n \ p\G) \ z=val(G,t)}" by force finally show " val(G,?n) = { z . t\A, (\p\\ . Q(\t,p\) \ p\G) \ z=val(G,t)}" by auto qed lemma val_of_name_alt : "val(G,{x\A\\. Q(x)}) = {z . t\A , (\p\\\G . Q(\t,p\)) \ z=val(G,t) }" using val_of_name by force lemma val_only_names: "val(F,\) = val(F,{x\\. \t\domain(\). \p\F. x=\t,p\})" (is "_ = val(F,?name)") proof - have "val(F,?name) = {z . t\domain(?name), (\p\F. \t, p\ \ ?name) \ z=val(F, t)}" using def_val by blast also have " ... = {val(F, t). t\{y\domain(\). \p\F. \y, p\ \ \ }}" by blast also have " ... = {z . t\domain(\), (\p\F. \t, p\ \ \) \ z=val(F, t)}" by blast also have " ... = val(F, \)" using def_val[symmetric] by blast finally show ?thesis .. qed lemma val_only_pairs: "val(F,\) = val(F,{x\\. \t p. x=\t,p\})" proof have "val(F,\) = val(F,{x\\. \t\domain(\). \p\F. x=\t,p\})" (is "_ = val(F,?name)") using val_only_names . also have "... \ val(F,{x\\. \t p. x=\t,p\})" using val_mono[of ?name "{x\\. \t p. x=\t,p\}"] by auto finally show "val(F,\) \ val(F,{x\\. \t p. x=\t,p\})" by simp next show "val(F,{x\\. \t p. x=\t,p\}) \ val(F,\)" using val_mono[of "{x\\. \t p. x=\t,p\}"] by auto qed lemma val_subset_domain_times_range: "val(F,\) \ val(F,domain(\)\range(\))" using val_only_pairs[THEN equalityD1] val_mono[of "{x \ \ . \t p. x = \t, p\}" "domain(\)\range(\)"] by blast lemma val_of_elem: "\\,p\ \ \ \ p\G \ val(G,\) \ val(G,\)" proof - assume "\\,p\ \ \" then have "\\domain(\)" by auto assume "p\G" with \\\domain(\)\ \\\,p\ \ \\ have "val(G,\) \ {z . t\domain(\) , (\p\G . \t, p\\\) \ z=val(G,t) }" by auto then show ?thesis by (subst def_val) qed lemma elem_of_val: "x\val(G,\) \ \\\domain(\). val(G,\) = x" by (subst (asm) def_val,auto) lemma elem_of_val_pair: "x\val(G,\) \ \\. \p\G. \\,p\\\ \ val(G,\) = x" by (subst (asm) def_val,auto) lemma elem_of_val_pair': assumes "\\M" "x\val(G,\)" shows "\\\M. \p\G. \\,p\\\ \ val(G,\) = x" proof - from assms obtain \ p where "p\G" "\\,p\\\" "val(G,\) = x" using elem_of_val_pair by blast moreover from this \\\M\ have "\\M" using pair_in_M_iff[THEN iffD1, THEN conjunct1, simplified] transitivity by blast ultimately show ?thesis by blast qed lemma GenExtD: "x \ M[G] \ \\\M. x = val(G,\)" by (simp add:GenExt_def) lemma GenExtI: "x \ M \ val(G,x) \ M[G]" by (auto simp add: GenExt_def) lemma Transset_MG : "Transset(M[G])" proof - { fix vc y assume "vc \ M[G]" and "y \ vc" then obtain c where "c\M" "val(G,c)\M[G]" "y \ val(G,c)" using GenExtD by auto from \y \ val(G,c)\ obtain \ where "\\domain(c)" "val(G,\) = y" using elem_of_val by blast with trans_M \c\M\ have "y \ M[G]" using domain_trans GenExtI by blast } then show ?thesis using Transset_def by auto qed lemmas transitivity_MG = Transset_intf[OF Transset_MG] text\This lemma can be proved before having \<^term>\check_in_M\. At some point Miguel naïvely thought that the \<^term>\check_in_M\ could be proved using this argument.\ lemma check_nat_M : assumes "n \ nat" shows "check(n) \ M" using assms proof (induct n) case 0 then show ?case using zero_in_M by (subst def_check,simp) next case (succ x) have "\ \ M" using one_in_P P_sub_M subsetD by simp with \check(x)\M\ have "\check(x),\\ \ M" using pair_in_M_iff by simp then have "{\check(x),\\} \ M" using singleton_closed by simp with \check(x)\M\ have "check(x) \ {\check(x),\\} \ M" using Un_closed by simp then show ?case using \x\nat\ def_checkS by simp qed lemma def_PHcheck: assumes "z\M" "f\M" shows "Hcheck(z,f) = Replace(z,PHcheck(##M,\,f))" proof - from assms have "\f`x,\\ \ M" "f`x\M" if "x\z" for x using pair_in_M_iff transitivity that apply_closed by simp_all then have "{y . x \ z, y = \f ` x, \\} = {y . x \ z, y = \f ` x, \\ \ y\M \ f`x\M}" by simp then show ?thesis using \z\M\ \f\M\ transitivity unfolding Hcheck_def PHcheck_def RepFun_def by auto qed (* instance of replacement for hcheck *) lemma wfrec_Hcheck : assumes "X\M" shows "wfrec_replacement(##M,is_Hcheck(##M,\),rcheck(X))" proof - let ?f="Exists(And(pair_fm(1,0,2), is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0)))" have "is_Hcheck(##M,\,a,b,c) \ sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,\,rcheck(x)])" if "a\M" "b\M" "c\M" "d\M" "e\M" "y\M" "x\M" "z\M" for a b c d e y x z using that \X\M\ rcheck_in_M is_Hcheck_iff_sats zero_in_M by simp then have "sats(M,is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0), [y,x,z,\,rcheck(X)]) \ is_wfrec(##M, is_Hcheck(##M,\),rcheck(X), x, y)" if "x\M" "y\M" "z\M" for x y z using that sats_is_wfrec_fm \X\M\ rcheck_in_M zero_in_M by simp moreover from this have satsf:"sats(M, ?f, [x,z,\,rcheck(X)]) \ (\y\M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,\),rcheck(X), x, y))" if "x\M" "z\M" for x z using that \X\M\ rcheck_in_M by (simp del:pair_abs) moreover have artyf:"arity(?f) = 4" using arity_wfrec_replacement_fm[where p="is_Hcheck_fm(8, 2, 1, 0)" and i=9] arity_is_Hcheck_fm ord_simp_union by simp ultimately have "strong_replacement(##M,\x z. sats(M,?f,[x,z,\,rcheck(X)]))" using ZF_ground_replacements(2) artyf \X\M\ rcheck_in_M unfolding replacement_assm_def wfrec_Hcheck_fm_def by simp then have "strong_replacement(##M,\x z. \y\M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,\),rcheck(X), x, y))" using repl_sats[of M ?f "[\,rcheck(X)]"] satsf by (simp del:pair_abs) then show ?thesis unfolding wfrec_replacement_def by simp qed lemma Hcheck_closed' : "f\M \ z\M \ {f ` x . x \ z} \ M" using RepFun_closed[OF lam_replacement_imp_strong_replacement] lam_replacement_apply apply_closed transM[of _ z] by simp lemma repl_PHcheck : assumes "f\M" shows "lam_replacement(##M,\x. Hcheck(x,f))" proof - have "Hcheck(x,f) = {f`y . y\x}\{\}" for x unfolding Hcheck_def by auto moreover note assms moreover from this have 1:"lam_replacement(##M, \x . {f`y . y\x}\{\})" using lam_replacement_RepFun_apply lam_replacement_constant lam_replacement_fst lam_replacement_snd singleton_closed cartprod_closed fst_snd_closed Hcheck_closed' by (rule_tac lam_replacement_CartProd[THEN [5] lam_replacement_hcomp2],simp_all) ultimately show ?thesis using singleton_closed cartprod_closed Hcheck_closed' by(rule_tac lam_replacement_cong[OF 1],auto) qed lemma univ_PHcheck : "\ z\M ; f\M \ \ univalent(##M,z,PHcheck(##M,\,f))" unfolding univalent_def PHcheck_def by simp lemma PHcheck_closed : "\z\M ; f\M ; x\z; PHcheck(##M,\,f,x,y) \ \ (##M)(y)" unfolding PHcheck_def by simp lemma relation2_Hcheck : "relation2(##M,is_Hcheck(##M,\),Hcheck)" proof - have "is_Replace(##M,z,PHcheck(##M,\,f),hc) \ hc = Replace(z,PHcheck(##M,\,f))" if "z\M" "f\M" "hc\M" for z f hc using that Replace_abs[OF _ _ univ_PHcheck] PHcheck_closed[of z f] by simp with def_PHcheck show ?thesis unfolding relation2_def is_Hcheck_def Hcheck_def by simp qed lemma Hcheck_closed : "\y\M. \g\M. Hcheck(y,g)\M" proof - have eq:"Hcheck(x,f) = {f`y . y\x}\{\}" for f x unfolding Hcheck_def by auto then have "Hcheck(y,g)\M" if "y\M" "g\M" for y g using eq that Hcheck_closed' cartprod_closed singleton_closed by simp then show ?thesis by auto qed lemma wf_rcheck : "x\M \ wf(rcheck(x))" unfolding rcheck_def using wf_trancl[OF wf_Memrel] . lemma trans_rcheck : "x\M \ trans(rcheck(x))" unfolding rcheck_def using trans_trancl . lemma relation_rcheck : "x\M \ relation(rcheck(x))" unfolding rcheck_def using relation_trancl . lemma check_in_M : "x\M \ check(x) \ M" using wfrec_Hcheck[of x] check_trancl wf_rcheck trans_rcheck relation_rcheck rcheck_in_M Hcheck_closed relation2_Hcheck trans_wfrec_closed[of "rcheck(x)"] by simp (* Internalization and absoluteness of rcheck\ *) lemma rcheck_abs[Rel] : "\ x\M ; r\M \ \ is_rcheck(##M,x,r) \ r = rcheck(x)" unfolding rcheck_def is_rcheck_def using singleton_closed trancl_closed Memrel_closed eclose_closed zero_in_M by simp lemma check_abs[Rel] : assumes "x\M" "z\M" shows "is_check(##M,\,x,z) \ z = check(x)" proof - have "is_check(##M,\,x,z) \ is_wfrec(##M,is_Hcheck(##M,\),rcheck(x),x,z)" unfolding is_check_def using assms rcheck_abs rcheck_in_M zero_in_M unfolding check_trancl is_check_def by simp then show ?thesis unfolding check_trancl using assms wfrec_Hcheck[of x] wf_rcheck trans_rcheck relation_rcheck rcheck_in_M Hcheck_closed relation2_Hcheck trans_wfrec_abs[of "rcheck(x)" x z "is_Hcheck(##M,\)" Hcheck] by (simp flip: setclass_iff) qed lemma check_lam_replacement: "lam_replacement(##M,check)" proof - have "arity(check_fm(2,0,1)) = 3" by (simp add:ord_simp_union arity) then have "Lambda(A, check) \ M" if "A\M" for A using that check_in_M transitivity[of _ A] sats_check_fm check_abs zero_in_M check_fm_type ZF_ground_replacements(3) by(rule_tac Lambda_in_M [of "check_fm(2,0,1)" "[\]"],simp_all) then show ?thesis using check_in_M lam_replacement_iff_lam_closed[THEN iffD2] by simp qed lemma check_replacement: "{check(x). x\\} \ M" using lam_replacement_imp_strong_replacement_aux[OF check_lam_replacement] transitivity check_in_M RepFun_closed by simp_all lemma M_subset_MG : "\ \ G \ M \ M[G]" using check_in_M GenExtI by (intro subsetI, subst val_check [of G,symmetric], auto) text\The name for the generic filter\ definition G_dot :: "i" where "G_dot \ {\check(p),p\ . p\\}" lemma G_dot_in_M : "G_dot \ M" using lam_replacement_Pair[THEN [5] lam_replacement_hcomp2,OF check_lam_replacement lam_replacement_identity] check_in_M lam_replacement_imp_strong_replacement_aux transitivity check_in_M RepFun_closed pair_in_M_iff unfolding G_dot_def by simp lemma zero_in_MG : "0 \ M[G]" proof - have "0 = val(G,0)" using zero_in_M elem_of_val by auto also have "... \ M[G]" using GenExtI zero_in_M by simp finally show ?thesis . qed declare check_in_M [simp,intro] end \ \\<^locale>\forcing_data1\\ context G_generic1 begin lemma val_G_dot : "val(G,G_dot) = G" proof (intro equalityI subsetI) fix x assume "x\val(G,G_dot)" then obtain \ p where "p\G" "\\,p\ \ G_dot" "val(G,\) = x" "\ = check(p)" unfolding G_dot_def using elem_of_val_pair G_dot_in_M by force then show "x \ G" using G_subset_P one_in_G val_check P_sub_M by auto next fix p assume "p\G" have "\check(q),q\ \ G_dot" if "q\\" for q unfolding G_dot_def using that by simp with \p\G\ have "val(G,check(p)) \ val(G,G_dot)" using val_of_elem G_dot_in_M by blast with \p\G\ show "p \ val(G,G_dot)" using one_in_G G_subset_P P_sub_M val_check by auto qed lemma G_in_Gen_Ext : "G \ M[G]" using G_subset_P one_in_G val_G_dot GenExtI[of _ G] G_dot_in_M by force lemmas generic_simps = val_check[OF one_in_G one_in_P] M_subset_MG[OF one_in_G, THEN subsetD] GenExtI P_in_M lemmas generic_dests = M_genericD M_generic_compatD bundle G_generic1_lemmas = generic_simps[simp] generic_dests[dest] end \ \\<^locale>\G_generic1\\ +sublocale G_generic1 \ ext: M_trans "##M[G]" + using generic transitivity_MG zero_in_MG + by unfold_locales force+ + end \ No newline at end of file diff --git a/thys/Independence_CH/Powerset_Axiom.thy b/thys/Independence_CH/Powerset_Axiom.thy --- a/thys/Independence_CH/Powerset_Axiom.thy +++ b/thys/Independence_CH/Powerset_Axiom.thy @@ -1,266 +1,231 @@ section\The Powerset Axiom in $M[G]$\ + theory Powerset_Axiom - imports Separation_Axiom Pairing_Axiom Union_Axiom + imports + Separation_Axiom Pairing_Axiom Union_Axiom begin simple_rename "perm_pow" src "[ss,p,l,o,fs,\]" tgt "[fs,ss,sp,p,l,o,\]" -lemma Collect_inter_Transset: - assumes - "Transset(M)" "b \ M" - shows - "{x\b . P(x)} = {x\b . P(x)} \ M" - using assms unfolding Transset_def - by (auto) - context G_generic1 begin lemma sats_fst_snd_in_M: assumes "A\M" "B\M" "\ \ formula" "p\M" "l\M" "o\M" "\\M" "arity(\) \ 6" shows "{\s,q\\A\B . M, [q,p,l,o,s,\] \ \} \ M" (is "?\ \ M") proof - let ?\' = "ren(\)`6`7`perm_pow_fn" from \A\M\ \B\M\ have "A\B \ M" using cartprod_closed by simp from \arity(\) \ 6\ \\\ formula\ have "?\' \ formula" "arity(?\')\7" unfolding perm_pow_fn_def using perm_pow_thm arity_ren ren_tc Nil_type by auto with \?\' \ formula\ have arty: "arity(Exists(Exists(And(pair_fm(0,1,2),?\'))))\5" (is "arity(?\)\5") using ord_simp_union pred_le by (auto simp:arity) { fix sp note \A\B \ M\ \A\M\ \B\M\ moreover assume "sp \ A\B" moreover from calculation have "fst(sp) \ A" "snd(sp) \ B" using fst_type snd_type by simp_all ultimately have "sp \ M" "fst(sp) \ M" "snd(sp) \ M" using transitivity by simp_all note inM = \A\M\ \B\M\ \p\M\ \l\M\ \o\M\ \\\M\ \sp\M\ \fst(sp)\M\ \snd(sp)\M\ with arty \sp \ M\ \?\' \ formula\ have "(M, [sp,p,l,o,\]@[p] \ ?\) \ M,[sp,p,l,o,\] \ ?\" (is "(M,?env0@ _\_) \ _") using arity_sats_iff[of ?\ "[p]" M ?env0] by auto also from inM \sp \ A\B\ have "... \ sats(M,?\',[fst(sp),snd(sp),sp,p,l,o,\])" by auto also from inM \\ \ formula\ \arity(\) \ 6\ have "... \ M, [snd(sp),p,l,o,fst(sp),\] \ \" (is "sats(_,_,?env1) \ sats(_,_,?env2)") using sats_iff_sats_ren[of \ 6 7 ?env2 M ?env1 perm_pow_fn] perm_pow_thm unfolding perm_pow_fn_def by simp finally have "(M,[sp,p,l,o,\,p] \ ?\) \ M, [snd(sp),p,l,o,fst(sp),\] \ \" by simp } then have "?\ = {sp\A\B . sats(M,?\,[sp,p,l,o,\,p])}" by auto with assms \A\B\M\ show ?thesis using separation_ax separation_iff arty leI \?\' \ formula\ by simp qed declare nat_into_M[rule del, simplified setclass_iff, intro] -lemmas ssimps = domain_closed cartprod_closed cons_closed +lemmas ssimps = domain_closed cartprod_closed cons_closed Pow_rel_closed declare ssimps [simp del, simplified setclass_iff, simp, intro] +\ \We keep \<^term>\Pow(a) \ M[G]\ to be consistent with Kunen.\ lemma Pow_inter_MG: assumes "a\M[G]" shows "Pow(a) \ M[G] \ M[G]" proof - from assms obtain \ where "\ \ M" "val(G, \) = a" using GenExtD by auto - let ?Q="Pow(domain(\)\\) \ M" + let ?Q="Pow\<^bsup>M\<^esup>(domain(\)\\)" + let ?\="?Q\{\}" + let ?b="val(G,?\)" from \\\M\ have "domain(\)\\ \ M" "domain(\) \ M" by simp_all then - have "?Q \ M" - proof - - from power_ax \domain(\)\\ \ M\ - obtain Q where "powerset(##M,domain(\)\\,Q)" "Q \ M" - unfolding power_ax_def by auto - moreover from calculation - have "z\Q \ z\M" for z - using transitivity by blast - ultimately - have "Q = {a\Pow(domain(\)\\) . a\M}" - using \domain(\)\\ \ M\ powerset_abs[of "domain(\)\\" Q] - by (simp flip: setclass_iff) - also - have " ... = ?Q" - by auto - finally - show ?thesis - using \Q\M\ by simp - qed - let ?\="?Q\{\}" - let ?b="val(G,?\)" - from \?Q\M\ - have "?\\M" - by auto - then have "?b \ M[G]" - using GenExtI by simp + by (auto intro!:GenExtI) have "Pow(a) \ M[G] \ ?b" proof fix c assume "c \ Pow(a) \ M[G]" then obtain \ where "c\M[G]" "\ \ M" "val(G,\) = c" using GenExt_iff by auto let ?\="{\\,p\ \domain(\)\\ . p \ \0 \ 1\ [\,\] }" - have "arity(forces(Member(0,1))) = 6" + have "arity(forces( \0 \ 1\ )) = 6" using arity_forces_at by auto with \domain(\) \ M\ \\ \ M\ have "?\ \ M" using sats_fst_snd_in_M by simp - then - have "?\ \ ?Q" by auto - then - have "val(G,?\) \ ?b" - using one_in_G generic val_of_elem [of ?\ \ ?\ G] - by auto + with \domain(\)\\ \ M\ + have "?\ \ ?Q" + using Pow_rel_char by auto have "val(G,?\) = c" proof(intro equalityI subsetI) fix x assume "x \ val(G,?\)" then obtain \ p where 1: "\\,p\\?\" "p\G" "val(G,\) = x" using elem_of_val_pair by blast moreover from \\\,p\\?\\ \?\ \ M\ have "\\M" using name_components_in_M[of _ _ ?\] by auto moreover from 1 have "p \ \0 \ 1\ [\,\]" "p\\" by simp_all moreover note \val(G,\) = c\ \\ \ M\ ultimately have "M[G], [x, c] \ \0 \ 1\" using generic definition_of_forcing[where \="\0 \ 1\"] ord_simp_union by auto moreover from \\\M\ \\\M\ have "x\M[G]" using \val(G,\) = x\ GenExtI by blast ultimately show "x\c" using \c\M[G]\ by simp next fix x assume "x \ c" with \c \ Pow(a) \ M[G]\ have "x \ a" "c\M[G]" "x\M[G]" using transitivity_MG by auto with \val(G, \) = a\ obtain \ where "\\domain(\)" "val(G,\) = x" using elem_of_val by blast moreover note \x\c\ \val(G,\) = c\ \c\M[G]\ \x\M[G]\ moreover from calculation have "val(G,\) \ val(G,\)" by simp moreover from calculation have "M[G], [x, c] \ \0 \ 1\" by simp moreover have "\\M" proof - from \\\domain(\)\ obtain p where "\\,p\ \ \" by auto with \\\M\ show ?thesis using name_components_in_M by blast qed moreover note \\ \ M\ ultimately obtain p where "p\G" "p \ \0 \ 1\ [\,\]" using generic truth_lemma[of "\0 \ 1\" "[\,\]" ] ord_simp_union by auto moreover from \p\G\ have "p\\" using generic by blast ultimately have "\\,p\\?\" using \\\domain(\)\ by simp with \val(G,\) = x\ \p\G\ show "x\val(G,?\)" using val_of_elem [of _ _ "?\" G] by auto qed - with \val(G,?\) \ ?b\ + with \?\ \ ?Q\ show "c\?b" - by simp + using one_in_G generic val_of_elem [of ?\ \ ?\ G] + by auto qed then have "Pow(a) \ M[G] = {x\?b . x\a \ x\M[G]}" by auto also from \a\M[G]\ - have " ... = {x\?b . ( M[G], [x,a] \ \0 \ 1\ ) \ x\M[G]}" + have " ... = {x\?b . ( M[G], [x,a] \ \0 \ 1\ )} \ M[G]" using Transset_MG by force - also - have " ... = {x\?b . ( M[G], [x,a] \ \0 \ 1\ )} \ M[G]" - by auto also from \?b\M[G]\ have " ... = {x\?b . ( M[G], [x,a] \ \0 \ 1\ )}" - using Collect_inter_Transset Transset_MG - by simp + by (intro equalityI) (auto dest:ext.transM) also from \?b\M[G]\ \a\M[G]\ have " ... \ M[G]" using Collect_sats_in_MG GenExtI ord_simp_union by (simp add:arity) finally show ?thesis . qed end \ \\<^locale>\G_generic1\\ sublocale G_generic1 \ ext: M_trivial "##M[G]" - using generic Union_MG pairing_in_MG zero_in_MG transitivity_MG - unfolding M_trivial_def M_trans_def M_trivial_axioms_def - by (simp; blast) + using generic Union_MG pairing_in_MG + by unfold_locales (simp; blast) context G_generic1 begin theorem power_in_MG : "power_ax(##(M[G]))" unfolding power_ax_def proof (intro rallI, simp only:setclass_iff rex_setclass_is_bex) fix a text\After simplification, we have to show that for every \<^term>\a\M[G]\ there exists some \<^term>\x\M[G]\ satisfying \<^term>\powerset(##M[G],a,x)\\ assume "a \ M[G]" have "{x\Pow(a) . x \ M[G]} = Pow(a) \ M[G]" by auto also from \a\M[G]\ have " ... \ M[G]" using Pow_inter_MG by simp finally have "{x\Pow(a) . x \ M[G]} \ M[G]" . moreover from \a\M[G]\ this have "powerset(##M[G], a, {x\Pow(a) . x \ M[G]})" using ext.powerset_abs by simp ultimately show "\x\M[G] . powerset(##M[G], a, x)" by auto qed end \ \\<^locale>\G_generic1\\ end \ No newline at end of file diff --git a/thys/Independence_CH/Replacement_Instances.thy b/thys/Independence_CH/Replacement_Instances.thy --- a/thys/Independence_CH/Replacement_Instances.thy +++ b/thys/Independence_CH/Replacement_Instances.thy @@ -1,1301 +1,1302 @@ section\More Instances of Replacement\ theory Replacement_Instances imports Separation_Instances Transitive_Models.Pointed_DC_Relative begin lemma composition_fm_type[TC]: "a0 \ \ \ a1 \ \ \ a2 \ \ \ composition_fm(a0,a1,a2) \ formula" unfolding composition_fm_def by simp arity_theorem for "composition_fm" definition is_omega_funspace :: "[i\o,i,i,i]\o" where "is_omega_funspace(N,B,n,z) \ \o[N]. omega(N,o) \ n\o \ is_funspace(N, n, B, z)" synthesize "omega_funspace" from_definition "is_omega_funspace" assuming "nonempty" arity_theorem for "omega_funspace_fm" definition HAleph_wfrec_repl_body where "HAleph_wfrec_repl_body(N,mesa,x,z) \ \y[N]. pair(N, x, y, z) \ (\g[N]. (\u[N]. u \ g \ (\a[N]. \y[N]. \ax[N]. \sx[N]. \r_sx[N]. \f_r_sx[N]. pair(N, a, y, u) \ pair(N, a, x, ax) \ upair(N, a, a, sx) \ pre_image(N, mesa, sx, r_sx) \ restriction(N, g, r_sx, f_r_sx) \ ax \ mesa \ is_HAleph(N, a, f_r_sx, y))) \ is_HAleph(N, x, g, y))" (* MOVE THIS to an appropriate place *) arity_theorem for "ordinal_fm" arity_theorem for "is_Limit_fm" arity_theorem for "empty_fm" arity_theorem for "fun_apply_fm" synthesize "HAleph_wfrec_repl_body" from_definition assuming "nonempty" arity_theorem for "HAleph_wfrec_repl_body_fm" definition dcwit_repl_body where "dcwit_repl_body(N,mesa,A,a,s,R) \ \x z. \y[N]. pair(N, x, y, z) \ is_wfrec (N, \n f. is_nat_case (N, a, \m bmfm. \fm[N]. \cp[N]. is_apply(N, f, m, fm) \ is_Collect(N, A, \x. \fmx[N]. (N(x) \ fmx \ R) \ pair(N, fm, x, fmx), cp) \ is_apply(N, s, cp, bmfm), n), mesa, x, y)" manual_schematic for "dcwit_repl_body" assuming "nonempty" unfolding dcwit_repl_body_def by (rule iff_sats is_nat_case_iff_sats is_eclose_iff_sats sep_rules | simp)+ synthesize "dcwit_repl_body" from_schematic definition dcwit_aux_fm where "dcwit_aux_fm(A,s,R) \ (\\\\4`2 is 0\ \ (\\\Collect_fm (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(A)))))))))), (\\\\0 \ succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(R)))))))))))) \ \ pair_fm(3, 1, 0) \\), 0) \ \ succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(s))))))))))`0 is 2\\\)\\)" arity_theorem for "dcwit_aux_fm" lemma dcwit_aux_fm_type[TC]: "A \ \ \ s \ \ \ R \ \ \ dcwit_aux_fm(A,s,R) \ formula" by (simp_all add: dcwit_aux_fm_def) definition is_nat_case_dcwit_aux_fm where "is_nat_case_dcwit_aux_fm(A,a,s,R) \ is_nat_case_fm (succ(succ(succ(succ(succ(succ(a)))))),dcwit_aux_fm(A,s,R), 2, 0)" lemma is_nat_case_dcwit_aux_fm_type[TC]: "A \ \ \ a \ \ \ s \ \ \ R \ \ \ is_nat_case_dcwit_aux_fm(A,a,s,R) \ formula" by (simp_all add: is_nat_case_dcwit_aux_fm_def) manual_arity for "is_nat_case_dcwit_aux_fm" unfolding is_nat_case_dcwit_aux_fm_def by (rule arity_dcwit_aux_fm[THEN [6] arity_is_nat_case_fm]) simp_all manual_arity for "dcwit_repl_body_fm" using arity_is_nat_case_dcwit_aux_fm[THEN [6] arity_is_wfrec_fm] unfolding dcwit_repl_body_fm_def is_nat_case_dcwit_aux_fm_def dcwit_aux_fm_def by (auto simp add: arity(1-33)) lemma arity_dcwit_repl_body: "arity(dcwit_repl_body_fm(6,5,4,3,2,0,1)) = 7" by (simp_all add: FOL_arities arity_dcwit_repl_body_fm ord_simp_union) definition fst2_snd2 where "fst2_snd2(x) \ \fst(fst(x)), snd(snd(x))\" relativize functional "fst2_snd2" "fst2_snd2_rel" relationalize "fst2_snd2_rel" "is_fst2_snd2" lemma (in M_trivial) fst2_snd2_abs: assumes "M(x)" "M(res)" shows "is_fst2_snd2(M, x, res) \ res = fst2_snd2(x)" unfolding is_fst2_snd2_def fst2_snd2_def using fst_rel_abs snd_rel_abs fst_abs snd_abs assms by simp synthesize "is_fst2_snd2" from_definition assuming "nonempty" arity_theorem for "is_fst2_snd2_fm" definition sndfst_fst2_snd2 where "sndfst_fst2_snd2(x) \ \snd(fst(x)), fst(fst(x)), snd(snd(x))\" relativize functional "sndfst_fst2_snd2" "sndfst_fst2_snd2_rel" relationalize "sndfst_fst2_snd2_rel" "is_sndfst_fst2_snd2" synthesize "is_sndfst_fst2_snd2" from_definition assuming "nonempty" arity_theorem for "is_sndfst_fst2_snd2_fm" definition order_eq_map where "order_eq_map(M,A,r,a,z) \ \x[M]. \g[M]. \mx[M]. \par[M]. ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)" synthesize "order_eq_map" from_definition assuming "nonempty" arity_theorem for "is_ord_iso_fm" arity_theorem for "order_eq_map_fm" (* Banach *) synthesize "is_banach_functor" from_definition assuming "nonempty" arity_theorem for "is_banach_functor_fm" definition banach_body_iterates where "banach_body_iterates(M,X,Y,f,g,W,n,x,z) \ \y[M]. pair(M, x, y, z) \ (\fa[M]. (\z[M]. z \ fa \ (\xa[M]. \y[M]. \xaa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. \sn[M]. \msn[M]. successor(M,n,sn) \ membership(M,sn,msn) \ pair(M, xa, y, z) \ pair(M, xa, x, xaa) \ upair(M, xa, xa, sx) \ pre_image(M, msn, sx, r_sx) \ restriction(M, fa, r_sx, f_r_sx) \ xaa \ msn \ (empty(M, xa) \ y = W) \ (\m[M]. successor(M, m, xa) \ (\gm[M]. is_apply(M, f_r_sx, m, gm) \ is_banach_functor(M, X, Y, f, g, gm, y))) \ (is_quasinat(M, xa) \ empty(M, y)))) \ (empty(M, x) \ y = W) \ (\m[M]. successor(M, m, x) \ (\gm[M]. is_apply(M, fa, m, gm) \ is_banach_functor(M, X, Y, f, g, gm, y))) \ (is_quasinat(M, x) \ empty(M, y)))" synthesize "is_quasinat" from_definition assuming "nonempty" arity_theorem for "is_quasinat_fm" synthesize "banach_body_iterates" from_definition assuming "nonempty" arity_theorem for "banach_body_iterates_fm" definition banach_is_iterates_body where "banach_is_iterates_body(M,X,Y,f,g,W,n,y) \ \om[M]. omega(M,om) \ n \ om \ (\sn[M]. \msn[M]. successor(M, n, sn) \ membership(M, sn, msn) \ (\fa[M]. (\z[M]. z \ fa \ (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M, x, y, z) \ pair(M, x, n, xa) \ upair(M, x, x, sx) \ pre_image(M, msn, sx, r_sx) \ restriction(M, fa, r_sx, f_r_sx) \ xa \ msn \ (empty(M, x) \ y = W) \ (\m[M]. successor(M, m, x) \ (\gm[M]. fun_apply(M, f_r_sx, m, gm) \ is_banach_functor(M, X, Y, f, g, gm, y))) \ (is_quasinat(M, x) \ empty(M, y)))) \ (empty(M, n) \ y = W) \ (\m[M]. successor(M, m, n) \ (\gm[M]. fun_apply(M, fa, m, gm) \ is_banach_functor(M, X, Y, f, g, gm, y))) \ (is_quasinat(M, n) \ empty(M, y))))" synthesize "banach_is_iterates_body" from_definition assuming "nonempty" arity_theorem for "banach_is_iterates_body_fm" (* (##M)(f) \ strong_replacement(##M, \x y. y = \x, transrec(x, \a g. f ` (g `` a))\) *) definition trans_apply_image where "trans_apply_image(f) \ \a g. f ` (g `` a)" relativize functional "trans_apply_image" "trans_apply_image_rel" relationalize "trans_apply_image" "is_trans_apply_image" (* MOVE THIS to an appropriate place *) schematic_goal arity_is_recfun_fm[arity]: "p \ formula \ a \ \ \ z \ \ \ r \ \ \ arity(is_recfun_fm(p, a, z ,r)) = ?ar" unfolding is_recfun_fm_def by (simp add:arity) (* clean simpset from arities, use correct attrib *) (* Don't know why it doesn't use the theorem at \<^file>\Arities\ *) schematic_goal arity_is_wfrec_fm[arity]: "p \ formula \ a \ \ \ z \ \ \ r \ \ \ arity(is_wfrec_fm(p, a, z ,r)) = ?ar" unfolding is_wfrec_fm_def by (simp add:arity) schematic_goal arity_is_transrec_fm[arity]: "p \ formula \ a \ \ \ z \ \ \ arity(is_transrec_fm(p, a, z)) = ?ar" unfolding is_transrec_fm_def by (simp add:arity) synthesize "is_trans_apply_image" from_definition assuming "nonempty" arity_theorem for "is_trans_apply_image_fm" definition transrec_apply_image_body where "transrec_apply_image_body(M,f,mesa,x,z) \ \y[M]. pair(M, x, y, z) \ (\fa[M]. (\z[M]. z \ fa \ (\xa[M]. \y[M]. \xaa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M, xa, y, z) \ pair(M, xa, x, xaa) \ upair(M, xa, xa, sx) \ pre_image(M, mesa, sx, r_sx) \ restriction(M, fa, r_sx, f_r_sx) \ xaa \ mesa \ is_trans_apply_image(M, f, xa, f_r_sx, y))) \ is_trans_apply_image(M, f, x, fa, y))" synthesize "transrec_apply_image_body" from_definition assuming "nonempty" arity_theorem for "transrec_apply_image_body_fm" definition is_trans_apply_image_body where "is_trans_apply_image_body(M,f,\,a,w) \ \z[M]. pair(M,a,z,w) \ a\\ \ (\sa[M]. \esa[M]. \mesa[M]. upair(M, a, a, sa) \ is_eclose(M, sa, esa) \ membership(M, esa, mesa) \ (\fa[M]. (\z[M]. z \ fa \ (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M, x, y, z) \ pair(M, x, a, xa) \ upair(M, x, x, sx) \ pre_image(M, mesa, sx, r_sx) \ restriction(M, fa, r_sx, f_r_sx) \ xa \ mesa \ is_trans_apply_image(M, f, x, f_r_sx, y))) \ is_trans_apply_image(M, f, a, fa, z)))" synthesize "is_trans_apply_image_body" from_definition assuming "nonempty" arity_theorem for "is_trans_apply_image_body_fm" definition replacement_is_omega_funspace_fm where "replacement_is_omega_funspace_fm \ omega_funspace_fm(2,0,1)" -definition replacement_HAleph_wfrec_repl_body_fm where "replacement_HAleph_wfrec_repl_body_fm \ HAleph_wfrec_repl_body_fm(2,0,1)" +definition wfrec_Aleph_fm where "wfrec_Aleph_fm \ HAleph_wfrec_repl_body_fm(2,0,1)" definition replacement_is_fst2_snd2_fm where "replacement_is_fst2_snd2_fm \ is_fst2_snd2_fm(0,1)" definition replacement_is_sndfst_fst2_snd2_fm where "replacement_is_sndfst_fst2_snd2_fm \ is_sndfst_fst2_snd2_fm(0,1)" -definition replacement_is_order_eq_map_fm where "replacement_is_order_eq_map_fm \ order_eq_map_fm(2,3,0,1)" -definition replacement_transrec_apply_image_body_fm where "replacement_transrec_apply_image_body_fm \ transrec_apply_image_body_fm(3,2,0,1)" +definition omap_replacement_fm where "omap_replacement_fm \ order_eq_map_fm(2,3,0,1)" +definition recursive_construction_abs_fm where "recursive_construction_abs_fm \ transrec_apply_image_body_fm(3,2,0,1)" definition banach_replacement_iterates_fm where "banach_replacement_iterates_fm \ banach_is_iterates_body_fm(6,5,4,3,2,0,1)" -definition replacement_is_trans_apply_image_fm where "replacement_is_trans_apply_image_fm \ is_trans_apply_image_body_fm(3,2,0,1)" +definition recursive_construction_fm where "recursive_construction_fm \ is_trans_apply_image_body_fm(3,2,0,1)" (* definition banach_iterates_fm where "banach_iterates_fm \ banach_body_iterates_fm(7,6,5,4,3,2,0,1)" *) -definition replacement_dcwit_repl_body_fm where "replacement_dcwit_repl_body_fm \ dcwit_repl_body_fm(6,5,4,3,2,0,1)" +definition dc_abs_fm where "dc_abs_fm \ dcwit_repl_body_fm(6,5,4,3,2,0,1)" +definition lam_replacement_check_fm where "lam_replacement_check_fm \ Lambda_in_M_fm(check_fm(2,0,1),1)" text\The following instances are needed only on the ground model. The first one corresponds to the recursive definition of forces for atomic formulas; the next two corresponds to \<^term>\PHcheck\; the following is used to get a generic filter using some form of choice.\ locale M_ZF_ground = M_ZF1 + assumes ZF_ground_replacements: "replacement_assm(M,env,wfrec_Hfrc_at_fm)" "replacement_assm(M,env,wfrec_Hcheck_fm)" - "replacement_assm(M,env,Lambda_in_M_fm(check_fm(2,0,1),1))" + "replacement_assm(M,env,lam_replacement_check_fm)" locale M_ZF_ground_trans = M_ZF1_trans + M_ZF_ground definition instances_ground_fms where "instances_ground_fms \ { wfrec_Hfrc_at_fm, wfrec_Hcheck_fm, - Lambda_in_M_fm(check_fm(2,0,1),1) }" + lam_replacement_check_fm }" lemmas replacement_instances_ground_defs = - wfrec_Hfrc_at_fm_def wfrec_Hcheck_fm_def + wfrec_Hfrc_at_fm_def wfrec_Hcheck_fm_def lam_replacement_check_fm_def declare (in M_ZF_ground) replacement_instances_ground_defs [simp] lemma instances_ground_fms_type[TC]: "instances_ground_fms \ formula" using Lambda_in_M_fm_type unfolding instances_ground_fms_def replacement_instances_ground_defs by simp locale M_ZF_ground_notCH = M_ZF_ground + assumes ZF_ground_notCH_replacements: - "replacement_assm(M,env,replacement_transrec_apply_image_body_fm)" - "replacement_assm(M,env,replacement_is_trans_apply_image_fm)" + "replacement_assm(M,env,recursive_construction_abs_fm)" + "replacement_assm(M,env,recursive_construction_fm)" definition instances_ground_notCH_fms where "instances_ground_notCH_fms \ - { replacement_transrec_apply_image_body_fm, - replacement_is_trans_apply_image_fm }" + { recursive_construction_abs_fm, + recursive_construction_fm }" lemma instances_ground_notCH_fms_type[TC]: "instances_ground_notCH_fms \ formula" - unfolding instances_ground_notCH_fms_def replacement_transrec_apply_image_body_fm_def - replacement_is_trans_apply_image_fm_def + unfolding instances_ground_notCH_fms_def recursive_construction_abs_fm_def + recursive_construction_fm_def by simp -declare (in M_ZF_ground_notCH) replacement_transrec_apply_image_body_fm_def[simp] - replacement_is_trans_apply_image_fm_def[simp] +declare (in M_ZF_ground_notCH) recursive_construction_abs_fm_def[simp] + recursive_construction_fm_def[simp] locale M_ZF_ground_notCH_trans = M_ZF_ground_trans + M_ZF_ground_notCH locale M_ZF_ground_CH = M_ZF_ground_notCH + assumes - dcwit_replacement: "replacement_assm(M,env,replacement_dcwit_repl_body_fm)" + dcwit_replacement: "replacement_assm(M,env,dc_abs_fm)" -declare (in M_ZF_ground_CH) replacement_dcwit_repl_body_fm_def [simp] +declare (in M_ZF_ground_CH) dc_abs_fm_def [simp] locale M_ZF_ground_CH_trans = M_ZF_ground_notCH_trans + M_ZF_ground_CH locale M_ctm1 = M_ZF1_trans + M_ZF_ground_trans + fixes enum assumes M_countable: "enum\bij(nat,M)" locale M_ctm1_AC = M_ctm1 + M_ZFC1_trans context M_ZF_ground_CH_trans begin lemma replacement_dcwit_repl_body: "(##M)(mesa) \ (##M)(A) \ (##M)(a) \ (##M)(s) \ (##M)(R) \ strong_replacement(##M, dcwit_repl_body(##M,mesa,A,a,s,R))" using strong_replacement_rel_in_ctm[where \="dcwit_repl_body_fm(6,5,4,3,2,0,1)" and env="[R,s,a,A,mesa]" and f="dcwit_repl_body(##M,mesa,A,a,s,R)"] zero_in_M arity_dcwit_repl_body dcwit_replacement - unfolding replacement_dcwit_repl_body_fm_def + unfolding dc_abs_fm_def by simp lemma dcwit_repl: "(##M)(sa) \ (##M)(esa) \ (##M)(mesa) \ (##M)(A) \ (##M)(a) \ (##M)(s) \ (##M)(R) \ strong_replacement ((##M), \x z. \y[(##M)]. pair((##M), x, y, z) \ is_wfrec ((##M), \n f. is_nat_case ((##M), a, \m bmfm. \fm[(##M)]. \cp[(##M)]. is_apply((##M), f, m, fm) \ is_Collect((##M), A, \x. \fmx[(##M)]. ((##M)(x) \ fmx \ R) \ pair((##M), fm, x, fmx), cp) \ is_apply((##M), s, cp, bmfm), n), mesa, x, y))" using replacement_dcwit_repl_body unfolding dcwit_repl_body_def by simp end \ \\<^locale>\M_ZF_ground_CH_trans\\ context M_ZF1_trans begin lemmas M_replacement_ZF_instances = lam_replacement_fst lam_replacement_snd lam_replacement_Union lam_replacement_Image lam_replacement_middle_del lam_replacement_prodRepl lemmas M_separation_ZF_instances = separation_fstsnd_in_sndsnd separation_sndfst_eq_fstsnd lemma separation_is_dcwit_body: assumes "(##M)(A)" "(##M)(a)" "(##M)(g)" "(##M)(R)" shows "separation(##M,is_dcwit_body(##M, A, a, g, R))" using assms separation_in_ctm[where env="[A,a,g,R]" and \="is_dcwit_body_fm(1,2,3,4,0)", OF _ _ _ is_dcwit_body_iff_sats[symmetric], of "\_.A" "\_.a" "\_.g" "\_.R" "\x. x"] nonempty arity_is_dcwit_body_fm is_dcwit_body_fm_type by (simp add:ord_simp_union) end \ \\<^locale>\M_ZF1_trans\\ sublocale M_ZF1_trans \ M_replacement "##M" using M_replacement_ZF_instances M_separation_ZF_instances by unfold_locales simp context M_ZF1_trans begin lemma separation_Pow_rel: "A\M \ separation(##M, \y. \x \ M . x\A \ y = \x, Pow\<^bsup>##M\<^esup>(x)\)" using separation_assm_sats[of "is_Pow_fm(0,1)"] arity_is_Pow_fm ord_simp_union Pow_rel_closed nonempty Pow_rel_iff by simp lemma strong_replacement_Powapply_rel: "f\M \ strong_replacement(##M, \x y. y = Powapply\<^bsup>##M\<^esup>(f,x))" using Powapply_rel_replacement separation_Pow_rel transM by simp end \ \\<^locale>\M_ZF1_trans\\ sublocale M_ZF1_trans \ M_Vfrom "##M" using power_ax strong_replacement_Powapply_rel phrank_repl trans_repl_HVFrom wfrec_rank by unfold_locales auto sublocale M_ZF1_trans \ M_Perm "##M" using separation_PiP_rel separation_injP_rel separation_surjP_rel lam_replacement_imp_strong_replacement[OF lam_replacement_Sigfun[OF lam_replacement_constant]] Pi_replacement1 unfolding Sigfun_def by unfold_locales simp_all sublocale M_ZF1_trans \ M_pre_seqspace "##M" by unfold_locales context M_ZF1_trans begin lemma separation_inj_rel: "A\M \ separation(##M, \y. \x\M. x \ A \ y = \x, inj_rel(##M,fst(x), snd(x))\)" using arity_is_inj_fm ord_simp_union nonempty inj_rel_closed[simplified] inj_rel_iff[simplified] by (rule_tac separation_assm_bin_sats[of "is_inj_fm(0,1,2)"]) (simp_all add:setclass_def) lemma lam_replacement_inj_rel: "lam_replacement(##M, \x . inj_rel(##M,fst(x),snd(x)))" using lam_replacement_inj_rel' separation_inj_rel by simp (* These lemmas were required for the original proof of Schröder-Bernstein. lemma banach_iterates: assumes "X\M" "Y\M" "f\M" "g\M" "W\M" shows "iterates_replacement(##M, is_banach_functor(##M,X,Y,f,g), W)" proof - have "strong_replacement(##M, \ x z . banach_body_iterates(##M,X,Y,f,g,W,n,x,z))" if "n\\" for n using assms that arity_banach_body_iterates_fm ord_simp_union nat_into_M strong_replacement_rel_in_ctm[where \="banach_body_iterates_fm(7,6,5,4,3,2,0,1)" and env="[n,W,g,f,Y,X]"] replacement_ax2(3) by simp then show ?thesis using assms nat_into_M Memrel_closed unfolding iterates_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def is_nat_case_def iterates_MH_def banach_body_iterates_def by simp qed lemma separation_banach_functor_iterates: assumes "X\M" "Y\M" "f\M" "g\M" "A\M" shows "separation(##M, \b. \x\A. x \ \ \ b = banach_functor(X, Y, f, g)^x (0))" proof - have " (\xa\M. xa \ A \ xa \ \ \ banach_is_iterates_body(##M, X, Y, f, g, 0, xa, x)) \ (\n\A. n \ \ \ banach_is_iterates_body(##M, X, Y, f, g, 0, n, x))" if "x\M" for x using assms nat_into_M nat_in_M transM[of _ A] transM[of _ \] that by auto then have "separation(##M, \ z . \n\A . n\\ \ banach_is_iterates_body(##M,X,Y,f,g,0,n,z))" using assms nat_into_M nat_in_M arity_banach_is_iterates_body_fm[of 6 5 4 3 2 0 1] ord_simp_union separation_in_ctm[where \="(\\ \\0\7\ \ \\0\8\ \ banach_is_iterates_body_fm(6,5,4,3,2,0,1) \\\)" and env="[0,g,f,Y,X,A,\]"] by (simp add:arity_Exists arity_And) moreover from assms have "(\x\A. x \ \ \ is_iterates(##M,is_banach_functor(##M,X, Y, f, g),0,x,z)) \ (\n\A . n\\ \ banach_is_iterates_body(##M,X,Y,f,g,0,n,z))" if "z\M" for z using nat_in_M nat_into_M transM[of _ A] transM[of _ \] unfolding is_iterates_def wfrec_replacement_def is_wfrec_def M_is_recfun_def is_nat_case_def iterates_MH_def banach_body_iterates_def banach_is_iterates_body_def by simp moreover from assms have "(\x\A. x \ \ \ is_iterates(##M,is_banach_functor(##M,X, Y, f, g),0,x,z)) \ (\x\A. x \ \ \ z = banach_functor(X, Y, f, g)^x (0))" if "z\M" for z using transM[of _ A] nat_in_M nat_into_M that iterates_abs[OF banach_iterates banach_functor_abs] banach_functor_closed by auto ultimately show ?thesis by(rule_tac separation_cong[THEN iffD2],auto) qed lemma banach_replacement: assumes "X\M" "Y\M" "f\M" "g\M" shows "strong_replacement(##M, \n y. n\nat \ y = banach_functor(X, Y, f, g)^n (0))" using assms banach_repl_iter' separation_banach_functor_iterates by simp *) end \ \\<^locale>\M_ZF1_trans\\ lemma (in M_basic) rel2_trans_apply: "M(f) \ relation2(M,is_trans_apply_image(M,f),trans_apply_image(f))" unfolding is_trans_apply_image_def trans_apply_image_def relation2_def by auto lemma (in M_basic) apply_image_closed: shows "M(f) \ \x[M]. \g[M]. M(trans_apply_image(f, x, g))" unfolding trans_apply_image_def by simp context M_ZF_ground_notCH_trans begin lemma replacement_transrec_apply_image_body : "(##M)(f) \ (##M)(mesa) \ strong_replacement(##M,transrec_apply_image_body(##M,f,mesa))" using strong_replacement_rel_in_ctm[where \="transrec_apply_image_body_fm(3,2,0,1)" and env="[mesa,f]"] zero_in_M arity_transrec_apply_image_body_fm ord_simp_union ZF_ground_notCH_replacements(1) by simp lemma transrec_replacement_apply_image: assumes "(##M)(f)" "(##M)(\)" shows "transrec_replacement(##M, is_trans_apply_image(##M, f), \)" using replacement_transrec_apply_image_body[unfolded transrec_apply_image_body_def] assms Memrel_closed singleton_closed eclose_closed unfolding transrec_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def by simp lemma rec_trans_apply_image_abs: assumes "(##M)(f)" "(##M)(x)" "(##M)(y)" "Ord(x)" shows "is_transrec(##M,is_trans_apply_image(##M, f),x,y) \ y = transrec(x,trans_apply_image(f))" using transrec_abs[OF transrec_replacement_apply_image rel2_trans_apply] assms apply_image_closed by simp lemma replacement_is_trans_apply_image: "(##M)(f) \ (##M)(\) \ strong_replacement(##M, \ x z . \y[##M]. pair(##M,x,y,z) \ x\\ \ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))" unfolding is_transrec_def is_wfrec_def M_is_recfun_def apply(rule_tac strong_replacement_cong[ where P="\ x z. M,[x,z,\,f] \ is_trans_apply_image_body_fm(3,2,0,1)",THEN iffD1]) apply(rule_tac is_trans_apply_image_body_iff_sats[symmetric,unfolded is_trans_apply_image_body_def,where env="[_,_,\,f]"]) apply(simp_all add:zero_in_M) apply(rule_tac ZF_ground_notCH_replacements(2)[unfolded replacement_assm_def, rule_format, where env="[\,f]",simplified]) apply(simp_all add: arity_is_trans_apply_image_body_fm is_trans_apply_image_body_fm_type ord_simp_union) done lemma trans_apply_abs: "(##M)(f) \ (##M)(\) \ Ord(\) \ (##M)(x) \ (##M)(z) \ (x\\ \ z = \x, transrec(x, \a g. f ` (g `` a)) \) \ (\y[##M]. pair(##M,x,y,z) \ x\\ \ (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))" using rec_trans_apply_image_abs Ord_in_Ord transrec_closed[OF transrec_replacement_apply_image rel2_trans_apply,of f,simplified] apply_image_closed unfolding trans_apply_image_def by auto lemma replacement_trans_apply_image: "(##M)(f) \ (##M)(\) \ Ord(\) \ strong_replacement(##M, \x y. x\\ \ y = \x, transrec(x, \a g. f ` (g `` a))\)" using strong_replacement_cong[THEN iffD1,OF _ replacement_is_trans_apply_image,simplified] trans_apply_abs Ord_in_Ord by simp end \ \\<^locale>\M_ZF_ground_notCH_trans\\ definition ifrFb_body where "ifrFb_body(M,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then if M(converse(f) ` i) then converse(f) ` i else 0 else 0 else if M(i) then i else 0)" relativize functional "ifrFb_body" "ifrFb_body_rel" relationalize "ifrFb_body_rel" "is_ifrFb_body" synthesize "is_ifrFb_body" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body_fm" definition ifrangeF_body :: "[i\o,i,i,i,i] \ o" where "ifrangeF_body(M,A,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body(M,b,f,x,i)\" relativize functional "ifrangeF_body" "ifrangeF_body_rel" relationalize "ifrangeF_body_rel" "is_ifrangeF_body" synthesize "is_ifrangeF_body" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body: "(##M)(A) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body(##M,A,r,s))" using separation_in_ctm[where \="is_ifrangeF_body_fm(1,2,3,0)" and env="[A,r,s]"] zero_in_M arity_is_ifrangeF_body_fm ord_simp_union is_ifrangeF_body_fm_type by simp lemma (in M_basic) is_ifrFb_body_closed: "M(r) \ M(s) \ is_ifrFb_body(M, r, s, x, i) \ M(i)" unfolding ifrangeF_body_def is_ifrangeF_body_def is_ifrFb_body_def If_abs by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body_abs: assumes "(##M)(A)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body(##M,A,r,s,x) \ ifrangeF_body(##M,A,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body(##M, r, s, z, i))= (\ i. is_ifrFb_body(##M, r, s, z, i))" for z using is_ifrFb_body_closed[of r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body(##M,r,s,z,i)"]) auto moreover have "(\ i. is_ifrFb_body(##M, r, s, z, i))= (\ i. ifrFb_body(##M, r, s, z, i))" for z proof (rule_tac Least_cong[of "\i. is_ifrFb_body(##M,r,s,z,i)" "\i. ifrFb_body(##M,r,s,z,i)"]) fix y from assms \a\M\ show "is_ifrFb_body(##M, r, s, z, y) \ ifrFb_body(##M, r, s, z, y)" using If_abs apply_0 unfolding ifrFb_body_def is_ifrFb_body_def by (cases "y\M"; cases "y\range(s)"; cases "converse(s)`y \ M"; auto dest:transM split del: split_if del:iffI) (auto simp flip:setclass_iff; (force simp only:setclass_iff))+ qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body(##M, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body(##M, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body(##M,r,s,z,i)" a] by simp ultimately have "least(##M, \i. i \ M \ is_ifrFb_body(##M, r, s, z, i), a) \ a = (\ i. ifrFb_body(##M, r, s, z,i))" for z by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body_def is_ifrangeF_body_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body: "(##M)(A) \ (##M)(b) \ (##M)(f) \ separation (##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\x. if (##M)(x) then x else 0, b, f, i)\)" using separation_is_ifrangeF_body ifrangeF_body_abs separation_cong[where P="is_ifrangeF_body(##M,A,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body_def if_range_F_def if_range_F_else_F_def ifrFb_body_def by simp (* (##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\a. if (##M)(a) then G`a else 0, b, f, i)\) *) definition ifrFb_body2 where "ifrFb_body2(M,G,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then if M(converse(f) ` i) then G`(converse(f) ` i) else 0 else 0 else if M(i) then G`i else 0)" relativize functional "ifrFb_body2" "ifrFb_body2_rel" relationalize "ifrFb_body2_rel" "is_ifrFb_body2" synthesize "is_ifrFb_body2" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body2_fm" definition ifrangeF_body2 :: "[i\o,i,i,i,i,i] \ o" where "ifrangeF_body2(M,A,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body2(M,G,b,f,x,i)\" relativize functional "ifrangeF_body2" "ifrangeF_body2_rel" relationalize "ifrangeF_body2_rel" "is_ifrangeF_body2" synthesize "is_ifrangeF_body2" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body2_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body2: "(##M)(A) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body2(##M,A,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body2_fm(1,2,3,4,0)" and env="[A,G,r,s]"] zero_in_M arity_is_ifrangeF_body2_fm ord_simp_union is_ifrangeF_body2_fm_type by simp lemma (in M_basic) is_ifrFb_body2_closed: "M(G) \ M(r) \ M(s) \ is_ifrFb_body2(M, G, r, s, x, i) \ M(i)" unfolding ifrangeF_body2_def is_ifrangeF_body2_def is_ifrFb_body2_def If_abs by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body2_abs: assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body2(##M,A,G,r,s,x) \ ifrangeF_body2(##M,A,G,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body2(##M, G, r, s, z, i))= (\ i. is_ifrFb_body2(##M, G, r, s, z, i))" for z using is_ifrFb_body2_closed[of G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body2(##M,G,r,s,z,i)"]) auto moreover have "(\ i. is_ifrFb_body2(##M, G, r, s, z, i))= (\ i. ifrFb_body2(##M, G, r, s, z, i))" for z proof (rule_tac Least_cong[of "\i. is_ifrFb_body2(##M,G,r,s,z,i)" "\i. ifrFb_body2(##M,G,r,s,z,i)"]) fix y from assms \a\M\ show "is_ifrFb_body2(##M, G, r, s, z, y) \ ifrFb_body2(##M, G, r, s, z, y)" using If_abs apply_0 unfolding ifrFb_body2_def is_ifrFb_body2_def by (cases "y\M"; cases "y\range(s)"; cases "converse(s)`y \ M"; auto dest:transM split del: split_if del:iffI) (auto simp flip:setclass_iff; (force simp only:setclass_iff))+ qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body2(##M, G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body2(##M, G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body2(##M,G,r,s,z,i)" a] by simp ultimately have "least(##M, \i. i \ M \ is_ifrFb_body2(##M, G, r, s, z, i), a) \ a = (\ i. ifrFb_body2(##M, G, r, s, z,i))" for z by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body2_def is_ifrangeF_body2_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body2: "(##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation (##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\a. if (##M)(a) then G ` a else 0, b, f, i)\)" using separation_is_ifrangeF_body2 ifrangeF_body2_abs separation_cong[where P="is_ifrangeF_body2(##M,A,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body2_def if_range_F_def if_range_F_else_F_def ifrFb_body2_def by simp (* (##M)(A) \ (##M)(b) \ (##M)(f) \ (##M)(F) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\a. if (##M)(a) then F -`` {a} else 0, b, f, i)\) *) definition ifrFb_body3 where "ifrFb_body3(M,G,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then if M(converse(f) ` i) then G-``{converse(f) ` i} else 0 else 0 else if M(i) then G-``{i} else 0)" relativize functional "ifrFb_body3" "ifrFb_body3_rel" relationalize "ifrFb_body3_rel" "is_ifrFb_body3" synthesize "is_ifrFb_body3" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body3_fm" definition ifrangeF_body3 :: "[i\o,i,i,i,i,i] \ o" where "ifrangeF_body3(M,A,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body3(M,G,b,f,x,i)\" relativize functional "ifrangeF_body3" "ifrangeF_body3_rel" relationalize "ifrangeF_body3_rel" "is_ifrangeF_body3" synthesize "is_ifrangeF_body3" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body3_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body3: "(##M)(A) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body3(##M,A,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body3_fm(1,2,3,4,0)" and env="[A,G,r,s]"] zero_in_M arity_is_ifrangeF_body3_fm ord_simp_union is_ifrangeF_body3_fm_type by simp lemma (in M_basic) is_ifrFb_body3_closed: "M(G) \ M(r) \ M(s) \ is_ifrFb_body3(M, G, r, s, x, i) \ M(i)" unfolding ifrangeF_body3_def is_ifrangeF_body3_def is_ifrFb_body3_def If_abs by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body3_abs: assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body3(##M,A,G,r,s,x) \ ifrangeF_body3(##M,A,G,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body3(##M, G, r, s, z, i))= (\ i. is_ifrFb_body3(##M, G, r, s, z, i))" for z using is_ifrFb_body3_closed[of G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body3(##M,G,r,s,z,i)"]) auto moreover have "(\ i. is_ifrFb_body3(##M, G, r, s, z, i))= (\ i. ifrFb_body3(##M, G, r, s, z, i))" for z proof (rule_tac Least_cong[of "\i. is_ifrFb_body3(##M,G,r,s,z,i)" "\i. ifrFb_body3(##M,G,r,s,z,i)"]) fix y from assms \a\M\ show "is_ifrFb_body3(##M, G, r, s, z, y) \ ifrFb_body3(##M, G, r, s, z, y)" using If_abs apply_0 unfolding ifrFb_body3_def is_ifrFb_body3_def by (cases "y\M"; cases "y\range(s)"; cases "converse(s)`y \ M"; auto dest:transM split del: split_if del:iffI) (auto simp flip:setclass_iff; (force simp only:setclass_iff))+ qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body3(##M, G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body3(##M, G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body3(##M,G,r,s,z,i)" a] by simp ultimately have "least(##M, \i. i \ M \ is_ifrFb_body3(##M, G, r, s, z, i), a) \ a = (\ i. ifrFb_body3(##M, G, r, s, z,i))" for z by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body3_def is_ifrangeF_body3_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body3: "(##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation (##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\a. if (##M)(a) then G-``{a} else 0, b, f, i)\)" using separation_is_ifrangeF_body3 ifrangeF_body3_abs separation_cong[where P="is_ifrangeF_body3(##M,A,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body3_def if_range_F_def if_range_F_else_F_def ifrFb_body3_def by simp (* (##M)(A) \ (##M)(b) \ (##M)(f) \ (##M)(A') \ separation(##M, \y. \x\A'. y = \x, \ i. x \ if_range_F_else_F((`)(A), b, f, i)\) *) definition ifrFb_body4 where "ifrFb_body4(G,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then G`(converse(f) ` i) else 0 else G`i)" relativize functional "ifrFb_body4" "ifrFb_body4_rel" relationalize "ifrFb_body4_rel" "is_ifrFb_body4" synthesize "is_ifrFb_body4" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body4_fm" definition ifrangeF_body4 :: "[i\o,i,i,i,i,i] \ o" where "ifrangeF_body4(M,A,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body4(G,b,f,x,i)\" relativize functional "ifrangeF_body4" "ifrangeF_body4_rel" relationalize "ifrangeF_body4_rel" "is_ifrangeF_body4" synthesize "is_ifrangeF_body4" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body4_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body4: "(##M)(A) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body4(##M,A,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body4_fm(1,2,3,4,0)" and env="[A,G,r,s]"] zero_in_M arity_is_ifrangeF_body4_fm ord_simp_union is_ifrangeF_body4_fm_type by simp lemma (in M_basic) is_ifrFb_body4_closed: "M(G) \ M(r) \ M(s) \ is_ifrFb_body4(M, G, r, s, x, i) \ M(i)" using If_abs unfolding ifrangeF_body4_def is_ifrangeF_body4_def is_ifrFb_body4_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body4_abs: assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body4(##M,A,G,r,s,x) \ ifrangeF_body4(##M,A,G,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body4(##M, G, r, s, z, i))= (\ i. is_ifrFb_body4(##M, G, r, s, z, i))" for z using is_ifrFb_body4_closed[of G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body4(##M,G,r,s,z,i)"]) auto moreover have "(\ i. is_ifrFb_body4(##M, G, r, s, z, i))= (\ i. ifrFb_body4(G, r, s, z, i))" if "z\M" for z proof (rule_tac Least_cong[of "\i. is_ifrFb_body4(##M,G,r,s,z,i)" "\i. ifrFb_body4(G,r,s,z,i)"]) fix y from assms \a\M\ \z\M\ show "is_ifrFb_body4(##M, G, r, s, z, y) \ ifrFb_body4(G, r, s, z, y)" using If_abs apply_0 unfolding ifrFb_body4_def is_ifrFb_body4_def apply (cases "y\M"; cases "y\range(s)"; cases "r=0"; cases "y\domain(G)"; auto dest:transM split del: split_if del:iffI) by (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff)) (auto simp flip:setclass_iff simp: fun_apply_def ) qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body4(##M, G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body4(##M, G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body4(##M,G,r,s,z,i)" a] by simp ultimately have "z\M \ least(##M, \i. i \ M \ is_ifrFb_body4(##M, G, r, s, z, i), a) \ a = (\ i. ifrFb_body4(G, r, s, z,i))" for z by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body4_def is_ifrangeF_body4_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body4: "(##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F((`)(G), b, f, i)\)" using separation_is_ifrangeF_body4 ifrangeF_body4_abs separation_cong[where P="is_ifrangeF_body4(##M,A,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body4_def if_range_F_def if_range_F_else_F_def ifrFb_body4_def by simp (* (##M)(G) \ (##M)(A) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\x. {xa \ G . x \ xa}, b, f, i)\) *) definition ifrFb_body5 where "ifrFb_body5(G,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then {xa \ G . converse(f) ` i \ xa} else 0 else {xa \ G . i \ xa})" relativize functional "ifrFb_body5" "ifrFb_body5_rel" relationalize "ifrFb_body5_rel" "is_ifrFb_body5" synthesize "is_ifrFb_body5" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body5_fm" definition ifrangeF_body5 :: "[i\o,i,i,i,i,i] \ o" where "ifrangeF_body5(M,A,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body5(G,b,f,x,i)\" relativize functional "ifrangeF_body5" "ifrangeF_body5_rel" relationalize "ifrangeF_body5_rel" "is_ifrangeF_body5" synthesize "is_ifrangeF_body5" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body5_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body5: "(##M)(A) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body5(##M,A,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body5_fm(1,2,3,4,0)" and env="[A,G,r,s]"] zero_in_M arity_is_ifrangeF_body5_fm ord_simp_union is_ifrangeF_body5_fm_type by simp lemma (in M_basic) is_ifrFb_body5_closed: "M(G) \ M(r) \ M(s) \ is_ifrFb_body5(M, G, r, s, x, i) \ M(i)" using If_abs unfolding ifrangeF_body5_def is_ifrangeF_body5_def is_ifrFb_body5_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body5_abs: assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body5(##M,A,G,r,s,x) \ ifrangeF_body5(##M,A,G,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body5(##M, G, r, s, z, i))= (\ i. is_ifrFb_body5(##M, G, r, s, z, i))" for z using is_ifrFb_body5_closed[of G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body5(##M,G,r,s,z,i)"]) auto moreover have "(\ i. is_ifrFb_body5(##M, G, r, s, z, i))= (\ i. ifrFb_body5(G, r, s, z, i))" if "z\M" for z proof (rule_tac Least_cong[of "\i. is_ifrFb_body5(##M,G,r,s,z,i)" "\i. ifrFb_body5(G,r,s,z,i)"]) fix y from assms \a\M\ \z\M\ show "is_ifrFb_body5(##M, G, r, s, z, y) \ ifrFb_body5(G, r, s, z, y)" using If_abs apply_0 separation_in_constant separation_in_rev unfolding ifrFb_body5_def is_ifrFb_body5_def apply (cases "y\M"; cases "y\range(s)"; cases "r=0"; cases "y\domain(G)"; auto dest:transM split del: split_if del:iffI) apply (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff)) apply (auto simp flip:setclass_iff simp: fun_apply_def) apply (auto dest:transM) done qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body5(##M, G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body5(##M, G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body5(##M,G,r,s,z,i)" a] by simp ultimately have "z\M \ least(##M, \i. i \ M \ is_ifrFb_body5(##M, G, r, s, z, i), a) \ a = (\ i. ifrFb_body5(G, r, s, z,i))" for z by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body5_def is_ifrangeF_body5_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body5: "(##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\x. {xa \ G . x \ xa}, b, f, i)\)" using separation_is_ifrangeF_body5 ifrangeF_body5_abs separation_cong[where P="is_ifrangeF_body5(##M,A,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body5_def if_range_F_def if_range_F_else_F_def ifrFb_body5_def by simp (* (##M)(A) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A'. y = \x, \ i. x \ if_range_F_else_F(\a. {p \ A . domain(p) = a}, b, f, i)\) *) definition ifrFb_body6 where "ifrFb_body6(G,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then {p\G . domain(p) = converse(f) ` i} else 0 else {p\G . domain(p) = i})" relativize functional "ifrFb_body6" "ifrFb_body6_rel" relationalize "ifrFb_body6_rel" "is_ifrFb_body6" synthesize "is_ifrFb_body6" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body6_fm" definition ifrangeF_body6 :: "[i\o,i,i,i,i,i] \ o" where "ifrangeF_body6(M,A,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body6(G,b,f,x,i)\" relativize functional "ifrangeF_body6" "ifrangeF_body6_rel" relationalize "ifrangeF_body6_rel" "is_ifrangeF_body6" synthesize "is_ifrangeF_body6" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body6_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body6: "(##M)(A) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body6(##M,A,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body6_fm(1,2,3,4,0)" and env="[A,G,r,s]"] zero_in_M arity_is_ifrangeF_body6_fm ord_simp_union is_ifrangeF_body6_fm_type by simp lemma (in M_basic) ifrFb_body6_closed: "M(G) \ M(r) \ M(s) \ ifrFb_body6(G, r, s, x, i) \ M(i) \ ifrFb_body6(G, r, s, x, i)" using If_abs unfolding ifrangeF_body6_def is_ifrangeF_body6_def ifrFb_body6_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_basic) is_ifrFb_body6_closed: "M(G) \ M(r) \ M(s) \ is_ifrFb_body6(M, G, r, s, x, i) \ M(i)" using If_abs unfolding ifrangeF_body6_def is_ifrangeF_body6_def is_ifrFb_body6_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body6_abs: assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body6(##M,A,G,r,s,x) \ ifrangeF_body6(##M,A,G,r,s,x)" proof - { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body6(##M, G, r, s, z, i))= (\ i. is_ifrFb_body6(##M, G, r, s, z, i))" for z using is_ifrFb_body6_closed[of G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body6(##M,G,r,s,z,i)"]) auto moreover have "(\ i. i\M \ is_ifrFb_body6(##M, G, r, s, z, i))= (\ i. i\M \ ifrFb_body6(G, r, s, z, i))" if "z\M" for z proof (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body6(##M,G,r,s,z,i)" "\i. i\M \ ifrFb_body6(G,r,s,z,i)"]) fix y from assms \a\M\ \z\M\ show "y\M \ is_ifrFb_body6(##M, G, r, s, z, y) \ y\M \ ifrFb_body6(G, r, s, z, y)" using If_abs apply_0 separation_in_constant transitivity[of _ G] separation_closed converse_closed apply_closed range_closed zero_in_M separation_cong[OF eq_commute,THEN iffD1,OF domain_eq_separation] unfolding ifrFb_body6_def is_ifrFb_body6_def by auto qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body6(##M, G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body6(##M, G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body6(##M,G,r,s,z,i)" a] by simp ultimately have "z\M \ least(##M, \i. i \ M \ is_ifrFb_body6(##M, G, r, s, z, i), a) \ a = (\ i. ifrFb_body6(G, r, s, z,i))" for z using Least_cong[OF ifrFb_body6_closed[of G r s]] assms by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body6_def is_ifrangeF_body6_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body6: "(##M)(A) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(\a. {p \ G . domain(p) = a}, b, f, i)\)" using separation_is_ifrangeF_body6 ifrangeF_body6_abs separation_cong[where P="is_ifrangeF_body6(##M,A,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body6_def if_range_F_def if_range_F_else_F_def ifrFb_body6_def by simp (* (##M)(A) \ (##M)(f) \ (##M)(b) \ (##M)(D) \ (##M)(r') \ (##M)(A') \ separation(##M, \y. \x\A'. y = \x, \ i. x \ if_range_F_else_F(drSR_Y(r', D, A), b, f, i)\) *) definition ifrFb_body7 where "ifrFb_body7(B,D,A,b,f,x,i) \ x \ (if b = 0 then if i \ range(f) then {d \ D . \r\A. restrict(r, B) = converse(f) ` i \ d = domain(r)} else 0 else {d \ D . \r\A. restrict(r, B) = i \ d = domain(r)})" relativize functional "ifrFb_body7" "ifrFb_body7_rel" relationalize "ifrFb_body7_rel" "is_ifrFb_body7" synthesize "is_ifrFb_body7" from_definition assuming "nonempty" arity_theorem for "is_ifrFb_body7_fm" definition ifrangeF_body7 :: "[i\o,i,i,i,i,i,i,i] \ o" where "ifrangeF_body7(M,A,B,D,G,b,f) \ \y. \x\A. y = \x,\ i. ifrFb_body7(B,D,G,b,f,x,i)\" relativize functional "ifrangeF_body7" "ifrangeF_body7_rel" relationalize "ifrangeF_body7_rel" "is_ifrangeF_body7" synthesize "is_ifrangeF_body7" from_definition assuming "nonempty" arity_theorem for "is_ifrangeF_body7_fm" lemma (in M_Z_trans) separation_is_ifrangeF_body7: "(##M)(A) \ (##M)(B) \ (##M)(D) \ (##M)(G) \ (##M)(r) \ (##M)(s) \ separation(##M, is_ifrangeF_body7(##M,A,B,D,G,r,s))" using separation_in_ctm[where \="is_ifrangeF_body7_fm(1,2,3,4,5,6,0)" and env="[A,B,D,G,r,s]"] zero_in_M arity_is_ifrangeF_body7_fm ord_simp_union is_ifrangeF_body7_fm_type by simp lemma (in M_basic) ifrFb_body7_closed: "M(B) \ M(D) \ M(G) \ M(r) \ M(s) \ ifrFb_body7(B,D,G, r, s, x, i) \ M(i) \ ifrFb_body7(B,D,G, r, s, x, i)" using If_abs unfolding ifrangeF_body7_def is_ifrangeF_body7_def ifrFb_body7_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_basic) is_ifrFb_body7_closed: "M(B) \ M(D) \ M(G) \ M(r) \ M(s) \ is_ifrFb_body7(M, B,D,G, r, s, x, i) \ M(i)" using If_abs unfolding ifrangeF_body7_def is_ifrangeF_body7_def is_ifrFb_body7_def fun_apply_def by (cases "i\range(s)"; cases "r=0"; auto dest:transM) lemma (in M_ZF1_trans) ifrangeF_body7_abs: assumes "(##M)(A)" "(##M)(B)" "(##M)(D)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)" shows "is_ifrangeF_body7(##M,A,B,D,G,r,s,x) \ ifrangeF_body7(##M,A,B,D,G,r,s,x)" proof - from assms have sep_dr: "y\M \ separation(##M, \d . \r\M . r\G \ y = restrict(r, B) \ d = domain(r))" for y by(rule_tac separation_cong[where P'="\d . \r\ M . r\G \ y = restrict(r, B) \ d = domain(r)",THEN iffD1,OF _ separation_restrict_eq_dom_eq[rule_format,of G B y]],auto simp:transitivity[of _ G]) from assms have sep_dr'': "y\M \ separation(##M, \d . \r\M. r \ G \ d = domain(r) \ converse(s) ` y = restrict(r, B))" for y by(rule_tac separation_cong[THEN iffD1,OF _ separation_restrict_eq_dom_eq[rule_format,of G B "converse(s) ` y "]], auto simp:transitivity[of _ G] apply_closed[simplified] converse_closed[simplified]) { fix a assume "a\M" with assms have "(\ i. i\ M \ is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (\ i. is_ifrFb_body7(##M,B,D, G, r, s, z, i))" for z using is_ifrFb_body7_closed[of B D G r s z] by (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body7(##M,B,D,G,r,s,z,i)"]) auto moreover from this have "(\ i. i\M \ is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (\ i. i\M \ ifrFb_body7(B,D,G, r, s, z, i))" if "z\M" for z proof (rule_tac Least_cong[of "\i. i\M \ is_ifrFb_body7(##M,B,D,G,r,s,z,i)" "\i. i\M \ ifrFb_body7(B,D,G,r,s,z,i)"]) from assms \a\M\ \z\M\ have "is_ifrFb_body7(##M, B,D,G, r, s, z, y) \ ifrFb_body7(B,D,G, r, s, z, y)" if "y\M" for y using If_abs apply_0 separation_closed converse_closed apply_closed range_closed zero_in_M transitivity[of _ D] transitivity[of _ G] that sep_dr sep_dr'' unfolding ifrFb_body7_def is_ifrFb_body7_def by auto then show " y \ M \ is_ifrFb_body7(##M, B, D, G, r, s, z, y) \ y \ M \ ifrFb_body7(B, D, G, r, s, z, y)" for y using conj_cong by simp qed moreover from \a\M\ have "least(##M, \i. i \ M \ is_ifrFb_body7(##M, B,D,G, r, s, z, i), a) \ a = (\ i. i\ M \ is_ifrFb_body7(##M,B,D,G, r, s, z,i))" for z using If_abs least_abs'[of "\i. (##M)(i) \ is_ifrFb_body7(##M,B,D,G,r,s,z,i)" a] by simp ultimately have "z\M \ least(##M, \i. i \ M \ is_ifrFb_body7(##M,B,D,G, r, s, z, i), a) \ a = (\ i. ifrFb_body7(B,D,G, r, s, z,i))" for z using Least_cong[OF ifrFb_body7_closed[of B D G r s]] assms by simp } with assms show ?thesis using pair_in_M_iff apply_closed zero_in_M transitivity[of _ A] unfolding ifrangeF_body7_def is_ifrangeF_body7_def by (auto dest:transM) qed lemma (in M_ZF1_trans) separation_ifrangeF_body7: "(##M)(A) \ (##M)(B) \ (##M)(D) \ (##M)(G) \ (##M)(b) \ (##M)(f) \ separation(##M, \y. \x\A. y = \x, \ i. x \ if_range_F_else_F(drSR_Y(B, D, G), b, f, i)\)" using separation_is_ifrangeF_body7 ifrangeF_body7_abs drSR_Y_equality separation_cong[where P="is_ifrangeF_body7(##M,A,B,D,G,b,f)" and M="##M",THEN iffD1] unfolding ifrangeF_body7_def if_range_F_def if_range_F_else_F_def ifrFb_body7_def by simp definition omfunspace :: "[i,i] \ o" where "omfunspace(B) \ \z. \x. \n\\. z\x \ x = n\B" relativize functional "omfunspace" "omfunspace_rel" relationalize "omfunspace_rel" "is_omfunspace" synthesize "is_omfunspace" from_definition assuming "nonempty" arity_theorem for "is_omfunspace_fm" context M_pre_seqspace begin is_iff_rel for "omfunspace" using is_function_space_iff unfolding omfunspace_rel_def is_omfunspace_def by (simp add:absolut) end \ \\<^locale>\M_pre_seqspace\\ context M_ZF1_trans begin lemma separation_omfunspace: assumes "(##M)(B)" shows "separation(##M, \z. \x[##M]. \n[##M]. n \ \ \ z \ x \ x = n \\<^bsup>M\<^esup> B)" using assms separation_in_ctm[where env="[B]" and \="is_omfunspace_fm(1,0)" and Q="is_omfunspace(##M,B)"] nonempty is_omfunspace_iff[of B, THEN separation_cong, of "##M"] arity_is_omfunspace_fm is_omfunspace_fm_type unfolding omfunspace_rel_def by (auto simp add:ord_simp_union) end \ \\<^locale>\M_ZF1_trans\\ sublocale M_ZF1_trans \ M_seqspace "##M" using separation_omfunspace by unfold_locales definition cdltgamma :: "[i,i] \ o" where "cdltgamma(\) \ \Z . |Z| < \" relativize functional "cdltgamma" "cdltgamma_rel" relationalize "cdltgamma_rel" "is_cdltgamma" synthesize "is_cdltgamma" from_definition assuming "nonempty" arity_theorem for "is_cdltgamma_fm" definition cdeqgamma :: "[i] \ o" where "cdeqgamma \ \Z . |fst(Z)| = snd(Z)" relativize functional "cdeqgamma" "cdeqgamma_rel" relationalize "cdeqgamma_rel" "is_cdeqgamma" synthesize "is_cdeqgamma" from_definition assuming "nonempty" arity_theorem for "is_cdeqgamma_fm" context M_Perm begin is_iff_rel for "cdltgamma" using is_cardinal_iff unfolding cdltgamma_rel_def is_cdltgamma_def by (simp add:absolut) is_iff_rel for "cdeqgamma" using is_cardinal_iff fst_rel_abs snd_rel_abs unfolding cdeqgamma_rel_def is_cdeqgamma_def by (auto simp add:absolut) lemma is_cdeqgamma_iff_split: "M(Z) \ cdeqgamma_rel(M, Z) \ (\\x,y\. |x|\<^bsup>M\<^esup> = y)(Z)" using fst_rel_abs snd_rel_abs unfolding cdeqgamma_rel_def split_def by simp end context M_ZF1_trans begin lemma separation_cdltgamma: assumes "(##M)(\)" shows "separation(##M, \Z . cardinal_rel(##M,Z) < \)" using assms separation_in_ctm[where env="[\]" and \="is_cdltgamma_fm(1,0)" and Q="cdltgamma_rel(##M,\)"] nonempty is_cdltgamma_iff[of \] arity_is_cdltgamma_fm is_cdltgamma_fm_type unfolding cdltgamma_rel_def by (auto simp add:ord_simp_union) lemma separation_cdeqgamma: shows "separation(##M, \Z. (\\x,y\ . cardinal_rel(##M,x) = y)(Z))" using separation_in_ctm[where env="[]" and \="is_cdeqgamma_fm(0)" and Q="cdeqgamma_rel(##M)"] is_cdeqgamma_iff_split nonempty is_cdeqgamma_iff arity_is_cdeqgamma_fm is_cdeqgamma_fm_type separation_cong[OF is_cdeqgamma_iff_split, of "##M"] unfolding cdeqgamma_rel_def by (simp add:ord_simp_union) end \ \\<^locale>\M_ZF1_trans\\ end \ No newline at end of file diff --git a/thys/Independence_CH/ZF_Trans_Interpretations.thy b/thys/Independence_CH/ZF_Trans_Interpretations.thy --- a/thys/Independence_CH/ZF_Trans_Interpretations.thy +++ b/thys/Independence_CH/ZF_Trans_Interpretations.thy @@ -1,677 +1,677 @@ section\Further instances of axiom-schemes\ theory ZF_Trans_Interpretations imports Internal_ZFC_Axioms Replacement_Instances begin locale M_ZF2 = M_ZF1 + assumes replacement_ax2: - "replacement_assm(M,env,replacement_is_order_body_fm)" - "replacement_assm(M,env,wfrec_replacement_order_pred_fm)" - "replacement_assm(M,env,replacement_HAleph_wfrec_repl_body_fm)" - "replacement_assm(M,env,replacement_is_order_eq_map_fm)" + "replacement_assm(M,env,ordtype_replacement_fm)" + "replacement_assm(M,env,wfrec_ordertype_fm)" + "replacement_assm(M,env,wfrec_Aleph_fm)" + "replacement_assm(M,env,omap_replacement_fm)" definition instances2_fms where "instances2_fms \ - { replacement_is_order_body_fm, - wfrec_replacement_order_pred_fm, - replacement_HAleph_wfrec_repl_body_fm, - replacement_is_order_eq_map_fm }" + { ordtype_replacement_fm, + wfrec_ordertype_fm, + wfrec_Aleph_fm, + omap_replacement_fm }" lemmas replacement_instances2_defs = - replacement_is_order_body_fm_def wfrec_replacement_order_pred_fm_def - replacement_HAleph_wfrec_repl_body_fm_def replacement_is_order_eq_map_fm_def + ordtype_replacement_fm_def wfrec_ordertype_fm_def + wfrec_Aleph_fm_def omap_replacement_fm_def declare (in M_ZF2) replacement_instances2_defs [simp] locale M_ZF2_trans = M_ZF1_trans + M_ZF2 locale M_ZFC2 = M_ZFC1 + M_ZF2 locale M_ZFC2_trans = M_ZFC1_trans + M_ZF2_trans + M_ZFC2 locale M_ZF2_ground_notCH = M_ZF2 + M_ZF_ground_notCH locale M_ZF2_ground_notCH_trans = M_ZF2_trans + M_ZF2_ground_notCH + M_ZF_ground_notCH_trans locale M_ZFC2_ground_notCH = M_ZFC2 + M_ZF2_ground_notCH locale M_ZFC2_ground_notCH_trans = M_ZFC2_trans + M_ZFC2_ground_notCH + M_ZF2_ground_notCH_trans locale M_ZFC2_ground_CH_trans = M_ZFC2_ground_notCH_trans + M_ZF_ground_CH_trans locale M_ctm2 = M_ctm1 + M_ZF2_ground_notCH_trans locale M_ctm2_AC = M_ctm2 + M_ctm1_AC + M_ZFC2_ground_notCH_trans locale M_ctm2_AC_CH = M_ctm2_AC + M_ZFC2_ground_CH_trans lemmas (in M_ZF1_trans) separation_instances = separation_well_ord_iso separation_obase_equals separation_is_obase separation_PiP_rel separation_surjP_rel separation_radd_body separation_rmult_body context M_ZF2_trans begin lemma replacement_HAleph_wfrec_repl_body: "B\M \ strong_replacement(##M, HAleph_wfrec_repl_body(##M,B))" using strong_replacement_rel_in_ctm[where \="HAleph_wfrec_repl_body_fm(2,0,1)" and env="[B]"] zero_in_M arity_HAleph_wfrec_repl_body_fm replacement_ax2(3) ord_simp_union by simp lemma HAleph_wfrec_repl: "(##M)(sa) \ (##M)(esa) \ (##M)(mesa) \ strong_replacement (##M, \x z. \y[##M]. pair(##M, x, y, z) \ (\f[##M]. (\z[##M]. z \ f \ (\xa[##M]. \y[##M]. \xaa[##M]. \sx[##M]. \r_sx[##M]. \f_r_sx[##M]. pair(##M, xa, y, z) \ pair(##M, xa, x, xaa) \ upair(##M, xa, xa, sx) \ pre_image(##M, mesa, sx, r_sx) \ restriction(##M, f, r_sx, f_r_sx) \ xaa \ mesa \ is_HAleph(##M, xa, f_r_sx, y))) \ is_HAleph(##M, x, f, y)))" using replacement_HAleph_wfrec_repl_body unfolding HAleph_wfrec_repl_body_def by simp lemma replacement_is_order_eq_map: "A\M \ r\M \ strong_replacement(##M, order_eq_map(##M,A,r))" using strong_replacement_rel_in_ctm[where \="order_eq_map_fm(2,3,0,1)" and env="[A,r]" and f="order_eq_map(##M,A,r)"] order_eq_map_iff_sats[where env="[_,_,A,r]"] zero_in_M fst_snd_closed pair_in_M_iff arity_order_eq_map_fm ord_simp_union replacement_ax2(4) by simp end \ \\<^locale>\M_ZF2_trans\\ definition omap_wfrec_body where "omap_wfrec_body(A,r) \ (\\\image_fm(2, 0, 1) \ pred_set_fm(A #+ 9, 3, r #+ 9, 0) \\)" lemma type_omap_wfrec_body_fm :"A\nat \ r\nat \ omap_wfrec_body(A,r)\formula" unfolding omap_wfrec_body_def by simp lemma arity_aux : "A\nat \ r\nat \ arity(omap_wfrec_body(A,r)) = (9+\<^sub>\A) \ (9+\<^sub>\r)" unfolding omap_wfrec_body_def using arity_image_fm arity_pred_set_fm pred_Un_distrib union_abs2[of 3] union_abs1 by (simp add:FOL_arities, auto simp add:Un_assoc[symmetric] union_abs1) lemma arity_omap_wfrec: "A\nat \ r\nat \ arity(is_wfrec_fm(omap_wfrec_body(A,r),succ(succ(succ(r))), 1, 0)) = (4+\<^sub>\A) \ (4+\<^sub>\r)" using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_aux,of A r "3+\<^sub>\r" 1 0] pred_Un_distrib union_abs1 union_abs2 type_omap_wfrec_body_fm by auto lemma arity_isordermap: "A\nat \ r\nat \d\nat\ arity(is_ordermap_fm(A,r,d)) = succ(d) \ (succ(A) \ succ(r))" unfolding is_ordermap_fm_def using arity_lambda_fm[where i="(4+\<^sub>\A) \ (4+\<^sub>\r)",OF _ _ _ _ arity_omap_wfrec, unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1 by auto lemma arity_is_ordertype: "A\nat \ r\nat \d\nat\ arity(is_ordertype_fm(A,r,d)) = succ(d) \ (succ(A) \ succ(r))" unfolding is_ordertype_fm_def using arity_isordermap arity_image_fm pred_Un_distrib FOL_arities by auto lemma arity_is_order_body: "arity(is_order_body_fm(1,0)) = 2" using arity_is_order_body_fm arity_is_ordertype ord_simp_union by (simp add:FOL_arities) lemma (in M_ZF2_trans) replacement_is_order_body: "strong_replacement(##M, \x z . \y[##M]. is_order_body(##M,x,y) \ z = \x,y\)" apply(rule_tac strong_replacement_cong[ where P="\ x f. M,[x,f] \ (\\ \is_order_body_fm(1,0) \ pair_fm(1,0,2) \\)",THEN iffD1]) apply(simp add: is_order_body_iff_sats[where env="[_,_]",symmetric]) apply(simp_all add:zero_in_M ) apply(rule_tac replacement_ax2(1)[unfolded replacement_assm_def, rule_format, where env="[]",simplified]) apply(simp_all add:arity_is_order_body arity pred_Un_distrib ord_simp_union) done definition H_order_pred where "H_order_pred(A,r) \ \x f . f `` Order.pred(A, x, r)" relationalize "H_order_pred" "is_H_order_pred" lemma (in M_basic) H_order_pred_abs : "M(A) \ M(r) \ M(x) \ M(f) \ M(z) \ is_H_order_pred(M,A,r,x,f,z) \ z = H_order_pred(A,r,x,f)" unfolding is_H_order_pred_def H_order_pred_def by simp synthesize "is_H_order_pred" from_definition assuming "nonempty" lemma (in M_ZF2_trans) wfrec_replacement_order_pred: "A\M \ r\M \ wfrec_replacement(##M, \x g z. is_H_order_pred(##M,A,r,x,g,z) , r)" unfolding wfrec_replacement_def is_wfrec_def M_is_recfun_def is_H_order_pred_def apply(rule_tac strong_replacement_cong[ where P="\ x f. M,[x,f,r,A] \ order_pred_wfrec_body_fm(3,2,1,0)",THEN iffD1]) apply(subst order_pred_wfrec_body_def[symmetric]) apply(rule_tac order_pred_wfrec_body_iff_sats[where env="[_,_,r,A]",symmetric]) apply(simp_all add:zero_in_M) apply(rule_tac replacement_ax2(2)[unfolded replacement_assm_def, rule_format, where env="[r,A]",simplified]) apply(simp_all add: arity_order_pred_wfrec_body_fm ord_simp_union) done lemma (in M_ZF2_trans) wfrec_replacement_order_pred': "A\M \ r\M \ wfrec_replacement(##M, \x g z. z = H_order_pred(A,r,x,g) , r)" using wfrec_replacement_cong[OF H_order_pred_abs[of A r,rule_format] refl,THEN iffD1, OF _ _ _ _ _ wfrec_replacement_order_pred[of A r]] by simp sublocale M_ZF2_trans \ M_pre_cardinal_arith "##M" using separation_instances wfrec_replacement_order_pred'[unfolded H_order_pred_def] replacement_is_order_eq_map[unfolded order_eq_map_def] by unfold_locales simp_all definition is_well_ord_fst_snd where "is_well_ord_fst_snd(A,x) \ (\a[A]. \b[A]. is_well_ord(A,a,b) \ is_snd(A, x, b) \ is_fst(A, x, a))" synthesize "is_well_ord_fst_snd" from_definition assuming "nonempty" arity_theorem for "is_well_ord_fst_snd_fm" lemma (in M_ZF2_trans) separation_well_ord: "separation(##M, \x. is_well_ord(##M,fst(x), snd(x)))" using arity_is_well_ord_fst_snd_fm is_well_ord_iff_sats[symmetric] nonempty fst_closed snd_closed fst_abs snd_abs separation_in_ctm[where env="[]" and \="is_well_ord_fst_snd_fm(0)"] by(simp_all add: is_well_ord_fst_snd_def) sublocale M_ZF2_trans \ M_pre_aleph "##M" using HAleph_wfrec_repl replacement_is_order_body separation_well_ord separation_Pow_rel by unfold_locales (simp_all add: transrec_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def flip:setclass_iff) arity_theorem intermediate for "is_HAleph_fm" lemma arity_is_HAleph_fm: "arity(is_HAleph_fm(2, 1, 0)) = 3" using arity_fun_apply_fm[of "11" 0 1,simplified] arity_is_HAleph_fm' arity_ordinal_fm arity_is_If_fm arity_empty_fm arity_is_Limit_fm arity_is_If_fm arity_is_Limit_fm arity_empty_fm arity_Replace_fm[where i="12" and v=10 and n=3] pred_Un_distrib ord_simp_union by (simp add:FOL_arities) lemma arity_is_Aleph[arity]: "arity(is_Aleph_fm(0, 1)) = 2" unfolding is_Aleph_fm_def using arity_transrec_fm[OF _ _ _ _ arity_is_HAleph_fm] ord_simp_union by simp definition bex_Aleph_rel :: "[i\o,i,i] \ o" where "bex_Aleph_rel(M,x) \ \y. \z\x. y = \\<^bsub>z\<^esub>\<^bsup>M\<^esup>" relationalize "bex_Aleph_rel" "is_bex_Aleph" schematic_goal sats_is_bex_Aleph_fm_auto: "a \ nat \ c \ nat \ env \ list(A) \ a < length(env) \ c < length(env) \ 0 \ A \ is_bex_Aleph(##A, nth(a, env), nth(c, env)) \ A, env \ ?fm(a, c)" unfolding is_bex_Aleph_def by (rule iff_sats | simp)+ synthesize_notc "is_bex_Aleph" from_schematic lemma is_bex_Aleph_fm_type [TC]: "x \ \ \ z \ \ \ is_bex_Aleph_fm(x, z) \ formula" unfolding is_bex_Aleph_fm_def by simp lemma sats_is_bex_Aleph_fm: "x \ \ \ z \ \ \ x < length(env) \ z < length(env) \ env \ list(Aa) \ 0 \ Aa \ (Aa, env \ is_bex_Aleph_fm(x, z)) \ is_bex_Aleph(##Aa,nth(x, env), nth(z, env))" using sats_is_bex_Aleph_fm_auto unfolding is_bex_Aleph_def is_bex_Aleph_fm_def by simp lemma is_bex_Aleph_iff_sats [iff_sats]: "nth(x, env) = xa \ nth(z, env) = za \ x \ \ \ z \ \ \ x < length(env) \ z < length(env) \ env \ list(Aa) \ 0 \ Aa \ is_bex_Aleph(##Aa, xa, za) \ Aa, env \ is_bex_Aleph_fm(x, z)" using sats_is_bex_Aleph_fm by simp arity_theorem for "is_bex_Aleph_fm" lemma (in M_ZF1_trans) separation_is_bex_Aleph: assumes "(##M)(A)" shows "separation(##M,is_bex_Aleph(##M, A))" using assms separation_in_ctm[where env="[A]" and \="is_bex_Aleph_fm(1,0)", OF _ _ _ is_bex_Aleph_iff_sats[symmetric], of "\_.A"] nonempty arity_is_bex_Aleph_fm is_bex_Aleph_fm_type by (simp add:ord_simp_union) lemma (in M_pre_aleph) bex_Aleph_rel_abs: assumes "Ord(u)" "M(u)" "M(v)" shows "is_bex_Aleph(M, u, v) \ bex_Aleph_rel(M,u,v)" unfolding is_bex_Aleph_def bex_Aleph_rel_def using assms is_Aleph_iff transM[of _ u] Ord_in_Ord by simp lemma (in M_ZF2_trans) separation_bex_Aleph_rel: "Ord(x) \ (##M)(x) \ separation(##M, bex_Aleph_rel(##M,x))" using separation_is_bex_Aleph bex_Aleph_rel_abs separation_cong[where P="is_bex_Aleph(##M,x)" and M="##M",THEN iffD1] unfolding bex_Aleph_rel_def by simp sublocale M_ZF2_trans \ M_aleph "##M" using separation_bex_Aleph_rel[unfolded bex_Aleph_rel_def] by unfold_locales sublocale M_ZF1_trans \ M_FiniteFun "##M" using separation_is_function separation_omfunspace by unfold_locales simp sublocale M_ZFC2_trans \ M_cardinal_AC "##M" using lam_replacement_minimum by unfold_locales simp (* TopLevel *) lemma (in M_ZF1_trans) separation_cardinal_rel_lesspoll_rel: "(##M)(\) \ separation(##M, \x. x \\<^bsup>M\<^esup> \)" using separation_in_ctm[where \="( \0 \ 1\ )" and env="[\]"] is_lesspoll_iff nonempty arity_is_cardinal_fm arity_is_lesspoll_fm arity_is_bij_fm ord_simp_union by (simp add:FOL_arities) sublocale M_ZFC2_trans \ M_library "##M" using separation_cardinal_rel_lesspoll_rel lam_replacement_minimum by unfold_locales simp_all locale M_ZF3 = M_ZF2 + assumes ground_replacements3: - "ground_replacement_assm(M,env,replacement_is_order_body_fm)" - "ground_replacement_assm(M,env,wfrec_replacement_order_pred_fm)" - "ground_replacement_assm(M,env,eclose_repl2_intf_fm)" + "ground_replacement_assm(M,env,ordtype_replacement_fm)" + "ground_replacement_assm(M,env,wfrec_ordertype_fm)" + "ground_replacement_assm(M,env,eclose_abs_fm)" "ground_replacement_assm(M,env,wfrec_rank_fm)" - "ground_replacement_assm(M,env,trans_repl_HVFrom_fm)" - "ground_replacement_assm(M,env,eclose_repl1_intf_fm)" - "ground_replacement_assm(M,env,replacement_HAleph_wfrec_repl_body_fm)" - "ground_replacement_assm(M,env,replacement_is_order_eq_map_fm)" + "ground_replacement_assm(M,env,transrec_VFrom_fm)" + "ground_replacement_assm(M,env,eclose_closed_fm)" + "ground_replacement_assm(M,env,wfrec_Aleph_fm)" + "ground_replacement_assm(M,env,omap_replacement_fm)" definition instances3_fms where "instances3_fms \ - { ground_repl_fm(replacement_is_order_body_fm), - ground_repl_fm(wfrec_replacement_order_pred_fm), - ground_repl_fm(eclose_repl2_intf_fm), + { ground_repl_fm(ordtype_replacement_fm), + ground_repl_fm(wfrec_ordertype_fm), + ground_repl_fm(eclose_abs_fm), ground_repl_fm(wfrec_rank_fm), - ground_repl_fm(trans_repl_HVFrom_fm), - ground_repl_fm(eclose_repl1_intf_fm), - ground_repl_fm(replacement_HAleph_wfrec_repl_body_fm), - ground_repl_fm(replacement_is_order_eq_map_fm) }" + ground_repl_fm(transrec_VFrom_fm), + ground_repl_fm(eclose_closed_fm), + ground_repl_fm(wfrec_Aleph_fm), + ground_repl_fm(omap_replacement_fm) }" text\This set has $8$ internalized formulas, corresponding to the total count of previous replacement instances (apart from those $5$ in \<^term>\instances_ground_fms\ and \<^term>\instances_ground_notCH_fms\, -and \<^term>\replacement_dcwit_repl_body_fm\).\ +and \<^term>\dc_abs_fm\).\ definition overhead where "overhead \ instances1_fms \ instances_ground_fms" definition overhead_notCH where "overhead_notCH \ overhead \ instances2_fms \ instances3_fms \ instances_ground_notCH_fms" definition overhead_CH where - "overhead_CH \ overhead_notCH \ { replacement_dcwit_repl_body_fm }" + "overhead_CH \ overhead_notCH \ { dc_abs_fm }" text\Hence, the “overhead” to create a proper extension of a ctm by forcing consists of $7$ replacement instances. To force $\neg\CH$, 21 instances are need, and one further instance is required to force $\CH$.\ lemma instances2_fms_type[TC] : "instances2_fms \ formula" unfolding instances2_fms_def replacement_instances2_defs by (auto simp del: Lambda_in_M_fm_def) lemma overhead_type: "overhead \ formula" using instances1_fms_type instances_ground_fms_type unfolding overhead_def replacement_instances1_defs by simp lemma overhead_notCH_type: "overhead_notCH \ formula" using overhead_type - unfolding overhead_notCH_def replacement_transrec_apply_image_body_fm_def - replacement_is_trans_apply_image_fm_def instances_ground_notCH_fms_def + unfolding overhead_notCH_def recursive_construction_abs_fm_def + recursive_construction_fm_def instances_ground_notCH_fms_def instances2_fms_def instances3_fms_def by (auto simp: replacement_instances1_defs replacement_instances2_defs simp del: Lambda_in_M_fm_def) lemma overhead_CH_type: "overhead_CH \ formula" - using overhead_notCH_type unfolding overhead_CH_def replacement_dcwit_repl_body_fm_def + using overhead_notCH_type unfolding overhead_CH_def dc_abs_fm_def by auto locale M_ZF3_trans = M_ZF2_trans + M_ZF3 locale M_ZFC3 = M_ZFC2 + M_ZF3 locale M_ZFC3_trans = M_ZFC2_trans + M_ZF3_trans + M_ZFC3 locale M_ctm3 = M_ctm2 + M_ZF3_trans locale M_ctm3_AC = M_ctm3 + M_ctm1_AC + M_ZFC3_trans lemma M_satT_imp_M_ZF2: "(M \ ZF) \ M_ZF1(M)" proof - assume "M \ ZF" then have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)" "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)" unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def using ZFC_fm_sats[of M] by simp_all { fix \ env assume "\ \ formula" "env\list(M)" moreover from \M \ ZF\ have "\p\formula. (M, [] \ (ZF_separation_fm(p)))" "\p\formula. (M, [] \ (ZF_replacement_fm(p)))" unfolding ZF_def ZF_schemes_def by auto moreover from calculation have "arity(\) \ succ(length(env)) \ separation(##M, \x. (M, Cons(x, env) \ \))" "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff unfolding replacement_assm_def by simp_all } with fin show "M_ZF1(M)" by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def) qed lemma M_satT_imp_M_ZFC1: shows "(M \ ZFC) \ M_ZFC1(M)" proof - have "(M \ ZF) \ choice_ax(##M) \ M_ZFC1(M)" using M_satT_imp_M_ZF2[of M] unfolding M_ZFC1_def M_ZC_basic_def M_ZF1_def M_AC_def by auto then show ?thesis unfolding ZFC_def by auto qed lemma M_satT_instances1_imp_M_ZF1: assumes "(M \ \Z\ \ {\Replacement(p)\ . p \ instances1_fms })" shows "M_ZF1(M)" proof - from assms have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)" "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)" unfolding ZF_fin_def Zermelo_fms_def ZFC_fm_defs satT_def using ZFC_fm_sats[of M] by simp_all moreover { fix \ env from \M \ \Z\ \ {\Replacement(p)\ . p \ instances1_fms }\ have "\p\formula. (M, [] \ (ZF_separation_fm(p)))" unfolding Zermelo_fms_def ZF_def instances1_fms_def by auto moreover assume "\ \ formula" "env\list(M)" ultimately have "arity(\) \ succ(length(env)) \ separation(##M, \x. (M, Cons(x, env) \ \))" using sats_ZF_separation_fm_iff by simp_all } moreover { fix \ env assume "\ \ instances1_fms" "env\list(M)" moreover from this and \M \ \Z\ \ {\Replacement(p)\ . p \ instances1_fms }\ have "M, [] \ \Replacement(\)\" by auto ultimately have "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_replacement_fm_iff[of \] instances1_fms_type unfolding replacement_assm_def by auto } ultimately show ?thesis unfolding instances1_fms_def by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def) qed theorem M_satT_imp_M_ZF_ground_trans: assumes "Transset(M)" "M \ \Z\ \ {\Replacement(p)\ . p \ overhead}" shows "M_ZF_ground_trans(M)" proof - from \M \ \Z\ \ _\ have "M \ \Z\ \ {\Replacement(p)\ . p \ instances1_fms }" "M \ {\Replacement(p)\ . p \ instances_ground_fms }" unfolding overhead_def by auto then interpret M_ZF1 M using M_satT_instances1_imp_M_ZF1 by simp from \Transset(M)\ interpret M_ZF1_trans M using M_satT_imp_M_ZF2 by unfold_locales { fix \ env assume "\ \ instances_ground_fms" "env\list(M)" moreover from this and \M \ {\Replacement(p)\ . p \ instances_ground_fms}\ have "M, [] \ \Replacement(\)\" by auto ultimately have "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_replacement_fm_iff[of \] instances_ground_fms_type unfolding replacement_assm_def by auto } then show ?thesis unfolding instances_ground_fms_def by unfold_locales (simp_all add:replacement_assm_def) qed theorem M_satT_imp_M_ZF_ground_notCH_trans: assumes "Transset(M)" "M \ \Z\ \ {\Replacement(p)\ . p \ overhead_notCH}" shows "M_ZF_ground_notCH_trans(M)" proof - from assms interpret M_ZF_ground_trans M using M_satT_imp_M_ZF_ground_trans unfolding overhead_notCH_def by force { fix \ env assume "\ \ instances_ground_notCH_fms" "env\list(M)" moreover from this and assms have "M, [] \ \Replacement(\)\" unfolding overhead_notCH_def by auto ultimately have "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_replacement_fm_iff[of \] instances_ground_notCH_fms_type unfolding replacement_assm_def by auto } then show ?thesis by unfold_locales (simp_all add:replacement_assm_def instances_ground_notCH_fms_def) qed theorem M_satT_imp_M_ZF_ground_CH_trans: assumes "Transset(M)" "M \ \Z\ \ {\Replacement(p)\ . p \ overhead_CH }" shows "M_ZF_ground_CH_trans(M)" proof - from assms interpret M_ZF_ground_notCH_trans M using M_satT_imp_M_ZF_ground_notCH_trans unfolding overhead_CH_def by auto { fix env assume "env \ list(M)" moreover from assms - have "M, [] \ \Replacement(replacement_dcwit_repl_body_fm)\" + have "M, [] \ \Replacement(dc_abs_fm)\" unfolding overhead_CH_def by auto ultimately - have "arity(replacement_dcwit_repl_body_fm) \ succ(succ(length(env))) - \ strong_replacement(##M,\x y. sats(M,replacement_dcwit_repl_body_fm,Cons(x,Cons(y, env))))" - using sats_ZF_replacement_fm_iff[of replacement_dcwit_repl_body_fm] + have "arity(dc_abs_fm) \ succ(succ(length(env))) + \ strong_replacement(##M,\x y. sats(M,dc_abs_fm,Cons(x,Cons(y, env))))" + using sats_ZF_replacement_fm_iff[of dc_abs_fm] unfolding replacement_assm_def - by (auto simp:replacement_dcwit_repl_body_fm_def) + by (auto simp:dc_abs_fm_def) } then show ?thesis by unfold_locales (simp_all add:replacement_assm_def) qed lemma (in M_Z_basic) M_satT_Zermelo_fms: "M \ \Z\" using upair_ax Union_ax power_ax extensionality foundation_ax infinity_ax separation_ax sats_ZF_separation_fm_iff unfolding Zermelo_fms_def ZF_fin_def by auto lemma (in M_ZFC1) M_satT_ZC: "M \ ZC" using upair_ax Union_ax power_ax extensionality foundation_ax infinity_ax separation_ax sats_ZF_separation_fm_iff choice_ax unfolding ZC_def Zermelo_fms_def ZF_fin_def by auto locale M_ZF = M_Z_basic + assumes replacement_ax:"replacement_assm(M,env,\)" sublocale M_ZF \ M_ZF3 using replacement_ax by unfold_locales (simp_all add:ground_replacement_assm_def) lemma M_satT_imp_M_ZF: " M \ ZF \ M_ZF(M)" proof - assume "M \ ZF" then have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)" "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)" unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def using ZFC_fm_sats[of M] by simp_all { fix \ env assume "\ \ formula" "env\list(M)" moreover from \M \ ZF\ have "\p\formula. (M, [] \ (ZF_separation_fm(p)))" "\p\formula. (M, [] \ (ZF_replacement_fm(p)))" unfolding ZF_def ZF_schemes_def by auto moreover from calculation have "arity(\) \ succ(length(env)) \ separation(##M, \x. (M, Cons(x, env) \ \))" "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff unfolding replacement_assm_def by simp_all } with fin show "M_ZF(M)" unfolding M_ZF_def M_Z_basic_def M_ZF_axioms_def replacement_assm_def by simp qed lemma (in M_ZF) M_satT_ZF: "M \ ZF" using upair_ax Union_ax power_ax extensionality foundation_ax infinity_ax separation_ax sats_ZF_separation_fm_iff replacement_ax sats_ZF_replacement_fm_iff unfolding ZF_def ZF_schemes_def ZF_fin_def replacement_assm_def by auto lemma M_ZF_iff_M_satT: "M_ZF(M) \ (M \ ZF)" using M_ZF.M_satT_ZF M_satT_imp_M_ZF by auto locale M_ZFC = M_ZF + M_ZC_basic sublocale M_ZFC \ M_ZFC3 by unfold_locales lemma M_ZFC_iff_M_satT: notes iff_trans[trans] shows "M_ZFC(M) \ (M \ ZFC)" proof - have "M_ZFC(M) \ (M \ ZF) \ choice_ax(##M)" using M_ZF_iff_M_satT unfolding M_ZFC_def M_ZC_basic_def M_AC_def M_ZF_def by auto also have " \ \ M \ ZFC" unfolding ZFC_def by auto ultimately show ?thesis by simp qed lemma M_satT_imp_M_ZF3: "(M \ ZF) \ M_ZF3(M)" proof assume "M \ ZF" then interpret M_ZF M using M_satT_imp_M_ZF by simp show "M_ZF3(M)" by unfold_locales qed lemma M_satT_imp_M_ZFC3: shows "(M \ ZFC) \ M_ZFC3(M)" proof assume "M \ ZFC" then interpret M_ZFC M using M_ZFC_iff_M_satT by simp show "M_ZFC3(M)" by unfold_locales qed lemma M_satT_overhead_imp_M_ZF3: "(M \ ZC \ {\Replacement(p)\ . p \ overhead_notCH}) \ M_ZFC3(M)" proof assume "M \ ZC \ {\Replacement(p)\ . p \ overhead_notCH}" then have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)" "choice_ax(##M)" "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)" unfolding ZC_def ZF_fin_def Zermelo_fms_def ZFC_fm_defs satT_def using ZFC_fm_sats[of M] by simp_all moreover { fix \ env from \M \ ZC \ {\Replacement(p)\ . p \ overhead_notCH}\ have "\p\formula. (M, [] \ (ZF_separation_fm(p)))" unfolding ZC_def Zermelo_fms_def ZF_def by auto moreover assume "\ \ formula" "env\list(M)" ultimately have "arity(\) \ succ(length(env)) \ separation(##M, \x. (M, Cons(x, env) \ \))" using sats_ZF_separation_fm_iff by simp_all } moreover { fix \ env assume "\ \ overhead_notCH" "env\list(M)" moreover from this and \M \ ZC \ {\Replacement(p)\ . p \ overhead_notCH}\ have "M, [] \ \Replacement(\)\" by auto ultimately have "arity(\) \ succ(succ(length(env))) \ strong_replacement(##M,\x y. sats(M,\,Cons(x,Cons(y, env))))" using sats_ZF_replacement_fm_iff[of \] overhead_notCH_type unfolding replacement_assm_def by auto } ultimately show "M_ZFC3(M)" unfolding overhead_def overhead_notCH_def instances1_fms_def instances2_fms_def instances3_fms_def by unfold_locales (simp_all add:replacement_assm_def ground_replacement_assm_def) qed end \ No newline at end of file diff --git a/thys/Independence_CH/document/root.tex b/thys/Independence_CH/document/root.tex --- a/thys/Independence_CH/document/root.tex +++ b/thys/Independence_CH/document/root.tex @@ -1,124 +1,125 @@ \documentclass[11pt,a4paper,english]{article} \usepackage{isabelle,isabellesym} \usepackage[numbers]{natbib} \usepackage{babel} +\renewcommand{\isasymbbbP}{\isamath{\mathbb{P}}} \usepackage{relsize} \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\itshape\smaller} \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\itshape\smaller} \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed \usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \, \, \, \, %\ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} \newcommand{\forces}{\Vdash} \newcommand{\dom}{\mathsf{dom}} \renewcommand{\isacharunderscorekeyword}{\mbox{\_}} \renewcommand{\isacharunderscore}{\mbox{\_}} \renewcommand{\isasymtturnstile}{\isamath{\Vdash}} \renewcommand{\isacharminus}{-} \newcommand{\session}[1]{\textit{#1}} \newcommand{\theory}[1]{\texttt{#1}} \newcommand{\axiomas}[1]{\mathit{#1}} \newcommand{\ZFC}{\axiomas{ZFC}} \newcommand{\ZF}{\axiomas{ZF}} \newcommand{\AC}{\axiomas{AC}} \newcommand{\CH}{\axiomas{CH}} \newcommand{\calV}{\mathcal{V}} \begin{document} \title{The Independence of the Continuum Hypothesis in Isabelle/ZF} \author{Emmanuel Gunther\thanks{Universidad Nacional de C\'ordoba. Facultad de Matem\'atica, Astronom\'{\i}a, F\'{\i}sica y Computaci\'on.} \and Miguel Pagano\footnotemark[1] \and Pedro S\'anchez Terraf\footnotemark[1] \thanks{Centro de Investigaci\'on y Estudios de Matem\'atica (CIEM-FaMAF), Conicet. C\'ordoba. Argentina. Supported by Secyt-UNC project 33620180100465CB.} \and Mat\'{\i}as Steinberg\footnotemark[1] } \maketitle \begin{abstract} We redeveloped our formalization of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of $\ZFC$, we construct proper generic extensions that satisfy the Continuum Hypothesis and its negation. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex \section{Introduction} We formalize the theory of forcing. We work on top of the Isabelle/ZF framework developed by \citet{DBLP:journals/jar/PaulsonG96}. Our mechanization is described in more detail in our papers \cite{2018arXiv180705174G} (LSFA 2018), \cite{2019arXiv190103313G}, and \cite{2020arXiv200109715G} (IJCAR 2020). The main entry point of the present session is \theory{Definitions\_Main.thy} (Section~\ref{sec:main-definitions}), in which a path from fundamental set theoretic concepts formalized in Isabelle reaching to our main theorems is expounded. Cross-references to major milestones are provided there. In order to provide evidence for the correctness of several of our relativized definitions, we needed to assume the Axiom of Choice ($\AC$) during the aforementioned theory. Nevertheless, the whole of our development is independent of $\AC$, and the theory \theory{CH.thy} already provides all of our results and does not import that axiom. \subsection*{Release notes} \label{sec:release-notes} Previous versions of this development can be found at \url{https://cs.famaf.unc.edu.ar/~pedro/forcing/}. % generated text of all theories \input{session} % optional bibliography \bibliographystyle{root} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: