Theory ZF_Trans_Interpretations

sectionFurther 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:
  "BM  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:
  "AM  rM  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 ― ‹localeM_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 :"Anat  rnat  omap_wfrec_body(A,r)formula"
  unfolding omap_wfrec_body_def by simp

lemma arity_aux : "Anat  rnat  arity(omap_wfrec_body(A,r)) = (9+ωA)  (9+ω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: "Anat  rnat 
  arity(is_wfrec_fm(omap_wfrec_body(A,r),succ(succ(succ(r))), 1, 0)) =
  (4+ωA)  (4+ωr)"
  using Arities.arity_is_wfrec_fm[OF _ _ _ _ _ arity_aux,of A r "3+ωr" 1 0] pred_Un_distrib
    union_abs1 union_abs2 type_omap_wfrec_body_fm
  by auto

lemma arity_isordermap: "Anat  rnat dnat
   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+ωA)  (4+ωr)",OF _ _ _ _ arity_omap_wfrec,
      unfolded omap_wfrec_body_def] pred_Un_distrib union_abs1
  by auto

lemma arity_is_ordertype: "Anat  rnat dnat
   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:
  "AM  rM  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':
  "AM  rM  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 :: "[io,i,i]  o" where
  "bex_Aleph_rel(M,x)  λy. zx. y = ℵ⇘z⇙⇗M"

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 ≺⇗Mκ)"
  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) }"

textThis set has $8$ internalized formulas, corresponding to the total
count of previous replacement instances (apart from those $5$ in
terminstances_ground_fms and terminstances_ground_notCH_fms,
and termdc_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 }"

textHence, 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 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" "envlist(M)"
    moreover from M  ZF
    have "pformula. (M, []  (ZF_separation_fm(p)))"
      "pformula. (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 "pformula. (M, []  (ZF_separation_fm(p)))"
      unfolding Zermelo_fms_def ZF_def instances1_fms_def
      by auto
    moreover
    assume "φ  formula" "envlist(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" "envlist(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" "envlist(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" "envlist(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" "envlist(M)"
    moreover from M  ZF
    have "pformula. (M, []  (ZF_separation_fm(p)))"
      "pformula. (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 "pformula. (M, []  (ZF_separation_fm(p)))"
      unfolding ZC_def Zermelo_fms_def ZF_def by auto
    moreover
    assume "φ  formula" "envlist(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" "envlist(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