Theory Interface

section‹Interface between set models and Constructibility›

text‹This theory provides an interface between Paulson's
relativization results and set models of ZFC. In particular,
it is used to prove that the locale termforcing_data is
a sublocale of all relevant locales in sessionZF-Constructible
(termM_trivial, termM_basic, termM_eclose, etc).

In order to interpret the locales in sessionZF-Constructible we
introduce new locales, each stronger than the previous one, assuming
only the instances of Replacement needed to interpret the subsequent
locales of that session. From the start we assume Separation for
every internalized formula (with one parameter, but this is not a
problem since we can use pairing).›

theory Interface
  imports
    Fm_Definitions
    Transitive_Models.Cardinal_AC_Relative
begin

locale M_Z_basic =
  fixes M
  assumes
    upair_ax:      "upair_ax(##M)" and
    Union_ax:      "Union_ax(##M)" and
    power_ax:      "power_ax(##M)" and
    extensionality:"extensionality(##M)" and
    foundation_ax: "foundation_ax(##M)" and
    infinity_ax:   "infinity_ax(##M)" and
    separation_ax: "φ  formula  env  list(M) 
                    arity(φ)  1 +ω length(env) 
                    separation(##M,λx. (M, [x] @ env  φ))"

locale M_transset =
  fixes M
  assumes
    trans_M:       "Transset(M)"

locale M_Z_trans = M_Z_basic + M_transset

locale M_ZF1 = M_Z_basic +
  assumes
    replacement_ax1:
    "replacement_assm(M,env,eclose_closed_fm)"
    "replacement_assm(M,env,eclose_abs_fm)"
    "replacement_assm(M,env,wfrec_rank_fm)"
    "replacement_assm(M,env,transrec_VFrom_fm)"

definition instances1_fms where "instances1_fms 
  { eclose_closed_fm,
    eclose_abs_fm,
    wfrec_rank_fm,
    transrec_VFrom_fm
 }"

text‹This set has 4 internalized formulas.›

lemmas replacement_instances1_defs =
  list_repl1_intf_fm_def list_repl2_intf_fm_def
  formula_repl1_intf_fm_def formula_repl2_intf_fm_def
  eclose_closed_fm_def eclose_abs_fm_def
  wfrec_rank_fm_def transrec_VFrom_fm_def tl_repl_intf_fm_def

lemma instances1_fms_type[TC]: "instances1_fms  formula"
  using Lambda_in_M_fm_type
  unfolding replacement_instances1_defs instances1_fms_def by simp

declare (in M_ZF1) replacement_instances1_defs[simp]

locale M_ZF1_trans = M_ZF1 + M_Z_trans

context M_Z_trans
begin

lemmas transitivity = Transset_intf[OF trans_M]

subsection‹Interface with termM_trivial

lemma zero_in_M:  "0  M"
proof -
  obtain z where "empty(##M,z)"  "zM"
    using empty_intf[OF infinity_ax]
    by auto
  moreover from this
  have "z=0"
    using transitivity empty_def
    by auto
  ultimately
  show ?thesis
    by simp
qed

lemma separation_in_ctm :
  assumes
    "φ  formula" "envlist(M)"
    "arity(φ)  1 +ω length(env)" and
    satsQ: "x. xM  (M, [x]@env  φ)  Q(x)"
  shows
    "separation(##M,Q)"
  using assms separation_ax satsQ transitivity
    separation_cong[of "##M" "λy. (M, [y]@env  φ)" "Q"]
  by simp

end ― ‹localeM_Z_trans

locale M_ZC_basic = M_Z_basic + M_AC "##M"

locale M_ZFC1 = M_ZF1 + M_ZC_basic

locale M_ZFC1_trans = M_ZF1_trans + M_ZFC1

sublocale M_Z_trans  M_trans "##M"
  using transitivity zero_in_M exI[of "λx. xM"]
  by unfold_locales simp_all

sublocale M_Z_trans  M_trivial "##M"
  using upair_ax Union_ax by unfold_locales

subsection‹Interface with termM_basic

definition Intersection where
  "Intersection(N,B,x)  (y[N]. yB  xy)"

synthesize "Intersection" from_definition "Intersection" assuming "nonempty"
arity_theorem for "Intersection_fm"

definition CartProd where
  "CartProd(N,B,C,z)  (x[N]. xB  (y[N]. yC  pair(N,x,y,z)))"

synthesize "CartProd" from_definition "CartProd" assuming "nonempty"
arity_theorem for "CartProd_fm"

definition ImageSep where
  "ImageSep(N,B,r,y)  (p[N]. pr  (x[N]. xB  pair(N,x,y,p)))"

synthesize "ImageSep" from_definition  assuming "nonempty"
arity_theorem for "ImageSep_fm"

definition Converse where
  "Converse(N,R,z)  p[N]. pR  (x[N].y[N]. pair(N,x,y,p)  pair(N,y,x,z))"

synthesize "Converse" from_definition "Converse" assuming "nonempty"
arity_theorem for "Converse_fm"

definition Restrict where
  "Restrict(N,A,z)  x[N]. xA  (y[N]. pair(N,x,y,z))"

synthesize "Restrict" from_definition "Restrict" assuming "nonempty"
arity_theorem for "Restrict_fm"

definition Comp where
  "Comp(N,R,S,xz)  x[N]. y[N]. z[N]. xy[N]. yz[N].
              pair(N,x,z,xz)  pair(N,x,y,xy)  pair(N,y,z,yz)  xyS  yzR"

synthesize "Comp" from_definition "Comp" assuming "nonempty"
arity_theorem for "Comp_fm"

definition Pred where
  "Pred(N,R,X,y)  p[N]. pR  pair(N,y,X,p)"

synthesize "Pred" from_definition "Pred" assuming "nonempty"
arity_theorem for "Pred_fm"

definition is_Memrel where
  "is_Memrel(N,z)  x[N]. y[N]. pair(N,x,y,z)  x  y"

synthesize "is_Memrel" from_definition "is_Memrel" assuming "nonempty"
arity_theorem for "is_Memrel_fm"

definition RecFun where
  "RecFun(N,r,f,g,a,b,x)  xa[N]. xb[N].
                    pair(N,x,a,xa)  xa  r  pair(N,x,b,xb)  xb  r 
                    (fx[N]. gx[N]. fun_apply(N,f,x,fx)  fun_apply(N,g,x,gx) 
                                     fx  gx)"

synthesize "RecFun" from_definition "RecFun" assuming "nonempty"
arity_theorem for "RecFun_fm"

arity_theorem for "rtran_closure_mem_fm"

synthesize "wellfounded_trancl" from_definition assuming "nonempty"
arity_theorem for "wellfounded_trancl_fm"

context M_Z_trans
begin

lemma inter_sep_intf :
  assumes "AM"
  shows "separation(##M,λx . yM . yA  xy)"
  using assms separation_in_ctm[of "Intersection_fm(1,0)" "[A]" "Intersection(##M,A)"]
    Intersection_iff_sats[of 1 "[_,A]" A 0 _ M] arity_Intersection_fm Intersection_fm_type
    ord_simp_union zero_in_M
  unfolding Intersection_def
  by simp

lemma diff_sep_intf :
  assumes "BM"
  shows "separation(##M,λx . xB)"
  using assms separation_in_ctm[of "Neg(Member(0,1))" "[B]" "λx . xB"] ord_simp_union
  by simp

lemma cartprod_sep_intf :
  assumes "AM" and "BM"
  shows "separation(##M,λz. xM. xA  (yM. yB  pair(##M,x,y,z)))"
  using assms separation_in_ctm[of "CartProd_fm(1,2,0)" "[A,B]" "CartProd(##M,A,B)"]
    CartProd_iff_sats[of 1 "[_,A,B]" A 2 B 0 _ M] arity_CartProd_fm  CartProd_fm_type
    ord_simp_union zero_in_M
  unfolding CartProd_def
  by simp

lemma image_sep_intf :
  assumes "AM" and "BM"
  shows "separation(##M, λy. pM. pB  (xM. xA  pair(##M,x,y,p)))"
  using assms separation_in_ctm[of "ImageSep_fm(1,2,0)" "[A,B]" "ImageSep(##M,A,B)"]
    ImageSep_iff_sats[of 1 "[_,A,B]" _ 2 _ 0 _ M] arity_ImageSep_fm ImageSep_fm_type
    ord_simp_union zero_in_M
  unfolding ImageSep_def
  by simp

lemma converse_sep_intf :
  assumes "RM"
  shows "separation(##M,λz. pM. pR  (xM.yM. pair(##M,x,y,p)  pair(##M,y,x,z)))"
  using assms separation_in_ctm[of "Converse_fm(1,0)" "[R]" "Converse(##M,R)"]
    Converse_iff_sats[of 1 "[_,R]" _ 0 _ M] arity_Converse_fm Converse_fm_type
    ord_simp_union zero_in_M
  unfolding Converse_def
  by simp

lemma restrict_sep_intf :
  assumes "AM"
  shows "separation(##M,λz. xM. xA  (yM. pair(##M,x,y,z)))"
  using assms separation_in_ctm[of "Restrict_fm(1,0)" "[A]" "Restrict(##M,A)"]
    Restrict_iff_sats[of 1 "[_,A]" _ 0 _ M] arity_Restrict_fm Restrict_fm_type
    ord_simp_union zero_in_M
  unfolding Restrict_def
  by simp

lemma comp_sep_intf :
  assumes "RM" and "SM"
  shows "separation(##M,λxz. xM. yM. zM. xyM. yzM.
           pair(##M,x,z,xz)  pair(##M,x,y,xy)  pair(##M,y,z,yz)  xyS  yzR)"
  using assms separation_in_ctm[of "Comp_fm(1,2,0)" "[R,S]" "Comp(##M,R,S)"]
    Comp_iff_sats[of 1 "[_,R,S]" _ 2 _ 0 _ M] arity_Comp_fm Comp_fm_type
    ord_simp_union zero_in_M
  unfolding Comp_def
  by simp

lemma pred_sep_intf:
  assumes "RM" and "XM"
  shows "separation(##M, λy. pM. pR  pair(##M,y,X,p))"
  using assms separation_in_ctm[of "Pred_fm(1,2,0)" "[R,X]" "Pred(##M,R,X)"]
    Pred_iff_sats[of 1 "[_,R,X]" _ 2 _ 0 _ M] arity_Pred_fm Pred_fm_type
    ord_simp_union zero_in_M
  unfolding Pred_def
  by simp

lemma memrel_sep_intf:
  "separation(##M, λz. xM. yM. pair(##M,x,y,z)  x  y)"
  using separation_in_ctm[of "is_Memrel_fm(0)" "[]" "is_Memrel(##M)"]
    is_Memrel_iff_sats[of 0 "[_]" _ M] arity_is_Memrel_fm is_Memrel_fm_type
    ord_simp_union zero_in_M
  unfolding is_Memrel_def
  by simp

lemma is_recfun_sep_intf :
  assumes "rM" "fM" "gM" "aM" "bM"
  shows "separation(##M,λx. xaM. xbM.
                    pair(##M,x,a,xa)  xa  r  pair(##M,x,b,xb)  xb  r 
                    (fxM. gxM. fun_apply(##M,f,x,fx)  fun_apply(##M,g,x,gx) 
                                     fx  gx))"
  using assms separation_in_ctm[of "RecFun_fm(1,2,3,4,5,0)" "[r,f,g,a,b]" "RecFun(##M,r,f,g,a,b)"]
    RecFun_iff_sats[of 1 "[_,r,f,g,a,b]" _ 2 _ 3 _ 4 _ 5 _ 0 _ M] arity_RecFun_fm RecFun_fm_type
    ord_simp_union zero_in_M
  unfolding RecFun_def
  by simp

lemmas M_basic_sep_instances =
  inter_sep_intf diff_sep_intf cartprod_sep_intf
  image_sep_intf converse_sep_intf restrict_sep_intf
  pred_sep_intf memrel_sep_intf comp_sep_intf is_recfun_sep_intf

end ― ‹localeM_Z_trans

sublocale M_Z_trans  M_basic_no_repl "##M"
  using power_ax M_basic_sep_instances
  by unfold_locales simp_all

lemma Replace_eq_Collect:
  assumes "x y y'. xA  P(x,y)  P(x,y')  y=y'" "{y . x  A, P(x, y)}  B"
  shows "{y . x  A, P(x, y)} = {yB . xA. P(x,y)}"
  using assms by blast

context M_Z_trans
begin

lemma Pow_inter_M_closed: assumes "A  M" shows "Pow(A)  M  M"
proof -
  have "{a  Pow(A) . a  M} = Pow(A)  M" by auto
  then
  show ?thesis
    using power_ax powerset_abs assms unfolding power_ax_def
    by auto
qed

lemma Pow'_inter_M_closed: assumes "A  M" shows "{a  Pow(A) . a  M}  M"
  using power_ax powerset_abs assms unfolding power_ax_def by auto

end ― ‹localeM_Z_trans

context M_basic_no_repl
begin

lemma Replace_funspace_succ_rep_intf_sub:
  assumes
    "M(A)" "M(n)"
  shows
    "{z . p  A, funspace_succ_rep_intf_rel(M,p,z,n)}
       Pow⇗M⇖(Pow⇗M⇖(domain(A)  ({n} × range(A))  (({n} × range(A)))))"
  unfolding funspace_succ_rep_intf_rel_def using assms mem_Pow_rel_abs
  by clarsimp (auto simp: cartprod_def)

lemma funspace_succ_rep_intf_uniq:
  assumes
    "funspace_succ_rep_intf_rel(M,p,z,n)" "funspace_succ_rep_intf_rel(M,p,z',n)"
  shows
    "z = z'"
  using assms unfolding funspace_succ_rep_intf_rel_def by auto

lemma Replace_funspace_succ_rep_intf_eq:
  assumes
    "M(A)" "M(n)"
  shows
    "{z . p  A, funspace_succ_rep_intf_rel(M,p,z,n)} =
     {z  Pow⇗M⇖(Pow⇗M⇖(domain(A)  ({n} × range(A))  (({n} × range(A))))) .
        pA. funspace_succ_rep_intf_rel(M,p,z,n)}"
  using assms Replace_eq_Collect[OF funspace_succ_rep_intf_uniq, of A,
      OF _ _ Replace_funspace_succ_rep_intf_sub[of A n], of "λx y z. x" "λx y z. n"]
  by (intro equalityI)
    (auto dest:transM simp:funspace_succ_rep_intf_rel_def)

end ― ‹localeM_basic_no_repl

definition fsri where
  "fsri(N,A,B)  λz. pA. f[N]. b[N]. p = f, b  z = {cons(B, b, f)}"

relationalize "fsri" "is_fsri"
synthesize "is_fsri" from_definition assuming "nonempty"
arity_theorem for "is_fsri_fm"


context M_Z_trans
begin

lemma separation_fsri:
  "(##M)(A)  (##M)(B)  separation(##M, is_fsri(##M,A,B))"
  using separation_in_ctm[where env="[A,B]" and φ="is_fsri_fm(1,2,0)"]
    zero_in_M is_fsri_iff_sats[symmetric] arity_is_fsri_fm is_fsri_fm_type
  by (simp_all add: ord_simp_union)

lemma separation_funspace_succ_rep_intf_rel:
  "(##M)(A)  (##M)(B)  separation(##M, λz. pA. funspace_succ_rep_intf_rel(##M,p,z,B))"
  using separation_fsri zero_in_M
  by (rule_tac separation_cong[THEN iffD1, of _ "is_fsri(##M,A,B)"])
    (auto simp flip:setclass_iff dest:transM
      simp:is_fsri_def funspace_succ_rep_intf_rel_def, force)

lemma Replace_funspace_succ_rep_intf_in_M:
  assumes
    "A  M" "n  M"
  shows
    "{z . p  A, funspace_succ_rep_intf_rel(##M,p,z,n)}  M"
proof -
  have "(##M)({z  Pow⇗M⇖(Pow⇗M⇖(domain(A)  ({n} × range(A))  (({n} × range(A))))) .
        pA. funspace_succ_rep_intf_rel(##M,p,z,n)})"
    using assms separation_funspace_succ_rep_intf_rel
    by (intro separation_closed) (auto simp flip:setclass_iff)
  with assms
  show ?thesis
    using Replace_funspace_succ_rep_intf_eq by auto
qed

lemma funspace_succ_rep_intf:
  assumes "nM"
  shows
    "strong_replacement(##M,
          λp z. fM. bM. nbM. cnbfM.
                pair(##M,f,b,p)  pair(##M,n,b,nb)  is_cons(##M,nb,f,cnbf) 
                upair(##M,cnbf,cnbf,z))"
  using assms pair_in_M_iff[simplified] cons_closed[simplified]
  unfolding strong_replacement_def univalent_def
  apply (clarsimp, rename_tac A)
  apply (rule_tac x="{z . p  A, funspace_succ_rep_intf_rel(##M,p,z,n)}" in bexI)
   apply (auto simp:funspace_succ_rep_intf_rel_def
      Replace_funspace_succ_rep_intf_in_M[unfolded funspace_succ_rep_intf_rel_def, simplified])
  done

end ― ‹localeM_Z_trans

sublocale M_Z_trans  M_basic "##M"
  using power_ax M_basic_sep_instances funspace_succ_rep_intf
  by unfold_locales auto

subsection‹Interface with termM_trancl

context M_ZF1_trans
begin

lemma rtrancl_separation_intf:
  assumes "rM" "AM"
  shows "separation (##M, rtran_closure_mem(##M,A,r))"
  using assms separation_in_ctm[of "rtran_closure_mem_fm(1,2,0)" "[A,r]" "rtran_closure_mem(##M,A,r)"]
    arity_rtran_closure_mem_fm ord_simp_union zero_in_M
  by simp

lemma wftrancl_separation_intf:
  assumes "rM" and "ZM"
  shows "separation (##M, wellfounded_trancl(##M,Z,r))"
  using assms separation_in_ctm[of "wellfounded_trancl_fm(1,2,0)" "[Z,r]" "wellfounded_trancl(##M,Z,r)"]
    arity_wellfounded_trancl_fm ord_simp_union zero_in_M
  by simp

text‹To prove termnat  M we get an infinite set termI from terminfinity_ax
closed under term0 and termsucc; that shows termnatI. Then we
can separate termI with the predicate termλx. xnat.›
lemma finite_sep_intf: "separation(##M, λx. xnat)"
proof -
  have "(vM. separation(##M,λx. (M, [x,v]  finite_ordinal_fm(0))))"
    using separation_ax arity_finite_ordinal_fm
    by simp
  then
  have "(vM. separation(##M,finite_ordinal(##M)))"
    unfolding separation_def
    by simp
  then
  have "separation(##M,finite_ordinal(##M))"
    using separation_in_ctm zero_in_M
    by auto
  then
  show ?thesis
    unfolding separation_def
    by simp
qed

lemma nat_subset_I: "IM. nat  I"
proof -
  have "nat  I"
    if "IM" and "0I" and "x. xI  succ(x)I" for I
    using that
    by (rule_tac subsetI,induct_tac x,simp_all)
  moreover
  obtain I where
    "IM" "0I" "x. xI  succ(x)I"
    using infinity_ax transitivity
    unfolding infinity_ax_def
    by auto
  ultimately
  show ?thesis
    by auto
qed

lemma nat_in_M: "nat  M"
proof -
  have "{xB . xA}=A" if "AB" for A B
    using that by auto
  moreover
  obtain I where
    "IM" "natI"
    using nat_subset_I by auto
  moreover from this
  have "{xI . xnat}  M"
    using finite_sep_intf separation_closed[of "λx . xnat"]
    by simp
  ultimately
  show ?thesis
    by simp
qed

end ― ‹localeM_ZF1_trans

sublocale M_ZF1_trans  M_trancl "##M"
  using rtrancl_separation_intf wftrancl_separation_intf nat_in_M
    wellfounded_trancl_def
  by unfold_locales auto

subsection‹Interface with termM_eclose

lemma repl_sats:
  assumes
    sat:"x z. xM  zM  (M, Cons(x,Cons(z,env))  φ)  P(x,z)"
  shows
    "strong_replacement(##M,λx z. (M, Cons(x,Cons(z,env))  φ)) 
   strong_replacement(##M,P)"
  by (rule strong_replacement_cong,simp add:sat)

arity_theorem for "list_functor_fm"
arity_theorem for "formula_functor_fm"
arity_theorem for "Inl_fm"
arity_theorem for "Inr_fm"
arity_theorem for "Nil_fm"
arity_theorem for "Cons_fm"
arity_theorem for "quasilist_fm"
arity_theorem for "tl_fm"
arity_theorem for "big_union_fm"

context M_ZF1_trans
begin

text‹This lemma obtains termiterates_replacement for predicates
without parameters.›
lemma iterates_repl_intf :
  assumes
    "vM" and
    isfm:"is_F_fm  formula" and
    arty:"arity(is_F_fm)=2" and
    satsf: "a b env'.  aM ; bM ; env'list(M) 
               is_F(a,b)  (M,  [b,a]@env'   is_F_fm)"
    and is_F_fm_replacement:
    "env. (⋅∃⋅⟨1,0 is 2  is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅)  formula  env  list(M) 
      arity((⋅∃⋅⟨1,0 is 2  is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅))  2 +ω length(env) 
     strong_replacement(##M,λx y.
         M, [x,y] @ env  (⋅∃⋅⟨1,0 is 2  is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅))"
  shows
    "iterates_replacement(##M,is_F,v)"
proof -
  let ?f="(⋅∃⋅⟨1,0 is 2  is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0) ⋅)"
  have "arity(?f) = 4" "?fformula"
    using arity_iterates_MH_fm[where isF=is_F_fm and i=2]
      arity_wfrec_replacement_fm[where i=10] isfm arty ord_simp_union
    by simp_all
  {
    fix n
    assume "nnat"
    then
    have "Memrel(succ(n))M"
      using nat_into_M Memrel_closed
      by simp
    moreover
    {
      fix a0 a1 a2 a3 a4 y x z
      assume "[a0,a1,a2,a3,a4,y,x,z]list(M)"
      moreover
      note vM Memrel(succ(n))M
      moreover from calculation
      have "(M, [b,a,c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]  is_F_fm) 
           is_F(a,b)"
        if "aM" "bM" "cM" "dM" for a b c d
        using that satsf[of a b "[c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]"]
        by simp
      moreover from calculation
      have "(M, [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]  iterates_MH_fm(is_F_fm,9,2,1,0)) 
           iterates_MH(##M,is_F,v,a2, a1, a0)"
        using sats_iterates_MH_fm[of M "is_F" "is_F_fm"]
        by simp
    }
    moreover from calculation
    have "(M, [y,x,z,Memrel(succ(n)),v]  is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0)) 
          is_wfrec(##M, iterates_MH(##M,is_F,v),Memrel(succ(n)), x, y)"
      if "yM" "xM" "zM" for y x z
      using that sats_is_wfrec_fm vM by simp
    moreover from calculation
    have "(M, [x,z,Memrel(succ(n)),v]  ?f) 

        (yM. pair(##M,x,y,z) 
        is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))"
      if "xM" "zM" for x z
      using that vM
      by (simp del:pair_abs)
    moreover
    note arity(?f) = 4 ?fformula
    moreover from calculation v_
    have "strong_replacement(##M,λx z. (M, [x,z,Memrel(succ(n)),v]  ?f))"
      using is_F_fm_replacement
      by simp
    ultimately
    have "strong_replacement(##M,λx z.
          yM. pair(##M,x,y,z)  is_wfrec(##M, iterates_MH(##M,is_F,v) ,
                Memrel(succ(n)), x, y))"
      using repl_sats[of M ?f "[Memrel(succ(n)),v]"]
      by (simp del:pair_abs)
  }
  then
  show ?thesis
    unfolding iterates_replacement_def wfrec_replacement_def
    by simp
qed

lemma eclose_repl1_intf:
  assumes "AM"
  shows "iterates_replacement(##M, big_union(##M), A)"
  using assms arity_big_union_fm
    iterates_repl_intf[where is_F_fm="big_union_fm(1,0)"]
    replacement_ax1(1)[unfolded replacement_assm_def]
    ord_simp_union
  by simp

lemma eclose_repl2_intf:
  assumes "AM"
  shows "strong_replacement(##M,λn y. nnat  is_iterates(##M, big_union(##M), A, n, y))"
proof -
  let ?f = "And(Member(0,3),is_iterates_fm(big_union_fm(1,0),2,0,1))"
  note nat_in_M AM
  moreover from this
  have "big_union(##M,a,b) 
        (M, [b,a,c,d,e,f,g,h,i,j,k,n,y,A,nat]  big_union_fm(1,0))"
    if "aM" "bM" "cM" "dM" "eM" "fM""gM""hM""iM""jM" "kM" "nM" "yM"
    for a b c d e f g h i j k n y
    using that by simp
  moreover from calculation
  have "(M, [n,y,A,nat]  is_iterates_fm(big_union_fm(1,0),2,0,1)) 
           is_iterates(##M, big_union(##M), A, n , y)"
    if "nM" "yM" for n y
    using that sats_is_iterates_fm[of M "big_union(##M)"]
    by simp
  moreover from calculation
  have "(M, [n,y,A,nat]  ?f) 
        nnat  is_iterates(##M, big_union(##M), A, n, y)"
    if "nM" "yM" for n y
    using that
    by simp
  moreover
  have "arity(?f) = 4"
    using arity_is_iterates_fm[where p="big_union_fm(1,0)" and i=2]
      arity_big_union_fm arity_And ord_simp_union
    by simp
  ultimately
  show ?thesis
    using repl_sats[of M ?f "[A,nat]"] replacement_ax1(2)[unfolded replacement_assm_def]
    by simp
qed

end ― ‹localeM_ZF1_trans

sublocale M_ZF1_trans  M_eclose "##M"
  using eclose_repl1_intf eclose_repl2_intf
  by unfold_locales auto

text‹Interface with localeM_eclose.›

schematic_goal sats_is_Vset_fm_auto:
  assumes
    "inat" "vnat" "envlist(A)" "0A"
    "i < length(env)" "v < length(env)"
  shows
    "is_Vset(##A,nth(i, env),nth(v, env))  (A, env  ?ivs_fm(i,v))"
  unfolding is_Vset_def is_Vfrom_def
  by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+)

synthesize "is_Vset" from_schematic "sats_is_Vset_fm_auto"
arity_theorem for "is_Vset_fm"

declare is_Hrank_fm_def[fm_definitions add]

context M_ZF1_trans
begin

lemma wfrec_rank :
  assumes "XM"
  shows "wfrec_replacement(##M,is_Hrank(##M),rrank(X))"
proof -
  let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)))"
  note assms zero_in_M
  moreover from this
  have
    "is_Hrank(##M,a2, a1, a0) 
             (M, [a0,a1,a2,a3,a4,y,x,z,rrank(X)]  is_Hrank_fm(2,1,0))"
    if "a4M" "a3M" "a2M" "a1M" "a0M" "yM" "xM" "zM" for a4 a3 a2 a1 a0 y x z
    using that rrank_in_M is_Hrank_iff_sats
    by simp
  moreover from calculation
  have "(M, [y,x,z,rrank(X)]  is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)) 
   is_wfrec(##M, is_Hrank(##M) ,rrank(X), x, y)"
    if "yM" "xM" "zM" for y x z
    using that rrank_in_M sats_is_wfrec_fm
    by simp
  moreover from calculation
  have "(M, [x,z,rrank(X)]  ?f) 
               (yM. pair(##M,x,y,z)  is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
    if "xM" "zM" for x z
    using that rrank_in_M
    by (simp del:pair_abs)
  moreover
  have "arity(?f) = 3"
    using arity_wfrec_replacement_fm[where p="is_Hrank_fm(2,1,0)" and i=3,simplified]
      arity_is_Hrank_fm[of 2 1 0,simplified] ord_simp_union
    by simp
  moreover from calculation
  have "strong_replacement(##M,λx z. (M, [x,z,rrank(X)]  ?f))"
    using replacement_ax1(3)[unfolded replacement_assm_def] rrank_in_M
    by simp
  ultimately
  show ?thesis
    using repl_sats[of M ?f "[rrank(X)]"]
    unfolding wfrec_replacement_def
    by (simp del:pair_abs)
qed

lemma trans_repl_HVFrom :
  assumes "AM" "iM"
  shows "transrec_replacement(##M,is_HVfrom(##M,A),i)"
proof -
  let ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)))"
  note facts = assms zero_in_M
  moreover
  have "saM. esaM. mesaM.
       upair(##M,a,a,sa)  is_eclose(##M,sa,esa)  membership(##M,esa,mesa)"
    if "aM" for a
    using that upair_ax eclose_closed Memrel_closed
    unfolding upair_ax_def
    by (simp del:upair_abs)
  moreover
  {
    fix mesa
    assume "mesaM"
    moreover
    note facts
    moreover from calculation
    have "is_HVfrom(##M,A,a2, a1, a0) 
      (M, [a0,a1,a2,a3,a4,y,x,z,A,mesa]  is_HVfrom_fm(8,2,1,0))"
      if "a4M" "a3M" "a2M" "a1M" "a0M" "yM" "xM" "zM" for a4 a3 a2 a1 a0 y x z
      using that sats_is_HVfrom_fm
      by simp
    moreover from calculation
    have "(M, [y,x,z,A,mesa]  is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)) 
         is_wfrec(##M, is_HVfrom(##M,A),mesa, x, y)"
      if "yM" "xM" "zM" for y x z
      using that sats_is_wfrec_fm
      by simp
    moreover from calculation
    have "(M, [x,z,A,mesa]  ?f) 
               (yM. pair(##M,x,y,z)  is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
      if "xM" "zM" for x z
      using that
      by (simp del:pair_abs)
    moreover
    have "arity(?f) = 4"
      using arity_wfrec_replacement_fm[where p="is_HVfrom_fm(8,2,1,0)" and i=9]
        arity_is_HVfrom_fm ord_simp_union
      by simp
    moreover from calculation
    have "strong_replacement(##M,λx z. (M, [x,z,A,mesa]  ?f))"
      using replacement_ax1(4)[unfolded replacement_assm_def]
      by simp
    ultimately
    have "wfrec_replacement(##M,is_HVfrom(##M,A),mesa)"
      using repl_sats[of M ?f "[A,mesa]"]
      unfolding wfrec_replacement_def
      by (simp del:pair_abs)
  }
  ultimately
  show ?thesis
    unfolding transrec_replacement_def
    by simp
qed

end ― ‹localeM_ZF1_trans

subsection‹Interface for proving Collects and Replace in M.›
context M_ZF1_trans
begin

lemma Collect_in_M :
  assumes
    "φ  formula" "envlist(M)"
    "arity(φ)  1 +ω length(env)" "AM" and
    satsQ: "x. xM  (M, [x]@env  φ)  Q(x)"
  shows
    "{yA . Q(y)}M"
proof -
  have "separation(##M,λx. (M, [x] @ env  φ))"
    using assms separation_ax by simp
  then
  show ?thesis
    using AM satsQ transitivity separation_closed
      separation_cong[of "##M" "λy. (M, [y]@env  φ)" "Q"]
    by simp
qed

― ‹This version has a weaker assumption.›
lemma separation_in_M :
  assumes
    "φ  formula" "envlist(M)"
    "arity(φ)  1 +ω length(env)" "AM" and
    satsQ: "x. xA  (M, [x]@env  φ)  Q(x)"
  shows
    "{yA . Q(y)}  M"
proof -
  let ?φ' = "And(φ,Member(0,length(env)+ω1))"
  note assms
  moreover
  have "arity(?φ')  1 +ω length(env@[A])"
    using assms Un_le le_trans[of "arity(φ)" "1+ωlength(env)" "2+ωlength(env)"]
    by (force simp:FOL_arities)
  moreover from calculation
  have "?φ'formula" "nth(length(env), env @ [A]) = A"
    using nth_append
    by auto
  moreover from calculation
  have " x . x  M  (M, [x]@env@[A]  ?φ')  Q(x)  xA"
    using arity_sats_iff[of _ "[A]" _ "[_]@env"]
    by auto
  ultimately
  show ?thesis
    using Collect_in_M[of ?φ' "env@[A]" _ "λx . Q(x)  xA", OF _ _ _ AM]
    by auto
qed

end ― ‹localeM_ZF1_trans

context M_Z_trans
begin

lemma strong_replacement_in_ctm:
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 2 +ω length(env)" and
    fsats: "x y. xM  yM  (M,[x,y]@env  φ)  y = f(x)" and
    fclosed: "x. xM  f(x)  M" and
    phi_replacement:"replacement_assm(M,env,φ)" and
    "envlist(M)"
  shows "strong_replacement(##M, λx y . y = f(x))"
  using assms
    strong_replacement_cong[of "##M" "λx y. M,[x,y]@envφ" "λx y. y = f(x)"]
  unfolding replacement_assm_def
  by auto

lemma strong_replacement_rel_in_ctm :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 2 +ω length(env)" and
    fsats: "x y. xM  yM  (M,[x,y]@env  φ)  f(x,y)"  and
    phi_replacement:"replacement_assm(M,env,φ)" and
    "envlist(M)"
  shows "strong_replacement(##M, f)"
  using assms
    strong_replacement_cong[of "##M" "λx y. M,[x,y]@envφ" "f"]
  unfolding replacement_assm_def
  by auto

lemma Replace_in_M :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 2 +ω length(env)" and
    fsats: "x y. xA  yM  (M,[x,y]@env  φ)  y = f(x)" and
    fclosed: "x. xA  f(x)  M"  and
    "AM" "envlist(M)" and
    phi'_replacement:"replacement_assm(M,env@[A], φ  0  length(env) +ω 2 )"
  shows "{f(x) . xA}M"
proof -
  let ?φ' = "And(φ,Member(0,length(env)+ω2))"
  note assms
  moreover from this
  have "arity(?φ')  2 +ω length(env@[A])"
    using Un_le le_trans[of "arity(φ)" "2+ω(length(env))" "3+ωlength(env)"]
    by (force simp:FOL_arities)
  moreover from calculation
  have "?φ'formula" "nth(length(env), env @ [A]) = A"
    using nth_append by auto
  moreover from calculation
  have " x y. x  M  yM  (M,[x,y]@env@[A]?φ')  y=f(x) xA"
    using arity_sats_iff[of _ "[A]" _ "[_,_]@env"]
    by auto
  moreover from calculation
  have "strong_replacement(##M, λx y. M,[x,y]@env@[A]  ?φ')"
    using phi'_replacement assms(1-6) unfolding replacement_assm_def by simp
  ultimately
  have 4:"strong_replacement(##M, λx y. y = f(x)  xA)"
    using
      strong_replacement_cong[of "##M" "λx y. M,[x,y]@env@[A]?φ'" "λx y. y = f(x)  xA"]
    by simp
  then
  have "{y . xA , y = f(x)}  M"
    using AM strong_replacement_closed[OF 4,of A] fclosed by simp
  moreover
  have "{f(x). xA} = { y . xA , y = f(x)}"
    by auto
  ultimately
  show ?thesis by simp
qed

lemma Replace_relativized_in_M :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 2 +ω length(env)" and
    fsats: "x y. xA  yM  (M,[x,y]@env  φ)  is_f(x,y)" and
    fabs:  "x y. xA  yM  is_f(x,y)  y = f(x)" and
    fclosed: "x. xA  f(x)  M"  and
    "AM" "envlist(M)" and
    phi'_replacement:"replacement_assm(M,env@[A], φ  0  length(env) +ω 2 )"
  shows "{f(x) . xA}M"
  using assms Replace_in_M[of φ] by auto

lemma ren_action :
  assumes
    "envlist(M)" "xM" "yM" "zM"
  shows " i . i < 2+ωlength(env) 
          nth(i,[x,z]@env) = nth(ρ_repl(length(env))`i,[z,x,y]@env)"
proof -
  let ?f="{0, 1, 1, 0}"
  have 1:"(j. j < length(env)  nth(j, env) = nth(id(length(env)) ` j, env))"
    using assms ltD by simp
  have 2:"nth(j, [x,z]) = nth(?f ` j, [z,x,y])" if "j<2" for j
  proof -
    consider "j=0" | "j=1" using  ltD[OF j<2] by auto
    then show ?thesis
    proof(cases)
      case 1
      then show ?thesis using apply_equality f_type by simp
    next
      case 2
      then show ?thesis using apply_equality f_type by simp
    qed
  qed
  show ?thesis
    using sum_action[OF _ _ _ _ f_type id_type _ _ _ _ _ _ _ 2 1,simplified] assms
    unfolding ρ_repl_def by simp
qed

lemma Lambda_in_M :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 2 +ω length(env)" and
    fsats: "x y. xA  yM  (M,[x,y]@env  φ)  is_f(x,y)" and
    fabs:  "x y. xA  yM  is_f(x,y)  y = f(x)" and
    fclosed: "x. xA  f(x)  M" and
    "AM" "envlist(M)" and
    phi'_replacement2: "replacement_assm(M,env@[A],Lambda_in_M_fm(φ,length(env)))"
  shows "(λxA . f(x)) M"
  unfolding lam_def
proof -
  let ?ren="ρ_repl(length(env))"
  let ?j="2+ωlength(env)"
  let ?k="3+ωlength(env)"
  let ="ren(φ)`?j`?k`?ren"
  let ?φ'="Exists(And(pair_fm(1,0,2),))"
  let ?p="λx y. zM. pair(##M,x,z,y)  is_f(x,z)"
  have "?φ'formula" "formula"
    using env_ length_type f_fm ren_type ren_tc[of φ "2+ωlength(env)" "3+ωlength(env)" ?ren]
    by simp_all
  moreover from this
  have "arity()3+ω(length(env))" "arity()nat"
    using assms arity_ren[OF f_fm _ _ ren_type,of "length(env)"] by simp_all
  then
  have "arity(?φ')  2+ω(length(env))"
    using Un_le pred_Un_distrib assms pred_le
    by (simp add:arity)
  moreover from this calculation
  have "xA  yM  (M,[x,y]@env  ?φ')  ?p(x,y)" for x y
    using env_ length_type[OF env_] assms transitivity[OF _ AM]
      sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type f_ar ren_action[rule_format,of _ x y],of _ M ]
    by auto
  moreover
  have "xA  yM  ?p(x,y)  y = <x,f(x)>" for x y
    using assms transitivity[OF _ A_] fclosed
    by simp
  moreover
  have " x . xA  <x,f(x)>  M"
    using transitivity[OF _ AM] pair_in_M_iff fclosed by simp
  ultimately
  show "{x,f(x) . xA }  M"
    using Replace_in_M[of ?φ' env A] phi'_replacement2 AM env_
    by simp
qed

lemma ren_action' :
  assumes
    "envlist(M)" "xM" "yM" "zM" "uM"
  shows " i . i < 3+ωlength(env) 
          nth(i,[x,z,u]@env) = nth(ρ_pair_repl(length(env))`i,[x,z,y,u]@env)"
proof -
  let ?f="{0, 0, 1, 1, 2,3}"
  have 1:"(j. j < length(env)  nth(j, env) = nth(id(length(env)) ` j, env))"
    using assms ltD by simp
  have 2:"nth(j, [x,z,u]) = nth(?f ` j, [x,z,y,u])" if "j<3" for j
  proof -
    consider "j=0" | "j=1" | "j=2" using  ltD[OF j<3] by auto
    then show ?thesis
    proof(cases)
      case 1
      then show ?thesis using apply_equality f_type' by simp
    next
      case 2
      then show ?thesis using apply_equality f_type' by simp
    next
      case 3
      then show ?thesis using apply_equality f_type' by simp
    qed
  qed
  show ?thesis
    using sum_action[OF _ _ _ _ f_type' id_type _ _ _ _ _ _ _ 2 1,simplified] assms
    unfolding ρ_pair_repl_def by simp
qed

lemma LambdaPair_in_M :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 3 +ω length(env)" and
    fsats: "x z r. xM  zM  rM  (M,[x,z,r]@env  φ)  is_f(x,z,r)" and
    fabs:  "x z r. xM  zM  rM  is_f(x,z,r)  r = f(x,z)" and
    fclosed: "x z. xM  zM  f(x,z)  M" and
    "AM" "envlist(M)" and
    phi'_replacement3: "replacement_assm(M,env@[A],LambdaPair_in_M_fm(φ,length(env)))"
  shows "(λxA . f(fst(x),snd(x))) M"
proof -
  let ?ren="ρ_pair_repl(length(env))"
  let ?j="3+ωlength(env)"
  let ?k="4+ωlength(env)"
  let ="ren(φ)`?j`?k`?ren"
  let ?φ'="Exists(Exists(And(fst_fm(2,0),(And(snd_fm(2,1),)))))"
  let ?p="λx y. is_f(fst(x),snd(x),y)"
  have "?φ'formula" "formula"
    using env_ length_type f_fm ren_type' ren_tc[of φ ?j ?k ?ren]
    by simp_all
  moreover from this
  have "arity()4+ω(length(env))" "arity()nat"
    using assms arity_ren[OF f_fm _ _ ren_type',of "length(env)"] by simp_all
  moreover from calculation
  have 1:"arity(?φ')  2+ω(length(env))" "?φ'formula"
    using Un_le pred_Un_distrib assms pred_le
    by (simp_all add:arity)
  moreover from this calculation
  have 2:"xA  yM  (M,[x,y]@env  ?φ')  ?p(x,y)" for x y
    using
      sats_iff_sats_ren[OF f_fm _ _ _ _ ren_type' f_ar
        ren_action'[rule_format,of _ "fst(x)" x "snd(x)" y],simplified]
      env_ length_type[OF env_] transitivity[OF _ AM]
      fst_snd_closed pair_in_M_iff fsats[of "fst(x)" "snd(x)" y,symmetric]
      fst_abs snd_abs
    by auto
  moreover from assms
  have 3:"xA  yM  ?p(x,y)  y = f(fst(x),snd(x))" for x y
    using fclosed fst_snd_closed pair_in_M_iff fabs transitivity
    by auto
  moreover
  have 4:" x . xA  <x,f(fst(x),snd(x))>  M" " x . xA  f(fst(x),snd(x))  M"
    using transitivity[OF _ AM] pair_in_M_iff fclosed fst_snd_closed
    by simp_all
  ultimately
  show ?thesis
    using Lambda_in_M[unfolded Lambda_in_M_fm_def, of ?φ', OF _ _ _ _ _ _ _
        phi'_replacement3[unfolded LambdaPair_in_M_fm_def]]
      env_ A_ by simp

qed

lemma (in M_ZF1_trans) lam_replacement2_in_ctm :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) 3 +ω length(env)" and
    fsats: "x z r. xM  zM  rM  (M,[x,z,r]@env  φ)  is_f(x,z,r)" and
    fabs:  "x z r. xM  zM  rM  is_f(x,z,r)  r = f(x,z)" and
    fclosed: "x z. xM  zM  f(x,z)  M" and
    "envlist(M)" and
    phi'_replacement3: "A. AM  replacement_assm(M,env@[A],LambdaPair_in_M_fm(φ,length(env)))"
  shows "lam_replacement(##M , λx . f(fst(x),snd(x)))"
  using
    LambdaPair_in_M fabs
    f_ar ord_simp_union transitivity assms fst_snd_closed
  by (rule_tac lam_replacement_iff_lam_closed[THEN iffD2],simp_all)

simple_rename "ren_U" src "[z1,x_P, x_leq, x_o, x_t, z2_c]"
  tgt "[z2_c,z1,z,x_P, x_leq, x_o, x_t]"

simple_rename "ren_V" src "[fz,x_P, x_leq, x_o,x_f, x_t, gz]"
  tgt "[gz,fz,z,x_P, x_leq, x_o,x_f, x_t]"

simple_rename "ren_V3" src "[fz,x_P, x_leq, x_o,x_f, gz, hz]"
  tgt "[hz,gz,fz,z,x_P, x_leq, x_o,x_f]"

lemma separation_sat_after_function_1:
  assumes "[a,b,c,d]list(M)" and  "χformula" and "arity(χ)  6"
    and
    f_fm:  "f_fm  formula" and
    f_ar:  "arity(f_fm)  6" and
    fsats: " fx x. fxM  xM  (M,[fx,x]@[a, b, c, d]  f_fm)  fx=f(x)" and
    fclosed: "x . xM  f(x)  M" and
    g_fm:  "g_fm  formula" and
    g_ar:  "arity(g_fm)  7" and
    gsats: " gx fx x. gxM   fxM  xM  (M,[gx,fx,x]@[a, b, c, d]  g_fm)  gx=g(x)" and
    gclosed: "x . xM  g(x)  M"
  shows  "separation(##M, λr. M, [f(r), a, b, c, d, g(r)]  χ)"
proof -
  note types = assms(1-4)
  let ="ren(χ)`6`7`ren_U_fn"
  let  ?ψ'="Exists(And(f_fm,Exists(And(g_fm,))))"
  let ="λz.[f(z), a, b, c, d, g(z)]"
  let ?env="[a, b, c, d]"
  let ="λz.[g(z),f(z),z]@?env"
  note types
  moreover from this
  have "arity(χ)  7" "formula"
    using ord_simp_union ren_tc ren_U_thm(2)[folded ren_U_fn_def] le_trans[of "arity(χ)" 6]
    by simp_all
  moreover from calculation
  have "arity()  7" "?ψ'formula"
    using arity_ren ren_U_thm(2)[folded ren_U_fn_def] f_fm g_fm
    by simp_all
  moreover from calculation f_ar g_ar f_fm g_fm
  have "arity(?ψ')  5"
    using ord_simp_union pred_le arity_type
    by (simp add:arity)
  moreover from calculation fclosed gclosed
  have 0:"(M, [f(z), a, b, c, d,  g(z)]  χ)  (M,(z) )" if "(##M)(z)" for z
    using sats_iff_sats_ren[of χ 6 7 _ _ "(z)"]
      ren_U_thm(1)[where A=M,folded ren_U_fn_def] ren_U_thm(2)[folded ren_U_fn_def] that
    by simp
  moreover from calculation
  have 1:"(M,(z) )  M,[z]@?env?ψ'" if "(##M)(z)" for z
    using that fsats[OF fclosed[of z],of z]  gsats[of "g(z)" "f(z)" z] fclosed gclosed f_fm g_fm
  proof(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp,(auto)[1])
    assume "M, [z] @ [a, b, c, d]  (⋅∃f_fm  (⋅∃g_fm  ren(χ) ` 6 ` 7 ` ren_U_fn⋅)⋅)"
    then
    have "xaM. (M, [xa, z, a, b, c, d]  f_fm) 
          (xM. (M, [x, xa, z, a, b, c, d]  g_fm) 
            (M, [x, xa, z, a, b, c, d]  ren(χ) ` 6 ` 7 ` ren_U_fn))"
      using that calculation by auto
    then
    obtain xa x where "xM" "xaM" "M, [xa, z, a, b, c, d]  f_fm"
      "(M, [x, xa, z, a, b, c, d]  g_fm)"
      "(M, [x, xa, z, a, b, c, d]  ren(χ) ` 6 ` 7 ` ren_U_fn)"
      using that calculation by auto
    moreover from this
    have "xa=f(z)" "x=g(z)" using fsats[of xa]  gsats[of x xa] that by simp_all
    ultimately
    show "M, [g(z), f(z), z] @ [a, b, c, d]  ren(χ) ` 6 ` 7 ` ren_U_fn"
      by auto
  qed
  moreover from calculation
  have "separation(##M, λz. (M,[z]@?env  ?ψ'))"
    using separation_ax
    by simp_all
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed

lemma separation_sat_after_function3:
  assumes "[a, b, c, d]list(M)" and  "χformula" and "arity(χ)  7"
    and
    f_fm:  "f_fm  formula" and
    f_ar:  "arity(f_fm)  6" and
    fsats: " fx x. fxM  xM  (M,[fx,x]@[a, b, c, d]  f_fm)  fx=f(x)" and
    fclosed: "x . xM  f(x)  M" and
    g_fm:  "g_fm  formula" and
    g_ar:  "arity(g_fm)  7" and
    gsats: " gx fx x. gxM  fxM  xM  (M,[gx,fx,x]@[a, b, c, d]  g_fm)  gx=g(x)" and
    gclosed: "x . xM  g(x)  M" and
    h_fm:  "h_fm  formula" and
    h_ar:  "arity(h_fm)  8" and
    hsats: " hx gx fx x. hxM  gxM  fxM  xM  (M,[hx,gx,fx,x]@[a, b, c, d]  h_fm)  hx=h(x)" and
    hclosed: "x . xM  h(x)  M"
  shows  "separation(##M, λr. M, [f(r), a, b, c, d, g(r), h(r)]  χ)"
proof -
  note types = assms(1-3)
  let ="χ"
  let ="ren()`7`8`ren_V3_fn"
  let ?ψ'="Exists(And(f_fm,Exists(And(g_fm,Exists(And(h_fm,))))))"
  let ="λz.[f(z), a, b, c, d,g(z), h(z)]"
  let ?env="[a, b, c, d]"
  let ="λz.[h(z),g(z),f(z),z]@?env"
  note types
  moreover from this
  have "formula" by simp
  moreover from calculation
  have "arity()  9" "formula"
    using ord_simp_union ren_tc ren_V3_thm(2)[folded ren_V3_fn_def] le_trans[of "arity(χ)" 7]
    by simp_all
  moreover from calculation
  have "arity()  8" "?ψ'formula"
    using arity_ren ren_V3_thm(2)[folded ren_V3_fn_def] f_fm g_fm h_fm
    by (simp_all)
  moreover from this f_ar g_ar f_fm g_fm h_fm h_ar ?ψ'_
  have "arity(?ψ')  5"
    using ord_simp_union arity_type nat_into_Ord
    by (simp add:arity,(rule_tac pred_le,simp,rule_tac Un_le,simp)+,simp_all add: _)
  moreover from calculation fclosed gclosed hclosed
  have 0:"(M, (z)  )  (M,(z) )" if "(##M)(z)" for z
    using sats_iff_sats_ren[of  7 8 "(z)" M "(z)"]
      ren_V3_thm(1)[where A=M,folded ren_V3_fn_def,simplified] ren_V3_thm(2)[folded ren_V3_fn_def] that
    by simp
  moreover from calculation
  have 1:"(M,(z) )  M,[z]@?env?ψ'" if "(##M)(z)" for z
    using that fsats[OF fclosed[of z],of z] gsats[of "g(z)" "f(z)" z]
      hsats[of "h(z)" "g(z)" "f(z)" z]
      fclosed gclosed hclosed f_fm g_fm h_fm
    apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp)
     apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="g(z)"],simp)
     apply(rule_tac conjI,simp,rule_tac rev_bexI[where x="h(z)"],simp,rule_tac conjI,simp,simp)
  proof -
    assume "M, [z] @ [a, b, c, d]  (⋅∃f_fm  (⋅∃g_fm  (⋅∃h_fm  ren(χ) ` 7 ` 8 ` ren_V3_fn⋅)⋅)⋅)"
    with calculation that
    have "xM. (M, [x, z, a, b, c, d]  f_fm) 
           (xaM. (M, [xa, x, z, a, b, c, d]  g_fm)  (xbM. (M, [xb, xa, x, z, a, b, c, d]  h_fm)  (M, [xb, xa, x, z, a, b, c, d]  ren(χ) ` 7 ` 8 ` ren_V3_fn)))"
      by auto
    with calculation
    obtain x where "xM" "(M, [x, z, a, b, c, d]  f_fm)"
      "(xaM. (M, [xa, x, z, a, b, c, d]  g_fm)  (xbM. (M, [xb, xa, x, z, a, b, c, d]  h_fm)  (M, [xb, xa, x, z, a, b, c, d]  ren(χ) ` 7 ` 8 ` ren_V3_fn)))"
      by force
    moreover from this
    have "x=f(z)" using fsats[of x] that by simp
    moreover from calculation
    obtain xa where "xaM" "(M, [xa, x, z, a, b, c, d]  g_fm)"
      "(xbM. (M, [xb, xa, x, z, a, b, c, d]  h_fm)  (M, [xb, xa, x, z, a, b, c, d]  ren(χ) ` 7 ` 8 ` ren_V3_fn))"
      by auto
    moreover from calculation
    have "xa=g(z)" using gsats[of xa x] that by simp
    moreover from calculation
    obtain xb where "xbM" "(M, [xb, xa, x, z, a, b, c, d]  h_fm)"
      "(M, [xb, xa, x, z, a, b, c, d]  ren(χ) ` 7 ` 8 ` ren_V3_fn)"
      by auto
    moreover from calculation
    have "xb=h(z)" using hsats[of xb xa x] that by simp
    ultimately
    show "M, [h(z), g(z), f(z), z] @ [a, b, c, d]  ren(χ) ` 7 ` 8 ` ren_V3_fn"
      by auto
  qed
  moreover from calculation ?ψ'_
  have "separation(##M, λz. (M,[z]@?env  ?ψ'))"
    using separation_ax
    by simp
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed

lemma separation_sat_after_function:
  assumes "[a, b, c, d, τ]list(M)" and  "χformula" and "arity(χ)  7"
    and
    f_fm:  "f_fm  formula" and
    f_ar:  "arity(f_fm)  7" and
    fsats: " fx x. fxM  xM  (M,[fx,x]@[a, b, c, d, τ]  f_fm)  fx=f(x)" and
    fclosed: "x . xM  f(x)  M" and
    g_fm:  "g_fm  formula" and
    g_ar:  "arity(g_fm)  8" and
    gsats: " gx fx x. gxM   fxM  xM  (M,[gx,fx,x]@[a, b, c, d, τ]  g_fm)  gx=g(x)" and
    gclosed: "x . xM  g(x)  M"
  shows  "separation(##M, λr. M, [f(r), a, b, c, d, τ, g(r)]  χ)"
proof -
  note types = assms(1-3)
  let ="χ"
  let ="ren()`7`8`ren_V_fn"
  let  ?ψ'="Exists(And(f_fm,Exists(And(g_fm,))))"
  let ="λz.[f(z), a, b, c, d, τ, g(z)]"
  let ?env="[a, b, c, d, τ]"
  let ="λz.[g(z),f(z),z]@?env"
  note types
  moreover from this
  have "formula" by simp
  moreover from calculation
  have "arity()  8" "formula"
    using ord_simp_union ren_tc ren_V_thm(2)[folded ren_V_fn_def] le_trans[of "arity(χ)" 7]
    by simp_all
  moreover from calculation
  have "arity()  8" "?ψ'formula"
    using arity_ren ren_V_thm(2)[folded ren_V_fn_def] f_fm g_fm
    by (simp_all)
  moreover from calculation f_ar g_ar f_fm g_fm
  have "arity(?ψ')  6"
    using ord_simp_union pred_le arity_type
    by (simp add:arity)
  moreover from calculation fclosed gclosed
  have 0:"(M, (z)  )  (M,(z) )" if "(##M)(z)" for z
    using sats_iff_sats_ren[of  7 8 "(z)" _ "(z)"]
      ren_V_thm(1)[where A=M,folded ren_V_fn_def] ren_V_thm(2)[folded ren_V_fn_def] that
    by simp
  moreover from calculation
  have 1:"(M,(z) )  M,[z]@?env?ψ'" if "(##M)(z)" for z
    using that fsats[OF fclosed[of z],of z]  gsats[of "g(z)" "f(z)" z]
      fclosed gclosed f_fm g_fm
    apply(rule_tac iffI,simp,rule_tac rev_bexI[where x="f(z)"],simp)
     apply(auto)[1]
  proof -
    assume "M, [z] @ [a, b, c, d, τ]  (⋅∃f_fm  (⋅∃g_fm  ren(χ) ` 7 ` 8 ` ren_V_fn⋅)⋅)"
    then have "xaM. (M, [xa, z, a, b, c, d, τ]  f_fm) 
       (xM. (M, [x, xa, z, a, b, c, d, τ]  g_fm)  (M, [x, xa, z, a, b, c, d, τ]  ren(χ) ` 7 ` 8 ` ren_V_fn))"
      using that calculation by auto
    then
    obtain xa where "xaM" "M, [xa, z, a, b, c, d, τ]  f_fm"
      "(xM. (M, [x, xa, z, a, b, c, d, τ]  g_fm)  (M, [x, xa, z, a, b, c, d, τ]  ren(χ) ` 7 ` 8 ` ren_V_fn))"
      by auto
    moreover from this
    have "xa=f(z)" using fsats[of xa] that by simp
    moreover from calculation
    obtain x where "xM" "M, [x, xa, z, a, b, c, d, τ]  g_fm" "M, [x, xa, z, a, b, c, d, τ]  ren(χ) ` 7 ` 8 ` ren_V_fn"
      by auto
    moreover from calculation
    have "x=g(z)" using gsats[of x xa] that by simp
    ultimately
    show "M, [g(z), f(z), z] @ [a, b, c, d, τ]  ren(χ) ` 7 ` 8 ` ren_V_fn"
      by auto
  qed
  moreover from calculation
  have "separation(##M, λz. (M,[z]@?env  ?ψ'))"
    using separation_ax
    by simp_all
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD2,OF iff_trans[OF 0 1]],clarify,force)
qed
end

definition separation_assm_fm :: "[i,i,i]  i"
  where
  "separation_assm_fm(A,x,f_fm)  (⋅∃ (⋅∃ 0  A +ω 2  ⋅⟨0,1 is x+ω 2   f_fm ⋅)⋅)" 

lemma separation_assm_fm_type[TC]: 
  "A  ω  y  ω  f_fm  formula  separation_assm_fm(A, y,f_fm)  formula"
  unfolding separation_assm_fm_def
  by simp

lemma arity_separation_assm_fm : "A  ω  x  ω  f_fm  formula 
  arity(separation_assm_fm(A, x, f_fm)) = succ(A)  succ(x)  pred(pred(arity(f_fm)))"
  using pred_Un_distrib
  unfolding separation_assm_fm_def
  by (auto simp add:arity)

definition separation_assm_bin_fm where
  "separation_assm_bin_fm(A,y,f_fm)  
    (⋅∃(⋅∃(⋅∃(⋅∃((3  A +ω 4   ⋅⟨3,2 is y +ω 4 )  f_fm   ⋅fst(3) is 0   ⋅snd(3) is 1 ) ⋅)⋅)⋅)⋅) "

lemma separation_assm_bin_fm_type[TC]: 
  "A  ω  y  ω  f_fm  formula  separation_assm_bin_fm(A, y,f_fm)  formula"
  unfolding separation_assm_bin_fm_def
  by simp

lemma arity_separation_assm_bin_fm : "A  ω  x  ω  f_fm  formula 
  arity(separation_assm_bin_fm(A, x, f_fm)) = succ(A)  succ(x)  (pred^4(arity(f_fm)))"
  using pred_Un_distrib
  unfolding separation_assm_bin_fm_def
  by (auto simp add:arity)

context M_Z_trans
begin

lemma separation_assm_sats : 
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) = 2" and
    fsats: "env x y. envlist(M)  xM  yM  (M,[x,y]@env  φ)  is_f(x,y)" and
    fabs:  "x y. xM  yM  is_f(x,y)  y = f(x)" and
    fclosed: "x. xM  f(x)  M" and
    "AM"
  shows "separation(##M, λy. x  M . xA  y = x, f(x))"
proof -
  let ?φ'="separation_assm_fm(1,0,φ)"
  let ?p="λy. xM . xA  y = x, f(x)"
  from f_fm
  have "?φ'formula"
     by simp
  moreover from this f_ar f_fm
  have "arity(?φ') = 2"
    using arity_separation_assm_fm[of 1 0 φ] ord_simp_union  
    by simp
  moreover from AM calculation
  have "separation(##M,λy . M,[y,A]  ?φ')"
    using separation_ax by auto
  moreover
  have "yM  (M,[y,A]  ?φ')  ?p(y)" for y
    using assms transitivity[OF _ AM]
    unfolding separation_assm_fm_def
    by auto  
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD1],auto)
qed

lemma separation_assm_bin_sats :
  assumes
    f_fm:  "φ  formula" and
    f_ar:  "arity(φ) = 3" and
    fsats: "env x z y. envlist(M)  xM  zM  yM  (M,[x,z,y]@env  φ)  is_f(x,z,y)" and
    fabs:  "x z y. xM   zM  yM  is_f(x,z,y)  y = f(x,z)" and
    fclosed: "x z . xM   zM  f(x,z)  M" and
    "AM"
  shows "separation(##M, λy. x  M . xA  y = x, f(fst(x),snd(x)))"
proof -
  let ?φ'="separation_assm_bin_fm(1,0,φ)"
  let ?p="λy. xM . xA  y = x, f(fst(x),snd(x))"
  from f_fm
  have "?φ'formula"
     by simp
  moreover from this f_ar f_fm
  have "arity(?φ') = 2"
    using arity_separation_assm_bin_fm[of 1 0 φ] ord_simp_union  
    by simp
  moreover from AM calculation
  have "separation(##M,λy . M,[y,A]  ?φ')"
    using separation_ax by auto
  moreover
  have "yM  (M,[y,A]  ?φ')  ?p(y)" for y
    using assms transitivity[OF _ AM] pair_in_M_iff fst_abs snd_abs fst_closed snd_closed
    unfolding separation_assm_bin_fm_def
    by auto
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD1],auto)
qed

lemma separation_Union: "AM 
    separation(##M, λy. x  M . xA  y = x, Union(x))"
  using separation_assm_sats[of "big_union_fm(0,1)"] arity_big_union_fm ord_simp_union
    Union_closed[simplified]
  by simp

lemma lam_replacement_Union: "lam_replacement(##M, Union)"
  using lam_replacement_Union' separation_Union transM by simp

lemma separation_fst: "AM 
    separation(##M, λy. x  M . xA  y = x, fst(x))"
  using separation_assm_sats[of "fst_fm(0,1)"] arity_fst_fm ord_simp_union
    fst_closed fst_abs
  by simp

lemma lam_replacement_fst: "lam_replacement(##M, fst)"
  using lam_replacement_fst' separation_fst transM by simp

lemma separation_snd: "AM 
    separation(##M, λy. x  M . xA  y = x, snd(x))"
  using separation_assm_sats[of "snd_fm(0,1)"] arity_snd_fm ord_simp_union
    snd_closed[simplified] snd_abs
  by simp

lemma lam_replacement_snd: "lam_replacement(##M, snd)"
  using lam_replacement_snd' separation_snd transM by simp

text‹Binary lambda-replacements›

lemma separation_Image: "AM 
     separation(##M, λy. xM. x  A  y = x, fst(x) `` snd(x))"
  using  arity_image_fm ord_simp_union
    nonempty image_closed image_abs
  by (rule_tac separation_assm_bin_sats[of "image_fm(0,1,2)"],auto)

lemma lam_replacement_Image: "lam_replacement(##M, λx . fst(x) `` snd(x))"
  using lam_replacement_Image' separation_Image
  by simp

lemma separation_middle_del: "AM 
     separation(##M, λy. xM. x  A  y = x, middle_del(fst(x), snd(x)))"
 using  arity_is_middle_del_fm ord_simp_union nonempty
    fst_abs snd_abs fst_closed snd_closed pair_in_M_iff
  by (rule_tac separation_assm_bin_sats[of "is_middle_del_fm(0,1,2)"],
      auto simp:is_middle_del_def middle_del_def)

lemma lam_replacement_middle_del: "lam_replacement(##M, λr . middle_del(fst(r),snd(r)))"
  using lam_replacement_middle_del' separation_middle_del
  by simp

lemma separation_prodRepl: "AM 
     separation(##M, λy. xM. x  A  y = x, prodRepl(fst(x), snd(x)))"
   using  arity_is_prodRepl_fm ord_simp_union nonempty
    fst_abs snd_abs fst_closed snd_closed pair_in_M_iff
  by (rule_tac separation_assm_bin_sats[of "is_prodRepl_fm(0,1,2)"],
      auto simp:is_prodRepl_def prodRepl_def)

lemma lam_replacement_prodRepl: "lam_replacement(##M, λr . prodRepl(fst(r),snd(r)))"
  using lam_replacement_prodRepl' separation_prodRepl
  by simp

end  ― ‹localeM_Z_trans

context M_trivial
begin

lemma first_closed:
  "M(B)  M(r)  first(u,r,B)  M(u)"
  using transM[OF first_is_elem] by simp

is_iff_rel for "first"
  unfolding is_first_def first_rel_def by auto

is_iff_rel for "minimum"
  unfolding is_minimum_def minimum_rel_def
  using is_first_iff The_abs nonempty
  by force

end ― ‹localeM_trivial

context M_Z_trans
begin

lemma (in M_basic) is_minimum_equivalence :
  "M(R)  M(X)  M(u)  is_minimum(M,R,X,u)  is_minimum'(M,R,X,u)"
  unfolding is_minimum_def is_minimum'_def is_The_def is_first_def by simp

lemma separation_minimum: "AM 
     separation(##M, λy. xM. x  A  y = x, minimum(fst(x), snd(x)))"
  using  arity_minimum_fm ord_simp_union is_minimum_iff minimum_abs
    is_minimum_equivalence nonempty minimum_closed minimum_abs
  by (rule_tac separation_assm_bin_sats[of "minimum_fm(0,1,2)"], auto)

lemma lam_replacement_minimum: "lam_replacement(##M, λx . minimum(fst(x),snd(x)))"
  using lam_replacement_minimum' separation_minimum
  by simp

end ― ‹localeM_Z_trans

end