Theory Names
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›
according to a (generic) filter \<^term>‹G›. Note the definition
in 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,𝟭⟩ . 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),𝟭⟩ . 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),𝟭⟩}"
proof -
have "check(succ(n)) = {⟨check(i),𝟭⟩ . i ∈ succ(n)} "
using def_check by blast
also
have "... = {⟨check(i),𝟭⟩ . i ∈ n} ∪ {⟨check(n),𝟭⟩}"
by blast
also
have "... = check(n) ∪ {⟨check(n),𝟭⟩}"
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
ground model. Here we show that this is the case.›
lemma val_check : "𝟭 ∈ G ⟹ 𝟭 ∈ ℙ ⟹ val(G,check(y)) = y"
proof (induct rule:eps_induct)
case (1 y)
then show ?case
proof -
have "check(y) = { ⟨check(w), 𝟭⟩ . w ∈ y}" (is "_ = ?C")
using def_check .
then
have "val(G,check(y)) = val(G, {⟨check(w), 𝟭⟩ . 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
thought 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 "𝟭 ∈ M"
using one_in_P P_sub_M subsetD by simp
with ‹check(x)∈M›
have "⟨check(x),𝟭⟩ ∈ M"
using pair_in_M_iff by simp
then
have "{⟨check(x),𝟭⟩} ∈ M"
using singleton_closed by simp
with ‹check(x)∈M›
have "check(x) ∪ {⟨check(x),𝟭⟩} ∈ 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,𝟭,f))"
proof -
from assms
have "⟨f`x,𝟭⟩ ∈ 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, 𝟭⟩} = {y . x ∈ z, y = ⟨f ` x, 𝟭⟩ ∧ 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
lemma wfrec_Hcheck :
assumes "X∈M"
shows "wfrec_replacement(##M,is_Hcheck(##M,𝟭),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,𝟭,a,b,c) ⟷
sats(M,is_Hcheck_fm(8,2,1,0),[c,b,a,d,e,y,x,z,𝟭,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,𝟭,rcheck(X)])
⟷ is_wfrec(##M, is_Hcheck(##M,𝟭),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,𝟭,rcheck(X)]) ⟷
(∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hcheck(##M,𝟭),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,𝟭,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,𝟭),rcheck(X), x, y))"
using repl_sats[of M ?f "[𝟭,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}×{𝟭}" for x
unfolding Hcheck_def by auto
moreover
note assms
moreover from this
have 1:"lam_replacement(##M, λx . {f`y . y∈x}×{𝟭})"
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,𝟭,f))"
unfolding univalent_def PHcheck_def
by simp
lemma PHcheck_closed : "⟦z∈M ; f∈M ; x∈z; PHcheck(##M,𝟭,f,x,y) ⟧ ⟹ (##M)(y)"
unfolding PHcheck_def by simp
lemma relation2_Hcheck : "relation2(##M,is_Hcheck(##M,𝟭),Hcheck)"
proof -
have "is_Replace(##M,z,PHcheck(##M,𝟭,f),hc) ⟷ hc = Replace(z,PHcheck(##M,𝟭,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}×{𝟭}" 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
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,𝟭,x,z) ⟷ z = check(x)"
proof -
have "is_check(##M,𝟭,x,z) ⟷ is_wfrec(##M,is_Hcheck(##M,𝟭),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,𝟭)" 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)" "[𝟭]"],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 : "𝟭 ∈ 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
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
sublocale G_generic1 ⊆ ext: M_trans "##M[G]"
using generic transitivity_MG zero_in_MG
by unfold_locales force+
end