Quelle  Interface.thy

section‹Interface between set models and Constructibility›

text‹This theory provides an interface between Paulson's
  results and set models of ZFC. In particular,
  is used to prove that the locale term‹forcing_data› is
  sublocale of all relevant locales in ZF-Constructibility
 term‹M_trivial›, term‹M_basic›, term‹M_eclose›, etc).›

theory Interface
  imports
    Nat_Miscellanea
    Relative_Univ
    Synthetic_Definition
begin

syntax
  "_sats"  :: "[i, i, i] ==> o"  (‹(_, _ ⊨ _)› [36,36,36] 60)
syntax_consts
  "_sats" ⇌ sats
translations
  "(M,env ⊨ φ)" ⇌ "CONST sats(M,φ,env)"

abbreviation
  dec10  :: i   (‹10›) where "10 ≡ succ(9)"

abbreviation
  dec11  :: i   (‹11›) where "11 ≡ succ(10)"

abbreviation
  dec12  :: i   (‹12›) where "12 ≡ succ(11)"

abbreviation
  dec13  :: i   (‹13›) where "13 ≡ succ(12)"

abbreviation
  dec14  :: i   (‹14›) where "14 ≡ succ(13)"


definition
  infinity_ax :: "(i ==> o) ==> o" where
  "infinity_ax(M) ≡
      (∃I[M]. (∃z[M]. empty(M,z) ∧ z∈I) ∧ (∀y[M]. y∈I ⟶ (∃sy[M]. successor(M,y,sy) ∧ sy∈I)))"

definition
  choice_ax :: "(i==>o) ==> o" where
  "choice_ax(M) ≡ ∀x[M]. ∃a[M]. ∃f[M]. ordinal(M,a) ∧ surjection(M,a,x,f)"

context M_basic begin

lemma choice_ax_abs :
  "choice_ax(M) ⟷ (∀x[M]. ∃a[M]. ∃f[M]. Ord(a) ∧ f ∈ surj(a,x))"
  unfolding choice_ax_def
  by (simp)

end (* M_basic *)

definition
  wellfounded_trancl :: "[i=>o,i,i,i] => o" where
  "wellfounded_trancl(M,Z,r,p) ≡
      ∃w[M]. ∃wx[M]. ∃rp[M].
               w ∈ Z & pair(M,w,p,wx) & tran_closure(M,r,rp) & wx ∈ rp"

lemma empty_intf :
  "infinity_ax(M) ==>
  (∃z[M]. empty(M,z))"
  by (auto simp add: empty_def infinity_ax_def)

lemma Transset_intf :
  "Transset(M) ==> y∈x ==> x ∈ M ==> y ∈ M"
  by (simp add: Transset_def,auto)

locale M_ZF_trans =
  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. sats(M,φ,[x] @ env))"
    and replacement_ax:   "φ∈formula ==> env∈list(M) ==> arity(φ) ≤ 2 #+ length(env) ==>
                    strong_replacement(##M,λx y. sats(M,φ,[x,y] @ env))"
    and trans_M:          "Transset(M)"
begin


lemma TranssetI :
  "(∧y x. y∈x ==> x∈M ==> y∈M) ==> Transset(M)"
  by (auto simp add: Transset_def)

lemma zero_in_M:  "0 ∈ M"
proof -
  from infinity_ax have
    "(∃z[##M]. empty(##M,z))"
    by (rule empty_intf)
  then obtain z where
    zm: "empty(##M,z)"  "z∈M"
    by auto
  with trans_M have "z=0"
    by (simp  add: empty_def, blast intro: Transset_intf )
  with zm show ?thesis
    by simp
qed

subsection‹Interface with term‹M_trivial››
lemma mtrans :
  "M_trans(##M)"
  using Transset_intf[OF trans_M] zero_in_M exI[of "λx. x∈M"]
  by unfold_locales auto


lemma mtriv :
  "M_trivial(##M)"
  using trans_M M_trivial.intro mtrans M_trivial_axioms.intro upair_ax Union_ax
  by simp

end

sublocale M_ZF_trans ⊆ M_trivial "##M"
  by (rule mtriv)

context M_ZF_trans
begin

subsection‹Interface with term‹M_basic››

(* Inter_separation: "M(A) \<Longrightarrow> separation(M, \<lambda>x. \<forall> y[M]. y\<in>A \<Longrightarrow> x\<in>y)" *)
schematic_goal inter_fm_auto:
  assumes
    "nth(i,env) = x" "nth(j,env) = B"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "(∀y∈A . y∈B ⟶ x∈y) ⟷ sats(A,?ifm(i,j),env)"
  by (insert assms ; (rule sep_rules | simp)+)

lemma inter_sep_intf :
  assumes
    "A∈M"
  shows
    "separation(##M,λx . ∀y∈M . y∈A ⟶ x∈y)"
proof -
  obtain ifm where
    fmsats:"∧env. env∈list(M) ==> (∀ y∈M. y∈(nth(1,env)) ⟶ nth(0,env)∈y)
    ⟷ sats(M,ifm(0,1),env)"
    and
    "ifm(0,1) ∈ formula"
    and
    "arity(ifm(0,1)) = 2"
    using ‹A∈M› inter_fm_auto
    by (simp del:FOL_sats_iff add: nat_simp_union)
  then
  have "∀a∈M. separation(##M, λx. sats(M,ifm(0,1) , [x, a]))"
    using separation_ax by simp
  moreover
  have "(∀y∈M . y∈a ⟶ x∈y) ⟷ sats(M,ifm(0,1),[x,a])"
    if "a∈M" "x∈M" for a x
    using that fmsats[of "[x,a]"] by simp
  ultimately
  have "∀a∈M. separation(##M, λx . ∀y∈M . y∈a ⟶ x∈y)"
    unfolding separation_def by simp
  with ‹A∈M› show ?thesis by simp
qed


(* Diff_separation: "M(B) \<Longrightarrow> separation(M, \<lambda>x. x \<notin> B)" *)
schematic_goal diff_fm_auto:
  assumes
    "nth(i,env) = x" "nth(j,env) = B"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "x∉B ⟷ sats(A,?dfm(i,j),env)"
  by (insert assms ; (rule sep_rules | simp)+)

lemma diff_sep_intf :
  assumes
    "B∈M"
  shows
    "separation(##M,λx . x∉B)"
proof -
  obtain dfm where
    fmsats:"∧env. env∈list(M) ==> nth(0,env)∉nth(1,env)
    ⟷ sats(M,dfm(0,1),env)"
    and
    "dfm(0,1) ∈ formula"
    and
    "arity(dfm(0,1)) = 2"
    using ‹B∈M› diff_fm_auto
    by (simp del:FOL_sats_iff add: nat_simp_union)
  then
  have "∀b∈M. separation(##M, λx. sats(M,dfm(0,1) , [x, b]))"
    using separation_ax by simp
  moreover
  have "x∉b ⟷ sats(M,dfm(0,1),[x,b])"
    if "b∈M" "x∈M" for b x
    using that fmsats[of "[x,b]"] by simp
  ultimately
  have "∀b∈M. separation(##M, λx . x∉b)"
    unfolding separation_def by simp
  with ‹B∈M› show ?thesis by simp
qed

schematic_goal cprod_fm_auto:
  assumes
    "nth(i,env) = z" "nth(j,env) = B" "nth(h,env) = C"
    "i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
  shows
    "(∃x∈A. x∈B ∧ (∃y∈A. y∈C ∧ pair(##A,x,y,z))) ⟷ sats(A,?cpfm(i,j,h),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma cartprod_sep_intf :
  assumes
    "A∈M"
    and
    "B∈M"
  shows
    "separation(##M,λz. ∃x∈M. x∈A ∧ (∃y∈M. y∈B ∧ pair(##M,x,y,z)))"
proof -
  obtain cpfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃x∈M. x∈nth(1,env) ∧ (∃y∈M. y∈nth(2,env) ∧ pair(##M,x,y,nth(0,env))))
    ⟷ sats(M,cpfm(0,1,2),env)"
    and
    "cpfm(0,1,2) ∈ formula"
    and
    "arity(cpfm(0,1,2)) = 3"
    using cprod_fm_auto by (simp del:FOL_sats_iff add: fm_defs nat_simp_union)
  then
  have "∀a∈M. ∀b∈M. separation(##M, λz. sats(M,cpfm(0,1,2) , [z, a, b]))"
    using separation_ax by simp
  moreover
  have "(∃x∈M. x∈a ∧ (∃y∈M. y∈b ∧ pair(##M,x,y,z))) ⟷ sats(M,cpfm(0,1,2),[z,a,b])"
    if "a∈M" "b∈M" "z∈M" for a b z
    using that fmsats[of "[z,a,b]"] by simp
  ultimately
  have "∀a∈M. ∀b∈M. separation(##M, λz . (∃x∈M. x∈a ∧ (∃y∈M. y∈b ∧ pair(##M,x,y,z))))"
    unfolding separation_def by simp
  with ‹A∈M› ‹B∈M› show ?thesis by simp
qed

schematic_goal im_fm_auto:
  assumes
    "nth(i,env) = y" "nth(j,env) = r" "nth(h,env) = B"
    "i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
  shows
    "(∃p∈A. p∈r & (∃x∈A. x∈B & pair(##A,x,y,p))) ⟷ sats(A,?imfm(i,j,h),env)"
  by (insert assms ; (rule sep_rules | simp)+)

lemma image_sep_intf :
  assumes
    "A∈M"
    and
    "r∈M"
  shows
    "separation(##M, λy. ∃p∈M. p∈r & (∃x∈M. x∈A & pair(##M,x,y,p)))"
proof -
  obtain imfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃p∈M. p∈nth(1,env) & (∃x∈M. x∈nth(2,env) & pair(##M,x,nth(0,env),p)))
    ⟷ sats(M,imfm(0,1,2),env)"
    and
    "imfm(0,1,2) ∈ formula"
    and
    "arity(imfm(0,1,2)) = 3"
    using im_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀r∈M. ∀a∈M. separation(##M, λy. sats(M,imfm(0,1,2) , [y,r,a]))"
    using separation_ax by simp
  moreover
  have "(∃p∈M. p∈k & (∃x∈M. x∈a & pair(##M,x,y,p))) ⟷ sats(M,imfm(0,1,2),[y,k,a])"
    if "k∈M" "a∈M" "y∈M" for k a y
    using that fmsats[of "[y,k,a]"] by simp
  ultimately
  have "∀k∈M. ∀a∈M. separation(##M, λy . ∃p∈M. p∈k & (∃x∈M. x∈a & pair(##M,x,y,p)))"
    unfolding separation_def by simp
  with ‹r∈M› ‹A∈M› show ?thesis by simp
qed

schematic_goal con_fm_auto:
  assumes
    "nth(i,env) = z" "nth(j,env) = R"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "(∃p∈A. p∈R & (∃x∈A.∃y∈A. pair(##A,x,y,p) & pair(##A,y,x,z)))
  ⟷ sats(A,?cfm(i,j),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma converse_sep_intf :
  assumes
    "R∈M"
  shows
    "separation(##M,λz. ∃p∈M. p∈R & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z)))"
proof -
  obtain cfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃p∈M. p∈nth(1,env) & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,nth(0,env))))an>
    ⟷ sats(M,cfm(0,1),env)"
    and
    "cfm(0,1) ∈ formula"
    and
    "arity(cfm(0,1)) = 2"
    using con_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀r∈M. separation(##M, λz. sats(M,cfm(0,1) , [z,r]))"
    using separation_ax by simp
  moreover
  have "(∃p∈M. p∈r & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z))) yle='font-size: 18px;'>⟷
          sats(M,cfm(0,1),[z,r])"
    if "z∈M" "r∈M" for z r
    using that fmsats[of "[z,r]"] by simp
  ultimately
  have "∀r∈M. separation(##M, λz . ∃p∈M. p∈r & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z)))"
    unfolding separation_def by simp
  with ‹R∈M› show ?thesis by simp
qed


schematic_goal rest_fm_auto:
  assumes
    "nth(i,env) = z" "nth(j,env) = C"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "(∃x∈A. x∈C & (∃y∈A. pair(##A,x,y,z)))
  ⟷ sats(A,?rfm(i,j),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma restrict_sep_intf :
  assumes
    "A∈M"
  shows
    "separation(##M,λz. ∃x∈M. x∈A & (∃y∈M. pair(##M,x,y,z)))"
proof -
  obtain rfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃x∈M. x∈nth(1,env) & (∃y∈M. pair(##M,x,y,nth(0,env))))
    ⟷ sats(M,rfm(0,1),env)"
    and
    "rfm(0,1) ∈ formula"
    and
    "arity(rfm(0,1)) = 2"
    using rest_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀a∈M. separation(##M, λz. sats(M,rfm(0,1) , [z,a]))"
    using separation_ax by simp
  moreover
  have "(∃x∈M. x∈a & (∃y∈M. pair(##M,x,y,z))) ⟷
          sats(M,rfm(0,1),[z,a])"
    if "z∈M" "a∈M" for z a
    using that fmsats[of "[z,a]"] by simp
  ultimately
  have "∀a∈M. separation(##M, λz . ∃x∈M. x∈a & (∃y∈M. pair(##M,x,y,z)))"
    unfolding separation_def by simp
  with ‹A∈M› show ?thesis by simp
qed

schematic_goal comp_fm_auto:
  assumes
    "nth(i,env) = xz" "nth(j,env) = S" "nth(h,env) = R"
    "i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
  shows
    "(∃x∈A. ∃y∈A. ∃z∈A. ∃xy∈A. ∃yz∈A.
              pair(##A,x,z,xz) & pair(##A,x,y,xy) & pair(##A,y,z,yz) & xy∈S & yz∈R)
  ⟷ sats(A,?cfm(i,j,h),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma comp_sep_intf :
  assumes
    "R∈M"
    and
    "S∈M"
  shows
    "separation(##M,λxz. ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
              pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈S & yz∈R)"
proof -
  obtain cfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M. pair(##M,x,z,nth(0,env)) &
            pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈nth(1,env) & yz∈nth(2,env))
    ⟷ sats(M,cfm(0,1,2),env)"
    and
    "cfm(0,1,2) ∈ formula"
    and
    "arity(cfm(0,1,2)) = 3"
    using comp_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀r∈M. ∀s∈M. separation(##M, λy. sats(M,cfm(0,1,2) , [y,s,r]))"
    using separation_ax by simp
  moreover
  have "(∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
              pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈s & yz∈r)
          ⟷ sats(M,cfm(0,1,2) , [xz,s,r])"
    if "xz∈M" "s∈M" "r∈M" for xz s r
    using that fmsats[of "[xz,s,r]"] by simp
  ultimately
  have "∀s∈M. ∀r∈M. separation(##M, λxz . ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
              pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈s & yz∈r)"
    unfolding separation_def by simp
  with ‹S∈M› ‹R∈M› show ?thesis by simp
qed


schematic_goal pred_fm_auto:
  assumes
    "nth(i,env) = y" "nth(j,env) = R" "nth(h,env) = X"
    "i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
  shows
    "(∃p∈A. p∈R & pair(##A,y,X,p)) ⟷ sats(A,?pfm(i,j,h),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma pred_sep_intf:
  assumes
    "R∈M"
    and
    "X∈M"
  shows
    "separation(##M, λy. ∃p∈M. p∈R & pair(##M,y,X,p))"
proof -
  obtain pfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃p∈M. p∈nth(1,env) & pair(##M,nth(0,env),nth(2,env),p)) ⟷ sats(M,pfm(0,1,2),env)"
    and
    "pfm(0,1,2) ∈ formula"
    and
    "arity(pfm(0,1,2)) = 3"
    using pred_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀x∈M. ∀r∈M. separation(##M, λy. sats(M,pfm(0,1,2) , [y,r,x]))"
    using separation_ax by simp
  moreover
  have "(∃p∈M. p∈r & pair(##M,y,x,p))
          ⟷ sats(M,pfm(0,1,2) , [y,r,x])"
    if "y∈M" "r∈M" "x∈M" for y x r
    using that fmsats[of "[y,r,x]"] by simp
  ultimately
  have "∀x∈M. ∀r∈M. separation(##M, λ y . ∃p∈M. p∈r & pair(##M,y,x,p))"
    unfolding separation_def by simp
  with ‹X∈M› ‹R∈M› show ?thesis by simp
qed

(* Memrel_separation:
     "separation(M, \<lambda>z. \<exists>x[M]. \<exists>y[M]. pair(M,x,y,z) & x \<in> y)"
*)
schematic_goal mem_fm_auto:
  assumes
    "nth(i,env) = z" "i ∈ nat" "env ∈ list(A)"
  shows
    "(∃x∈A. ∃y∈A. pair(##A,x,y,z) & x ∈ y) ⟷ sats(A,?mfm(i),env)"
  by (insert assms ; (rule sep_rules | simp)+)

lemma memrel_sep_intf:
  "separation(##M, λz. ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y)"
proof -
  obtain mfm where
    fmsats:"∧env. env∈list(M) ==>
    (∃x∈M. ∃y∈M. pair(##M,x,y,nth(0,env)) & x ∈ y) ⟷ sats(M,mfm(0),env)"
    and
    "mfm(0) ∈ formula"
    and
    "arity(mfm(0)) = 1"
    using mem_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "separation(##M, λz. sats(M,mfm(0) , [z]))"
    using separation_ax by simp
  moreover
  have "(∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y) ⟷ sats(M,mfm(0),[z])"
    if "z∈M" for z
    using that fmsats[of "[z]"] by simp
  ultimately
  have "separation(##M, λz . ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y)"
    unfolding separation_def by simp
  then show ?thesis by simp
qed

schematic_goal recfun_fm_auto:
  assumes
    "nth(i1,env) = x" "nth(i2,env) = r" "nth(i3,env) = f" "nth(i4,env) = g" "nth(i5,env) = a"
    "nth(i6,env) = b" "i1∈nat" "i2∈nat" "i3∈nat" "i4∈nat" "i5∈nat" "i6∈nat" "env ∈ list(A)"
  shows
    "(∃xa∈A. ∃xb∈A. pair(##A,x,a,xa) & xa ∈ r & pair(##A,x,b,xb) & xb ∈ r &>
                  (∃fx∈A. ∃gx∈A. fun_apply(##A,f,x,fx) & fun_apply(##A,g,x,gx) & fx ≠ gx))
    ⟷ sats(A,?rffm(i1,i2,i3,i4,i5,i6),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma is_recfun_sep_intf :
  assumes
    "r∈M" "f∈M" "g∈M" "a∈M" "b∈M"
  shows
    "separation(##M,λx. ∃xa∈M. ∃xb∈M.
                    pair(##M,x,a,xa) & xa ∈ r & pair(##M,x,b,xb) & xb ∈ r &
                    (∃fx∈M. ∃gx∈M. fun_apply(##M,f,x,fx) & fun_apply(##M,g,x,gx) &
                                     fx ≠ gx))"
proof -
  obtain rffm where
    fmsats:"∧env. env∈list(M) ==>
    (∃xa∈M. ∃xb∈M. pair(##M,nth(0,env),nth(4,env),xa) & xa ∈ nth(1,env) &
    pair(##M,nth(0,env),nth(5,env),xb) & xb ∈ nth(1,env) & (an style='font-size: 18px;'>∃fx∈M. ∃gx∈M.
    fun_apply(##M,nth(2,env),nth(0,env),fx) & fun_apply(##M,nth(3,env),nth(0,env),gx) & fx ≠ gx))
    ⟷ sats(M,rffm(0,1,2,3,4,5),env)"
    and
    "rffm(0,1,2,3,4,5) ∈ formula"
    and
    "arity(rffm(0,1,2,3,4,5)) = 6"
    using recfun_fm_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀a1∈M. ∀a2∈M. ∀a3∈M. ∀a4∈M. ∀a5∈M.
        separation(##M, λx. sats(M,rffm(0,1,2,3,4,5) , [x,a1,a2,a3,a4,a5]))"
    using separation_ax by simp
  moreover
  have "(∃xa∈M. ∃xb∈M. pair(##M,x,a4,xa) & xa ∈ a1 & pair(##M,x,a5,xb) & xb ∈ a1 &
          (∃fx∈M. ∃gx∈M. fun_apply(##M,a2,x,fx) & fun_apply(##M,a3,x,gx) & fx ≠ gx))
          ⟷ sats(M,rffm(0,1,2,3,4,5) , [x,a1,a2,a3,a4,a5])"
    if "x∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "a5∈M"  for x a1 a2 a3 a4 a5
    using that fmsats[of "[x,a1,a2,a3,a4,a5]"] by simp
  ultimately
  have "∀a1∈M. ∀a2∈M. ∀a3∈M. ∀a4∈M. ∀a5∈M. separation(##M, λ x .
          ∃xa∈M. ∃xb∈M. pair(##M,x,a4,xa) & xa ∈ a1 & pair(##M,x,a5,xb) & xb ∈ a1 &n>
          (∃fx∈M. ∃gx∈M. fun_apply(##M,a2,x,fx) & fun_apply(##M,a3,x,gx) & fx ≠ gx))"
    unfolding separation_def by simp
  with ‹r∈M› ‹f∈M› ‹g∈M› ‹a∈M› ‹b∈M› show ?thesis by simp
qed


(* Instance of Replacement for M_basic *)

schematic_goal funsp_fm_auto:
  assumes
    "nth(i,env) = p" "nth(j,env) = z" "nth(h,env) = n"
    "i ∈ nat" "j ∈ nat" "h ∈ nat" "env ∈ list(A)"
  shows
    "(∃f∈A. ∃b∈A. ∃nb∈A. ∃cnbf∈A. pair(##A,f,b,p) & pair(##A,n,b,nb) & is_cons(##A,nb,f,cnbf) &
    upair(##A,cnbf,cnbf,z)) ⟷ sats(A,?fsfm(i,j,h),env)"
  by (insert assms ; (rule sep_rules | simp)+)


lemma funspace_succ_rep_intf :
  assumes
    "n∈M"
  shows
    "strong_replacement(##M,
          λp z. ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M.
                pair(##M,f,b,p) & pair(##M,n,b,nb) & is_cons(##M,nb,f,cnbf) &
                upair(##M,cnbf,cnbf,z))"
proof -
  obtain fsfm where
    fmsats:"env∈list(M) ==>
    (∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,nth(0,env)) & pair(##M,nth(2,env),b,nb)
      & is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,nth(1,env)))
    ⟷ sats(M,fsfm(0,1,2),env)"
    and "fsfm(0,1,2) ∈ formula" and "arity(fsfm(0,1,2)) = 3" for env
    using funsp_fm_auto[of concl:M] by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀n0∈M. strong_replacement(##M, λp z. sats(M,fsfm(0,1,2) , [p,z,n0]))"
    using replacement_ax by simp
  moreover
  have "(∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,p) & pair(##M,n0,b,nb) &
          is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,z))
          ⟷ sats(M,fsfm(0,1,2) , [p,z,n0])"
    if "p∈M" "z∈M" "n0∈M" for p z n0
    using that fmsats[of "[p,z,n0]"] by simp
  ultimately
  have "∀n0∈M. strong_replacement(##M, λ p z.
          ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M. pair(##M,f,b,p) & pair(##M,n0,b,nb) &
          is_cons(##M,nb,f,cnbf) & upair(##M,cnbf,cnbf,z))"
    unfolding strong_replacement_def univalent_def by simp
  with ‹n∈M› show ?thesis by simp
qed


(* Interface with M_basic *)

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

lemma mbasic : "M_basic(##M)"
  using trans_M zero_in_M power_ax M_basic_sep_instances funspace_succ_rep_intf mtriv
  by unfold_locales auto

end

sublocale M_ZF_trans ⊆ M_basic "##M"
  by (rule mbasic)

subsection‹Interface with term‹M_trancl››

(* rtran_closure_mem *)
schematic_goal rtran_closure_mem_auto:
  assumes
    "nth(i,env) = p" "nth(j,env) = r"  "nth(k,env) = B"
    "i ∈ nat" "j ∈ nat" "k ∈ nat" "env ∈ list(A)"
  shows
    "rtran_closure_mem(##A,B,r,p) ⟷ sats(A,?rcfm(i,j,k),env)"
  unfolding rtran_closure_mem_def
  by (insert assms ; (rule sep_rules | simp)+)


lemma (in M_ZF_trans) rtrancl_separation_intf:
  assumes
    "r∈M"
    and
    "A∈M"
  shows
    "separation (##M, rtran_closure_mem(##M,A,r))"
proof -
  obtain rcfm where
    fmsats:"∧env. env∈list(M) ==>
    (rtran_closure_mem(##M,nth(2,env),nth(1,env),nth(0,env))) ⟷ sats(M,rcfm(0,1,2),env)"
    and
    "rcfm(0,1,2) ∈ formula"
    and
    "arity(rcfm(0,1,2)) = 3"
    using rtran_closure_mem_auto by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀x∈M. ∀a∈M. separation(##M, λy. sats(M,rcfm(0,1,2) , [y,x,a]))"
    using separation_ax by simp
  moreover
  have "(rtran_closure_mem(##M,a,x,y))
          ⟷ sats(M,rcfm(0,1,2) , [y,x,a])"
    if "y∈M" "x∈M" "a∈M" for y x a
    using that fmsats[of "[y,x,a]"] by simp
  ultimately
  have "∀x∈M. ∀a∈M. separation(##M, rtran_closure_mem(##M,a,x))"
    unfolding separation_def by simp
  with ‹r∈M› ‹A∈M› show ?thesis by simp
qed

schematic_goal rtran_closure_fm_auto:
  assumes
    "nth(i,env) = r" "nth(j,env) = rp"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "rtran_closure(##A,r,rp) ⟷ sats(A,?rtc(i,j),env)"
  unfolding rtran_closure_def
  by (insert assms ; (rule sep_rules rtran_closure_mem_auto | simp)+)

schematic_goal trans_closure_fm_auto:
  assumes
    "nth(i,env) = r" "nth(j,env) = rp"
    "i ∈ nat" "j ∈ nat" "env ∈ list(A)"
  shows
    "tran_closure(##A,r,rp) ⟷ sats(A,?tc(i,j),env)"
  unfolding tran_closure_def
  by (insert assms ; (rule sep_rules rtran_closure_fm_auto | simp))+

synthesize "trans_closure_fm" from_schematic trans_closure_fm_auto

schematic_goal wellfounded_trancl_fm_auto:
  assumes
    "nth(i,env) = p" "nth(j,env) = r"  "nth(k,env) = B"
    "i ∈ nat" "j ∈ nat" "k ∈ nat" "env ∈ list(A)"
  shows
    "wellfounded_trancl(##A,B,r,p) ⟷ sats(A,?wtf(i,j,k),env)"
  unfolding  wellfounded_trancl_def
  by (insert assms ; (rule sep_rules trans_closure_fm_iff_sats | simp)+)

lemma (in M_ZF_trans) wftrancl_separation_intf:
  assumes
    "r∈M"
    and
    "Z∈M"
  shows
    "separation (##M, wellfounded_trancl(##M,Z,r))"
proof -
  obtain rcfm where
    fmsats:"∧env. env∈list(M) ==>
    (wellfounded_trancl(##M,nth(2,env),nth(1,env),nth(0,env))) ⟷ sats(M,rcfm(0,1,2),env)"
    and
    "rcfm(0,1,2) ∈ formula"
    and
    "arity(rcfm(0,1,2)) = 3"
    using wellfounded_trancl_fm_auto[of concl:M "nth(2,_)"] unfolding fm_defs trans_closure_fm_def
    by (simp del:FOL_sats_iff pair_abs add: fm_defs nat_simp_union)
  then
  have "∀x∈M. ∀z∈M. separation(##M, λy. sats(M,rcfm(0,1,2) , [y,x,z]))"
    using separation_ax by simp
  moreover
  have "(wellfounded_trancl(##M,z,x,y))
          ⟷ sats(M,rcfm(0,1,2) , [y,x,z])"
    if "y∈M" "x∈M" "z∈M" for y x z
    using that fmsats[of "[y,x,z]"] by simp
  ultimately
  have "∀x∈M. ∀z∈M. separation(##M, wellfounded_trancl(##M,z,x))"
    unfolding separation_def by simp
  with ‹r∈M› ‹Z∈M› show ?thesis by simp
qed

(* nat \<in> M *)

lemma (in M_ZF_trans) finite_sep_intf:
  "separation(##M, λx. x∈nat)"
proof -
  have "arity(finite_ordinal_fm(0)) = 1 "
    unfolding finite_ordinal_fm_def limit_ordinal_fm_def empty_fm_def succ_fm_def cons_fm_def
      union_fm_def upair_fm_def
    by (simp add: nat_union_abs1 Un_commute)
  with separation_ax
  have "(∀v∈M. separation(##M,λx. sats(M,finite_ordinal_fm(0),[x,v])))"
    by simp
  then have "(∀v∈M. separation(##M,finite_ordinal(##M)))"
    unfolding separation_def by simp
  then have "separation(##M,finite_ordinal(##M))"
    using zero_in_M by auto
  then show ?thesis unfolding separation_def by simp
qed


lemma (in M_ZF_trans) nat_subset_I' :
  "[ I∈M ; 0∈I ; ∧x. x∈I ==> succ(x)∈I ] ==> nat ⊆ I"
  by (rule subsetI,induct_tac x,simp+)


lemma (in M_ZF_trans) nat_subset_I :
  "∃I∈M. nat ⊆ I"
proof -
  have "∃I∈M. 0∈I ∧ (∀x∈M. x∈I ⟶ succ(x)∈I)"
    using infinity_ax unfolding infinity_ax_def by auto
  then obtain I where
    "I∈M" "0∈I" "(∀x∈M. x∈I ⟶ succ(x)∈I)"
    by auto
  then have "∧x. x∈I ==> succ(x)∈I"
    using Transset_intf[OF trans_M]  by simp
  then have "nat⊆I"
    using  ‹I∈M› ‹0∈I› nat_subset_I' by simp
  then show ?thesis using ‹I∈M› by auto
qed

lemma (in M_ZF_trans) nat_in_M :
  "nat ∈ M"
proof -
  have 1:"{x∈B . x∈A}=A" if "A⊆B" for A B
    using that by auto
  obtain I where
    "I∈M" "nat⊆I"
    using nat_subset_I by auto
  then have "{x∈I . x∈nat} ∈ M"
    using finite_sep_intf separation_closed[of "λx . x∈nat"] by simp
  then show ?thesis
    using ‹nat⊆I› 1 by simp
qed
  (* end nat \<in> M *)


lemma (in M_ZF_trans) mtrancl : "M_trancl(##M)"
  using  mbasic rtrancl_separation_intf wftrancl_separation_intf nat_in_M
    wellfounded_trancl_def
  by unfold_locales auto

sublocale M_ZF_trans ⊆ M_trancl "##M"
  by (rule mtrancl)

subsection‹Interface with term‹M_eclose››

lemma repl_sats:
  assumes
    sat:"∧x z. x∈M ==> z∈M ==> sats(M,φ,Cons(x,Cons(z,env))) ⟷ P(x,z)"
  shows
    "strong_replacement(##M,λx z. sats(M,φ,Cons(x,Cons(z,env)))) ⟷
   strong_replacement(##M,P)"
  by (rule strong_replacement_cong,simp add:sat)

lemma (in M_ZF_trans) nat_trans_M :
  "n∈M" if "n∈nat" for n
  using that nat_in_M Transset_intf[OF trans_M] by simp

lemma (in M_ZF_trans) list_repl1_intf:
  assumes
    "A∈M"
  shows
    "iterates_replacement(##M, is_list_functor(##M,A), 0)"
proof -
  {
    fix n
    assume "n∈nat"
    have "succ(n)∈M"
      using ‹n∈nat› nat_trans_M by simp
    then have 1:"Memrel(succ(n))∈M"
      using ‹n∈nat› Memrel_closed by simp
    have "0∈M"
      using  nat_0I nat_trans_M by simp
    then have "is_list_functor(##M, A, a, b)
       ⟷ sats(M, list_functor_fm(13,1,0), [b,a,c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),A,0])"
      if "a∈M" "b∈M" "c∈M" "d∈M" "a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
      for a b c d a0 a1 a2 a3 a4 y x z
      using that 1 ‹A∈M› list_functor_iff_sats by simp
    then have "sats(M, iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0), [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),A,0])
        ⟷ iterates_MH(##M,is_list_functor(##M,A),0,a2, a1, a0)"
      if "a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
      for a0 a1 a2 a3 a4 y x z
      using that sats_iterates_MH_fm[of M "is_list_functor(##M,A)" _] 1 ‹0∈M› ‹A∈M›  by simp
    then have 2:"sats(M, is_wfrec_fm(iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0),3,1,0),
                            [y,x,z,Memrel(succ(n)),A,0])
        ⟷
        is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) , Memrel(succ(n)), x, y)"
      if "y∈M" "x∈M" "z∈M" for y x z
      using  that sats_is_wfrec_fm 1 ‹0∈M› ‹A∈M› by simp
    let
      ?f="Exists(And(pair_fm(1,0,2),
               is_wfrec_fm(iterates_MH_fm(list_functor_fm(13,1,0),10,2,1,0),3,1,0)))"
    have satsf:"sats(M, ?f, [x,z,Memrel(succ(n)),A,0])
        ⟷
        (∃y∈M. pair(##M,x,y,z) &
        is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) , Memrel(succ(n)), x, y))"
      if "x∈M" "z∈M" for x z
      using that 2 1 ‹0∈M› ‹A∈M› by (simp del:pair_abs)
    have "arity(?f) = 5"
      unfolding iterates_MH_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
        restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
        sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
      by (simp add:nat_simp_union)
    then
    have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),A,0]))"
      using replacement_ax 1 ‹A∈M› ‹0∈M› by simp
    then
    have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, iterates_MH(##M,is_list_functor(##M,A),0) ,
                Memrel(succ(n)), x, y))"
      using repl_sats[of M ?f "[Memrel(succ(n)),A,0]"]  satsf by (simp del:pair_abs)
  }
  then
  show ?thesis unfolding iterates_replacement_def wfrec_replacement_def by simp
qed



(* Iterates_replacement para predicados sin parámetros *)
lemma (in M_ZF_trans) iterates_repl_intf :
  assumes
    "v∈M" and
    isfm:"is_F_fm ∈ formula" and
    arty:"arity(is_F_fm)=2" and
    satsf: "∧a b env'. [ a∈M ; b∈M ; env'∈list(M) ]
              ==> is_F(a,b) ⟷ sats(M, is_F_fm, [b,a]@env')"
  shows
    "iterates_replacement(##M,is_F,v)"
proof -
  {
    fix n
    assume "n∈nat"
    have "succ(n)∈M"
      using ‹n∈nat› nat_trans_M by simp
    then have 1:"Memrel(succ(n))∈M"
      using ‹n∈nat› Memrel_closed by simp
    {
      fix a0 a1 a2 a3 a4 y x z
      assume as:"a0∈M" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "y∈M" "x∈M" "z∈M"
      have "sats(M, is_F_fm, Cons(b,Cons(a,Cons(c,Cons(d,[a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v])))))
          ⟷ is_F(a,b)"
        if "a∈M" "b∈M" "c∈M" "d∈M" for a b c d
        using as that 1 satsf[of a b "[c,d,a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v]"] ‹v∈M› by simp
      then
      have "sats(M, iterates_MH_fm(is_F_fm,9,2,1,0), [a0,a1,a2,a3,a4,y,x,z,Memrel(succ(n)),v])
          ⟷ iterates_MH(##M,is_F,v,a2, a1, a0)"
        using as
          sats_iterates_MH_fm[of M "is_F" "is_F_fm"] 1 ‹v∈M› by simp
    }
    then have 2:"sats(M, is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0),
                            [y,x,z,Memrel(succ(n)),v])
        ⟷
        is_wfrec(##M, iterates_MH(##M,is_F,v),Memrel(succ(n)), x, y)"
      if "y∈M" "x∈M" "z∈M" for y x z
      using  that sats_is_wfrec_fm 1 ‹v∈M› by simp
    let
      ?f="Exists(And(pair_fm(1,0,2),
               is_wfrec_fm(iterates_MH_fm(is_F_fm,9,2,1,0),3,1,0)))"
    have satsf:"sats(M, ?f, [x,z,Memrel(succ(n)),v])
        ⟷
        (∃y∈M. pair(##M,x,y,z) &
        is_wfrec(##M, iterates_MH(##M,is_F,v) , Memrel(succ(n)), x, y))"
      if "x∈M" "z∈M" for x z
      using that 2 1 ‹v∈M› by (simp del:pair_abs)
    have "arity(?f) = 4"
      unfolding iterates_MH_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
        restriction_fm_def pre_image_fm_def quasinat_fm_def fm_defs
      using arty by (simp add:nat_simp_union)
    then
    have "strong_replacement(##M,λx z. sats(M,?f,[x,z,Memrel(succ(n)),v]))"
      using replacement_ax 1 ‹v∈M› ‹is_F_fm∈formula› by simp
    then
    have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, iterates_MH(##M,is_F,v) ,
                Memrel(succ(n)), x, y))"
      using repl_sats[of M ?f "[Memrel(succ(n)),v]"]  satsf by (simp del:pair_abs)
  }
  then
  show ?thesis unfolding iterates_replacement_def wfrec_replacement_def by simp
qed

lemma (in M_ZF_trans) formula_repl1_intf :
  "iterates_replacement(##M, is_formula_functor(##M), 0)"
proof -
  have "0∈M"
    using  nat_0I nat_trans_M by simp
  have 1:"arity(formula_functor_fm(1,0)) = 2"
    unfolding formula_functor_fm_def fm_defs sum_fm_def cartprod_fm_def number1_fm_def
    by (simp add:nat_simp_union)
  have 2:"formula_functor_fm(1,0)∈formula" by simp
  have "is_formula_functor(##M,a,b) ⟷
        sats(M, formula_functor_fm(1,0), [b,a])"
    if "a∈M" "b∈M"  for a b
    using that by simp
  then show ?thesis using ‹0∈M› 1 2 iterates_repl_intf by simp
qed

lemma (in M_ZF_trans) nth_repl_intf:
  assumes
    "l ∈ M"
  shows
    "iterates_replacement(##M,λl' t. is_tl(##M,l',t),l)"
proof -
  have 1:"arity(tl_fm(1,0)) = 2"
    unfolding tl_fm_def fm_defs quasilist_fm_def Cons_fm_def Nil_fm_def Inr_fm_def number1_fm_def
      Inl_fm_def by (simp add:nat_simp_union)
  have 2:"tl_fm(1,0)∈formula" by simp
  have "is_tl(##M,a,b) ⟷ sats(M, tl_fm(1,0), [b,a])"
    if "a∈M" "b∈M" for a b
    using that by simp
  then show ?thesis using ‹l∈M› 1 2 iterates_repl_intf by simp
qed


lemma (in M_ZF_trans) eclose_repl1_intf:
  assumes
    "A∈M"
  shows
    "iterates_replacement(##M, big_union(##M), A)"
proof -
  have 1:"arity(big_union_fm(1,0)) = 2"
    unfolding big_union_fm_def fm_defs by (simp add:nat_simp_union)
  have 2:"big_union_fm(1,0)∈formula" by simp
  have "big_union(##M,a,b) ⟷ sats(M, big_union_fm(1,0), [b,a])"
    if "a∈M" "b∈M" for a b
    using that by simp
  then show ?thesis using ‹A∈M› 1 2 iterates_repl_intf by simp
qed

(*
    and list_replacement2:
   "M(A) \<Longrightarrow> strong_replacement(M,
         \<lambda>n y. n\<in>nat & is_iterates(M, is_list_functor(M,A), 0, n, y))"

*)
lemma (in M_ZF_trans) list_repl2_intf:
  assumes
    "A∈M"
  shows
    "strong_replacement(##M,λn y. n∈nat & is_iterates(##M, is_list_functor(##M,A), 0, n, y))"
proof -
  have "0∈M"
    using  nat_0I nat_trans_M by simp
  have "is_list_functor(##M,A,a,b) ⟷
        sats(M,list_functor_fm(13,1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,A,0,nat])"
    if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
    for a b c d e f g h i j k n y
    using that ‹0∈M› nat_in_M ‹A∈M› by simp
  then
  have 1:"sats(M, is_iterates_fm(list_functor_fm(13,1,0),3,0,1),[n,y,A,0,nat] ) ⟷
           is_iterates(##M, is_list_functor(##M,A), 0, n , y)"
    if "n∈M" "y∈M" for n y
    using that ‹0∈M› ‹A∈M› nat_in_M
      sats_is_iterates_fm[of M "is_list_functor(##M,A)"] by simp
  let ?f = "And(Member(0,4),is_iterates_fm(list_functor_fm(13,1,0),3,0,1))"
  have satsf:"sats(M, ?f,[n,y,A,0,nat] ) ⟷
        n∈nat & is_iterates(##M, is_list_functor(##M,A), 0, n, y)"
    if "n∈M" "y∈M" for n y
    using that ‹0∈M› ‹A∈M› nat_in_M 1 by simp
  have "arity(?f) = 5"
    unfolding is_iterates_fm_def restriction_fm_def list_functor_fm_def number1_fm_def Memrel_fm_def
      cartprod_fm_def sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs is_wfrec_fm_def
      is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def
    by (simp add:nat_simp_union)
  then
  have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,0,nat]))"
    using replacement_ax 1 nat_in_M ‹A∈M› ‹0∈M› by simp
  then
  show ?thesis using repl_sats[of M ?f "[A,0,nat]"]  satsf  by simp
qed

lemma (in M_ZF_trans) formula_repl2_intf:
  "strong_replacement(##M,λn y. n∈nat & is_iterates(##M, is_formula_functor(##M), 0, n, y))"
proof -
  have "0∈M"
    using  nat_0I nat_trans_M by simp
  have "is_formula_functor(##M,a,b) ⟷
        sats(M,formula_functor_fm(1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,0,nat])"
    if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
    for a b c d e f g h i j k n y
    using that ‹0∈M› nat_in_M by simp
  then
  have 1:"sats(M, is_iterates_fm(formula_functor_fm(1,0),2,0,1),[n,y,0,nat] ) ⟷
           is_iterates(##M, is_formula_functor(##M), 0, n , y)"
    if "n∈M" "y∈M" for n y
    using that ‹0∈M› nat_in_M
      sats_is_iterates_fm[of M "is_formula_functor(##M)"] by simp
  let ?f = "And(Member(0,3),is_iterates_fm(formula_functor_fm(1,0),2,0,1))"
  have satsf:"sats(M, ?f,[n,y,0,nat] ) ⟷
        n∈nat & is_iterates(##M, is_formula_functor(##M), 0, n, y)"
    if "n∈M" "y∈M" for n y
    using that ‹0∈M› nat_in_M 1 by simp
  have artyf:"arity(?f) = 4"
    unfolding is_iterates_fm_def formula_functor_fm_def fm_defs sum_fm_def quasinat_fm_def
      cartprod_fm_def number1_fm_def Memrel_fm_def ordinal_fm_def transset_fm_def
      is_wfrec_fm_def is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def subset_fm_def
      pre_image_fm_def restriction_fm_def
    by (simp add:nat_simp_union)
  then
  have "strong_replacement(##M,λn y. sats(M,?f,[n,y,0,nat]))"
    using replacement_ax 1 artyf ‹0∈M› nat_in_M by simp
  then
  show ?thesis using repl_sats[of M ?f "[0,nat]"]  satsf  by simp
qed


(*
   "M(A) \<Longrightarrow> strong_replacement(M,
         \<lambda>n y. n\<in>nat & is_iterates(M, big_union(M), A, n, y))"
*)

lemma (in M_ZF_trans) eclose_repl2_intf:
  assumes
    "A∈M"
  shows
    "strong_replacement(##M,λn y. n∈nat & is_iterates(##M, big_union(##M), A, n, y))"
proof -
  have "big_union(##M,a,b) ⟷
        sats(M,big_union_fm(1,0),[b,a,c,d,e,f,g,h,i,j,k,n,y,A,nat])"
    if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "f∈M""g∈M""h∈M""i∈M""j∈M" "k∈M" "n∈M" "y∈M"
    for a b c d e f g h i j k n y
    using that ‹A∈M› nat_in_M by simp
  then
  have 1:"sats(M, is_iterates_fm(big_union_fm(1,0),2,0,1),[n,y,A,nat] ) ⟷
           is_iterates(##M, big_union(##M), A, n , y)"
    if "n∈M" "y∈M" for n y
    using that ‹A∈M› nat_in_M
      sats_is_iterates_fm[of M "big_union(##M)"] by simp
  let ?f = "And(Member(0,3),is_iterates_fm(big_union_fm(1,0),2,0,1))"
  have satsf:"sats(M, ?f,[n,y,A,nat] ) ⟷
        n∈nat & is_iterates(##M, big_union(##M), A, n, y)"
    if "n∈M" "y∈M" for n y
    using that ‹A∈M› nat_in_M 1 by simp
  have artyf:"arity(?f) = 4"
    unfolding is_iterates_fm_def formula_functor_fm_def fm_defs sum_fm_def quasinat_fm_def
      cartprod_fm_def number1_fm_def Memrel_fm_def ordinal_fm_def transset_fm_def
      is_wfrec_fm_def is_recfun_fm_def iterates_MH_fm_def is_nat_case_fm_def subset_fm_def
      pre_image_fm_def restriction_fm_def
    by (simp add:nat_simp_union)
  then
  have "strong_replacement(##M,λn y. sats(M,?f,[n,y,A,nat]))"
    using replacement_ax 1 artyf ‹A∈M› nat_in_M by simp
  then
  show ?thesis using repl_sats[of M ?f "[A,nat]"]  satsf  by simp
qed

lemma (in M_ZF_trans) mdatatypes : "M_datatypes(##M)"
  using  mtrancl list_repl1_intf list_repl2_intf formula_repl1_intf
    formula_repl2_intf nth_repl_intf
  by unfold_locales auto

sublocale M_ZF_trans ⊆ M_datatypes "##M"
  by (rule mdatatypes)

lemma (in M_ZF_trans) meclose : "M_eclose(##M)"
  using mdatatypes eclose_repl1_intf eclose_repl2_intf
  by unfold_locales auto

sublocale M_ZF_trans ⊆ M_eclose "##M"
  by (rule meclose)

(* Interface with locale M_eclose_pow *)

(* "powerset(M,A,z) \<equiv> \<forall>x[M]. x \<in> z \<longleftrightarrow> subset(M,x,A)" *)
definition
  powerset_fm :: "[i,i] ==> i" where
  "powerset_fm(A,z) ≡ Forall(Iff(Member(0,succ(z)),subset_fm(0,succ(A))))"

lemma powerset_type [TC]:
  "[ x ∈ nat; y ∈ nat ] ==> powerset_fm(x,y) ∈ formula"
  by (simp add:powerset_fm_def)

definition
  is_powapply_fm :: "[i,i,i] ==> i" where
  "is_powapply_fm(f,y,z) ≡
      Exists(And(fun_apply_fm(succ(f), succ(y), 0),
            Forall(Iff(Member(0, succ(succ(z))),
            Forall(Implies(Member(0, 1), Member(0, 2)))))))"

lemma is_powapply_type [TC] :
  "[f∈nat ; y∈nat; z∈nat] ==> is_powapply_fm(f,y,z)∈formula"
  unfolding is_powapply_fm_def by simp

lemma sats_is_powapply_fm :
  assumes
    "f∈nat" "y∈nat" "z∈nat" "env∈list(A)" "0∈A"
  shows
    "is_powapply(##A,nth(f, env),nth(y, env),nth(z, env))
    ⟷ sats(A,is_powapply_fm(f,y,z),env)"
  unfolding is_powapply_def is_powapply_fm_def is_Collect_def powerset_def subset_def
  using nth_closed assms by simp


lemma (in M_ZF_trans) powapply_repl :
  assumes
    "f∈M"
  shows
    "strong_replacement(##M,is_powapply(##M,f))"
proof -
  have "arity(is_powapply_fm(2,0,1)) = 3"
    unfolding is_powapply_fm_def
    by (simp add: fm_defs nat_simp_union)
  then
  have "∀f0∈M. strong_replacement(##M, λp z. sats(M,is_powapply_fm(2,0,1) , [p,z,f0]))"
    using replacement_ax by simp
  moreover
  have "is_powapply(##M,f0,p,z) ⟷ sats(M,is_powapply_fm(2,0,1) , [p,z,f0])"
    if "p∈M" "z∈M" "f0∈M" for p z f0
    using that zero_in_M sats_is_powapply_fm[of 2 0 1 "[p,z,f0]" M] by simp
  ultimately
  have "∀f0∈M. strong_replacement(##M, is_powapply(##M,f0))"
    unfolding strong_replacement_def univalent_def by simp
  with ‹f∈M› show ?thesis by simp
qed


(*"PHrank(M,f,y,z) \<equiv> M(z) \<and> (\<exists>fy[M]. fun_apply(M,f,y,fy) \<and> successor(M,fy,z))"*)
definition
  PHrank_fm :: "[i,i,i] ==> i" where
  "PHrank_fm(f,y,z) ≡ Exists(And(fun_apply_fm(succ(f),succ(y),0)
                                 ,succ_fm(0,succ(z))))"

lemma PHrank_type [TC]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat ] ==> PHrank_fm(x,y,z) ∈ formula"
  by (simp add:PHrank_fm_def)


lemma (in M_ZF_trans) sats_PHrank_fm [simp]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(M) ]
    ==> sats(M,PHrank_fm(x,y,z),env) ⟷
        PHrank(##M,nth(x,env),nth(y,env),nth(z,env))"
  using zero_in_M Internalizations.nth_closed by (simp add: PHrank_def PHrank_fm_def)


lemma (in M_ZF_trans) phrank_repl :
  assumes
    "f∈M"
  shows
    "strong_replacement(##M,PHrank(##M,f))"
proof -
  have "arity(PHrank_fm(2,0,1)) = 3"
    unfolding PHrank_fm_def
    by (simp add: fm_defs nat_simp_union)
  then
  have "∀f0∈M. strong_replacement(##M, λp z. sats(M,PHrank_fm(2,0,1) , [p,z,f0]))"
    using replacement_ax by simp
  then
  have "∀f0∈M. strong_replacement(##M, PHrank(##M,f0))"
    unfolding strong_replacement_def univalent_def by simp
  with ‹f∈M› show ?thesis by simp
qed


(*"is_Hrank(M,x,f,hc) \<equiv> (\<exists>R[M]. big_union(M,R,hc) \<and>is_Replace(M,x,PHrank(M,f),R)) "*)
definition
  is_Hrank_fm :: "[i,i,i] ==> i" where
  "is_Hrank_fm(x,f,hc) ≡ Exists(And(big_union_fm(0,succ(hc)),
                                Replace_fm(succ(x),PHrank_fm(succ(succ(succ(f))),0,1),0)))"

lemma is_Hrank_type [TC]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat ] ==> is_Hrank_fm(x,y,z) ∈ formula"
  by (simp add:is_Hrank_fm_def)

lemma (in M_ZF_trans) sats_is_Hrank_fm [simp]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(M)]
    ==> sats(M,is_Hrank_fm(x,y,z),env) ⟷
        is_Hrank(##M,nth(x,env),nth(y,env),nth(z,env))"
  using zero_in_M is_Hrank_def is_Hrank_fm_def sats_Replace_fm
  by simp

(* M(x) \<Longrightarrow> wfrec_replacement(M,is_Hrank(M),rrank(x)) *)
lemma (in M_ZF_trans) wfrec_rank :
  assumes
    "X∈M"
  shows
    "wfrec_replacement(##M,is_Hrank(##M),rrank(X))"
proof -
  have
    "is_Hrank(##M,a2, a1, a0) ⟷
             sats(M, is_Hrank_fm(2,1,0), [a0,a1,a2,a3,a4,y,x,z,rrank(X)])"
    if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
    using that rrank_in_M ‹X∈M› by simp
  then
  have
    1:"sats(M, is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0),[y,x,z,rrank(X)])
  ⟷ is_wfrec(##M, is_Hrank(##M) ,rrank(X), x, y)"
    if "y∈M" "x∈M" "z∈M" for y x z
    using that ‹X∈M› rrank_in_M sats_is_wfrec_fm by simp
  let
    ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_Hrank_fm(2,1,0),3,1,0)))"
  have satsf:"sats(M, ?f, [x,z,rrank(X)])
              ⟷ (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
    if "x∈M" "z∈M" for x z
    using that 1 ‹X∈M› rrank_in_M by (simp del:pair_abs)
  have "arity(?f) = 3"
    unfolding is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def is_Hrank_fm_def PHrank_fm_def
      restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
      sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
    by (simp add:nat_simp_union)
  then
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,rrank(X)]))"
    using replacement_ax 1 ‹X∈M› rrank_in_M by simp
  then
  have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hrank(##M) , rrank(X), x, y))"
    using repl_sats[of M ?f "[rrank(X)]"]  satsf by (simp del:pair_abs)
  then
  show ?thesis unfolding wfrec_replacement_def  by simp
qed

(*"is_HVfrom(M,A,x,f,h) \<equiv> \<exists>U[M]. \<exists>R[M].  union(M,A,U,h)
        \<and> big_union(M,R,U) \<and> is_Replace(M,x,is_powapply(M,f),R)"*)
definition
  is_HVfrom_fm :: "[i,i,i,i] ==> i" where
  "is_HVfrom_fm(A,x,f,h) ≡ Exists(Exists(And(union_fm(A #+ 2,1,h #+ 2),
                            And(big_union_fm(0,1),
                            Replace_fm(x #+ 2,is_powapply_fm(f #+ 4,0,1),0)))))"

lemma is_HVfrom_type [TC]:
  "[ A∈nat; x ∈ nat; f ∈ nat; h ∈ nat ] ==> is_HVfrom_fm(A,x,f,h) ∈ formula"
  by (simp add:is_HVfrom_fm_def)

lemma sats_is_HVfrom_fm :
  "[ a∈nat; x ∈ nat; f ∈ nat; h ∈ nat; env ∈ list(A); 0∈A]
    ==> sats(A,is_HVfrom_fm(a,x,f,h),env) ⟷
        is_HVfrom(##A,nth(a,env),nth(x,env),nth(f,env),nth(h,env))"
  using is_HVfrom_def is_HVfrom_fm_def sats_Replace_fm[OF sats_is_powapply_fm]
  by simp

lemma is_HVfrom_iff_sats:
  assumes
    "nth(a,env) = aa" "nth(x,env) = xx" "nth(f,env) = ff" "nth(h,env) = hh"
    "a∈nat" "x∈nat" "f∈nat" "h∈nat" "env∈list(A)" "0∈A"
  shows
    "is_HVfrom(##A,aa,xx,ff,hh) ⟷ sats(A, is_HVfrom_fm(a,x,f,h), env)"
  using assms sats_is_HVfrom_fm by simp

(* FIX US *)
schematic_goal sats_is_Vset_fm_auto:
  assumes
    "i∈nat" "v∈nat" "env∈list(A)" "0∈A"
    "i < length(env)" "v < length(env)"
  shows
    "is_Vset(##A,nth(i, env),nth(v, env))
    ⟷ sats(A,?ivs_fm(i,v),env)"
  unfolding is_Vset_def is_Vfrom_def
  by (insert assms; (rule sep_rules is_HVfrom_iff_sats is_transrec_iff_sats | simp)+)

schematic_goal is_Vset_iff_sats:
  assumes
    "nth(i,env) = ii" "nth(v,env) = vv"
    "i∈nat" "v∈nat" "env∈list(A)" "0∈A"
    "i < length(env)" "v < length(env)"
  shows
    "is_Vset(##A,ii,vv) ⟷ sats(A, ?ivs_fm(i,v), env)"
  unfolding ‹nth(i,env) = ii›[symmetric] ‹nth(v,env) = vv›[symmetric]
  by (rule sats_is_Vset_fm_auto(1); simp add:assms)


lemma (in M_ZF_trans) memrel_eclose_sing :
  "a∈M ==> ∃sa∈M. ∃esa∈M. ∃mesa∈M.
       upair(##M,a,a,sa) & is_eclose(##M,sa,esa) & membership(##M,esa,mesa)"
  using upair_ax eclose_closed Memrel_closed unfolding upair_ax_def
  by (simp del:upair_abs)


lemma (in M_ZF_trans) trans_repl_HVFrom :
  assumes
    "A∈M" "i∈M"
  shows
    "transrec_replacement(##M,is_HVfrom(##M,A),i)"
proof -
  { fix mesa
    assume "mesa∈M"
    have
      0:"is_HVfrom(##M,A,a2, a1, a0) ⟷
      sats(M, is_HVfrom_fm(8,2,1,0), [a0,a1,a2,a3,a4,y,x,z,A,mesa])"
      if "a4∈M" "a3∈M" "a2∈M" "a1∈M" "a0∈M" "y∈M" "x∈M" "z∈M" for a4 a3 a2 a1 a0 y x z
      using that zero_in_M sats_is_HVfrom_fm ‹mesa∈M› ‹A∈M› by simp
    have
      1:"sats(M, is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0),[y,x,z,A,mesa])
        ⟷ is_wfrec(##M, is_HVfrom(##M,A),mesa, x, y)"
      if "y∈M" "x∈M" "z∈M" for y x z
      using that ‹A∈M› ‹mesa∈M› sats_is_wfrec_fm[OF 0] by simp
    let
      ?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(is_HVfrom_fm(8,2,1,0),4,1,0)))"
    have satsf:"sats(M, ?f, [x,z,A,mesa])
              ⟷ (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
      if "x∈M" "z∈M" for x z
      using that 1 ‹A∈M› ‹mesa∈M› by (simp del:pair_abs)
    have "arity(?f) = 4"
      unfolding is_HVfrom_fm_def is_wfrec_fm_def is_recfun_fm_def is_nat_case_fm_def
        restriction_fm_def list_functor_fm_def number1_fm_def cartprod_fm_def
        is_powapply_fm_def sum_fm_def quasinat_fm_def pre_image_fm_def fm_defs
      by (simp add:nat_simp_union)
    then
    have "strong_replacement(##M,λx z. sats(M,?f,[x,z,A,mesa]))"
      using replacement_ax 1 ‹A∈M› ‹mesa∈M› by simp
    then
    have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_HVfrom(##M,A) , mesa, x, y))"
      using repl_sats[of M ?f "[A,mesa]"]  satsf by (simp del:pair_abs)
    then
    have "wfrec_replacement(##M,is_HVfrom(##M,A),mesa)"
      unfolding wfrec_replacement_def  by simp
  }
  then show ?thesis unfolding transrec_replacement_def
    using ‹i∈M› memrel_eclose_sing by simp
qed


lemma (in M_ZF_trans) meclose_pow : "M_eclose_pow(##M)"
  using meclose power_ax powapply_repl phrank_repl trans_repl_HVFrom wfrec_rank
  by unfold_locales auto

sublocale M_ZF_trans ⊆ M_eclose_pow "##M"
  by (rule meclose_pow)

lemma (in M_ZF_trans) repl_gen :
  assumes
    f_abs: "∧x y. [ x∈M; y∈M ] ==> is_F(##M,x,y) ⟷ y = f(x)"
    and
    f_sats: "∧x y. [x∈M ; y∈M ] ==>
             sats(M,f_fm,Cons(x,Cons(y,env))) ⟷ is_F(##M,x,y)"
    and
    f_form: "f_fm ∈ formula"
    and
    f_arty: "arity(f_fm) = 2"
    and
    "env∈list(M)"
  shows
    "strong_replacement(##M, λx y. y = f(x))"
proof -
  have "sats(M,f_fm,[x,y]@env) ⟷ is_F(##M,x,y)" if "x∈M" "y∈M" for x y
    using that f_sats[of x y] by simp
  moreover
  from f_form f_arty
  have "strong_replacement(##M, λx y. sats(M,f_fm,[x,y]@env))"
    using ‹env∈list(M)› replacement_ax by simp
  ultimately
  have "strong_replacement(##M, is_F(##M))"
    using strong_replacement_cong[of "##M" "λx y. sats(M,f_fm,[x,y]@env)" "is_F(##M)"] by simp
  with f_abs show ?thesis
    using strong_replacement_cong[of "##M" "is_F(##M)" "λx y. y = f(x)"] by simp
qed

(* Proof Scheme for instances of separation *)
lemma (in M_ZF_trans) sep_in_M :
  assumes
    "φ ∈ formula" "env∈list(M)"
    "arity(φ) ≤ 1 #+ length(env)" "A∈M" and
    satsQ: "∧x. x∈M ==> sats(M,φ,[x]@env) ⟷ Q(x)"
  shows
    "{y∈A . Q(y)}∈M"
proof -
  have "separation(##M,λx. sats(M,φ,[x] @ env))"
    using assms separation_ax by simp
  then show ?thesis using
      ‹A∈M› satsQ trans_M
      separation_cong[of "##M" "λy. sats(M,φ,[y]@env)" "Q"]
      separation_closed  by simp
qed

end