theory Names imports Forcing_Data Interface Recursion_Thms begin
lemma transD : "Transset(M) ⟹ y ∈ M ⟹ y ⊆ M"
by (unfold Transset_def, blast)
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)
section‹eclose properties›
lemma eclose_sing : "x ∈ eclose(a) ⟹ x ∈ eclose({a})"
by(rule subsetD[OF mem_eclose_subset],simp+)
lemma ecloseE : "x ∈ eclose(A) ⟹ x ∈ A ∨ (∃ B ∈ A . x ∈ eclose(B))"
apply(erule eclose_induct_down,simp,erule disjE,rule disjI2,simp add:arg_into_eclose)
apply(subgoal_tac "z ∈ eclose(y)",blast,simp add: arg_into_eclose)
apply(rule disjI2,erule bexE,subgoal_tac "z ∈ eclose(B)",blast,simp add:ecloseD)
done
lemma eclose_singE : "x ∈ eclose({a}) ⟹ x = a ∨ x ∈ eclose(a)"
by(blast dest: ecloseE)
lemma in_eclose_sing : "x ∈ eclose({a}) ⟹ a ∈ eclose(z) ⟹ x ∈ eclose({z})"
apply(drule eclose_singE,erule disjE,simp add: eclose_sing)
apply(rule eclose_sing,erule mem_eclose_trans,assumption)
done
lemma in_dom_in_eclose : "x ∈ domain(z) ⟹ x ∈ eclose(z)"
apply(auto simp add:domain_def)
apply(rule_tac A="{x}" in ecloseD)
apply(subst (asm) Pair_def)
apply(rule_tac A="{{x,x},{x,y}}" in ecloseD,auto simp add:arg_into_eclose)
done
text‹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) == {<x,y> ∈ A*A . x ∈ domain(y)}"
lemma edrel_dest [dest]: "x ∈ edrel(A) ⟹ ∃ a∈ A. ∃ b ∈ A. x =<a,b>"
by(auto simp add:edrel_def)
lemma edrelD : "x ∈ edrel(A) ⟹ ∃ a∈ A. ∃ b ∈ A. x =<a,b> ∧ a ∈ domain(b)"
by(auto simp add:edrel_def)
lemma edrelI [intro!]: "x∈A ⟹ y∈A ⟹ x ∈ domain(y) ⟹ <x,y>∈edrel(A)"
by (simp add:edrel_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 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)"
by (auto simp add: edrel_def)
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))"
apply (rule_tac wf_subset [of "trancl(Memrel(eclose(A)))"])
apply (auto simp add:edrel_sub_memrel wf_trancl wf_Memrel)
done
lemma dom_under_edrel_eclose: "edrel(eclose({x})) -`` {x}= domain(x)"
apply(simp add:edrel_def,rule,rule,drule underD,simp,rule,rule underI)
apply(auto simp add:in_dom_in_eclose eclose_sing arg_into_eclose)
done
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
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∩?ez*?ez"
"a ∈ ?ez" "b ∈ ?ez" "<a,b> ∈ ?ec(x)" "y=<a,b>" by blast
then have "a ∈ domain(b)" using edrelD by blast
with 1 have "y ∈ edrel(eclose({z}))" by blast
}
then show "?rr ⊆ edrel(?ez)" using subsetI by auto
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 1: "a ∈ ?ez" "b ∈ ?ez" "y=<a,b>" "a ∈ domain(b)"
using edrelD by blast
with assms have "z ∈ eclose(x)" using in_dom_in_eclose by simp
with assms 1 have "a ∈ eclose({x})" "b ∈ eclose({x})" using in_eclose_sing by simp_all
with ‹a∈domain(b)› have "<a,b> ∈ edrel(eclose({x}))" by blast
with 1 have "y ∈ ?rr" by simp
}
then show "edrel(eclose({z})) ⊆ ?rr" by blast
qed
lemma tr_edrel_subset :
assumes "z ∈ domain(x)"
shows "tr_down(edrel(eclose({x})),z) ⊆ eclose({z})"
proof -
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 have "y ∈ eclose({z})" using tr_edrel_eclose eclose_sing by simp
}
then show ?thesis by blast
qed
context forcing_data
begin
lemma upairM : "x ∈ M ⟹ y ∈ M ⟹ {x,y} ∈ M"
by (simp del:setclass_iff add:setclass_iff[symmetric])
lemma singletonM : "a ∈ M ⟹ {a} ∈ M"
by (simp del:setclass_iff add:setclass_iff[symmetric])
lemma pairM : "x ∈ M ⟹ y ∈ M ⟹ <x,y> ∈ M"
by (simp del:setclass_iff add:setclass_iff[symmetric])
lemma P_sub_M : "P ⊆ M"
by (simp add: P_in_M trans_M transD)
lemma Rep_simp : "Replace(u,λ y z . z = f(y)) = { f(y) . y ∈ u}"
by(auto)
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 ..
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}))"
from wf_Memrel have
wfr: "∀w . wf(?r(w))" ..
with wfrec [of "?r(y)" y "Hcheck"] have
"check(y)= Hcheck( y, λx∈?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))"
using 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_Memrel : "x ∈ M ⟹ field(Memrel(eclose({x}))) ⊆ M"
apply(rule subset_trans,rule field_rel_subset,rule Ordinal.Memrel_type)
apply(rule eclose_least,rule trans_M,auto)
done
definition
Hv :: "i⇒i⇒i⇒i" where
"Hv(G,x,f) == { f`y .. y∈ domain(x), ∃p∈P. <y,p> ∈ x ∧ p ∈ G }"
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
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)
lemma valcheck : "one ∈ G ⟹ one ∈ P ⟹ val(G,check(y)) = y"
proof (induct rule:eps_induct)
case (1 y)
then show ?case
proof -
from def_check have
Eq1: "check(y) = { ⟨check(w), one⟩ . w ∈ y}" (is "_ = ?C") .
from Eq1 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 -
from dom_under_edrel_eclose have
"domain(?n) ⊆ ?r(?n)-``{?n}"
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
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 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"
from ‹vc∈M[G]› and ‹y ∈ vc› 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
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 pairM 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
end
locale M_extra_assms = forcing_data +
assumes
check_in_M : "⋀x. x ∈ M ⟹ check(x) ∈ M"
and repl_check_pair : "strong_replacement(##M,λp y. y =<check(p),p>)"
begin
definition
G_dot :: "i" where
"G_dot == {<check(p),p> . p∈P}"
lemma G_dot_in_M :
"G_dot ∈ M"
proof -
have 0:"G_dot = { y . p∈P , y = <check(p),p> }"
unfolding G_dot_def by auto
from P_in_M check_in_M pairM P_sub_M have
1: "p∈P ⟹ <check(p),p> ∈ M" for p
by auto
with 1 repl_check_pair P_in_M strong_replacement_closed have
"{ y . p∈P , y = <check(p),p> } ∈ M" by simp
then show ?thesis using 0 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 "q∈P ⟹ <check(q),q> ∈ G_dot" for q
unfolding G_dot_def 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
end
end