Quelle  Names.thy

section‹Names and generic extensions›

theory Names
  imports
    Forcing_Data
    FrecR_Arities
    ZF_Trans_Interpretations
begin

definition
  Hv :: "[i,i,i]==>i" where
  "Hv(G,x,f) ≡ { z . y∈ domain(x), (∃p∈G. ⟨y,p⟩ ∈ x) ∧ z=f`y}"

text‹The funcion term‹val› interprets a name in term‹M›
  to a (generic) filter term‹G›. Note the definition
  terms of the well-founded recursor.›

definition
  val :: "[i,i]==>i" where
  "val(G,τ) ≡ wfrec(edrel(eclose({τ})), τ ,Hv(G))"

definition
  GenExt :: "[i,i]==>i"     (‹_[_]› [71,1])
  where "M[G] ≡ {val(G,τ). τ ∈ M}"

lemma map_val_in_MG:
  assumes
    "env∈list(M)"
  shows
    "map(val(G),env)∈list(M[G])"
  unfolding GenExt_def using assms map_type2 by simp

subsection‹Values and check-names›
context forcing_data1
begin

lemma name_components_in_M:
  assumes "⟨σ,p⟩∈θ" "θ ∈ M"
  shows   "σ∈M" "p∈M"
  using assms transitivity pair_in_M_iff
  by auto

definition
  Hcheck :: "[i,i] ==> i" where
  "Hcheck(z,f) ≡ { ⟨f`y,1⟩ . y ∈ z}"

definition
  check :: "i ==> i" where
  "check(x) ≡ transrec(x , Hcheck)"

lemma checkD:
  "check(x) = wfrec(Memrel(eclose({x})), x, Hcheck)"
  unfolding check_def transrec_def ..

lemma Hcheck_trancl:"Hcheck(y, restrict(f,Memrel(eclose({x}))-``{y}))
                   = Hcheck(y, restrict(f,(Memrel(eclose({x}))^+)-``{y}))"
  unfolding Hcheck_def
  using restrict_trans_eq by simp

lemma check_trancl: "check(x) = wfrec(rcheck(x), x, Hcheck)"
  using checkD wf_eq_trancl Hcheck_trancl unfolding rcheck_def by simp

lemma rcheck_in_M : "x ∈ M ==> rcheck(x) ∈ M"
  unfolding rcheck_def by (simp flip: setclass_iff)

lemma rcheck_subset_M : "x ∈ M ==> field(rcheck(x)) ⊆ eclose({x})"
  unfolding rcheck_def using field_Memrel field_trancl by auto

lemma  aux_def_check: "x ∈ y ==>
  wfrec(Memrel(eclose({y})), x, Hcheck) =
  wfrec(Memrel(eclose({x})), x, Hcheck)"
  by (rule wfrec_eclose_eq,auto simp add: arg_into_eclose eclose_sing)

lemma def_check : "check(y) = { ⟨check(w),1⟩ . w ∈ y}"
proof -
  let
    ?r="λy. Memrel(eclose({y}))"
  have wfr:   "∀w . wf(?r(w))"
    using wf_Memrel ..
  then
  have "check(y)= Hcheck( y, λx∈?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))"
    using wfrec[of "?r(y)" y "Hcheck"] checkD by simp
  also
  have " ... = Hcheck( y, λx∈y. wfrec(?r(y), x, Hcheck))"
    using under_Memrel_eclose arg_into_eclose by simp
  also
  have " ... = Hcheck( y, λx∈y. check(x))"
    using aux_def_check checkD by simp
  finally
  show ?thesis
    using Hcheck_def by simp
qed

lemma def_checkS :
  fixes n
  assumes "n ∈ nat"
  shows "check(succ(n)) = check(n) ∪ {⟨check(n),1⟩}"
proof -
  have "check(succ(n)) = {⟨check(i),1⟩ . i ∈ succ(n)} "
    using def_check by blast
  also
  have "... = {⟨check(i),1⟩ . i ∈ n} ∪ {⟨check(n),1⟩}"
    by blast
  also
  have "... = check(n) ∪ {⟨check(n),1⟩}"
    using def_check[of n,symmetric] by simp
  finally
  show ?thesis .
qed

lemma field_Memrel2 :
  assumes "x ∈ M"
  shows "field(Memrel(eclose({x}))) ⊆ M"
proof -
  have "field(Memrel(eclose({x}))) ⊆ eclose({x})" "eclose({x}) ⊆ M"
    using Ordinal.Memrel_type field_rel_subset assms eclose_least[OF trans_M] by auto
  then
  show ?thesis
    using subset_trans by simp
qed

lemma aux_def_val:
  assumes "z ∈ domain(x)"
  shows "wfrec(edrel(eclose({x})),z,Hv(G)) = wfrec(edrel(eclose({z})),z,Hv(G))"
proof -
  let ?r="λx . edrel(eclose({x}))"
  have "z∈eclose({z})"
    using arg_in_eclose_sing .
  moreover
  have "relation(?r(x))"
    using relation_edrel .
  moreover
  have "wf(?r(x))"
    using wf_edrel .
  moreover from assms
  have "tr_down(?r(x),z) ⊆ eclose({z})"
    using tr_edrel_subset by simp
  ultimately
  have "wfrec(?r(x),z,Hv(G)) = wfrec[eclose({z})](?r(x),z,Hv(G))"
    using wfrec_restr by simp
  also from ‹z∈domain(x)›
  have "... = wfrec(?r(z),z,Hv(G))"
    using restrict_edrel_eq wfrec_restr_eq by simp
  finally
  show ?thesis .
qed

text‹The next lemma provides the usual recursive expresion for the definition of term‹val›.›

lemma def_val:  "val(G,x) = {z . t∈domain(x) , (∃p∈G . ⟨t,p⟩∈x) ∧ z=val(G,t)}"
proof -
  let
    ?r="λτ . edrel(eclose({τ}))"
  let
    ?f="λz∈?r(x)-``{x}. wfrec(?r(x),z,Hv(G))"
  have "∀τ. wf(?r(τ))"
    using wf_edrel by simp
  with wfrec [of _ x]
  have "val(G,x) = Hv(G,x,?f)"
    using val_def by simp
  also
  have " ... = Hv(G,x,λz∈domain(x). wfrec(?r(x),z,Hv(G)))"
    using dom_under_edrel_eclose by simp
  also
  have " ... = Hv(G,x,λz∈domain(x). val(G,z))"
    using aux_def_val val_def by simp
  finally
  show ?thesis
    using Hv_def by simp
qed

lemma val_mono : "x⊆y ==> val(G,x) ⊆ val(G,y)"
  by (subst (1 2) def_val, force)

text‹Check-names are the canonical names for elements of the
  model. Here we show that this is the case.›

lemma val_check : "1 ∈ G ==> 1 ∈ ℙ ==> val(G,check(y)) = y"
proof (induct rule:eps_induct)
  case (1 y)
  then show ?case
  proof -
    have "check(y) = { ⟨check(w), 1⟩ . w ∈ y}"  (is "_ = ?C")
      using def_check .
    then
    have "val(G,check(y)) = val(G, {⟨check(w), 1⟩ . w ∈ y})"
      by simp
    also
    have " ... = {z . t∈domain(?C) , (∃p∈G . ⟨t, p⟩∈?C ) ∧ z=val(G,t) }"
      using def_val by blast
    also
    have " ... = {z . t∈domain(?C) , (∃w∈y. t=check(w)) ∧ z=val(G,t) }"
      using 1 by simp
    also
    have " ... = {val(G,check(w)) . w∈y }"
      by force
    finally
    show "val(G,check(y)) = y"
      using 1 by simp
  qed
qed

lemma val_of_name :
  "val(G,{x∈A×ℙ. Q(x)}) = {z . t∈A , (∃p∈ℙ . Q(⟨t,p⟩) ∧ p ∈ G) ∧ z=val(G,t)}"
proof -
  let
    ?n="{x∈A×ℙ. Q(x)}" and
    ?r="λτ . edrel(eclose({τ}))"
  let
    ?f="λz∈?r(?n)-``{?n}. val(G,z)"
  have
    wfR : "wf(?r(τ))" for τ
    by (simp add: wf_edrel)
  have "domain(?n) ⊆ A" by auto
  { fix t
    assume H:"t ∈ domain({x ∈ A × ℙ . Q(x)})"
    then have "?f ` t = (if t ∈ ?r(?n)-``{?n} then val(G,t) else 0)"
      by simp
    moreover have "... = val(G,t)"
      using dom_under_edrel_eclose H if_P by auto
  }
  then
  have Eq1: "t ∈ domain({x ∈ A × ℙ . Q(x)}) ==> val(G,t) = ?f` t"  for t
    by simp
  have "val(G,?n) = {z . t∈domain(?n), (∃p ∈ G . ⟨t,p⟩ ∈ ?n) ∧ z=val(G,t)}"
    by (subst def_val,simp)
  also
  have "... = {z . t∈domain(?n), (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=?f`t}"
    unfolding Hv_def
    by (auto simp add:Eq1)
  also
  have "... = {z . t∈domain(?n), (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=(if t∈?r(?n)-``{?n} then val(G,t) else 0)}"
    by (simp)
  also
  have "... = { z . t∈domain(?n), (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=val(G,t)}"
  proof -
    have "domain(?n) ⊆ ?r(?n)-``{?n}"
      using dom_under_edrel_eclose by simp
    then
    have "∀t∈domain(?n). (if t∈?r(?n)-``{?n} then val(G,t) else 0) = val(G,t)"
      by auto
    then
    show "{ z . t∈domain(?n), (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=(if t∈?r(?n)-``{?n} then val(G,t) else 0)} =
          { z . t∈domain(?n), (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=val(G,t)}"
      by auto
  qed
  also
  have " ... = { z . t∈A, (∃p∈ℙ . ⟨t,p⟩∈?n ∧ p∈G) ∧ z=val(G,t)}"
    by force
  finally
  show " val(G,?n) = { z . t∈A, (∃p∈ℙ . Q(⟨t,p⟩) ∧ p∈G) ∧ z=val(G,t)}"
    by auto
qed

lemma val_of_name_alt :
  "val(G,{x∈A×ℙ. Q(x)}) = {z . t∈A , (∃p∈ℙ∩G . Q(⟨t,p⟩)) ∧ z=val(G,t) }"
  using val_of_name by force

lemma val_only_names: "val(F,τ) = val(F,{x∈τ. ∃t∈domain(τ). ∃p∈F. x=⟨t,p⟩})"
  (is "_ = val(F,?name)")
proof -
  have "val(F,?name) = {z . t∈domain(?name), (∃p∈F. ⟨t, p⟩ ∈ ?name) ∧ z=val(F, t)}"
    using def_val by blast
  also
  have " ... = {val(F, t). t∈{y∈domain(τ). ∃p∈F. ⟨y, p⟩ ∈ τ }}"
    by blast
  also
  have " ... = {z . t∈domain(τ), (∃p∈F. ⟨t, p⟩ ∈ τ) ∧ z=val(F, t)}"
    by blast
  also
  have " ... = val(F, τ)"
    using def_val[symmetric] by blast
  finally
  show ?thesis ..
qed

lemma val_only_pairs: "val(F,τ) = val(F,{x∈τ. ∃t p. x=⟨t,p⟩})"
proof
  have "val(F,τ) = val(F,{x∈τ. ∃t∈domain(τ). ∃p∈F. x=⟨t,p⟩})" (is "_ = val(F,?name)")
    using val_only_names .
  also
  have "... ⊆ val(F,{x∈τ. ∃t p. x=⟨t,p⟩})"
    using val_mono[of ?name "{x∈τ. ∃t p. x=⟨t,p⟩}"] by auto
  finally
  show "val(F,τ) ⊆ val(F,{x∈τ. ∃t p. x=⟨t,p⟩})" by simp
next
  show "val(F,{x∈τ. ∃t p. x=⟨t,p⟩}) ⊆ val(F,τ)"
    using val_mono[of "{x∈τ. ∃t p. x=⟨t,p⟩}"] by auto
qed

lemma val_subset_domain_times_range: "val(F,τ) ⊆ val(F,domain(τ)×range(τ))"
  using val_only_pairs[THEN equalityD1]
    val_mono[of "{x ∈ τ . ∃t p. x = ⟨t, p⟩}" "domain(τ)×range(τ)"] by blast

lemma val_of_elem: "⟨θ,p⟩ ∈ π ==> p∈G ==> val(G,θ) ∈ val(G,π)"
proof -
  assume "⟨θ,p⟩ ∈ π"
  then
  have "θ∈domain(π)"
    by auto
  assume "p∈G"
  with ‹θ∈domain(π)› ‹⟨θ,p⟩ ∈ π›
  have "val(G,θ) ∈ {z . t∈domain(π) , (∃p∈G . ⟨t, p⟩∈π) ∧ z=val(G,t) }"
    by auto
  then
  show ?thesis
    by (subst def_val)
qed

lemma elem_of_val: "x∈val(G,π) ==> ∃θ∈domain(π). val(G,θ) = x"
  by (subst (asm) def_val,auto)

lemma elem_of_val_pair: "x∈val(G,π) ==> ∃θ. ∃p∈G. ⟨θ,p⟩∈π ∧ val(G,θ) = x"
  by (subst (asm) def_val,auto)

lemma elem_of_val_pair':
  assumes "π∈M" "x∈val(G,π)"
  shows "∃θ∈M. ∃p∈G. ⟨θ,p⟩∈π ∧ val(G,θ) = x"
proof -
  from assms
  obtain θ p where "p∈G" "⟨θ,p⟩∈π" "val(G,θ) = x"
    using elem_of_val_pair by blast
  moreover from this ‹π∈M›
  have "θ∈M"
    using pair_in_M_iff[THEN iffD1, THEN conjunct1, simplified]
      transitivity by blast
  ultimately
  show ?thesis
    by blast
qed

lemma GenExtD: "x ∈ M[G] ==> ∃τ∈M. x = val(G,τ)"
  by (simp add:GenExt_def)

lemma GenExtI: "x ∈ M ==> val(G,x) ∈ M[G]"
  by (auto simp add: GenExt_def)

lemma Transset_MG : "Transset(M[G])"
proof -
  { fix vc y
    assume "vc ∈ M[G]" and "y ∈ vc"
    then
    obtain c where "c∈M" "val(G,c)∈M[G]" "y ∈ val(G,c)"
      using GenExtD by auto
    from ‹y ∈ val(G,c)›
    obtain θ where "θ∈domain(c)" "val(G,θ) = y"
      using elem_of_val by blast
    with trans_M ‹c∈M›
    have "y ∈ M[G]"
      using domain_trans GenExtI by blast
  }
  then
  show ?thesis
    using Transset_def by auto
qed

lemmas transitivity_MG = Transset_intf[OF Transset_MG]

text‹This lemma can be proved before having term‹check_in_M›. At some point Miguel naïvely
  that the term‹check_in_M› could be proved using this argument.›
lemma check_nat_M :
  assumes "n ∈ nat"
  shows "check(n) ∈ M"
  using assms
proof (induct n)
  case 0
  then
  show ?case
    using zero_in_M by (subst def_check,simp)
next
  case (succ x)
  have "1 ∈ M"
    using one_in_P P_sub_M subsetD by simp
  with ‹check(x)∈M›
  have "⟨check(x),1⟩ ∈ M"
    using pair_in_M_iff by simp
  then
  have "{⟨check(x),1⟩} ∈ M"
    using singleton_closed by simp
  with ‹check(x)∈M›
  have "check(x) ∪ {⟨check(x),1⟩} ∈ M"
    using Un_closed by simp
  then
  show ?case
    using ‹x∈nat› def_checkS by simp
qed

lemma def_PHcheck:
  assumes
    "z∈M" "f∈M"
  shows
    "Hcheck(z,f) = Replace(z,PHcheck(##M,1,f))"
proof -
  from assms
  have "⟨f`x,1⟩ ∈ M" "f`x∈M" if "x∈z" for x
    using pair_in_M_iff transitivity that apply_closed by simp_all
  then
  have "{y . x ∈ z, y = ⟨f ` x, 1⟩} = {y . x ∈ z, y = ⟨f ` x, 1⟩ ∧ y∈M ∧ f`x∈M}"
    by simp
  then
  show ?thesis
    using ‹z∈M› ‹f∈M› transitivity
    unfolding Hcheck_def PHcheck_def RepFun_def
    by auto
qed

(* instance of replacement for hcheck *)
lemma wfrec_Hcheck :
  assumes "X∈M"
  shows "wfrec_replacement(##M,is_Hcheck(##M,1),rcheck(X))"
proof -
  let ?f="Exists(And(pair_fm(1,0,2),
               is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0)))"
  have "is_Hcheck(##M,1,a,b,c) ⟷
        sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,1,rcheck(x)])"
    if "a∈M" "b∈M" "c∈M" "d∈M" "e∈M" "y∈M" "x∈M" "z∈M"
    for a b c d e y x z
    using that ‹X∈M› rcheck_in_M is_Hcheck_iff_sats zero_in_M
    by simp
  then
  have "sats(M,is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0), [y,x,z,1,rcheck(X)])
        ⟷ is_wfrec(##M, is_Hcheck(##M,1),rcheck(X), x, y)"
    if "x∈M" "y∈M" "z∈M" for x y z
    using that sats_is_wfrec_fm ‹X∈M› rcheck_in_M zero_in_M
    by simp
  moreover from this
  have satsf:"sats(M, ?f, [x,z,1,rcheck(X)]) ⟷
              (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,1),rcheck(X), x, y))"
    if "x∈M" "z∈M" for x z
    using that ‹X∈M› rcheck_in_M
    by (simp del:pair_abs)
  moreover
  have artyf:"arity(?f) = 4"
    using arity_wfrec_replacement_fm[where p="is_Hcheck_fm(8, 2, 1, 0)" and i=9]
      arity_is_Hcheck_fm ord_simp_union
    by simp
  ultimately
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,1,rcheck(X)]))"
    using ZF_ground_replacements(2) artyf ‹X∈M› rcheck_in_M
    unfolding replacement_assm_def wfrec_Hcheck_fm_def by simp
  then
  have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,1),rcheck(X), x, y))"
    using repl_sats[of M ?f "[1,rcheck(X)]"] satsf by (simp del:pair_abs)
  then
  show ?thesis
    unfolding wfrec_replacement_def by simp
qed

lemma Hcheck_closed' : "f∈M ==> z∈M ==> {f ` x . x ∈ z} ∈ M"
  using RepFun_closed[OF lam_replacement_imp_strong_replacement]
          lam_replacement_apply apply_closed transM[of _ z]
  by simp

lemma repl_PHcheck :
  assumes "f∈M"
  shows "lam_replacement(##M,λx. Hcheck(x,f))"
proof -
  have "Hcheck(x,f) = {f`y . y∈x}×{1}" for x
    unfolding Hcheck_def by auto
  moreover
  note assms
  moreover from this
  have 1:"lam_replacement(##M, λx . {f`y . y∈x}×{1})"
    using lam_replacement_RepFun_apply
      lam_replacement_constant lam_replacement_fst lam_replacement_snd
      singleton_closed cartprod_closed fst_snd_closed Hcheck_closed'
    by (rule_tac lam_replacement_CartProd[THEN [5] lam_replacement_hcomp2],simp_all)
  ultimately
  show ?thesis
    using singleton_closed cartprod_closed Hcheck_closed'
    by(rule_tac lam_replacement_cong[OF 1],auto)
qed

lemma univ_PHcheck : "[ z∈M ; f∈M ] ==> univalent(##M,z,PHcheck(##M,1,f))"
  unfolding univalent_def PHcheck_def
  by simp

lemma PHcheck_closed : "[z∈M ; f∈M ; x∈z; PHcheck(##M,1,f,x,y) ] ==> (##M)(y)"
  unfolding PHcheck_def by simp

lemma relation2_Hcheck : "relation2(##M,is_Hcheck(##M,1),Hcheck)"
proof -
  have "is_Replace(##M,z,PHcheck(##M,1,f),hc) ⟷ hc = Replace(z,PHcheck(##M,1,f))"
    if "z∈M" "f∈M" "hc∈M" for z f hc
    using that Replace_abs[OF _ _ univ_PHcheck] PHcheck_closed[of z f]
    by simp
  with def_PHcheck
  show ?thesis
    unfolding relation2_def is_Hcheck_def Hcheck_def
    by simp
qed

lemma Hcheck_closed : "∀y∈M. ∀g∈M. Hcheck(y,g)∈M"
proof -
  have eq:"Hcheck(x,f) = {f`y . y∈x}×{1}" for f x
    unfolding Hcheck_def by auto
  then
  have "Hcheck(y,g)∈M" if "y∈M" "g∈M" for y g
    using eq that Hcheck_closed' cartprod_closed singleton_closed
    by simp
  then
  show ?thesis
    by auto
qed

lemma wf_rcheck : "x∈M ==> wf(rcheck(x))"
  unfolding rcheck_def using wf_trancl[OF wf_Memrel] .

lemma trans_rcheck : "x∈M ==> trans(rcheck(x))"
  unfolding rcheck_def using trans_trancl .

lemma relation_rcheck : "x∈M ==> relation(rcheck(x))"
  unfolding rcheck_def using relation_trancl .

lemma check_in_M : "x∈M ==> check(x) ∈ M"
  using wfrec_Hcheck[of x] check_trancl wf_rcheck trans_rcheck relation_rcheck rcheck_in_M
    Hcheck_closed relation2_Hcheck trans_wfrec_closed[of "rcheck(x)"]
  by simp

(* Internalization and absoluteness of rcheck\<close> *)
lemma rcheck_abs[Rel] : "[ x∈M ; r∈M ] ==> is_rcheck(##M,x,r) ⟷ r = rcheck(x)"
  unfolding rcheck_def is_rcheck_def
  using singleton_closed trancl_closed Memrel_closed eclose_closed zero_in_M
  by simp

lemma check_abs[Rel] :
  assumes "x∈M" "z∈M"
  shows "is_check(##M,1,x,z) ⟷ z = check(x)"
proof -
  have "is_check(##M,1,x,z) ⟷ is_wfrec(##M,is_Hcheck(##M,1),rcheck(x),x,z)"
    unfolding is_check_def
    using assms rcheck_abs rcheck_in_M zero_in_M
    unfolding check_trancl is_check_def
    by simp
  then
  show ?thesis
    unfolding check_trancl
    using assms wfrec_Hcheck[of x] wf_rcheck trans_rcheck relation_rcheck rcheck_in_M
      Hcheck_closed relation2_Hcheck trans_wfrec_abs[of "rcheck(x)" x z "is_Hcheck(##M,1)" Hcheck]
    by (simp flip: setclass_iff)
qed

lemma check_lam_replacement: "lam_replacement(##M,check)"
proof -
  have "arity(check_fm(2,0,1)) = 3"
    by (simp add:ord_simp_union arity)
  then
  have "Lambda(A, check) ∈ M" if "A∈M" for A
    using that check_in_M transitivity[of _ A]
      sats_check_fm check_abs zero_in_M
      check_fm_type ZF_ground_replacements(3)
    by(rule_tac Lambda_in_M [of "check_fm(2,0,1)" "[1]"],simp_all)
  then
  show ?thesis
    using check_in_M lam_replacement_iff_lam_closed[THEN iffD2]
    by simp
qed

lemma check_replacement: "{check(x). x∈ℙ} ∈ M"
  using lam_replacement_imp_strong_replacement_aux[OF check_lam_replacement]
    transitivity check_in_M RepFun_closed
    by simp_all

lemma M_subset_MG : "1 ∈ G ==> M ⊆ M[G]"
  using check_in_M GenExtI
  by (intro subsetI, subst val_check [of G,symmetric], auto)

text‹The name for the generic filter›
definition
  G_dot :: "i" where
  "G_dot ≡ {⟨check(p),p⟩ . p∈ℙ}"

lemma G_dot_in_M : "G_dot ∈ M"
  using lam_replacement_Pair[THEN [5] lam_replacement_hcomp2,OF
    check_lam_replacement lam_replacement_identity]
    check_in_M lam_replacement_imp_strong_replacement_aux
    transitivity check_in_M RepFun_closed pair_in_M_iff
  unfolding G_dot_def
  by simp

lemma zero_in_MG : "0 ∈ M[G]"
proof -
  have "0 = val(G,0)"
    using zero_in_M elem_of_val by auto
  also
  have "... ∈ M[G]"
    using GenExtI zero_in_M by simp
  finally
  show ?thesis .
qed

declare check_in_M [simp,intro]

end ― ‹🍋‹forcing_data1››

context G_generic1
begin

lemma val_G_dot : "val(G,G_dot) = G"
proof (intro equalityI subsetI)
  fix x
  assume "x∈val(G,G_dot)"
  then obtain θ p where "p∈G" "⟨θ,p⟩ ∈ G_dot" "val(G,θ) = x" "θ = check(p)"
    unfolding G_dot_def using elem_of_val_pair G_dot_in_M
    by force
  then
  show "x ∈ G"
    using G_subset_P one_in_G val_check P_sub_M by auto
next
  fix p
  assume "p∈G"
  have "⟨check(q),q⟩ ∈ G_dot" if "q∈ℙ" for q
    unfolding G_dot_def using that by simp
  with ‹p∈G›
  have "val(G,check(p)) ∈ val(G,G_dot)"
    using val_of_elem G_dot_in_M by blast
  with ‹p∈G›
  show "p ∈ val(G,G_dot)"
    using one_in_G G_subset_P P_sub_M val_check by auto
qed

lemma G_in_Gen_Ext : "G ∈ M[G]"
  using G_subset_P one_in_G val_G_dot GenExtI[of _ G] G_dot_in_M
  by force

lemmas generic_simps = val_check[OF one_in_G one_in_P]
  M_subset_MG[OF one_in_G, THEN subsetD]
  GenExtI P_in_M

lemmas generic_dests = M_genericD M_generic_compatD

bundle G_generic1_lemmas = generic_simps[simp] generic_dests[dest]

end  ― ‹🍋‹G_generic1››

sublocale G_generic1 ⊆ ext: M_trans "##M[G]"
  using generic transitivity_MG zero_in_MG
  by unfold_locales force+

end