Session Independence_CH

Theory Forcing_Notions

section‹Forcing notions›
text‹This theory defines a locale for forcing notions, that is,
 preorders with a distinguished maximum element.›

theory Forcing_Notions
  imports
    "ZF-Constructible.Relative"
    "Delta_System_Lemma.ZF_Library"
begin

subsection‹Basic concepts›
text‹We say that two elements $p,q$ are
  ∗‹compatible› if they have a lower bound in $P$›
definition compat_in :: "i⇒i⇒i⇒i⇒o" where
  "compat_in(A,r,p,q) ≡ ∃d∈A . ⟨d,p⟩∈r ∧ ⟨d,q⟩∈r"

lemma compat_inI :
  "⟦ d∈A ; ⟨d,p⟩∈r ; ⟨d,g⟩∈r ⟧ ⟹ compat_in(A,r,p,g)"
  by (auto simp add: compat_in_def)

lemma refl_compat:
  "⟦ refl(A,r) ; ⟨p,q⟩ ∈ r | p=q | ⟨q,p⟩ ∈ r ; p∈A ; q∈A⟧ ⟹ compat_in(A,r,p,q)"
  by (auto simp add: refl_def compat_inI)

lemma  chain_compat:
  "refl(A,r) ⟹ linear(A,r) ⟹  (∀p∈A.∀q∈A. compat_in(A,r,p,q))"
  by (simp add: refl_compat linear_def)

lemma subset_fun_image: "f:N→P ⟹ f``N⊆P"
  by (auto simp add: image_fun apply_funtype)

lemma refl_monot_domain: "refl(B,r) ⟹ A⊆B ⟹ refl(A,r)"
  unfolding refl_def by blast

locale forcing_notion =
  fixes P leq one
  assumes one_in_P:       "one ∈ P"
    and leq_preord:       "preorder_on(P,leq)"
    and one_max:          "∀p∈P. ⟨p,one⟩∈leq"
begin

notation one (‹𝟭›)

abbreviation Leq :: "[i, i] ⇒ o"  (infixl "≼" 50)
  where "x ≼ y ≡ ⟨x,y⟩∈leq"

lemma refl_leq:
  "r∈P ⟹ r≼r"
  using leq_preord unfolding preorder_on_def refl_def by simp

text‹A set $D$ is ∗‹dense› if every element $p\in P$ has a lower
bound in $D$.›
definition
  dense :: "i⇒o" where
  "dense(D) ≡ ∀p∈P. ∃d∈D . d≼p"

text‹There is also a weaker definition which asks for
a lower bound in $D$ only for the elements below some fixed
element $q$.›
definition
  dense_below :: "i⇒i⇒o" where
  "dense_below(D,q) ≡ ∀p∈P. p≼q ⟶ (∃d∈D. d∈P ∧ d≼p)"

lemma P_dense: "dense(P)"
  by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)

definition
  increasing :: "i⇒o" where
  "increasing(F) ≡ ∀x∈F. ∀ p ∈ P . x≼p ⟶ p∈F"

definition
  compat :: "i⇒i⇒o" where
  "compat(p,q) ≡ compat_in(P,leq,p,q)"

lemma leq_transD:  "a≼b ⟹ b≼c ⟹ a ∈ P⟹ b ∈ P⟹ c ∈ P⟹ a≼c"
  using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "A⊆P ⟹ a≼b ⟹ b≼c ⟹ a ∈ A ⟹ b ∈ P⟹ c ∈ P⟹ a≼c"
  using leq_preord trans_onD subsetD unfolding preorder_on_def by blast

lemma compatD[dest!]: "compat(p,q) ⟹ ∃d∈P. d≼p ∧ d≼q"
  unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i] ⇒ o"  (infixl "⊥" 50)
  where "p ⊥ q ≡ ¬ compat(p,q)"

lemma compatI[intro!]: "d∈P ⟹ d≼p ⟹ d≼q ⟹ compat(p,q)"
  unfolding compat_def compat_in_def by blast

lemma denseD [dest]: "dense(D) ⟹ p∈P ⟹  ∃d∈D. d≼ p"
  unfolding dense_def by blast

lemma denseI [intro!]: "⟦ ⋀p. p∈P ⟹ ∃d∈D. d≼ p ⟧ ⟹ dense(D)"
  unfolding dense_def by blast

lemma dense_belowD [dest]:
  assumes "dense_below(D,p)" "q∈P" "q≼p"
  shows "∃d∈D. d∈P ∧ d≼q"
  using assms unfolding dense_below_def by simp

lemma dense_belowI [intro!]:
  assumes "⋀q. q∈P ⟹ q≼p ⟹ ∃d∈D. d∈P ∧ d≼q"
  shows "dense_below(D,p)"
  using assms unfolding dense_below_def by simp

lemma dense_below_cong: "p∈P ⟹ D = D' ⟹ dense_below(D,p) ⟷ dense_below(D',p)"
  by blast

lemma dense_below_cong': "p∈P ⟹ ⟦⋀x. x∈P ⟹ Q(x) ⟷ Q'(x)⟧ ⟹
           dense_below({q∈P. Q(q)},p) ⟷ dense_below({q∈P. Q'(q)},p)"
  by blast

lemma dense_below_mono: "p∈P ⟹ D ⊆ D' ⟹ dense_below(D,p) ⟹ dense_below(D',p)"
  by blast

lemma dense_below_under:
  assumes "dense_below(D,p)" "p∈P" "q∈P" "q≼p"
  shows "dense_below(D,q)"
  using assms leq_transD by blast

lemma ideal_dense_below:
  assumes "⋀q. q∈P ⟹ q≼p ⟹ q∈D"
  shows "dense_below(D,p)"
  using assms refl_leq by blast

lemma dense_below_dense_below:
  assumes "dense_below({q∈P. dense_below(D,q)},p)" "p∈P"
  shows "dense_below(D,p)"
  using assms leq_transD refl_leq  by blast

text‹A filter is an increasing set $G$ with all its elements
being compatible in $G$.›
definition
  filter :: "i⇒o" where
  "filter(G) ≡ G⊆P ∧ increasing(G) ∧ (∀p∈G. ∀q∈G. compat_in(G,leq,p,q))"

lemma filterD : "filter(G) ⟹ x ∈ G ⟹ x ∈ P"
  by (auto simp add : subsetD filter_def)

lemma filter_leqD : "filter(G) ⟹ x ∈ G ⟹ y ∈ P ⟹ x≼y ⟹ y ∈ G"
  by (simp add: filter_def increasing_def)

lemma filter_imp_compat: "filter(G) ⟹ p∈G ⟹ q∈G ⟹ compat(p,q)"
  unfolding filter_def compat_in_def compat_def by blast

lemma low_bound_filter: ― ‹says the compatibility is attained inside G›
  assumes "filter(G)" and "p∈G" and "q∈G"
  shows "∃r∈G. r≼p ∧ r≼q"
  using assms
  unfolding compat_in_def filter_def by blast

text‹We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.›
definition
  upclosure :: "i⇒i" where
  "upclosure(A) ≡ {p∈P.∃a∈A. a≼p}"

lemma  upclosureI [intro] : "p∈P ⟹ a∈A ⟹ a≼p ⟹ p∈upclosure(A)"
  by (simp add:upclosure_def, auto)

lemma  upclosureE [elim] :
  "p∈upclosure(A) ⟹ (⋀x a. x∈P ⟹ a∈A ⟹ a≼x ⟹ R) ⟹ R"
  by (auto simp add:upclosure_def)

lemma  upclosureD [dest] :
  "p∈upclosure(A) ⟹ ∃a∈A.(a≼p) ∧ p∈P"
  by (simp add:upclosure_def)

lemma upclosure_increasing :
  assumes "A⊆P"
  shows "increasing(upclosure(A))"
  unfolding increasing_def upclosure_def
  using leq_transD'[OF ‹A⊆P›] by auto

lemma  upclosure_in_P: "A ⊆ P ⟹ upclosure(A) ⊆ P"
  using subsetI upclosure_def by simp

lemma  A_sub_upclosure: "A ⊆ P ⟹ A⊆upclosure(A)"
  using subsetI leq_preord
  unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "A⊆P ⟹ x∈A  ⟹ x∈upclosure(A)"
  by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
  assumes "A⊆P" "(∀p∈A.∀q∈A. compat_in(A,leq,p,q))"
  shows "filter(upclosure(A))"
  unfolding filter_def
proof(auto)
  show "increasing(upclosure(A))"
    using assms upclosure_increasing by simp
next
  let ?UA="upclosure(A)"
  show "compat_in(upclosure(A), leq, p, q)" if "p∈?UA" "q∈?UA" for p q
  proof -
    from that
    obtain a b where 1:"a∈A" "b∈A" "a≼p" "b≼q" "p∈P" "q∈P"
      using upclosureD[OF ‹p∈?UA›] upclosureD[OF ‹q∈?UA›] by auto
    with assms(2)
    obtain d where "d∈A" "d≼a" "d≼b"
      unfolding compat_in_def by auto
    with 1
    have "d≼p" "d≼q" "d∈?UA"
      using A_sub_upclosure[THEN subsetD] ‹A⊆P›
        leq_transD'[of A d a] leq_transD'[of A d b] by auto
    then
    show ?thesis unfolding compat_in_def by auto
  qed
qed

lemma  aux_RS1:  "f ∈ N → P ⟹ n∈N ⟹ f`n ∈ upclosure(f ``N)"
  using elem_upclosure[OF subset_fun_image] image_fun
  by (simp, blast)

lemma decr_succ_decr:
  assumes "f ∈ nat → P" "preorder_on(P,leq)"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "m∈nat"
  shows "n∈nat ⟹ n≤m ⟹ ⟨f ` m, f ` n⟩ ∈ leq"
  using ‹m∈_›
proof(induct m)
  case 0
  then show ?case using assms refl_leq by simp
next
  case (succ x)
  then
  have 1:"f`succ(x) ≼ f`x" "f`n∈P" "f`x∈P" "f`succ(x)∈P"
    using assms by simp_all
  consider (lt) "n<succ(x)" | (eq) "n=succ(x)"
    using succ le_succ_iff by auto
  then
  show ?case
  proof(cases)
    case lt
    with 1 show ?thesis using leI succ leq_transD by auto
  next
    case eq
    with 1 show ?thesis using refl_leq by simp
  qed
qed

lemma decr_seq_linear:
  assumes "refl(P,leq)" "f ∈ nat → P"
    "∀n∈nat.  ⟨f ` succ(n), f ` n⟩ ∈ leq"
    "trans[P](leq)"
  shows "linear(f `` nat, leq)"
proof -
  have "preorder_on(P,leq)"
    unfolding preorder_on_def using assms by simp
  {
    fix n m
    assume "n∈nat" "m∈nat"
    then
    have "f`m ≼ f`n ∨ f`n ≼ f`m"
    proof(cases "m≤n")
      case True
      with ‹n∈_› ‹m∈_›
      show ?thesis
        using decr_succ_decr[of f n m] assms leI ‹preorder_on(P,leq)› by simp
    next
      case False
      with ‹n∈_› ‹m∈_›
      show ?thesis
        using decr_succ_decr[of f m n] assms leI not_le_iff_lt ‹preorder_on(P,leq)› by simp
    qed
  }
  then
  show ?thesis
    unfolding linear_def using ball_image_simp assms by auto
qed

end ― ‹locale‹forcing_notion››

subsection‹Towards Rasiowa-Sikorski Lemma (RSL)›
locale countable_generic = forcing_notion +
  fixes 𝒟
  assumes countable_subs_of_P:  "𝒟 ∈ nat→Pow(P)"
    and     seq_of_denses:        "∀n ∈ nat. dense(𝒟`n)"

begin

definition
  D_generic :: "i⇒o" where
  "D_generic(G) ≡ filter(G) ∧ (∀n∈nat.(𝒟`n)∩G≠0)"

text‹The next lemma identifies a sufficient condition for obtaining
RSL.›
lemma RS_sequence_imp_rasiowa_sikorski:
  assumes
    "p∈P" "f : nat→P" "f ` 0 = p"
    "⋀n. n∈nat ⟹ f ` succ(n)≼ f ` n ∧ f ` succ(n) ∈ 𝒟 ` n"
  shows
    "∃G. p∈G ∧ D_generic(G)"
proof -
  note assms
  moreover from this
  have "f``nat  ⊆ P"
    by (simp add:subset_fun_image)
  moreover from calculation
  have "refl(f``nat, leq) ∧ trans[P](leq)"
    using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
  moreover from calculation
  have "∀n∈nat.  f ` succ(n)≼ f ` n" by (simp)
  moreover from calculation
  have "linear(f``nat, leq)"
    using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
  moreover from calculation
  have "(∀p∈f``nat.∀q∈f``nat. compat_in(f``nat,leq,p,q))"
    using chain_compat by (auto)
  ultimately
  have "filter(upclosure(f``nat))" (is "filter(?G)")
    using closure_compat_filter by simp
  moreover
  have "∀n∈nat. 𝒟 ` n ∩ ?G ≠ 0"
  proof
    fix n
    assume "n∈nat"
    with assms
    have "f`succ(n) ∈ ?G ∧ f`succ(n) ∈ 𝒟 ` n"
      using aux_RS1 by simp
    then
    show "𝒟 ` n ∩ ?G ≠ 0"  by blast
  qed
  moreover from assms
  have "p ∈ ?G"
    using aux_RS1 by auto
  ultimately
  show ?thesis unfolding D_generic_def by auto
qed

end ― ‹locale‹countable_generic››

text‹Now, the following recursive definition will fulfill the
requirements of lemma term‹RS_sequence_imp_rasiowa_sikorski› ›

consts RS_seq :: "[i,i,i,i,i,i] ⇒ i"
primrec
  "RS_seq(0,P,leq,p,enum,𝒟) = p"
  "RS_seq(succ(n),P,leq,p,enum,𝒟) =
    enum`(μ m. ⟨enum`m, RS_seq(n,P,leq,p,enum,𝒟)⟩ ∈ leq ∧ enum`m ∈ 𝒟 ` n)"

context countable_generic
begin

lemma countable_RS_sequence_aux:
  fixes p enum
  defines "f(n) ≡ RS_seq(n,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
    "⋀x k. x∈P ⟹ k∈nat ⟹  ∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k"
  shows
    "f(succ(n)) ∈ P ∧ f(succ(n))≼ f(n) ∧ f(succ(n)) ∈ 𝒟 ` n"
  using ‹n∈nat›
proof (induct)
  case 0
  from assms
  obtain q where "q∈P" "q≼ p" "q ∈ 𝒟 ` 0" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m = q"
    using Pi_rangeD[OF ‹enum:nat→M›] by blast
  moreover
  have "𝒟`0 ⊆ P"
    using apply_funtype[OF countable_subs_of_P] by simp
  moreover note ‹p∈P›
  ultimately
  show ?case
    using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
  case (succ n)
  with assms
  obtain q where "q∈P" "q≼ f(succ(n))" "q ∈ 𝒟 ` succ(n)" by blast
  moreover from this and ‹P ⊆ range(enum)›
  obtain m where "m∈nat" "enum`m≼ f(succ(n))" "enum`m ∈ 𝒟 ` succ(n)"
    using Pi_rangeD[OF ‹enum:nat→M›] by blast
  moreover note succ
  moreover from calculation
  have "𝒟`succ(n) ⊆ P"
    using apply_funtype[OF countable_subs_of_P] by auto
  ultimately
  show ?case
    using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed

lemma countable_RS_sequence:
  fixes p enum
  defines "f ≡ λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)"
    and   "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
  assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows
    "f`0 = p" "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n) ∈ P"
proof -
  from assms
  show "f`0 = p" by simp
  {
    fix x k
    assume "x∈P" "k∈nat"
    then
    have "∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k"
      using seq_of_denses apply_funtype[OF countable_subs_of_P]
      unfolding dense_def by blast
  }
  with assms
  show "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n)∈P"
    unfolding f_def using countable_RS_sequence_aux by simp_all
qed

lemma RS_seq_type:
  assumes "n ∈ nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows "RS_seq(n,P,leq,p,enum,𝒟) ∈ P"
  using assms countable_RS_sequence(1,3)
  by (induct;simp)

lemma RS_seq_funtype:
  assumes "p∈P" "P ⊆ range(enum)" "enum:nat→M"
  shows "(λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)): nat → P"
  using assms lam_type RS_seq_type by auto

lemmas countable_rasiowa_sikorski =
  RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]

end ― ‹locale‹countable_generic››

end
ad>

Theory Cohen_Posets_Relative

section‹Cohen forcing notions›

theory Cohen_Posets_Relative
  imports
    Forcing_Notions
    Transitive_Models.Delta_System_Relative
    Transitive_Models.Partial_Functions_Relative
begin

locale cohen_data =
  fixes κ I J::i
  assumes zero_lt_kappa: "0<κ"
begin

lemmas zero_lesspoll_kappa = zero_lesspoll[OF zero_lt_kappa]

end ― ‹locale‹cohen_data››

locale add_reals = cohen_data nat _ 2

subsection‹Combinatorial results on Cohen posets›

sublocale cohen_data ⊆ forcing_notion "Fn(κ,I,J)" "Fnle(κ,I,J)" 0
proof
  show "0 ∈ Fn(κ, I, J)"
    using zero_lt_kappa zero_in_Fn by simp
  then
  show "∀p∈Fn(κ, I, J). ⟨p, 0⟩ ∈ Fnle(κ, I, J)"
    unfolding preorder_on_def refl_def trans_on_def
    by auto
next
  show "preorder_on(Fn(κ, I, J), Fnle(κ, I, J))"
    unfolding preorder_on_def refl_def trans_on_def
    by blast
qed

context cohen_data
begin

lemma compat_imp_Un_is_function:
  assumes "G ⊆ Fn(κ, I, J)" "⋀p q. p ∈ G ⟹ q ∈ G ⟹ compat(p,q)"
  shows "function(⋃G)"
  unfolding function_def
proof (intro allI ballI impI)
  fix x y y'
  assume "⟨x, y⟩ ∈ ⋃G" "⟨x, y'⟩ ∈ ⋃G"
  then
  obtain p q where "⟨x, y⟩ ∈ p" "⟨x, y'⟩ ∈ q" "p ∈ G" "q ∈ G"
    by auto
  moreover from this and assms
  obtain r where "r ∈ Fn(κ, I, J)" "r ⊇ p" "r ⊇ q"
    using compatD[of p q] by force
  moreover from this
  have "function(r)"
    using Fn_is_function by simp
  ultimately
  show "y = y'"
    unfolding function_def by fastforce
qed

(* MOVE THIS to an appropriate place *)
lemma filter_subset_notion: "filter(G) ⟹ G ⊆ Fn(κ, I, J)"
  unfolding filter_def by simp

lemma Un_filter_is_function: "filter(G) ⟹ function(⋃G)"
  using compat_imp_Un_is_function filter_imp_compat[of G]
    filter_subset_notion
  by simp

end ― ‹locale‹cohen_data››

locale M_cohen = M_delta +
  assumes
    countable_lepoll_assms2:
    "M(A') ⟹ M(A) ⟹ M(b) ⟹ M(f) ⟹ separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. {p ∈ A . domain(p) = a}, b, f, i)⟩)"
    and
    countable_lepoll_assms3:
    "M(A) ⟹ M(f) ⟹ M(b) ⟹ M(D) ⟹ M(r') ⟹ M(A')⟹
        separation(M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(drSR_Y(r', D, A), b, f, i)⟩)"

context M_cardinal_library
begin

lemma lesspoll_nat_imp_lesspoll_rel:
  assumes "A ≺ ω" "M(A)"
  shows "A ≺⇗M⇖ ω"
proof -
  note assms
  moreover from this
  obtain f n where "f∈bij⇗M⇖(A,n)" "n∈ω" "A ≈⇗M⇖ n"
    using lesspoll_nat_is_Finite Finite_rel_def[of M A]
    by auto
  moreover from calculation
  have "A ≲⇗M⇖ ω"
    using lesspoll_nat_is_Finite Infinite_imp_nats_lepoll_rel[of ω n]
      nat_not_Finite eq_lepoll_rel_trans[of A n ω]
    by auto
  moreover from calculation
  have "¬ g ∈ bij⇗M⇖(A,ω)" for g
    using mem_bij_rel unfolding lesspoll_def by auto
  ultimately
  show ?thesis
    unfolding lesspoll_rel_def
    by auto
qed

lemma Finite_imp_lesspoll_rel_nat:
  assumes "Finite(A)" "M(A)"
  shows "A ≺⇗M⇖ ω"
  using Finite_imp_lesspoll_nat assms lesspoll_nat_imp_lesspoll_rel
  by auto

lemma InfCard_rel_lesspoll_rel_Un:
  includes Ord_dests
  assumes "InfCard_rel(M,κ)" "A ≺⇗M⇖ κ" "B ≺⇗M⇖ κ"
    and types: "M(κ)" "M(A)" "M(B)"
  shows "A ∪ B ≺⇗M⇖ κ"
proof -
  from assms
  have "|A|⇗M⇖ < κ" "|B|⇗M⇖ < κ"
    using lesspoll_rel_cardinal_rel_lt InfCard_rel_is_Card_rel
    by auto
  show ?thesis
  proof (cases "Finite(A) ∧ Finite(B)")
    case True
    with assms
    show ?thesis
      using lesspoll_rel_trans2[OF _ le_imp_lepoll_rel, of _ nat κ]
        Finite_imp_lesspoll_rel_nat[OF Finite_Un]
      unfolding InfCard_rel_def
      by simp
  next
    case False
    with types
    have "InfCard_rel(M,max(|A|⇗M⇖,|B|⇗M⇖))"
      using Infinite_InfCard_rel_cardinal_rel InfCard_rel_is_Card_rel
        le_trans[of nat] not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖"]
      unfolding max_def InfCard_rel_def
      by auto
    with ‹M(A)› ‹M(B)›
    have "|A ∪ B|⇗M⇖ ≤ max(|A|⇗M⇖,|B|⇗M⇖)"
      using cardinal_rel_Un_le[of "max(|A|⇗M⇖,|B|⇗M⇖)" A B]
        not_le_iff_lt[THEN iffD1, THEN leI, of "|A|⇗M⇖" "|B|⇗M⇖" ]
      unfolding max_def
      by simp
    moreover from ‹|A|⇗M⇖ < κ› ‹|B|⇗M⇖ < κ›
    have "max(|A|⇗M⇖,|B|⇗M⇖) < κ"
      unfolding max_def
      by simp
    ultimately
    have "|A ∪ B|⇗M⇖ <  κ"
      using lt_trans1
      by blast
    moreover
    note ‹InfCard_rel(M,κ)›
    moreover from calculation types
    have "|A ∪ B|⇗M⇖ ≺⇗M⇖ κ"
      using lt_Card_rel_imp_lesspoll_rel InfCard_rel_is_Card_rel
      by simp
    ultimately
    show ?thesis
      using cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[of "A ∪ B" "|A ∪ B|⇗M⇖" κ]
        eqpoll_rel_sym types
      by simp
  qed
qed

end ― ‹locale‹M_cardinal_library››

lemma (in M_cohen) Fn_rel_unionI:
  assumes "p ∈ Fn⇗M⇖(κ,I,J)" "q∈Fn⇗M⇖(κ,I,J)" "InfCard⇗M⇖(κ)"
    "M(κ)" "M(I)" "M(J)" "domain(p) ∩ domain(q) = 0"
  shows "p∪q ∈ Fn⇗M⇖(κ,I,J)"
proof -
  note assms
  moreover from calculation
  have "p ≺⇗M⇖ κ" "q ≺⇗M⇖ κ" "M(p)" "M(q)"
    using Fn_rel_is_function by simp_all
  moreover from calculation
  have "p∪q ≺⇗M⇖ κ"
    using eqpoll_rel_sym cardinal_rel_eqpoll_rel InfCard_rel_lesspoll_rel_Un
    by simp_all
  ultimately
  show ?thesis
    unfolding Fn_rel_def
    using pfun_unionI cardinal_rel_eqpoll_rel eq_lesspoll_rel_trans[OF _ ‹p∪q ≺⇗M⇖ _›]
    by auto
qed

lemma (in M_cohen) restrict_eq_imp_compat_rel:
  assumes "p ∈ Fn⇗M⇖(κ, I, J)" "q ∈ Fn⇗M⇖(κ, I, J)" "InfCard⇗M⇖(κ)" "M(J)" "M(κ)"
    "restrict(p, domain(p) ∩ domain(q)) = restrict(q, domain(p) ∩ domain(q))"
  shows "p ∪ q ∈ Fn⇗M⇖(κ, I, J)"
proof -
  note assms
  moreover from calculation
  have "p ≺⇗M⇖ κ" "q ≺⇗M⇖ κ" "M(p)" "M(q)"
    using Fn_rel_is_function by simp_all
  moreover from calculation
  have "p∪q ≺⇗M⇖ κ"
    using InfCard_rel_lesspoll_rel_Un cardinal_rel_eqpoll_rel[THEN eqpoll_rel_sym]
    by auto
  ultimately
  show ?thesis
    unfolding Fn_rel_def
    using pfun_restrict_eq_imp_compat cardinal_rel_eqpoll_rel
      eq_lesspoll_rel_trans[OF _ ‹p∪q ≺⇗M⇖ _›]
    by auto
qed

lemma (in M_cohen) InfCard_rel_imp_n_lesspoll_rel :
  assumes "InfCard⇗M⇖(κ)" "M(κ)" "n∈ω"
  shows "n ≺⇗M⇖ κ"
proof -
  note assms
  moreover from this
  have "n ≺⇗M⇖ ω"
    using n_lesspoll_rel_nat by simp
  ultimately
  show ?thesis
    using lesspoll_rel_trans2 Infinite_iff_lepoll_rel_nat InfCard_rel_imp_Infinite nat_into_M
    by simp
qed

lemma (in M_cohen) cons_in_Fn_rel:
  assumes "x ∉ domain(p)" "p ∈ Fn⇗M⇖(κ,I,J)" "x ∈ I" "j ∈ J" "InfCard⇗M⇖(κ)"
    "M(κ)" "M(I)" "M(J)"
  shows "cons(⟨x,j⟩, p) ∈ Fn⇗M⇖(κ,I,J)"
  using assms cons_eq Fn_rel_unionI[OF Fn_rel_singletonI[of x I j J] ‹p∈_›]
    InfCard_rel_imp_n_lesspoll_rel
  by auto

lemma (in M_library) Fnle_rel_Aleph_rel1_closed[intro,simp]:
  "M(Fnle⇗M⇖(ℵ⇘1⇙⇗M⇖, ℵ⇘1⇙⇗M⇖, ω →⇗M⇖ 2))"
  by simp

locale M_add_reals = M_cohen + add_reals
begin

lemmas zero_lesspoll_rel_kappa = zero_lesspoll_rel[OF zero_lt_kappa]

end ― ‹locale‹M_add_reals››

(* MOVE THIS to some appropriate place. Notice that in Forcing_Notions
we don't import anything relative. *)
relativize relational "compat_in" "is_compat_in" external
synthesize "compat_in" from_definition "is_compat_in" assuming "nonempty"
context
  notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "compat_in_fm"
end

lemma (in M_trivial) compat_in_abs[absolut]:
  assumes
    "M(A)" "M(r)" "M(p)" "M(q)"
  shows
    "is_compat_in(M,A,r,p,q) ⟷ compat_in(A,r,p,q)"
  using assms unfolding is_compat_in_def compat_in_def by simp

definition
  antichain :: "i⇒i⇒i⇒o" where
  "antichain(P,leq,A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A. p≠q ⟶ ¬compat_in(P,leq,p,q))"

relativize relational  "antichain" "antichain_rel"
definition
  ccc :: "i ⇒ i ⇒ o" where
  "ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"

abbreviation
  antichain_rel_abbr :: "[i⇒o,i,i,i] ⇒ o" (‹antichain⇗_⇖'(_,_,_')›) where
  "antichain⇗M⇖(P,leq,A) ≡ antichain_rel(M,P,leq,A)"

abbreviation
  antichain_r_set :: "[i,i,i,i] ⇒ o" (‹antichain⇗_⇖'(_,_,_')›) where
  "antichain⇗M⇖(P,leq,A) ≡ antichain_rel(##M,P,leq,A)"

context M_trivial
begin

lemma antichain_abs [absolut]:
  "⟦ M(A); M(P); M(leq) ⟧ ⟹ antichain⇗M⇖(P,leq,A) ⟷ antichain(P,leq,A)"
  unfolding antichain_rel_def antichain_def by (simp add:absolut)

end ― ‹locale‹M_trivial››

relativize relational "ccc" "ccc_rel"

abbreviation
  ccc_rel_abbr :: "[i⇒o,i,i]⇒o" (‹ccc⇗_⇖'(_,_')›) where
  "ccc_rel_abbr(M) ≡ ccc_rel(M)"

abbreviation
  ccc_r_set :: "[i,i,i]⇒o" (‹ccc⇗_⇖'(_,_')›) where
  "ccc_r_set(M) ≡ ccc_rel(##M)"

context M_cardinals
begin

lemma def_ccc_rel:
  shows
    "ccc⇗M⇖(P,leq) ⟷ (∀A[M]. antichain⇗M⇖(P,leq,A) ⟶ |A|⇗M⇖ ≤ ω)"
  using is_cardinal_iff
  unfolding ccc_rel_def by (simp add:absolut)

end ― ‹locale‹M_cardinals››

context M_FiniteFun
begin

lemma Fnle_nat_closed[intro,simp]:
  assumes "M(I)" "M(J)"
  shows "M(Fnle(ω,I,J))"
  unfolding Fnle_def Fnlerel_def Rrel_def
  using supset_separation FiniteFun_closed Fn_nat_eq_FiniteFun assms by simp

lemma Fn_nat_closed:
  assumes "M(A)" "M(B)" shows "M(Fn(ω,A,B))"
  using assms Fn_nat_eq_FiniteFun
  by simp

end ― ‹locale‹M_FiniteFun››

context M_add_reals
begin

lemma lam_replacement_drSR_Y: "M(A) ⟹ M(D) ⟹ M(r') ⟹ lam_replacement(M, drSR_Y(r',D,A))"
  using lam_replacement_drSR_Y
  by simp

lemma (in M_trans) mem_F_bound3:
  fixes F A
  defines "F ≡ dC_F"
  shows "x∈F(A,c) ⟹ c ∈ (range(f) ∪ {domain(x). x∈A})"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)

lemma ccc_rel_Fn_nat:
  assumes "M(I)"
  shows "ccc⇗M⇖(Fn(nat,I,2), Fnle(nat,I,2))"
proof -
  have repFun_dom_closed:"M({domain(p) . p ∈ A})" if "M(A)" for A
    using RepFun_closed domain_replacement_simp transM[OF _ ‹M(A)›] that
    by auto
  from assms
  have "M(Fn(nat,I,2))" using Fn_nat_eq_FiniteFun by simp
  {
    fix A
    assume "¬ |A|⇗M⇖ ≤ nat" "M(A)" "A ⊆ Fn(nat, I, 2)"
    moreover from this
    have "countable_rel(M,{p∈A. domain(p) = d})" if "M(d)" for d
    proof (cases "d≺⇗M⇖nat ∧ d ⊆ I")
      case True
      with ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
      have "{p ∈ A . domain(p) = d} ⊆ d →⇗M⇖ 2"
        using domain_of_fun function_space_rel_char[of _ 2]
        by (auto,subgoal_tac "M(domain(x))",simp_all add:transM[of _ A],force)
      moreover from True ‹M(d)›
      have "Finite(d →⇗M⇖ 2)"
        using Finite_Pi[THEN [2] subset_Finite, of _ d "λ_. 2"]
          lesspoll_rel_nat_is_Finite_rel function_space_rel_char[of _ 2]
        by auto
      moreover from ‹M(d)›
      have "M(d →⇗M⇖ 2)"
        by simp
      moreover from ‹M(A)›
      have "M({p ∈ A . domain(p) = d})"
        using separation_closed domain_eq_separation[OF ‹M(d)›] by simp
      ultimately
      show ?thesis using subset_Finite[of _ "d→⇗M⇖2" ]
        by (auto intro!:Finite_imp_countable_rel)
    next
      case False
      with ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
      have "domain(p) ≠ d" if "p∈A" for p
      proof -
        note False that ‹M(A)›
        moreover from this
        obtain d' where "d' ⊆ I" "p∈d' → 2" "d' ≺ ω"
          using FnD[OF subsetD[OF ‹A⊆_› ‹p∈A›]]
          by auto
        moreover from this
        have "p ≈ d'" "domain(p) = d'"
          using function_eqpoll Pi_iff
          by auto
        ultimately
        show ?thesis
          using lesspoll_nat_imp_lesspoll_rel transM[of p]
          by auto
      qed
      then
      show ?thesis
        using empty_lepoll_relI by auto
    qed
    have 2:"M(x) ⟹ x ∈ dC_F(X, i) ⟹ M(i)" for x X i
      unfolding dC_F_def
      by auto
    moreover
    have "uncountable_rel(M,{domain(p) . p ∈ A})"
    proof
      interpret M_replacement_lepoll M dC_F
        using lam_replacement_dC_F domain_eq_separation lam_replacement_inj_rel
        unfolding dC_F_def
      proof(unfold_locales,simp_all)
        fix X b f
        assume "M(X)" "M(b)" "M(f)"
        with 2[of X]
        show "lam_replacement(M, λx. μ i. x ∈ if_range_F_else_F(λd. {p ∈ X . domain(p) = d}, b, f, i))"
          using lam_replacement_dC_F domain_eq_separation
            mem_F_bound3 countable_lepoll_assms2 repFun_dom_closed
          by (rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈X}"],auto)
      qed (auto)
      have "∃a∈A. x = domain(a) ⟹ M(dC_F(A,x))" for x
        using ‹M(A)› transM[OF _ ‹M(A)›] by (auto)
      moreover
      have "w ∈ A ∧ domain(w) = x ⟹ M(x)" for w x
        using transM[OF _ ‹M(A)›] by auto
      ultimately
      interpret M_cardinal_UN_lepoll _ "dC_F(A)" "{domain(p). p∈A}"
        using lam_replacement_dC_F lam_replacement_inj_rel ‹M(A)›
          lepoll_assumptions domain_eq_separation
          countable_lepoll_assms2 repFun_dom_closed
          lepoll_assumptions1[OF ‹M(A)› repFun_dom_closed[OF ‹M(A)›]]
        apply(unfold_locales)
        by(simp_all del:if_range_F_else_F_def,
            rule_tac lam_Least_assumption_general[where U="λ_. {domain(x). x∈A}"])
          (auto simp del:if_range_F_else_F_def simp add:dC_F_def)
      from ‹A ⊆ Fn(nat, I, 2)›
      have x:"(⋃d∈{domain(p) . p ∈ A}. {p∈A. domain(p) = d}) = A"
        by auto
      moreover
      assume "countable_rel(M,{domain(p) . p ∈ A})"
      moreover
      note ‹⋀d. M(d) ⟹ countable_rel(M,{p∈A. domain(p) = d})›
      moreover from ‹M(A)›
      have "p∈A ⟹ M(domain(p))" for p
        by (auto dest: transM)
      ultimately
      have "countable_rel(M,A)"
        using countable_rel_imp_countable_rel_UN
        unfolding dC_F_def
        by auto
      with ‹¬ |A|⇗M⇖ ≤ nat› ‹M(A)›
      show False
        using countable_rel_iff_cardinal_rel_le_nat by simp
    qed
    moreover from ‹A ⊆ Fn(nat, I, 2)› ‹M(A)›
    have "p ∈ A ⟹ Finite(domain(p))" for p
      using lesspoll_rel_nat_is_Finite_rel[of "domain(p)"]
        lesspoll_nat_imp_lesspoll_rel[of "domain(p)"]
        domain_of_fun[of p _ "λ_. 2"] by (auto dest:transM)
    moreover
    note repFun_dom_closed[OF ‹M(A)›]
    ultimately
    obtain D where "delta_system(D)" "D ⊆ {domain(p) . p ∈ A}" "D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(D)"
      using delta_system_uncountable_rel[of "{domain(p) . p ∈ A}"] by auto
    then
    have delta:"∀d1∈D. ∀d2∈D. d1 ≠ d2 ⟶ d1 ∩ d2 = ⋂D"
      using delta_system_root_eq_Inter
      by simp
    moreover from ‹D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› ‹M(D)›
    have "uncountable_rel(M,D)"
      using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1 by auto
    moreover from this and ‹D ⊆ {domain(p) . p ∈ A}›
    obtain p1 where "p1 ∈ A" "domain(p1) ∈ D"
      using uncountable_rel_not_empty[of D] by blast
    moreover from this and ‹p1 ∈ A ⟹ Finite(domain(p1))›
    have "Finite(domain(p1))"
      using Finite_domain by simp
    moreover
    define r where "r ≡ ⋂D"
    moreover from ‹M(D)›
    have "M(r)" "M(r×2)"
      unfolding r_def by simp_all
    ultimately
    have "Finite(r)" using subset_Finite[of "r" "domain(p1)"]
      by auto
    have "countable_rel(M,{restrict(p,r) . p∈A})"
    proof -
      note ‹M(Fn(nat, I, 2))› ‹M(r)›
      moreover from this
      have "f∈Fn(nat, I, 2) ⟹ M(restrict(f,r))" for f
        by (blast dest: transM)
      ultimately
      have "f∈Fn(nat, I, 2) ⟹ restrict(f,r) ∈ Pow_rel(M,r × 2)" for f
        using restrict_subset_Sigma[of f _ "λ_. 2" r] Pow_rel_char
        by (auto del:FnD dest!:FnD simp: Pi_def) (auto dest:transM)
      with ‹A ⊆ Fn(nat, I, 2)›
      have "{restrict(f,r) . f ∈ A } ⊆ Pow_rel(M,r × 2)"
        by fast
      moreover from ‹M(A)› ‹M(r)›
      have "M({restrict(f,r) . f ∈ A })"
        using RepFun_closed restrict_strong_replacement transM[OF _ ‹M(A)›] by auto
      moreover
      note ‹Finite(r)› ‹M(r)›
      ultimately
      show ?thesis
        using Finite_Sigma[THEN Finite_Pow_rel, of r "λ_. 2"]
        by (intro Finite_imp_countable_rel) (auto intro:subset_Finite)
    qed
    moreover from ‹M(A)› ‹M(D)›
    have "M({p∈A. domain(p) ∈ D})"
      using domain_mem_separation by simp
    have "uncountable_rel(M,{p∈A. domain(p) ∈ D})" (is "uncountable_rel(M,?X)")
    proof
      from ‹D ⊆ {domain(p) . p ∈ A}›
      have "(λp∈?X. domain(p)) ∈ surj(?X, D)"
        using lam_type unfolding surj_def by auto
      moreover from ‹M(A)› ‹M(?X)›
      have "M(λp∈?X. domain(p))"
        using lam_closed[OF domain_replacement ‹M(?X)›] transM[OF _ ‹M(?X)›] by simp
      moreover
      note ‹M(?X)› ‹M(D)›
      moreover from calculation
      have surjection:"(λp∈?X. domain(p)) ∈ surj⇗M⇖(?X, D)"
        using surj_rel_char by simp
      moreover
      assume "countable_rel(M,?X)"
      moreover
      note ‹uncountable_rel(M,D)›
      ultimately
      show False
        using surj_rel_countable_rel[OF _ surjection] by auto
    qed
    moreover
    have "D = (⋃f∈Pow_rel(M,r×2) . {y . p∈A, restrict(p,r) = f ∧ y=domain(p) ∧ domain(p) ∈ D})"
    proof -
      {
        fix z
        assume "z ∈ D"
        with ‹M(D)›
        have ‹M(z)› by (auto dest:transM)
        from ‹z∈D› ‹D ⊆ _› ‹M(A)›
        obtain p  where "domain(p) = z" "p ∈ A" "M(p)"
          by (auto dest:transM)
        moreover from ‹A ⊆ Fn(nat, I, 2)› ‹M(z)› and this
        have "p ∈ z →⇗M⇖ 2"
          using domain_of_fun function_space_rel_char by (auto del:FnD dest!:FnD)
        moreover from this ‹M(z)›
        have "p ∈ z → 2"
          using domain_of_fun function_space_rel_char by (auto)
        moreover from this ‹M(r)›
        have "restrict(p,r) ⊆ r × 2"
          using function_restrictI[of p r] fun_is_function[of p z "λ_. 2"]
            restrict_subset_Sigma[of p z "λ_. 2" r] function_space_rel_char
          by (auto simp:Pi_def)
        moreover from ‹M(p)› ‹M(r)›
        have "M(restrict(p,r))" by simp
        moreover
        note ‹M(r)›
        ultimately
        have "∃p∈A.  restrict(p,r) ∈ Pow_rel(M,r×2) ∧ domain(p) = z"
          using Pow_rel_char by auto
      }
      then
      show ?thesis
        by (intro equalityI) (force)+
    qed
    from ‹M(D)›‹M(r)›
    have "M({y . p∈A, restrict(p,r) = f ∧ y=domain(p) ∧ domain(p) ∈ D})" (is "M(?Y(A,f))")
      if "M(f)" "M(A)" for f A
      using drSR_Y_closed[unfolded drSR_Y_def] that
      by simp
    then
    obtain f where "uncountable_rel(M,?Y(A,f))" "M(f)"
    proof -
      have 1:"M(i)"
        if "M(B)" "M(x)"
          "x ∈ {y . x ∈ B, restrict(x, r) = i ∧ y = domain(x) ∧ domain(x) ∈ D}"
        for B x i
        using that ‹M(r)›
        by (auto dest:transM)
      note ‹M(r)›
      moreover from this
      have "M(Pow⇗M⇖(r × 2))" by simp
      moreover
      note ‹M(A)› ‹⋀f A. M(f) ⟹ M(A) ⟹ M(?Y(A,f))› ‹M(D)›
      moreover from calculation
      interpret M_replacement_lepoll M "drSR_Y(r,D)"
        using countable_lepoll_assms3 lam_replacement_inj_rel lam_replacement_drSR_Y
          drSR_Y_closed lam_Least_assumption_drSR_Y
        by (unfold_locales,simp_all add:drSR_Y_def,rule_tac 1,simp_all)
      from calculation
      have "x ∈ Pow⇗M⇖(r × 2) ⟹ M(drSR_Y(r, D, A, x))" for x
        unfolding drSR_Y_def by (auto dest:transM)
      ultimately
      interpret M_cardinal_UN_lepoll _ "?Y(A)" "Pow_rel(M,r×2)"
        using countable_lepoll_assms3 lam_replacement_drSR_Y
          lepoll_assumptions[where S="Pow_rel(M,r×2)", unfolded lepoll_assumptions_defs]
          lam_Least_assumption_drSR_Y[unfolded drSR_Y_def]
        unfolding drSR_Y_def
        apply unfold_locales
                        apply (simp_all add:lam_replacement_inj_rel del: if_range_F_else_F_def,rule_tac 1,simp_all)
        by ((fastforce dest:transM[OF _ ‹M(A)›])+)
      {
        from ‹Finite(r)› ‹M(r)›
        have "countable_rel(M,Pow_rel(M,r×2))"
          using Finite_Sigma[THEN Finite_Pow_rel] Finite_imp_countable_rel
          by simp
        moreover
        assume "M(f) ⟹ countable_rel(M,?Y(A,f))" for f
        moreover
        note ‹D = (⋃f∈Pow_rel(M,r×2) .?Y(A,f))› ‹M(r)›
        moreover
        note ‹uncountable_rel(M,D)›
        ultimately
        have "False"
          using countable_rel_imp_countable_rel_UN by (auto dest: transM)
      }
      with that
      show ?thesis
        by auto
    qed
    moreover from this ‹M(A)› and ‹M(f) ⟹ M(A) ⟹ M(?Y(A,f))›
    have "M(?Y(A,f))"
      by blast
    ultimately
    obtain j where "j ∈ inj_rel(M,nat, ?Y(A,f))" "M(j)"
      using uncountable_rel_iff_nat_lt_cardinal_rel[THEN iffD1, THEN leI,
          THEN cardinal_rel_le_imp_lepoll_rel, THEN lepoll_relD]
      by auto
    with ‹M(?Y(A,f))›
    have "j`0 ≠ j`1" "j`0 ∈ ?Y(A,f)" "j`1 ∈ ?Y(A,f)"
      using inj_is_fun[THEN apply_type, of j nat "?Y(A,f)"]
        inj_rel_char
      unfolding inj_def by auto
    then
    obtain p q where "domain(p) ≠ domain(q)" "p ∈ A" "q ∈ A"
      "domain(p) ∈ D" "domain(q) ∈ D"
      "restrict(p,r) = restrict(q,r)" by auto
    moreover from this and delta
    have "domain(p) ∩ domain(q) = r"
      unfolding r_def by simp
    moreover
    note ‹A ⊆ Fn(nat, I, 2)› Fn_nat_abs[OF ‹M(I)› nat_into_M[of 2],simplified]
    moreover from calculation
    have "p ∈ Fn⇗M⇖(nat, I, 2)" "q ∈ Fn⇗M⇖(nat, I, 2)"
      by auto
    moreover from calculation
    have "p ∪ q ∈ Fn(nat, I, 2)"
      using restrict_eq_imp_compat_rel InfCard_rel_nat
      by simp
    ultimately
    have "∃p∈A. ∃q∈A. p ≠ q ∧ compat_in(Fn(nat, I, 2), Fnle(nat, I, 2), p, q)"
      unfolding compat_in_def
      by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
  }
  moreover from assms
  have "M(Fnle(ω,I,2))"
    by simp
  moreover note ‹M(Fn(ω,I,2))›
  ultimately
  show ?thesis using def_ccc_rel by (auto simp:absolut antichain_def) fastforce
qed

end ― ‹locale‹M_add_reals››

end
v class="head">

Theory Edrel

theory Edrel
  imports
    Transitive_Models.ZF_Miscellanea
    Transitive_Models.Recursion_Thms

begin

subsection‹The well-founded relation term‹ed››

lemma eclose_sing : "x ∈ eclose(a) ⟹ x ∈ eclose({a})"
  using subsetD[OF mem_eclose_subset]
  by simp

lemma ecloseE :
  assumes  "x ∈ eclose(A)"
  shows  "x ∈ A ∨ (∃ B ∈ A . x ∈ eclose(B))"
  using assms
proof (induct rule:eclose_induct_down)
  case (1 y)
  then
  show ?case
    using arg_into_eclose by auto
next
  case (2 y z)
  from ‹y ∈ A ∨ (∃B∈A. y ∈ eclose(B))›
  consider (inA) "y ∈ A" | (exB) "(∃B∈A. y ∈ eclose(B))"
    by auto
  then show ?case
  proof (cases)
    case inA
    then
    show ?thesis using 2 arg_into_eclose by auto
  next
    case exB
    then obtain B where "y ∈ eclose(B)" "B∈A"
      by auto
    then
    show ?thesis using 2 ecloseD[of y B z] by auto
  qed
qed

lemma eclose_singE : "x ∈ eclose({a}) ⟹ x = a ∨ x ∈ eclose(a)"
  by(blast dest: ecloseE)

lemma in_eclose_sing :
  assumes "x ∈ eclose({a})" "a ∈ eclose(z)"
  shows "x ∈ eclose({z})"
proof -
  from ‹x∈eclose({a})›
  consider "x=a" | "x∈eclose(a)"
    using eclose_singE by auto
  then
  show ?thesis
    using eclose_sing mem_eclose_trans assms
    by (cases, auto)
qed

lemma in_dom_in_eclose :
  assumes "x ∈ domain(z)"
  shows "x ∈ eclose(z)"
proof -
  from assms
  obtain y where "⟨x,y⟩ ∈ z"
    unfolding domain_def by auto
  then
  show ?thesis
    unfolding Pair_def
    using ecloseD[of "{x,x}"] ecloseD[of "{{x,x},{x,y}}"] arg_into_eclose
    by auto
qed

text‹term‹ed› is the well-founded relation on which term‹val› is defined.›
definition
  ed :: "[i,i] ⇒ o" where
  "ed(x,y) ≡ x ∈ domain(y)"

definition
  edrel :: "i ⇒ i" where
  "edrel(A) ≡ Rrel(ed,A)"

lemma edI[intro!]: "t∈domain(x) ⟹ ed(t,x)"
  unfolding ed_def .

lemma edD[dest!]: "ed(t,x) ⟹ t∈domain(x)"
  unfolding ed_def .

lemma rank_ed:
  assumes "ed(y,x)"
  shows "succ(rank(y)) ≤ rank(x)"
proof
  from assms
  obtain p where "⟨y,p⟩∈x" by auto
  moreover
  obtain s where "y∈s" "s∈⟨y,p⟩" unfolding Pair_def by auto
  ultimately
  have "rank(y) < rank(s)" "rank(s) < rank(⟨y,p⟩)" "rank(⟨y,p⟩) < rank(x)"
    using rank_lt by blast+
  then
  show "rank(y) < rank(x)"
    using lt_trans by blast
qed

lemma edrel_dest [dest]: "x ∈ edrel(A) ⟹ ∃ a∈ A. ∃ b ∈ A. x =⟨a,b⟩"
  by(auto simp add:ed_def edrel_def Rrel_def)

lemma edrelD : "x ∈ edrel(A) ⟹ ∃ a∈ A. ∃ b ∈ A. x =⟨a,b⟩ ∧ a ∈ domain(b)"
  by(auto simp add:ed_def edrel_def Rrel_def)

lemma edrelI [intro!]: "x∈A ⟹ y∈A ⟹ x ∈ domain(y) ⟹ ⟨x,y⟩∈edrel(A)"
  by (simp add:ed_def edrel_def Rrel_def)

lemma edrel_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ ⟨x,y⟩∈edrel(A)"
  by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)

lemma domain_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ x∈A"
  by (auto simp add: Transset_def domain_def Pair_def)

lemma relation_edrel : "relation(edrel(A))"
  by(auto simp add: relation_def)

lemma field_edrel : "field(edrel(A))⊆A"
  by blast

lemma edrel_sub_memrel: "edrel(A) ⊆ trancl(Memrel(eclose(A)))"
proof
  let
    ?r="trancl(Memrel(eclose(A)))"
  fix z
  assume "z∈edrel(A)"
  then
  obtain x y where "x∈A" "y∈A" "z=⟨x,y⟩" "x∈domain(y)"
    using edrelD
    by blast
  moreover from this
  obtain u v where "x∈u" "u∈v" "v∈y"
    unfolding domain_def Pair_def by auto
  moreover from calculation
  have "x∈eclose(A)" "y∈eclose(A)" "y⊆eclose(A)"
    using arg_into_eclose Transset_eclose[unfolded Transset_def]
    by simp_all
  moreover from calculation
  have "v∈eclose(A)"
    by auto
  moreover from calculation
  have "u∈eclose(A)"
    using Transset_eclose[unfolded Transset_def]
    by auto
  moreover from calculation
  have"⟨x,u⟩∈?r" "⟨u,v⟩∈?r" "⟨v,y⟩∈?r"
    by (auto simp add: r_into_trancl)
  moreover from this
  have "⟨x,y⟩∈?r"
    using trancl_trans[OF _ trancl_trans[of _ v _ y]]
    by simp
  ultimately
  show "z∈?r"
    by simp
qed

lemma wf_edrel : "wf(edrel(A))"
  using wf_subset [of "trancl(Memrel(eclose(A)))"] edrel_sub_memrel
    wf_trancl wf_Memrel
  by auto

lemma ed_induction:
  assumes "⋀x. ⟦⋀y.  ed(y,x) ⟹ Q(y) ⟧ ⟹ Q(x)"
  shows "Q(a)"
proof(induct rule: wf_induct2[OF wf_edrel[of "eclose({a})"] ,of a "eclose({a})"])
  case 1
  then show ?case using arg_into_eclose by simp
next
  case 2
  then show ?case using field_edrel .
next
  case (3 x)
  then
  show ?case
    using assms[of x] edrelI domain_trans[OF Transset_eclose 3(1)] by blast
qed

lemma dom_under_edrel_eclose: "edrel(eclose({x})) -`` {x} = domain(x)"
proof(intro equalityI)
  show "edrel(eclose({x})) -`` {x} ⊆ domain(x)"
    unfolding edrel_def Rrel_def ed_def
    by auto
next
  show "domain(x) ⊆ edrel(eclose({x})) -`` {x}"
    unfolding edrel_def Rrel_def
    using in_dom_in_eclose eclose_sing arg_into_eclose
    by blast
qed

lemma ed_eclose : "⟨y,z⟩ ∈ edrel(A) ⟹ y ∈ eclose(z)"
  by(drule edrelD,auto simp add:domain_def in_dom_in_eclose)

lemma tr_edrel_eclose : "⟨y,z⟩ ∈ edrel(eclose({x}))^+ ⟹ y ∈ eclose(z)"
  by(rule trancl_induct,(simp add: ed_eclose mem_eclose_trans)+)

lemma restrict_edrel_eq :
  assumes "z ∈ domain(x)"
  shows "edrel(eclose({x})) ∩ eclose({z})×eclose({z}) = edrel(eclose({z}))"
proof(intro equalityI subsetI)
  let ?ec="λ y . edrel(eclose({y}))"
  let ?ez="eclose({z})"
  let ?rr="?ec(x) ∩ ?ez × ?ez"
  fix y
  assume "y ∈ ?rr"
  then
  obtain a b where "⟨a,b⟩ ∈ ?rr" "a ∈ ?ez" "b ∈ ?ez" "⟨a,b⟩ ∈ ?ec(x)" "y=⟨a,b⟩"
    by blast
  moreover from this
  have "a ∈ domain(b)"
    using edrelD by blast
  ultimately
  show "y ∈ edrel(eclose({z}))"
    by blast
next
  let ?ec="λ y . edrel(eclose({y}))"
  let ?ez="eclose({z})"
  let ?rr="?ec(x) ∩ ?ez × ?ez"
  fix y
  assume "y ∈ edrel(?ez)"
  then
  obtain a b where "a ∈ ?ez" "b ∈ ?ez" "y=⟨a,b⟩" "a ∈ domain(b)"
    using edrelD by blast
  moreover
  from this assms
  have "z ∈ eclose(x)"
    using in_dom_in_eclose by simp
  moreover
  from assms calculation
  have "a ∈ eclose({x})" "b ∈ eclose({x})"
    using in_eclose_sing by simp_all
  moreover from calculation
  have "⟨a,b⟩ ∈ edrel(eclose({x}))"
    by blast
  ultimately
  show "y ∈ ?rr"
    by simp
qed

lemma tr_edrel_subset :
  assumes "z ∈ domain(x)"
  shows   "tr_down(edrel(eclose({x})),z) ⊆ eclose({z})"
proof(intro subsetI)
  let ?r="λ x . edrel(eclose({x}))"
  fix y
  assume "y ∈ tr_down(?r(x),z)"
  then
  have "⟨y,z⟩ ∈ ?r(x)^+"
    using tr_downD by simp
  with assms
  show "y ∈ eclose({z})"
    using tr_edrel_eclose eclose_sing by simp
qed

end
v class="head">

Theory FrecR

section‹Well-founded relation on names›
theory FrecR
  imports
    Transitive_Models.Discipline_Function
    Edrel
begin

text‹term‹frecR› is the well-founded relation on names that allows
us to define forcing for atomic formulas.›

definition
  ftype :: "i⇒i" where
  "ftype ≡ fst"

definition
  name1 :: "i⇒i" where
  "name1(x) ≡ fst(snd(x))"

definition
  name2 :: "i⇒i" where
  "name2(x) ≡ fst(snd(snd(x)))"

definition
  cond_of :: "i⇒i" where
  "cond_of(x) ≡ snd(snd(snd((x))))"

lemma components_simp:
  "ftype(⟨f,n1,n2,c⟩) = f"
  "name1(⟨f,n1,n2,c⟩) = n1"
  "name2(⟨f,n1,n2,c⟩) = n2"
  "cond_of(⟨f,n1,n2,c⟩) = c"
  unfolding ftype_def name1_def name2_def cond_of_def
  by simp_all

definition eclose_n :: "[i⇒i,i] ⇒ i" where
  "eclose_n(name,x) = eclose({name(x)})"

definition
  ecloseN :: "i ⇒ i" where
  "ecloseN(x) = eclose_n(name1,x) ∪ eclose_n(name2,x)"

lemma components_in_eclose :
  "n1 ∈ ecloseN(⟨f,n1,n2,c⟩)"
  "n2 ∈ ecloseN(⟨f,n1,n2,c⟩)"
  unfolding ecloseN_def eclose_n_def
  using components_simp arg_into_eclose by auto

lemmas names_simp = components_simp(2) components_simp(3)

lemma ecloseNI1 :
  assumes "x ∈ eclose(n1) ∨ x∈eclose(n2)"
  shows "x ∈ ecloseN(⟨f,n1,n2,c⟩)"
  unfolding ecloseN_def eclose_n_def
  using assms eclose_sing names_simp
  by auto

lemmas ecloseNI = ecloseNI1

lemma ecloseN_mono :
  assumes "u ∈ ecloseN(x)" "name1(x) ∈ ecloseN(y)" "name2(x) ∈ ecloseN(y)"
  shows "u ∈ ecloseN(y)"
proof -
  from ‹u∈_›
  consider (a) "u∈eclose({name1(x)})" | (b) "u ∈ eclose({name2(x)})"
    unfolding ecloseN_def  eclose_n_def by auto
  then
  show ?thesis
  proof cases
    case a
    with ‹name1(x) ∈ _›
    show ?thesis
      unfolding ecloseN_def  eclose_n_def
      using eclose_singE[OF a] mem_eclose_trans[of u "name1(x)" ] by auto
  next
    case b
    with ‹name2(x) ∈ _›
    show ?thesis
      unfolding ecloseN_def eclose_n_def
      using eclose_singE[OF b] mem_eclose_trans[of u "name2(x)"] by auto
  qed
qed

definition
  is_ftype :: "(i⇒o)⇒i⇒i⇒o" where
  "is_ftype ≡ is_fst"

definition
  ftype_fm :: "[i,i] ⇒ i" where
  "ftype_fm ≡ fst_fm"

lemma is_ftype_iff_sats [iff_sats]:
  assumes
    "nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
  shows
    "is_ftype(##A,x,y)  ⟷ sats(A,ftype_fm(a,b), env)"
  unfolding ftype_fm_def is_ftype_def
  using assms sats_fst_fm
  by simp

definition
  is_name1 :: "(i⇒o)⇒i⇒i⇒o" where
  "is_name1(M,x,t2) ≡ is_hcomp(M,is_fst(M),is_snd(M),x,t2)"

definition
  name1_fm :: "[i,i] ⇒ i" where
  "name1_fm(x,t) ≡ hcomp_fm(fst_fm,snd_fm,x,t)"

lemma sats_name1_fm [simp]:
  "⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
    (A, env ⊨ name1_fm(x,y)) ⟷ is_name1(##A, nth(x,env), nth(y,env))"
  unfolding name1_fm_def is_name1_def
  using sats_fst_fm sats_snd_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd(##A)"]
  by simp

lemma is_name1_iff_sats [iff_sats]:
  assumes
    "nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
  shows
    "is_name1(##A,x,y)  ⟷ A , env ⊨ name1_fm(a,b)"
  using assms sats_name1_fm
  by simp

definition
  is_snd_snd :: "(i⇒o)⇒i⇒i⇒o" where
  "is_snd_snd(M,x,t) ≡ is_hcomp(M,is_snd(M),is_snd(M),x,t)"

definition
  snd_snd_fm :: "[i,i]⇒i" where
  "snd_snd_fm(x,t) ≡ hcomp_fm(snd_fm,snd_fm,x,t)"

lemma sats_snd2_fm [simp]:
  "⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
    (A, env  ⊨ snd_snd_fm(x,y)) ⟷ is_snd_snd(##A, nth(x,env), nth(y,env))"
  unfolding snd_snd_fm_def is_snd_snd_def
  using sats_snd_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd(##A)"]
  by simp

definition
  is_name2 :: "(i⇒o)⇒i⇒i⇒o" where
  "is_name2(M,x,t3) ≡ is_hcomp(M,is_fst(M),is_snd_snd(M),x,t3)"

definition
  name2_fm :: "[i,i] ⇒ i" where
  "name2_fm(x,t3) ≡ hcomp_fm(fst_fm,snd_snd_fm,x,t3)"

lemma sats_name2_fm :
  "⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧
    ⟹ (A , env ⊨ name2_fm(x,y)) ⟷ is_name2(##A, nth(x,env), nth(y,env))"
  unfolding name2_fm_def is_name2_def
  using sats_fst_fm sats_snd2_fm sats_hcomp_fm[of A "is_fst(##A)" _ fst_fm "is_snd_snd(##A)"]
  by simp

lemma is_name2_iff_sats [iff_sats]:
  assumes
    "nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
  shows
    "is_name2(##A,x,y)  ⟷ A, env ⊨ name2_fm(a,b)"
  using assms sats_name2_fm
  by simp

definition
  is_cond_of :: "(i⇒o)⇒i⇒i⇒o" where
  "is_cond_of(M,x,t4) ≡ is_hcomp(M,is_snd(M),is_snd_snd(M),x,t4)"

definition
  cond_of_fm :: "[i,i] ⇒ i" where
  "cond_of_fm(x,t4) ≡ hcomp_fm(snd_fm,snd_snd_fm,x,t4)"

lemma sats_cond_of_fm :
  "⟦ x ∈ nat; y ∈ nat;env ∈ list(A) ⟧ ⟹
    (A, env ⊨ cond_of_fm(x,y)) ⟷ is_cond_of(##A, nth(x,env), nth(y,env))"
  unfolding cond_of_fm_def is_cond_of_def
  using sats_snd_fm sats_snd2_fm sats_hcomp_fm[of A "is_snd(##A)" _ snd_fm "is_snd_snd(##A)"]
  by simp

lemma is_cond_of_iff_sats [iff_sats]:
  assumes
    "nth(a,env) = x" "nth(b,env) = y" "a∈nat" "b∈nat" "env ∈ list(A)"
  shows
    "is_cond_of(##A,x,y) ⟷ A, env ⊨ cond_of_fm(a,b)"
  using assms sats_cond_of_fm
  by simp

lemma components_type[TC] :
  assumes "a∈nat" "b∈nat"
  shows
    "ftype_fm(a,b)∈formula"
    "name1_fm(a,b)∈formula"
    "name2_fm(a,b)∈formula"
    "cond_of_fm(a,b)∈formula"
  using assms
  unfolding ftype_fm_def fst_fm_def snd_fm_def snd_snd_fm_def name1_fm_def name2_fm_def
    cond_of_fm_def hcomp_fm_def
  by simp_all

lemmas components_iff_sats = is_ftype_iff_sats is_name1_iff_sats is_name2_iff_sats
  is_cond_of_iff_sats

lemmas components_defs = ftype_fm_def snd_snd_fm_def hcomp_fm_def
  name1_fm_def name2_fm_def cond_of_fm_def

definition
  is_eclose_n :: "[i⇒o,[i⇒o,i,i]⇒o,i,i] ⇒ o" where
  "is_eclose_n(N,is_name,en,t) ≡
        ∃n1[N].∃s1[N]. is_name(N,t,n1) ∧ is_singleton(N,n1,s1) ∧ is_eclose(N,s1,en)"

definition
  eclose_n1_fm :: "[i,i] ⇒ i" where
  "eclose_n1_fm(m,t) ≡ Exists(Exists(And(And(name1_fm(t+ω2,0),singleton_fm(0,1)),
                                       is_eclose_fm(1,m+ω2))))"

definition
  eclose_n2_fm :: "[i,i] ⇒ i" where
  "eclose_n2_fm(m,t) ≡ Exists(Exists(And(And(name2_fm(t+ω2,0),singleton_fm(0,1)),
                                       is_eclose_fm(1,m+ω2))))"

definition
  is_ecloseN :: "[i⇒o,i,i] ⇒ o" where
  "is_ecloseN(N,t,en) ≡ ∃en1[N].∃en2[N].
                is_eclose_n(N,is_name1,en1,t) ∧ is_eclose_n(N,is_name2,en2,t)∧
                union(N,en1,en2,en)"

definition
  ecloseN_fm :: "[i,i] ⇒ i" where
  "ecloseN_fm(en,t) ≡ Exists(Exists(And(eclose_n1_fm(1,t+ω2),
                            And(eclose_n2_fm(0,t+ω2),union_fm(1,0,en+ω2)))))"

lemma ecloseN_fm_type [TC] :
  "⟦ en ∈ nat ; t ∈ nat ⟧ ⟹ ecloseN_fm(en,t) ∈ formula"
  unfolding ecloseN_fm_def eclose_n1_fm_def eclose_n2_fm_def by simp

lemma sats_ecloseN_fm [simp]:
  "⟦ en ∈ nat; t ∈ nat ; env ∈ list(A) ⟧
    ⟹ (A, env ⊨ ecloseN_fm(en,t)) ⟷ is_ecloseN(##A,nth(t,env),nth(en,env))"
  unfolding ecloseN_fm_def is_ecloseN_def eclose_n1_fm_def eclose_n2_fm_def is_eclose_n_def
  using nth_0 nth_ConsI sats_name1_fm sats_name2_fm singleton_iff_sats[symmetric]
  by auto

lemma is_ecloseN_iff_sats [iff_sats]:
  "⟦ nth(en, env) = ena; nth(t, env) = ta; en ∈ nat; t ∈ nat ; env ∈ list(A) ⟧
    ⟹ is_ecloseN(##A,ta,ena) ⟷ A, env ⊨ ecloseN_fm(en,t)"
  by simp

(* Relation of forces *)
definition
  frecR :: "i ⇒ i ⇒ o" where
  "frecR(x,y) ≡
    (ftype(x) = 1 ∧ ftype(y) = 0
      ∧ (name1(x) ∈ domain(name1(y)) ∪ domain(name2(y)) ∧ (name2(x) = name1(y) ∨ name2(x) = name2(y))))
   ∨ (ftype(x) = 0 ∧ ftype(y) =  1 ∧ name1(x) = name1(y) ∧ name2(x) ∈ domain(name2(y)))"

lemma frecR_ftypeD :
  assumes "frecR(x,y)"
  shows "(ftype(x) = 0 ∧ ftype(y) = 1) ∨ (ftype(x) = 1 ∧ ftype(y) = 0)"
  using assms unfolding frecR_def by auto

lemma frecRI1: "s ∈ domain(n1) ∨ s ∈ domain(n2) ⟹ frecR(⟨1, s, n1, q⟩, ⟨0, n1, n2, q'⟩)"
  unfolding frecR_def by (simp add:components_simp)

lemma frecRI1': "s ∈ domain(n1) ∪ domain(n2) ⟹ frecR(⟨1, s, n1, q⟩, ⟨0, n1, n2, q'⟩)"
  unfolding frecR_def by (simp add:components_simp)

lemma frecRI2: "s ∈ domain(n1) ∨ s ∈ domain(n2) ⟹ frecR(⟨1, s, n2, q⟩, ⟨0, n1, n2, q'⟩)"
  unfolding frecR_def by (simp add:components_simp)

lemma frecRI2': "s ∈ domain(n1) ∪ domain(n2) ⟹ frecR(⟨1, s, n2, q⟩, ⟨0, n1, n2, q'⟩)"
  unfolding frecR_def by (simp add:components_simp)

lemma frecRI3: "⟨s, r⟩ ∈ n2 ⟹ frecR(⟨0, n1, s, q⟩, ⟨1, n1, n2, q'⟩)"
  unfolding frecR_def by (auto simp add:components_simp)

lemma frecRI3': "s ∈ domain(n2) ⟹ frecR(⟨0, n1, s, q⟩, ⟨1, n1, n2, q'⟩)"
  unfolding frecR_def by (auto simp add:components_simp)

lemma frecR_D1 :
  "frecR(x,y) ⟹ ftype(y) = 0 ⟹ ftype(x) = 1 ∧
      (name1(x) ∈ domain(name1(y)) ∪ domain(name2(y)) ∧ (name2(x) = name1(y) ∨ name2(x) = name2(y)))"
  unfolding frecR_def
  by auto

lemma frecR_D2 :
  "frecR(x,y) ⟹ ftype(y) = 1 ⟹ ftype(x) = 0 ∧
      ftype(x) = 0 ∧ ftype(y) =  1 ∧ name1(x) = name1(y) ∧ name2(x) ∈ domain(name2(y))"
  unfolding frecR_def
  by auto

lemma frecR_DI :
  assumes "frecR(⟨a,b,c,d⟩,⟨ftype(y),name1(y),name2(y),cond_of(y)⟩)"
  shows "frecR(⟨a,b,c,d⟩,y)"
  using assms
  unfolding frecR_def
  by (force simp add:components_simp)

reldb_add "ftype" "is_ftype"
reldb_add "name1" "is_name1"
reldb_add "name2" "is_name2"

relativize "frecR" "is_frecR"

schematic_goal sats_frecR_fm_auto:
  assumes
    "i∈nat" "j∈nat" "env∈list(A)"
  shows
    "is_frecR(##A,nth(i,env),nth(j,env)) ⟷ A, env ⊨ ?fr_fm(i,j)"
  unfolding is_frecR_def
  by (insert assms ; (rule sep_rules' cartprod_iff_sats components_iff_sats
        | simp del:sats_cartprod_fm)+)

synthesize "frecR" from_schematic sats_frecR_fm_auto

text‹Third item of Kunen's observations (p. 257) about the trcl relation.›
lemma eq_ftypep_not_frecrR:
  assumes "ftype(x) = ftype(y)"
  shows "¬ frecR(x,y)"
  using assms frecR_ftypeD by force

definition
  rank_names :: "i ⇒ i" where
  "rank_names(x) ≡ max(rank(name1(x)),rank(name2(x)))"

lemma rank_names_types [TC]:
  shows "Ord(rank_names(x))"
  unfolding rank_names_def max_def using Ord_rank Ord_Un by auto

definition
  mtype_form :: "i ⇒ i" where
  "mtype_form(x) ≡ if rank(name1(x)) < rank(name2(x)) then 0 else 2"

definition
  type_form :: "i ⇒ i" where
  "type_form(x) ≡ if ftype(x) = 0 then 1 else mtype_form(x)"

lemma type_form_tc [TC]:
  shows "type_form(x) ∈ 3"
  unfolding type_form_def mtype_form_def by auto

lemma frecR_le_rnk_names :
  assumes  "frecR(x,y)"
  shows "rank_names(x)≤rank_names(y)"
proof -
  obtain a b c d where
    H: "a = name1(x)" "b = name2(x)"
    "c = name1(y)" "d = name2(y)"
    "(a ∈ domain(c)∪domain(d) ∧ (b=c ∨ b = d)) ∨ (a = c ∧ b ∈ domain(d))"
    using assms
    unfolding frecR_def
    by force
  then
  consider
    (m) "a ∈ domain(c) ∧ (b = c ∨ b = d) "
    | (n) "a ∈ domain(d) ∧ (b = c ∨ b = d)"
    | (o) "b ∈ domain(d) ∧ a = c"
    by auto
  then
  show ?thesis
  proof(cases)
    case m
    then
    have "rank(a) < rank(c)"
      using eclose_rank_lt  in_dom_in_eclose
      by simp
    with ‹rank(a) < rank(c)› H m
    show ?thesis
      unfolding rank_names_def
      using Ord_rank max_cong max_cong2 leI
      by auto
  next
    case n
    then
    have "rank(a) < rank(d)"
      using eclose_rank_lt in_dom_in_eclose
      by simp
    with ‹rank(a) < rank(d)› H n
    show ?thesis
      unfolding rank_names_def
      using Ord_rank max_cong2 max_cong max_commutes[of "rank(c)" "rank(d)"] leI
      by auto
  next
    case o
    then
    have "rank(b) < rank(d)" (is "?b < ?d") "rank(a) = rank(c)" (is "?a = _")
      using eclose_rank_lt in_dom_in_eclose
      by simp_all
    with H
    show ?thesis
      unfolding rank_names_def
      using Ord_rank max_commutes max_cong2[OF leI[OF ‹?b < ?d›], of ?a]
      by simp
  qed
qed

definition
  Γ :: "i ⇒ i" where
  "Γ(x) = 3 ** rank_names(x) ++ type_form(x)"

lemma Γ_type [TC]:
  shows "Ord(Γ(x))"
  unfolding Γ_def by simp

lemma Γ_mono :
  assumes "frecR(x,y)"
  shows "Γ(x) < Γ(y)"
proof -
  have F: "type_form(x) < 3" "type_form(y) < 3"
    using ltI
    by simp_all
  from assms
  have A: "rank_names(x) ≤ rank_names(y)" (is "?x ≤ ?y")
    using frecR_le_rnk_names
    by simp
  then
  have "Ord(?y)"
    unfolding rank_names_def
    using Ord_rank max_def
    by simp
  note leE[OF ‹?x≤?y›]
  then
  show ?thesis
  proof(cases)
    case 1
    then
    show ?thesis
      unfolding Γ_def
      using oadd_lt_mono2 ‹?x < ?y› F
      by auto
  next
    case 2
    consider (a) "ftype(x) = 0 ∧ ftype(y) = 1" | (b) "ftype(x) = 1 ∧ ftype(y) = 0"
      using frecR_ftypeD[OF ‹frecR(x,y)›]
      by auto
    then show ?thesis
    proof(cases)
      case b
      moreover from this
      have "type_form(y) = 1"
        using type_form_def by simp
      moreover from calculation
      have "name2(x) = name1(y) ∨ name2(x) = name2(y) "  (is "?τ = ?σ' ∨ ?τ = ?τ'")
        "name1(x) ∈ domain(name1(y)) ∪ domain(name2(y))" (is "?σ ∈ domain(?σ') ∪ domain(?τ')")
        using assms unfolding type_form_def frecR_def by auto
      moreover from calculation
      have E: "rank(?τ) = rank(?σ') ∨ rank(?τ) = rank(?τ')" by auto
      from calculation
      consider (c) "rank(?σ) < rank(?σ')" |  (d) "rank(?σ) < rank(?τ')"
        using eclose_rank_lt in_dom_in_eclose by force
      then
      have "rank(?σ) < rank(?τ)"
      proof (cases)
        case c
        with ‹rank_names(x) = rank_names(y) ›
        show ?thesis
          unfolding rank_names_def mtype_form_def type_form_def
          using max_D2[OF E c] E assms Ord_rank
          by simp
      next
        case d
        with ‹rank_names(x) = rank_names(y) ›
        show ?thesis
          unfolding rank_names_def mtype_form_def type_form_def
          using max_D2[OF _ d] max_commutes E assms Ord_rank disj_commute
          by simp
      qed
      with b
      have "type_form(x) = 0" unfolding type_form_def mtype_form_def by simp
      with ‹rank_names(x) = rank_names(y) › ‹type_form(y) = 1› ‹type_form(x) = 0›
      show ?thesis
        unfolding Γ_def by auto
    next
      case a
      then
      have "name1(x) = name1(y)" (is "?σ = ?σ'")
        "name2(x) ∈ domain(name2(y))" (is "?τ ∈ domain(?τ')")
        "type_form(x) = 1"
        using assms
        unfolding type_form_def frecR_def
        by auto
      then
      have "rank(?σ) = rank(?σ')" "rank(?τ) < rank(?τ')"
        using  eclose_rank_lt in_dom_in_eclose
        by simp_all
      with ‹rank_names(x) = rank_names(y) ›
      have "rank(?τ') ≤ rank(?σ')"
        using Ord_rank max_D1
        unfolding rank_names_def
        by simp
      with a
      have "type_form(y) = 2"
        unfolding type_form_def mtype_form_def
        using not_lt_iff_le assms
        by simp
      with ‹rank_names(x) = rank_names(y) › ‹type_form(y) = 2› ‹type_form(x) = 1›
      show ?thesis
        unfolding Γ_def by auto
    qed
  qed
qed

definition
  frecrel :: "i ⇒ i" where
  "frecrel(A) ≡ Rrel(frecR,A)"

lemma frecrelI :
  assumes "x ∈ A" "y∈A" "frecR(x,y)"
  shows "⟨x,y⟩∈frecrel(A)"
  using assms unfolding frecrel_def Rrel_def by auto

lemma frecrelD :
  assumes "⟨x,y⟩ ∈ frecrel(A1×A2×A3×A4)"
  shows
    "ftype(x) ∈ A1" "ftype(x) ∈ A1"
    "name1(x) ∈ A2" "name1(y) ∈ A2"
    "name2(x) ∈ A3" "name2(x) ∈ A3"
    "cond_of(x) ∈ A4" "cond_of(y) ∈ A4"
    "frecR(x,y)"
  using assms
  unfolding frecrel_def Rrel_def ftype_def by (auto simp add:components_simp)

lemma wf_frecrel :
  shows "wf(frecrel(A))"
proof -
  have "frecrel(A) ⊆ measure(A,Γ)"
    unfolding frecrel_def Rrel_def measure_def
    using Γ_mono
    by force
  then
  show ?thesis
    using wf_subset wf_measure by auto
qed

lemma core_induction_aux:
  fixes A1 A2 :: "i"
  assumes
    "Transset(A1)"
    "⋀τ θ p.  p ∈ A2 ⟹ ⟦⋀q σ. ⟦ q∈A2 ; σ∈domain(θ)⟧ ⟹ Q(0,τ,σ,q)⟧ ⟹ Q(1,τ,θ,p)"
    "⋀τ θ p.  p ∈ A2 ⟹ ⟦⋀q σ. ⟦ q∈A2 ; σ∈domain(τ) ∪ domain(θ)⟧ ⟹ Q(1,σ,τ,q) ∧ Q(1,σ,θ,q)⟧ ⟹ Q(0,τ,θ,p)"
  shows "a∈2×A1×A1×A2 ⟹ Q(ftype(a),name1(a),name2(a),cond_of(a))"
proof (induct a rule:wf_induct[OF wf_frecrel[of "2×A1×A1×A2"]])
  case (1 x)
  let ?τ = "name1(x)"
  let ?θ = "name2(x)"
  let ?D = "2×A1×A1×A2"
  assume "x ∈ ?D"
  then
  have "cond_of(x)∈A2"
    by (auto simp add:components_simp)
  from ‹x∈?D›
  consider (eq) "ftype(x)=0" | (mem) "ftype(x)=1"
    by (auto simp add:components_simp)
  then
  show ?case
  proof cases
    case eq
    then
    have "Q(1, σ, ?τ, q) ∧ Q(1, σ, ?θ, q)" if "σ ∈ domain(?τ) ∪ domain(?θ)" and "q∈A2" for q σ
    proof -
      from 1
      have "?τ∈A1" "?θ∈A1" "?τ∈eclose(A1)" "?θ∈eclose(A1)"
        using  arg_into_eclose
        by (auto simp add:components_simp)
      moreover from ‹Transset(A1)› that(1)
      have "σ∈eclose(?τ) ∪ eclose(?θ)"
        using in_dom_in_eclose
        by auto
      then
      have "σ∈A1"
        using mem_eclose_subset[OF ‹?τ∈A1›] mem_eclose_subset[OF ‹?θ∈A1›]
          Transset_eclose_eq_arg[OF ‹Transset(A1)›]
        by auto
      with ‹q∈A2› ‹?θ ∈ A1› ‹cond_of(x)∈A2› ‹?τ∈A1›
      have "frecR(⟨1, σ, ?τ, q⟩, x)" (is "frecR(?T,_)")
           "frecR(⟨1, σ, ?θ, q⟩, x)" (is "frecR(?U,_)")
        using frecRI1'[OF that(1)] frecR_DI  ‹ftype(x) = 0›
          frecRI2'[OF that(1)]
        by (auto simp add:components_simp)
      with ‹x∈?D› ‹σ∈A1› ‹q∈A2›
      have "⟨?T,x⟩∈ frecrel(?D)" "⟨?U,x⟩∈ frecrel(?D)"
        using frecrelI[of ?T ?D x]  frecrelI[of ?U ?D x]
        by (auto simp add:components_simp)
      with ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1›
      have "Q(1, σ, ?τ, q)"
        using 1
        by (force simp add:components_simp)
      moreover from ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1› ‹⟨?U,x⟩∈ frecrel(?D)›
      have "Q(1, σ, ?θ, q)"
        using 1 by (force simp add:components_simp)
      ultimately
      show ?thesis
        by simp
    qed
    with assms(3) ‹ftype(x) = 0› ‹cond_of(x)∈A2›
    show ?thesis
      by auto
  next
    case mem
    have "Q(0, ?τ,  σ, q)" if "σ ∈ domain(?θ)" and "q∈A2" for q σ
    proof -
      from 1 assms
      have "?τ∈A1" "?θ∈A1" "cond_of(x)∈A2" "?τ∈eclose(A1)" "?θ∈eclose(A1)"
        using arg_into_eclose
        by (auto simp add:components_simp)
      with  ‹Transset(A1)› that(1)
      have "σ∈ eclose(?θ)"
        using in_dom_in_eclose
        by auto
      then
      have "σ∈A1"
        using mem_eclose_subset[OF ‹?θ∈A1›] Transset_eclose_eq_arg[OF ‹Transset(A1)›]
        by auto
      with ‹q∈A2› ‹?θ ∈ A1› ‹cond_of(x)∈A2› ‹?τ∈A1› ‹ftype(x) = 1›
      have "frecR(⟨0, ?τ, σ, q⟩, x)" (is "frecR(?T,_)")
        using frecRI3'[OF that(1)] frecR_DI
        by (auto simp add:components_simp)
      with ‹x∈?D› ‹σ∈A1› ‹q∈A2› ‹?τ∈A1›
      have "⟨?T,x⟩∈ frecrel(?D)" "?T∈?D"
        using frecrelI[of ?T ?D x]
        by (auto simp add:components_simp)
      with ‹q∈A2› ‹σ∈A1› ‹?τ∈A1› ‹?θ∈A1› 1
      show ?thesis
        by (force simp add:components_simp)
    qed
    with assms(2) ‹ftype(x) = 1› ‹cond_of(x)∈A2›
    show ?thesis
      by auto
  qed
qed

lemma def_frecrel : "frecrel(A) = {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ frecR(x,y)}"
  unfolding frecrel_def Rrel_def ..

lemma frecrel_fst_snd:
  "frecrel(A) = {z ∈ A×A .
            ftype(fst(z)) = 1 ∧
        ftype(snd(z)) = 0 ∧ name1(fst(z)) ∈ domain(name1(snd(z))) ∪ domain(name2(snd(z))) ∧
            (name2(fst(z)) = name1(snd(z)) ∨ name2(fst(z)) = name2(snd(z)))
          ∨ (ftype(fst(z)) = 0 ∧
        ftype(snd(z)) = 1 ∧  name1(fst(z)) = name1(snd(z)) ∧ name2(fst(z)) ∈ domain(name2(snd(z))))}"
  unfolding def_frecrel frecR_def
  by (intro equalityI subsetI CollectI; elim CollectE; auto)

end
ody>

Theory FrecR_Arities

theory FrecR_Arities
  imports
    FrecR
begin

context
  notes FOL_arities[simp]
begin

arity_theorem intermediate for "fst_fm"
lemma arity_fst_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(fst_fm(x,t)) = succ(x) ∪ succ(t)"
  using arity_fst_fm'
  by auto

arity_theorem intermediate for "snd_fm"
lemma arity_snd_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_fm(x,t)) = succ(x) ∪ succ(t)"
  using arity_snd_fm'
  by auto

lemma arity_snd_snd_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_snd_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding snd_snd_fm_def hcomp_fm_def
  using arity_snd_fm arity_empty_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_ftype_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(ftype_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding ftype_fm_def
  using arity_fst_fm
  by auto

lemma arity_name1_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(name1_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding name1_fm_def hcomp_fm_def
  using arity_fst_fm arity_snd_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_name2_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(name2_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding name2_fm_def hcomp_fm_def
  using arity_fst_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_cond_of_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(cond_of_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding cond_of_fm_def hcomp_fm_def
  using arity_snd_fm arity_snd_snd_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_eclose_n1_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n1_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding eclose_n1_fm_def
  using arity_is_eclose_fm arity_singleton_fm arity_name1_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_eclose_n2_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n2_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding eclose_n2_fm_def
  using arity_is_eclose_fm arity_singleton_fm arity_name2_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_ecloseN_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(ecloseN_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding ecloseN_fm_def
  using arity_eclose_n1_fm arity_eclose_n2_fm arity_union_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_frecR_fm [arity]:
  "⟦a∈nat;b∈nat⟧ ⟹ arity(frecR_fm(a,b)) = succ(a) ∪ succ(b)"
  unfolding frecR_fm_def
  using arity_ftype_fm arity_name1_fm arity_name2_fm arity_domain_fm
      arity_empty_fm arity_union_fm pred_Un_distrib arity_succ_fm
  by auto

end ― ‹@{thm [source] FOL_arities}›

end
body>

Theory Fm_Definitions

section‹Concepts involved in instances of Replacement›
theory Fm_Definitions
  imports
    Transitive_Models.Renaming_Auto
    Transitive_Models.Aleph_Relative
    FrecR_Arities
begin

txt‹In this theory we put every concept that should be synthesized in a formula
to have an instance of replacement.

The automatic synthesis of a concept /foo/ requires that every concept used to
define /foo/ is already synthesized. We try to use our meta-programs to synthesize
concepts: given the absolute concept /foo/ we relativize in relational form
obtaining /is\_foo/ and the we synthesize the formula /is\_foo\_fm/.
The meta-program that synthesizes formulas also produce satisfactions lemmas.

Having one file to collect every formula needed for replacements breaks
the reading flow: we need to introduce the concept in this theory in order
to use the meta-programs; moreover there are some concepts for which we prove
here the satisfaction lemmas manually, while for others we prove them
on its theory.
›

declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del]
  FOL_arities[simp del]

txt‹Formulas for particular replacement instances›

text‹Now we introduce some definitions used in the definition of check; which
is defined by well-founded recursion using replacement in the recursive call.›

― ‹The well-founded relation for defining check.›
definition
  rcheck :: "i ⇒ i" where
  "rcheck(x) ≡ Memrel(eclose({x}))^+"

relativize "rcheck" "is_rcheck"
synthesize "is_rcheck" from_definition
arity_theorem for "is_rcheck_fm"

― ‹The function used for the replacement.›
definition
  PHcheck :: "[i⇒o,i,i,i,i] ⇒ o" where
  "PHcheck(M,o,f,y,p) ≡ M(p) ∧ (∃fy[M]. fun_apply(M,f,y,fy) ∧ pair(M,fy,o,p))"

synthesize "PHcheck" from_definition assuming "nonempty"
arity_theorem for "PHcheck_fm"

― ‹The recursive call for check. We could use the meta-program relationalize for
this; but it makes some proofs more involved.›
definition
  is_Hcheck :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_Hcheck(M,o,z,f,hc)  ≡ is_Replace(M,z,PHcheck(M,o,f),hc)"

synthesize "is_Hcheck" from_definition assuming "nonempty"

lemma arity_is_Hcheck_fm:
  assumes "m∈nat" "n∈nat" "p∈nat" "o∈nat"
  shows "arity(is_Hcheck_fm(m,n,p,o)) = succ(o) ∪ succ(n) ∪ succ(p) ∪ succ(m) "
  unfolding is_Hcheck_fm_def
  using assms arity_Replace_fm[rule_format,OF PHcheck_fm_type _ _ _ arity_PHcheck_fm]
    pred_Un_distrib Un_assoc Un_nat_type
  by simp

― ‹The relational version of check is hand-made because our automatic tool
does not handle term‹wfrec›.›
definition
  is_check :: "[i⇒o,i,i,i] ⇒ o" where
  "is_check(M,o,x,z) ≡ ∃rch[M]. is_rcheck(M,x,rch) ∧
      is_wfrec(M,is_Hcheck(M,o),rch,x,z)"

― ‹Finally, we internalize the formula.›
definition
  check_fm :: "[i,i,i] ⇒ i" where
  "check_fm(x,o,z) ≡ Exists(And(is_rcheck_fm(1+ωx,0),
                      is_wfrec_fm(is_Hcheck_fm(6+ωo,2,1,0),0,1+ωx,1+ωz)))"

lemma check_fm_type[TC]: "x∈nat ⟹ o∈nat ⟹ z∈nat ⟹ check_fm(x,o,z) ∈ formula"
  by (simp add:check_fm_def)

lemma sats_check_fm :
  assumes
    "o∈nat" "x∈nat" "z∈nat" "env∈list(M)" "0∈M"
  shows
    "(M , env ⊨ check_fm(x,o,z)) ⟷ is_check(##M,nth(o,env),nth(x,env),nth(z,env))"
proof -
  have sats_is_Hcheck_fm:
    "⋀a0 a1 a2 a3 a4 a6. ⟦ a0∈M; a1∈M; a2∈M; a3∈M; a4∈M;a6 ∈M⟧ ⟹
         is_Hcheck(##M,a6,a2, a1, a0) ⟷
         (M , [a0,a1,a2,a3,a4,r,a6]@env ⊨ is_Hcheck_fm(6,2,1,0))" if "r∈M" for r
    using that assms
    by simp
  then
  have "(M , [r]@env ⊨ is_wfrec_fm(is_Hcheck_fm(6+ωo,2,1,0),0,1+ωx,1+ωz))
        ⟷ is_wfrec(##M,is_Hcheck(##M,nth(o,env)),r,nth(x,env),nth(z,env))"
    if "r∈M" for r
    using that assms is_wfrec_iff_sats'[symmetric]
    by simp
  then
  show ?thesis
    unfolding is_check_def check_fm_def
    using assms is_rcheck_iff_sats[symmetric]
    by simp
qed

lemma iff_sats_check_fm[iff_sats] :
  assumes
    "nth(o, env) = oa" "nth(x, env) = xa" "nth(z, env) = za" "o ∈ nat" "x ∈ nat" "z ∈ nat" "env ∈ list(A)" "0 ∈ A"
  shows "is_check(##A, oa,xa, za) ⟷ A, env ⊨ check_fm(x,o, z)"
  using assms sats_check_fm[symmetric]
  by auto

lemma arity_check_fm[arity]:
  assumes "m∈nat" "n∈nat" "o∈nat"
  shows "arity(check_fm(m,n,o)) = succ(o) ∪ succ(n) ∪ succ(m) "
  unfolding check_fm_def
  using assms arity_is_wfrec_fm[rule_format,OF _ _ _ _ _ arity_is_Hcheck_fm]
    pred_Un_distrib Un_assoc arity_tran_closure_fm
  by (auto simp add:arity)

notation check_fm (‹⋅_v_ is _⋅›)

subsection‹Names for forcing the Axiom of Choice.›
definition
  upair_name :: "i ⇒ i ⇒ i ⇒ i" where
  "upair_name(τ,ρ,on) ≡ Upair(⟨τ,on⟩,⟨ρ,on⟩)"

relativize "upair_name" "is_upair_name"
synthesize "upair_name" from_definition "is_upair_name"
arity_theorem for "upair_name_fm"

definition
  opair_name :: "i ⇒ i ⇒ i ⇒ i" where
  "opair_name(τ,ρ,on) ≡ upair_name(upair_name(τ,τ,on),upair_name(τ,ρ,on),on)"

relativize "opair_name" "is_opair_name"
synthesize "opair_name" from_definition "is_opair_name"
arity_theorem for "opair_name_fm"

definition
  is_opname_check :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_opname_check(M,on,s,x,y) ≡ ∃chx[M]. ∃sx[M]. is_check(M,on,x,chx) ∧
        fun_apply(M,s,x,sx) ∧ is_opair_name(M,chx,sx,on,y)"

synthesize "is_opname_check" from_definition assuming "nonempty"
arity_theorem for "is_opname_check_fm"

― ‹The pair of elements belongs to some set. The intended set is the preorder.›
definition
  is_leq :: "[i⇒o,i,i,i] ⇒ o" where
  "is_leq(A,l,q,p) ≡ ∃qp[A]. (pair(A,q,p,qp) ∧ qp∈l)"

synthesize "is_leq" from_definition assuming "nonempty"
arity_theorem for "is_leq_fm"

abbreviation
  fm_leq :: "[i,i,i] ⇒ i" (‹⋅_≼⇗_⇖_⋅›) where
  "fm_leq(A,l,B) ≡ is_leq_fm(l,A,B)"

subsection‹Formulas used to prove some generic instances.›

definition ρ_repl :: "i⇒i" where
  "ρ_repl(l) ≡ rsum({⟨0, 1⟩, ⟨1, 0⟩}, id(l), 2, 3, l)"

lemma f_type : "{⟨0, 1⟩, ⟨1, 0⟩} ∈ 2 → 3"
  using Pi_iff unfolding function_def by auto

― ‹thm‹Internalize.sum_type› clashes with thm‹Renaming.sum_type›.›
hide_fact Internalize.sum_type

lemma ren_type :
  assumes "l∈nat"
  shows "