Quelle  Names.thy

section‹Names and generic extensions›

theory Names
  imports
    Forcing_Data
    Interface
    Recursion_Thms
    Synthetic_Definition
begin

definition
  SepReplace :: "[i, i==>i, i==> o] ==> i" where
  "SepReplace(A,b,Q) ≡ {y . x∈A, y=b(x) ∧ Q(x)}"

syntax
  "_SepReplace"  :: "[i, pttrn, i, o] ==> i"  (‹(1{_ ../ _ ∈ _, _})›)
syntax_consts
  "_SepReplace" == SepReplace
translations
  "{b .. x∈A, Q}" => "CONST SepReplace(A, λx. b, λx. Q)"

lemma Sep_and_Replace: "{b(x) .. x∈A, P(x) } = {b(x) . x∈{y∈A. P(y)}}"
  by (auto simp add:SepReplace_def)

lemma SepReplace_subset : "A⊆A'==> {b .. x∈A, Q}⊆{b .. x∈A', Q}"
  by (auto simp add:SepReplace_def)

lemma SepReplace_iff [simp]: "y∈{b(x) .. x∈A, P(x)} ⟷ (∃x∈A. y=b(x) & P(x))"
  by (auto simp add:SepReplace_def)

lemma SepReplace_dom_implies :
  "(∧ x . x ∈A ==> b(x) = b'(x))==> {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (simp add:SepReplace_def)

lemma SepReplace_pred_implies :
  "∀x. Q(x)⟶ b(x) = b'(x)==> {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (force simp add:SepReplace_def)

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

lemma eclose_sing : "x ∈ eclose(a) ==> x ∈ eclose({a})"
  by(rule subsetD[OF mem_eclose_subset],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 (eq) "x=a" | (lt) "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
  fix z
  assume
    "z∈edrel(A)"
  then obtain x y where
    Eq1:   "x∈A" "y∈A" "z=⟨x,y⟩" "x∈domain(y)"
    using edrelD
    by blast
  then obtain u v where
    Eq2:   "x∈u" "u∈v" "v∈y"
    unfolding domain_def Pair_def by auto
  with Eq1 have
    Eq3:   "x∈eclose(A)" "y∈eclose(A)" "u∈eclose(A)" "v∈eclose(A)"
    by (auto, rule_tac [3-4] ecloseD, rule_tac [3] ecloseD, simp_all add:arg_into_eclose)
  let
    ?r="trancl(Memrel(eclose(A)))"
  from Eq2 and Eq3 have
    "⟨x,u⟩∈?r" "⟨u,v⟩∈?r" "⟨v,y⟩∈?r"
    by (auto simp add: r_into_trancl)
  then  have
    "⟨x,y⟩∈?r"
    by (rule_tac trancl_trans, rule_tac [2] trancl_trans, simp)
  with Eq1 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
  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 yr:"y ∈ ?rr"
  with yr obtain a b where 1:"⟨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 yr:"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 this ‹a∈domain(b)›
  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


context M_ctm
begin

lemma upairM : "x ∈ M ==> y ∈ M ==> {x,y} ∈ M"
  by (simp flip: setclass_iff)

lemma singletonM : "a ∈ M ==> {a} ∈ M"
  by (simp flip: setclass_iff)

lemma Rep_simp : "Replace(u,λ y z . z = f(y)) = { f(y) . y ∈ u}"
  by(auto)

end (* M_ctm *)

subsection‹Values and check-names›
context forcing_data
begin

definition
  Hcheck :: "[i,i] ==> i" where
  "Hcheck(z,f) ≡ { ⟨f`y,one⟩ . 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 ..

definition
  rcheck :: "i ==> i" where
  "rcheck(x) ≡ Memrel(eclose({x}))^+"


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

(* relation of check is in M *)
lemma rcheck_in_M :
  "x ∈ M ==> rcheck(x) ∈ M"
  unfolding rcheck_def by (simp flip: setclass_iff)


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),one⟩ . 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),one⟩}"
proof -
  have "check(succ(n)) = {⟨check(i),one⟩ . i ∈ succ(n)} "
    using def_check by blast
  also have "... = {⟨check(i),one⟩ . i ∈ n} ∪ {⟨check(n),one⟩}"
    by blast
  also have "... = check(n) ∪ {⟨check(n),one⟩}"
    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

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

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))"

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) = {val(G,t) .. t∈domain(x) , ∃p∈P . ⟨t,p⟩∈x ∧ p ∈ G }"
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 SepReplace_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 valcheck : "one ∈ G ==> one ∈ P ==> val(G,check(y)) = y"
proof (induct rule:eps_induct)
  case (1 y)
  then show ?case
  proof -    
    have "check(y) = { ⟨check(w), one⟩ . w ∈ y}"  (is "_ = ?C") 
      using def_check .
    then
    have "val(G,check(y)) = val(G, {⟨check(w), one⟩ . w ∈ y})"
      by simp
    also
    have " ... = {val(G,t) .. t∈domain(?C) , ∃p∈P . ⟨t, p⟩∈?C ∧ p ∈ G }"
      using def_val by blast
    also
    have " ... = {val(G,t) .. t∈domain(?C) , ∃w∈y. t=check(w) }"
      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×P. Q(x)}) = {val(G,t) .. t∈A , ∃p∈P . Q(⟨t,p⟩) ∧ p ∈ G }"
proof -
  let
    ?n="{x∈A×P. 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 × P . 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 × P . Q(x)}) ==> val(G,t) = ?f` t"  for t
    by simp
  have "val(G,?n) = {val(G,t) .. t∈domain(?n), ∃p ∈ P . ⟨t,p⟩ ∈ ?n ∧ p ∈ G}"
    by (subst def_val,simp)
  also
  have "... = {?f`t .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
    unfolding Hv_def
    by (subst SepReplace_dom_implies,auto simp add:Eq1)
  also
  have  "... = { (if t∈?r(?n)-``{?n} then val(G,t) else 0) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
    by (simp)
  also
  have Eq2:  "... = { val(G,t) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
  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 "{ (if t∈?r(?n)-``{?n} then val(G,t) else 0) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G} =
          { val(G,t) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
      by auto
  qed
  also
  have " ... = { val(G,t) .. t∈A, ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
    by force
  finally
  show " val(G,?n) = { val(G,t) .. t∈A, ∃p∈P . Q(⟨t,p⟩) ∧ p∈G}"
    by auto
qed

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

lemma val_only_names: "val(F,τ) = val(F,{x∈τ. ∃t∈domain(τ). ∃p∈P. x=⟨t,p⟩})"
  (is "_ = val(F,?name)")
proof -
  have "val(F,?name) = {val(F, t).. t∈domain(?name), ∃p∈P. ⟨t, p⟩ ∈ ?name ∧ p ∈ F}"
    using def_val by blast
  also
  have " ... = {val(F, t). t∈{y∈domain(?name). ∃p∈P. ⟨y, p⟩ ∈ ?name ∧ p ∈ F}}"
    using Sep_and_Replace by simp
  also
  have " ... = {val(F, t). t∈{y∈domain(τ). ∃p∈P. ⟨y, p⟩ ∈ τ ∧ p ∈ F}}"
    by blast
  also
  have " ... = {val(F, t).. t∈domain(τ), ∃p∈P. ⟨t, p⟩ ∈ τ ∧ p ∈ F}"
    using Sep_and_Replace by simp
  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∈P. 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_subset_domain_times_P: "val(F,τ) ⊆ val(F,domain(τ)×P)"
  using val_only_names[of F τ] val_mono[of "{x∈τ. ∃t∈domain(τ). ∃p∈P. x=⟨t,p⟩}" "domain(τ)×P" F]
  by auto

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


lemma val_of_elem: "⟨θ,p⟩ ∈ π ==> p∈G ==> p∈P ==> val(G,θ) ∈ val(G,π)"
proof -
  assume
    "⟨θ,p⟩ ∈ π"
  then
  have "θ∈domain(π)" by auto
  assume "p∈G" "p∈P"
  with ‹θ∈domain(π)› ‹⟨θ,p⟩ ∈ π›
  have "val(G,θ) ∈ {val(G,t) .. t∈domain(π) , ∃p∈P . ⟨t, p⟩∈π ∧ p ∈ G }"
    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]

lemma check_n_M :
  fixes n
  assumes "n ∈ nat"
  shows "check(n) ∈ M"
  using ‹n∈nat›
proof (induct n)
  case 0
  then show ?case using zero_in_M by (subst def_check,simp)
next
  case (succ x)
  have "one ∈ M" using one_in_P P_sub_M subsetD by simp
  with ‹check(x)∈M›
  have "⟨check(x),one⟩ ∈ M"
    using tuples_in_M by simp
  then
  have "{⟨check(x),one⟩} ∈ M"
    using singletonM by simp
  with ‹check(x)∈M›
  have "check(x) ∪ {⟨check(x),one⟩} ∈ M"
    using Un_closed by simp
  then show ?case using ‹x∈nat› def_checkS by simp
qed


definition
  PHcheck :: "[i,i,i,i] ==> o" where
  "PHcheck(o,f,y,p) ≡ p∈M ∧ (∃fy[##M]. fun_apply(##M,f,y,fy) ∧ pair(##M,fy,o,p))"

definition
  is_Hcheck :: "[i,i,i,i] ==> o" where
  "is_Hcheck(o,z,f,hc) ≡ is_Replace(##M,z,PHcheck(o,f),hc)"

lemma one_in_M: "one ∈ M"
  by (insert one_in_P P_in_M, simp add: transitivity)

lemma def_PHcheck:
  assumes
    "z∈M" "f∈M"
  shows
    "Hcheck(z,f) = Replace(z,PHcheck(one,f))"
proof -
  from assms
  have "⟨f`x,one⟩ ∈ M" "f`x∈M" if "x∈z" for x
    using tuples_in_M one_in_M transitivity that apply_closed by simp_all
  then
  have "{y . x ∈ z, y = ⟨f ` x, one⟩} = {y . x ∈ z, y = ⟨f ` x, one⟩ ∧ 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

(*
  "PHcheck(o,f,y,p) \<equiv> \<exists>fy[##M]. fun_apply(##M,f,y,fy) \<and> pair(##M,fy,o,p)"
*)
definition
  PHcheck_fm :: "[i,i,i,i] ==> i" where
  "PHcheck_fm(o,f,y,p) ≡ Exists(And(fun_apply_fm(succ(f),succ(y),0)
                                 ,pair_fm(0,succ(o),succ(p))))"

lemma PHcheck_type [TC]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; u ∈ nat ] ==> PHcheck_fm(x,y,z,u) ∈ formula"
  by (simp add:PHcheck_fm_def)

lemma sats_PHcheck_fm [simp]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; u ∈ nat ; env ∈ list(M)]
    ==> sats(M,PHcheck_fm(x,y,z,u),env) ⟷
        PHcheck(nth(x,env),nth(y,env),nth(z,env),nth(u,env))"
  using zero_in_M Internalizations.nth_closed by (simp add: PHcheck_def PHcheck_fm_def)

(*
  "is_Hcheck(o,z,f,hc)  \<equiv> is_Replace(##M,z,PHcheck(o,f),hc)"
*)
definition
  is_Hcheck_fm :: "[i,i,i,i] ==> i" where
  "is_Hcheck_fm(o,z,f,hc) ≡ Replace_fm(z,PHcheck_fm(succ(succ(o)),succ(succ(f)),0,1),hc)"

lemma is_Hcheck_type [TC]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; u ∈ nat ] ==> is_Hcheck_fm(x,y,z,u) ∈ formula"
  by (simp add:is_Hcheck_fm_def)

lemma sats_is_Hcheck_fm [simp]:
  "[ x ∈ nat; y ∈ nat; z ∈ nat; u ∈ nat ; env ∈ list(M)]
    ==> sats(M,is_Hcheck_fm(x,y,z,u),env) ⟷
        is_Hcheck(nth(x,env),nth(y,env),nth(z,env),nth(u,env))"
  using sats_Replace_fm unfolding is_Hcheck_def is_Hcheck_fm_def
  by simp


(* instance of replacement for hcheck *)
lemma wfrec_Hcheck :
  assumes
    "X∈M"
  shows
    "wfrec_replacement(##M,is_Hcheck(one),rcheck(X))"
proof -
  have "is_Hcheck(one,a,b,c) ⟷
        sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,one,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 one_in_M ‹X∈M› rcheck_in_M by simp
  then have 1:"sats(M,is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0),
                    [y,x,z,one,rcheck(X)]) ⟷
            is_wfrec(##M, is_Hcheck(one),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 one_in_M by simp
  let
    ?f="Exists(And(pair_fm(1,0,2),
               is_wfrec_fm(is_Hcheck_fm(8,2,1,0),4,1,0)))"
  have satsf:"sats(M, ?f, [x,z,one,rcheck(X)]) ⟷
              (∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(one),rcheck(X), x, y))"
    if "x∈M" "z∈M" for x z
    using that 1 ‹X∈M› rcheck_in_M one_in_M by (simp del:pair_abs)
  have artyf:"arity(?f) = 4"
    unfolding is_wfrec_fm_def is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def
      pair_fm_def upair_fm_def is_recfun_fm_def fun_apply_fm_def big_union_fm_def
      pre_image_fm_def restriction_fm_def image_fm_def
    by (simp add:nat_simp_union)
  then
  have "strong_replacement(##M,λx z. sats(M,?f,[x,z,one,rcheck(X)]))"
    using replacement_ax 1 artyf ‹X∈M› rcheck_in_M one_in_M by simp
  then
  have "strong_replacement(##M,λx z.
          ∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(one),rcheck(X), x, y))"
    using repl_sats[of M ?f "[one,rcheck(X)]"] satsf by (simp del:pair_abs)
  then
  show ?thesis unfolding wfrec_replacement_def by simp
qed

lemma repl_PHcheck :
  assumes
    "f∈M"
  shows
    "strong_replacement(##M,PHcheck(one,f))"
proof -
  have "arity(PHcheck_fm(2,3,0,1)) = 4"
    unfolding PHcheck_fm_def fun_apply_fm_def big_union_fm_def pair_fm_def image_fm_def
      upair_fm_def
    by (simp add:nat_simp_union)
  with ‹f∈M›
  have "strong_replacement(##M,λx y. sats(M,PHcheck_fm(2,3,0,1),[x,y,one,f]))"
    using replacement_ax one_in_M by simp
  with ‹f∈M›
  show ?thesis using one_in_M unfolding strong_replacement_def univalent_def by simp
qed

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

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

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

lemma Hcheck_closed :
  "∀y∈M. ∀g∈M. function(g) ⟶ Hcheck(y,g)∈M"
proof -
  have "Replace(y,PHcheck(one,f))∈M" if "f∈M" "y∈M" for f y
    using that repl_PHcheck  PHcheck_closed[of y f] univ_PHcheck
      strong_replacement_closed
    by (simp flip: setclass_iff)
  then show ?thesis using def_PHcheck 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"
  unfolding transrec_def
  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)" x "is_Hcheck(one)" Hcheck]
  by (simp flip: setclass_iff)

end (* forcing_data *)

(* check if this should go to Relative! *)
definition
  is_singleton :: "[i==>o,i,i] ==> o" where
  "is_singleton(A,x,z) ≡ ∃c[A]. empty(A,c) ∧ is_cons(A,x,c,z)"

lemma (in M_trivial) singleton_abs[simp] : "[ M(x) ; M(s) ] ==> is_singleton(M,x,s) ⟷ s = {x}"
  unfolding is_singleton_def using nonempty by simp

definition
  singleton_fm :: "[i,i] ==> i" where
  "singleton_fm(i,j) ≡ Exists(And(empty_fm(0), cons_fm(succ(i),0,succ(j))))"

lemma singleton_type[TC] : "[ x ∈ nat; y ∈ nat ] ==> singleton_fm(x,y) ∈ formula"
  unfolding singleton_fm_def by simp

lemma is_singleton_iff_sats:
  "[ nth(i,env) = x; nth(j,env) = y;
          i ∈ nat; j∈nat ; env ∈ list(A)]
       ==> is_singleton(##A,x,y) ⟷ sats(A, singleton_fm(i,j), env)"
  unfolding is_singleton_def singleton_fm_def by simp

context forcing_data begin

(* Internalization and absoluteness of rcheck *)
definition
  is_rcheck :: "[i,i] ==> o" where
  "is_rcheck(x,z) ≡ ∃r∈M. tran_closure(##M,r,z) ∧ (∃ec∈M. membership(##M,ec,r) ∧
                           (∃s∈M. is_singleton(##M,x,s) ∧ is_eclose(##M,s,ec)))"

lemma rcheck_abs :
  "[ x∈M ; r∈M ] ==> is_rcheck(x,r) ⟷ r = rcheck(x)"
  unfolding rcheck_def is_rcheck_def
  using singletonM trancl_closed Memrel_closed eclose_closed by simp

schematic_goal rcheck_fm_auto:
  assumes
    "i ∈ nat" "j ∈ nat" "env ∈ list(M)"
  shows
    "is_rcheck(nth(i,env),nth(j,env)) ⟷ sats(M,?rch(i,j),env)"
  unfolding is_rcheck_def
  by (insert assms ; (rule sep_rules is_singleton_iff_sats is_eclose_iff_sats
        trans_closure_fm_iff_sats | simp)+)

synthesize "rcheck_fm" from_schematic rcheck_fm_auto

definition
  is_check :: "[i,i] ==> o" where
  "is_check(x,z) ≡ ∃rch∈M. is_rcheck(x,rch) ∧ is_wfrec(##M,is_Hcheck(one),rch,x,z)"

lemma check_abs :
  assumes
    "x∈M" "z∈M"
  shows
    "is_check(x,z) ⟷ z = check(x)"
proof -
  have
    "is_check(x,z) ⟷ is_wfrec(##M,is_Hcheck(one),rcheck(x),x,z)"
    unfolding is_check_def using assms rcheck_abs rcheck_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(one)" Hcheck]
    by (simp flip: setclass_iff)
qed

(* \<exists>rch\<in>M. is_rcheck(x,rch) \<and> is_wfrec(##M,is_Hcheck(one),rch,x,z) *)
definition
  check_fm :: "[i,i,i] ==> i" where
  "check_fm(x,o,z) ≡ Exists(And(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"
  unfolding check_fm_def by simp

lemma sats_check_fm :
  assumes
    "nth(o,env) = one" "x∈nat" "z∈nat" "o∈nat" "env∈list(M)" "x < length(env)" "z < length(env)"
  shows
    "sats(M, check_fm(x,o,z), env) ⟷ is_check(nth(x,env),nth(z,env))"
proof -
  have sats_is_Hcheck_fm:
    "∧a0 a1 a2 a3 a4. [ a0∈M; a1∈M; a2∈M; a3∈M; a4∈M ] ==>
         is_Hcheck(one,a2, a1, a0) ⟷
         sats(M, is_Hcheck_fm(6#+o,2,1,0), [a0,a1,a2,a3,a4,r]@env)" if "r∈M" for r
    using that one_in_M assms  by simp
  then
  have "sats(M, is_wfrec_fm(is_Hcheck_fm(6#+o,2,1,0),0,1#+x,1#+z),Cons(r,env))
        ⟷ is_wfrec(##M,is_Hcheck(one),r,nth(x,env),nth(z,env))" if "r∈M" for r
    using that assms one_in_M sats_is_wfrec_fm by simp
  then
  show ?thesis unfolding is_check_def check_fm_def
    using assms rcheck_in_M one_in_M rcheck_fm_iff_sats[symmetric] by simp
qed


lemma check_replacement:
  "{check(x). x∈P} ∈ M"
proof -
  have "arity(check_fm(0,2,1)) = 3"
    unfolding check_fm_def rcheck_fm_def trans_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
      is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
      is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
      is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
    by (simp add:nat_simp_union)
  moreover
  have "check(x)∈M" if "x∈P" for x
    using that Transset_intf[of M x P] trans_M check_in_M P_in_M by simp
  ultimately
  show ?thesis using sats_check_fm check_abs P_in_M check_in_M one_in_M
      Repl_in_M[of "check_fm(0,2,1)" "[one]" is_check check] by simp
qed

lemma pair_check : "[ p∈M ; y∈M ] ==> (∃c∈M. is_check(p,c) ∧ pair(##M,c,p,y)) ⟷ y = ⟨check(p),p⟩"
  using check_abs check_in_M tuples_in_M by simp


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

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

lemma G_dot_in_M :
  "G_dot ∈ M"
proof -
  let ?is_pcheck = "λx y. ∃ch∈M. is_check(x,ch) ∧ pair(##M,ch,x,y)"
  let ?pcheck_fm = "Exists(And(check_fm(1,3,0),pair_fm(0,1,2)))"
  have "sats(M,?pcheck_fm,[x,y,one]) ⟷ ?is_pcheck(x,y)" if "x∈M" "y∈M" for x y
    using sats_check_fm that one_in_M by simp
  moreover
  have "?is_pcheck(x,y) ⟷ y = ⟨check(x),x⟩" if "x∈M" "y∈M" for x y
    using that check_abs check_in_M by simp
  moreover
  have "?pcheck_fm∈formula" by simp
  moreover
  have "arity(?pcheck_fm)=3"
    unfolding check_fm_def rcheck_fm_def trans_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
      is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
      is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
      is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
    by (simp add:nat_simp_union)
  moreover
  from P_in_M check_in_M tuples_in_M P_sub_M
  have "⟨check(p),p⟩ ∈ M" if "p∈P" for p
    using that by auto
  ultimately
  show ?thesis
    unfolding G_dot_def
    using one_in_M P_in_M Repl_in_M[of ?pcheck_fm "[one]"]
    by simp
qed


lemma val_G_dot :
  assumes "G ⊆ P"
    "one ∈ G"
  shows "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
  with ‹one∈G› ‹G⊆P› show
    "x ∈ G"
    using valcheck P_sub_M by auto
next
  fix p
  assume "p∈G"
  have "⟨check(q),q⟩ ∈ G_dot" if "q∈P" for q
    unfolding G_dot_def using that by simp
  with ‹p∈G› ‹G⊆P›
  have "val(G,check(p)) ∈ val(G,G_dot)"
    using val_of_elem G_dot_in_M by blast
  with ‹p∈G› ‹G⊆P› ‹one∈G›
  show "p ∈ val(G,G_dot)"
    using P_sub_M valcheck by auto
qed


lemma G_in_Gen_Ext :
  assumes "G ⊆ P" and "one ∈ G"
  shows   "G ∈ M[G]"
  using assms val_G_dot GenExtI[of _ G] G_dot_in_M
  by force

(* Move this to M_trivial *)
lemma fst_snd_closed: "p∈M ==> fst(p) ∈ M ∧ snd(p)∈ M"
proof (cases "∃a. ∃b. p = ⟨a, b⟩")
  case False
  then
  show "fst(p) ∈ M ∧ snd(p) ∈ M" unfolding fst_def snd_def using zero_in_M by auto
next
  case True
  then
  obtain a b where "p = ⟨a, b⟩" by blast
  with True
  have "fst(p) = a" "snd(p) = b" unfolding fst_def snd_def by simp_all
  moreover
  assume "p∈M"
  moreover from this
  have "a∈M"
    unfolding ‹p = _› Pair_def by (force intro:Transset_M[OF trans_M])
  moreover from  ‹p∈M›
  have "b∈M"
    using Transset_M[OF trans_M, of "{a,b}" p] Transset_M[OF trans_M, of "b" "{a,b}"]
    unfolding ‹p = _› Pair_def by (simp)
  ultimately
  show ?thesis by simp
qed

end (* forcing_data *)

locale G_generic = forcing_data +
  fixes G :: "i"
  assumes generic : "M_generic(G)"
begin

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

lemma G_nonempty: "G≠0"
proof -
  have "P⊆P" ..
  with P_in_M P_dense ‹P⊆P›
  show "G ≠ 0"
    using generic unfolding M_generic_def by auto
qed

end (* context G_generic *)
end