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,1302 +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 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 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 rec_constr_abs_fm where "rec_constr_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 recursive_construction_fm where "recursive_construction_fm \ is_trans_apply_image_body_fm(3,2,0,1)" +definition rec_constr_fm where "rec_constr_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 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,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, lam_replacement_check_fm }" lemmas replacement_instances_ground_defs = 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,recursive_construction_abs_fm)" - "replacement_assm(M,env,recursive_construction_fm)" + "replacement_assm(M,env,rec_constr_abs_fm)" + "replacement_assm(M,env,rec_constr_fm)" definition instances_ground_notCH_fms where "instances_ground_notCH_fms \ - { recursive_construction_abs_fm, - recursive_construction_fm }" + { rec_constr_abs_fm, + rec_constr_fm }" lemma instances_ground_notCH_fms_type[TC]: "instances_ground_notCH_fms \ formula" - unfolding instances_ground_notCH_fms_def recursive_construction_abs_fm_def - recursive_construction_fm_def + unfolding instances_ground_notCH_fms_def rec_constr_abs_fm_def + rec_constr_fm_def by simp -declare (in M_ZF_ground_notCH) recursive_construction_abs_fm_def[simp] - recursive_construction_fm_def[simp] +declare (in M_ZF_ground_notCH) rec_constr_abs_fm_def[simp] + rec_constr_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,dc_abs_fm)" 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 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,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 \ { ordtype_replacement_fm, wfrec_ordertype_fm, wfrec_Aleph_fm, omap_replacement_fm }" lemmas replacement_instances2_defs = 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,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,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(ordtype_replacement_fm), ground_repl_fm(wfrec_ordertype_fm), ground_repl_fm(eclose_abs_fm), ground_repl_fm(wfrec_rank_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>\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 \ { 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 recursive_construction_abs_fm_def - recursive_construction_fm_def instances_ground_notCH_fms_def + unfolding overhead_notCH_def rec_constr_abs_fm_def + rec_constr_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 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(dc_abs_fm)\" unfolding overhead_CH_def by auto ultimately 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: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/Transitive_Models/document/root.tex b/thys/Transitive_Models/document/root.tex --- a/thys/Transitive_Models/document/root.tex +++ b/thys/Transitive_Models/document/root.tex @@ -1,191 +1,206 @@ \documentclass[11pt,a4paper,english]{article} \usepackage{isabelle,isabellesym} \usepackage[numbers]{natbib} \usepackage{babel} \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}} \begin{document} \title{Transitive Models of Fragments of 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 extend the ZF-Constructibility library by relativizing theories of the Isabelle/ZF and Delta System Lemma sessions to a transitive class. We also relativize Paulson's work on Aleph and our former treatment of the Axiom of Dependent Choices. This work is a prerequisite to our formalization of the independence of the Continuum Hypothesis. \end{abstract} \tableofcontents % sane default for proof documents \parindent 0pt\parskip 0.5ex \section{Introduction} Relativization of concepts is a key tool to obtain results in forcing, as it is explained in \cite[Sect.~3]{2020arXiv200109715G} and elsewhere. In this session, we cast some theories in relative form, in a way that they now refer to a fixed class $M$ as the universe of discourse. Whenever it was possible, we tried to minimize the changes to the structure and proof scripts of the absolute concepts. For this reason, some comments of the original text as well as outdated \textbf{apply} commands appear profusely in the following theories. A repeated pattern that appears is that the relativized result can be proved \emph{mutatis mutandis}, with remaining proof obligations that the objects constructed actually belong to the model $M$. Another aspect was that the management of higher order constructs always posed some extra problems, already noted by Paulson \cite[Sect.~7.3]{MR2051585}. In the theory \theory{Lambda\_Replacement} we introduce a new locale assuming two instances of separation and six instances of ``lambda replacements'' (i.e., replacements using definable functions of the form $\lambda x y. y=\langle x, f(x) \rangle$) that allow some form of compositionality of further instances of separations and replacements. We proceed to enumerate the theories that were ``ported'' to relative form, briefly commenting on each of them. Below, we refer to the original theories as the \emph{source} and, correspondingly, call \emph{target} the relativized version. We omit the \theory{.thy} suffixes. \begin{enumerate} \item From \session{ZF}: \begin{enumerate} \item \theory{Univ}. Here we decided to relativize only the term \isatt{Vfrom} that constructs the cumulative hierarchy up to some ordinal length and starting from an arbitrary set. \item \theory{Cardinal}. There are two targets for this source, \theory{Least} and \theory{Cardinal\_Relative}. Both require some fair amount of preparation, trying to take advantage of absolute concepts. It is not straightforward to compare source and targets in a line-by-line fashion at this point. \item \theory{CardinalArith}. The hardest part was to formalize the cardinal successor function and ordertypes. We also disregarded the part treating finite cardinals since it is an absolute concept. Apart from that, the relative version closely parallels the source. \item \theory{Cardinal\_AC}. After some boilerplate, porting was rather straightforward, excepting cardinal arithmetic involving the higher-order union operator. \end{enumerate} \item From \session{ZF-Constructible}: \begin{enumerate} \item \theory{Normal}. The target here is \theory{Aleph\_Relative} since that is the only concept that we ported. Instead of porting all the machinery of normal functions (since it involved higher-order variables), we particularized the results for the Aleph function. We also used an alternative definition of the latter that worked better with our relativization discipline. \end{enumerate} \item From \session{Delta\_System\_Lemma}: \begin{enumerate} \item \theory{ZF\_Library}. The target includes a big section of auxiliary lemmas and commands that aid the relativization. We needed to make explicit the witnesses (mainly functions) in some of the existential results proved in the source, since only in that way we would be able to show that they belonged to the model. \item \theory{Cardinal\_Library}. Porting was relatively straightforward; most of the extra work laid in adjusting locale assumptions to obtain an appropriate context to state and prove the theorems. \item \theory{Delta\_System}. Same comments as in the case of \theory{Cardinal\_Library} apply here. \end{enumerate} \item From \session{Forcing}: \begin{enumerate} \item \theory{Pointed\_DC}. This case was similar to \theory{Cardinal\_AC} above, although a bit of care was needed to handle the recursive construction. Also, a fraction of the theory \theory{AC} from \session{ZF} was ported here as it was a prerequisite. A complete relativization of \theory{AC} would be desirable but still missing. \end{enumerate} \end{enumerate} -Finally, we had to repeat some material from \theory{Relative} in -\session{ZF-Constructible} (in our theory \theory{M\_Basic\_No\_Repl}) +Finally, there are some repetitions from \session{ZF-Constructible} in +the present project. We had to duplicate some material from +\theory{Relative} in our theory \theory{M\_Basic\_No\_Repl} in order to eliminate one replacement instance appearing in the locale -\texttt{M\_Basic}. +\texttt{M\_Basic}. The same goes for theories +\theory{DPow\_absolute}, +\theory{Datatype\_absolute}, +\theory{Internalizations}, +\theory{Internalize}, +\theory{Rank\_Separation}, +\theory{Rec\_Separation}, +\theory{Recursion\_Thms}, +\theory{Relativization}, and +\theory{Satisfies\_absolute}, that were modified to remodularize the +locale structure (namely, by eliminating the dependence of locale +\texttt{M\_eclose} on \texttt{M\_datatypes}, which defines lists and +formulas). In order to get the rest of the top-level theories of +\session{ZF-Constructible} to work, we added a new theory called +\theory{Eclose\_Absolute}. % generated text of all theories \input{session} \bibliographystyle{root} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% ispell-local-dictionary: "american" %%% End: