section‹Names and generic extensions›
theory Names
imports
Forcing_Data
Interface
Recursion_Thms
Relativization
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{_ ../ _ ∈ _, _})")
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
definition
Hv :: "[i,i,i,i]⇒i" where
"Hv(P,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›
according to a (generic) filter \<^term>‹G›. Note the definition
in terms of the well-founded recursor.›
definition
val :: "[i,i,i]⇒i" where
"val(P,G,τ) ≡ wfrec(edrel(eclose({τ})), τ ,Hv(P,G))"
definition
GenExt :: "[i,i,i]⇒i" ("_⇗_⇖[_]" [71,1])
where "M⇗P⇖[G] ≡ {val(P,G,τ). τ ∈ M}"
abbreviation (in forcing_notion)
GenExt_at_P :: "i⇒i⇒i" ("_[_]" [71,1])
where "M[G] ≡ M⇗P⇖[G]"
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)
end
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
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
lemma aux_def_val:
assumes "z ∈ domain(x)"
shows "wfrec(edrel(eclose({x})),z,Hv(P,G)) = wfrec(edrel(eclose({z})),z,Hv(P,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(P,G)) = wfrec[eclose({z})](?r(x),z,Hv(P,G))"
using wfrec_restr by simp
also from ‹z∈domain(x)›
have "... = wfrec(?r(z),z,Hv(P,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(P,G,x) = {val(P,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(P,G))"
have "∀τ. wf(?r(τ))" using wf_edrel by simp
with wfrec [of _ x]
have "val(P,G,x) = Hv(P,G,x,?f)" using val_def by simp
also
have " ... = Hv(P,G,x,λz∈domain(x). wfrec(?r(x),z,Hv(P,G)))"
using dom_under_edrel_eclose by simp
also
have " ... = Hv(P,G,x,λz∈domain(x). val(P,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(P,G,x) ⊆ val(P,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 valcheck : "one ∈ G ⟹ one ∈ P ⟹ val(P,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(P,G,check(y)) = val(P,G, {⟨check(w), one⟩ . w ∈ y})"
by simp
also
have " ... = {val(P,G,t) .. t∈domain(?C) , ∃p∈P . ⟨t, p⟩∈?C ∧ p ∈ G }"
using def_val by blast
also
have " ... = {val(P,G,t) .. t∈domain(?C) , ∃w∈y. t=check(w) }"
using 1 by simp
also
have " ... = {val(P,G,check(w)) . w∈y }"
by force
finally
show "val(P,G,check(y)) = y"
using 1 by simp
qed
qed
lemma val_of_name :
"val(P,G,{x∈A×P. Q(x)}) = {val(P,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(P,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(P,G,t) else 0)"
by simp
moreover have "... = val(P,G,t)"
using dom_under_edrel_eclose H if_P by auto
}
then
have Eq1: "t ∈ domain({x ∈ A × P . Q(x)}) ⟹ val(P,G,t) = ?f` t" for t
by simp
have "val(P,G,?n) = {val(P,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(P,G,t) else 0) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
by (simp)
also
have Eq2: "... = { val(P,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(P,G,t) else 0) = val(P,G,t)"
by auto
then
show "{ (if t∈?r(?n)-``{?n} then val(P,G,t) else 0) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G} =
{ val(P,G,t) .. t∈domain(?n), ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
by auto
qed
also
have " ... = { val(P,G,t) .. t∈A, ∃p∈P . ⟨t,p⟩∈?n ∧ p∈G}"
by force
finally
show " val(P,G,?n) = { val(P,G,t) .. t∈A, ∃p∈P . Q(⟨t,p⟩) ∧ p∈G}"
by auto
qed
lemma val_of_name_alt :
"val(P,G,{x∈A×P. Q(x)}) = {val(P,G,t) .. t∈A , ∃p∈P∩G . Q(⟨t,p⟩) }"
using val_of_name by force
lemma val_only_names: "val(P,F,τ) = val(P,F,{x∈τ. ∃t∈domain(τ). ∃p∈P. x=⟨t,p⟩})"
(is "_ = val(P,F,?name)")
proof -
have "val(P,F,?name) = {val(P,F, t).. t∈domain(?name), ∃p∈P. ⟨t, p⟩ ∈ ?name ∧ p ∈ F}"
using def_val by blast
also
have " ... = {val(P,F, t). t∈{y∈domain(?name). ∃p∈P. ⟨y, p⟩ ∈ ?name ∧ p ∈ F}}"
using Sep_and_Replace by simp
also
have " ... = {val(P,F, t). t∈{y∈domain(τ). ∃p∈P. ⟨y, p⟩ ∈ τ ∧ p ∈ F}}"
by blast
also
have " ... = {val(P,F, t).. t∈domain(τ), ∃p∈P. ⟨t, p⟩ ∈ τ ∧ p ∈ F}"
using Sep_and_Replace by simp
also
have " ... = val(P,F, τ)"
using def_val[symmetric] by blast
finally
show ?thesis ..
qed
lemma val_only_pairs: "val(P,F,τ) = val(P,F,{x∈τ. ∃t p. x=⟨t,p⟩})"
proof
have "val(P,F,τ) = val(P,F,{x∈τ. ∃t∈domain(τ). ∃p∈P. x=⟨t,p⟩})"
(is "_ = val(P,F,?name)")
using val_only_names .
also
have "... ⊆ val(P,F,{x∈τ. ∃t p. x=⟨t,p⟩})"
using val_mono[of ?name "{x∈τ. ∃t p. x=⟨t,p⟩}"] by auto
finally
show "val(P,F,τ) ⊆ val(P,F,{x∈τ. ∃t p. x=⟨t,p⟩})" by simp
next
show "val(P,F,{x∈τ. ∃t p. x=⟨t,p⟩}) ⊆ val(P,F,τ)"
using val_mono[of "{x∈τ. ∃t p. x=⟨t,p⟩}"] by auto
qed
lemma val_subset_domain_times_range: "val(P,F,τ) ⊆ val(P,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(P,F,τ) ⊆ val(P,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
lemma val_of_elem: "⟨θ,p⟩ ∈ π ⟹ p∈G ⟹ p∈P ⟹ val(P,G,θ) ∈ val(P,G,π)"
proof -
assume
"⟨θ,p⟩ ∈ π"
then
have "θ∈domain(π)" by auto
assume "p∈G" "p∈P"
with ‹θ∈domain(π)› ‹⟨θ,p⟩ ∈ π›
have "val(P,G,θ) ∈ {val(P,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(P,G,π) ⟹ ∃θ∈domain(π). val(P,G,θ) = x"
by (subst (asm) def_val,auto)
lemma elem_of_val_pair: "x∈val(P,G,π) ⟹ ∃θ. ∃p∈G. ⟨θ,p⟩∈π ∧ val(P,G,θ) = x"
by (subst (asm) def_val,auto)
lemma elem_of_val_pair':
assumes "π∈M" "x∈val(P,G,π)"
shows "∃θ∈M. ∃p∈G. ⟨θ,p⟩∈π ∧ val(P,G,θ) = x"
proof -
from assms
obtain θ p where "p∈G" "⟨θ,p⟩∈π" "val(P,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(P,G,τ)"
by (simp add:GenExt_def)
lemma GenExtI:
"x ∈ M ⟹ val(P,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(P,G,c)∈M[G]" "y ∈ val(P,G,c)"
using GenExtD by auto
from ‹y ∈ val(P,G,c)›
obtain θ where "θ∈domain(c)" "val(P,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
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))))"
declare PHcheck_fm_def[fm_definitions]
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)
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)"
declare is_Hcheck_fm_def [fm_definitions]
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
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 fm_definitions
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
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))))"
declare singleton_fm_def[fm_definitions]
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
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[Rel] :
"⟦ 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[Rel] :
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
definition
check_fm :: "[i,i,i] ⇒ i" where
[fm_definitions] :
"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 eclose_n_fm_def is_eclose_fm_def mem_eclose_fm_def fm_definitions
by (simp add:nat_simp_union)
moreover
have "check(x)∈M" if "x∈P" for x
using that transitivity 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 is_eclose_fm_def mem_eclose_fm_def eclose_n_fm_def fm_definitions
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(P,G,G_dot) = G"
proof (intro equalityI subsetI)
fix x
assume "x∈val(P,G,G_dot)"
then obtain θ p where "p∈G" "⟨θ,p⟩ ∈ G_dot" "val(P,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(P,G,check(p)) ∈ val(P,G,G_dot)"
using val_of_elem G_dot_in_M by blast
with ‹p∈G› ‹G⊆P› ‹one∈G›
show "p ∈ val(P,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
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
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(P,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
end