Theory Forces_Definition
section‹The definition of \<^term>‹forces››
theory Forces_Definition
imports
Forcing_Data
begin
text‹This is the core of our development.›
subsection‹The relation \<^term>‹frecrel››
lemma names_belowsD:
assumes "x ∈ names_below(P,z)"
obtains f n1 n2 p where
"x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈P"
using assms unfolding names_below_def by auto
context forcing_data1
begin
lemma ftype_abs:
"⟦x∈M; y∈M ⟧ ⟹ is_ftype(##M,x,y) ⟷ y = ftype(x)"
unfolding ftype_def is_ftype_def by (simp add:absolut)
lemma name1_abs:
"⟦x∈M; y∈M ⟧ ⟹ is_name1(##M,x,y) ⟷ y = name1(x)"
unfolding name1_def is_name1_def
by (rule is_hcomp_abs[OF fst_abs],simp_all add: fst_snd_closed[simplified] absolut)
lemma snd_snd_abs:
"⟦x∈M; y∈M ⟧ ⟹ is_snd_snd(##M,x,y) ⟷ y = snd(snd(x))"
unfolding is_snd_snd_def
by (rule is_hcomp_abs[OF snd_abs],
simp_all add: conjunct2[OF fst_snd_closed,simplified] absolut)
lemma name2_abs:
"⟦x∈M; y∈M ⟧ ⟹ is_name2(##M,x,y) ⟷ y = name2(x)"
unfolding name2_def is_name2_def
by (rule is_hcomp_abs[OF fst_abs snd_snd_abs],simp_all add:absolut conjunct2[OF fst_snd_closed,simplified])
lemma cond_of_abs:
"⟦x∈M; y∈M ⟧ ⟹ is_cond_of(##M,x,y) ⟷ y = cond_of(x)"
unfolding cond_of_def is_cond_of_def
by (rule is_hcomp_abs[OF snd_abs snd_snd_abs];simp_all add:fst_snd_closed[simplified])
lemma tuple_abs:
"⟦z∈M;t1∈M;t2∈M;p∈M;t∈M⟧ ⟹
is_tuple(##M,z,t1,t2,p,t) ⟷ t = ⟨z,t1,t2,p⟩"
unfolding is_tuple_def using pair_in_M_iff by simp
lemmas components_abs = ftype_abs name1_abs name2_abs cond_of_abs
tuple_abs
lemma comp_in_M:
"p ≼ q ⟹ p∈M"
"p ≼ q ⟹ q∈M"
using transitivity[of _ leq] pair_in_M_iff by auto
lemma eq_case_abs [simp]:
assumes "t1∈M" "t2∈M" "p∈M" "f∈M"
shows "is_eq_case(##M,t1,t2,p,ℙ,leq,f) ⟷ eq_case(t1,t2,p,ℙ,leq,f)"
proof -
have "q ≼ p ⟹ q∈M" for q
using comp_in_M by simp
moreover
have "⟨s,y⟩∈t ⟹ s∈domain(t)" if "t∈M" for s y t
using that unfolding domain_def by auto
ultimately
have
"(∀s∈M. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q∈M. q∈ℙ ∧ q ≼ p ⟶
(f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1))) ⟷
(∀s. s ∈ domain(t1) ∨ s ∈ domain(t2) ⟶ (∀q. q∈ℙ ∧ q ≼ p ⟶
(f ` ⟨1, s, t1, q⟩ =1 ⟷ f ` ⟨1, s, t2, q⟩=1)))"
using assms domain_trans[OF trans_M,of t1] domain_trans[OF trans_M,of t2]
by auto
then
show ?thesis
unfolding eq_case_def is_eq_case_def
using assms pair_in_M_iff nat_into_M domain_closed apply_closed zero_in_M Un_closed
by (simp add:components_abs)
qed
lemma mem_case_abs [simp]:
assumes "t1∈M" "t2∈M" "p∈M" "f∈M"
shows "is_mem_case(##M,t1,t2,p,ℙ,leq,f) ⟷ mem_case(t1,t2,p,ℙ,leq,f)"
proof
{
fix v
assume "v∈ℙ" "v ≼ p" "is_mem_case(##M,t1,t2,p,ℙ,leq,f)"
moreover
from this
have "v∈M" "⟨v,p⟩ ∈ M" "(##M)(v)"
using transitivity[OF _ P_in_M,of v] transitivity[OF _ leq_in_M]
by simp_all
moreover
from calculation assms
obtain q r s where
"r ∈ ℙ ∧ q ∈ ℙ ∧ ⟨q, v⟩ ∈ M ∧ ⟨s, r⟩ ∈ M ∧ ⟨q, r⟩ ∈ M ∧ 0 ∈ M ∧
⟨0, t1, s, q⟩ ∈ M ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
unfolding is_mem_case_def by (auto simp add:components_abs)
then
have "∃q s r. r ∈ ℙ ∧ q ∈ ℙ ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
by auto
}
then
show "mem_case(t1, t2, p, ℙ, leq, f)" if "is_mem_case(##M, t1, t2, p, ℙ, leq, f)"
unfolding mem_case_def using that assms by auto
next
{ fix v
assume "v ∈ M" "v ∈ ℙ" "⟨v, p⟩ ∈ M" "v ≼ p" "mem_case(t1, t2, p, ℙ, leq, f)"
moreover
from this
obtain q s r where "r ∈ ℙ ∧ q ∈ ℙ ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
unfolding mem_case_def by auto
moreover
from this ‹t2∈M›
have "r∈M" "q∈M" "s∈M" "r ∈ ℙ ∧ q ∈ ℙ ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
using transitivity domainI[of s r] domain_closed
by auto
moreover
note ‹t1∈M›
ultimately
have "∃q∈M . ∃s∈M. ∃r∈M.
r ∈ ℙ ∧ q ∈ ℙ ∧ ⟨q, v⟩ ∈ M ∧ ⟨s, r⟩ ∈ M ∧ ⟨q, r⟩ ∈ M ∧ 0 ∈ M ∧
⟨0, t1, s, q⟩ ∈ M ∧ q ≼ v ∧ ⟨s, r⟩ ∈ t2 ∧ q ≼ r ∧ f ` ⟨0, t1, s, q⟩ = 1"
using pair_in_M_iff zero_in_M by auto
}
then
show "is_mem_case(##M, t1, t2, p, ℙ, leq, f)" if "mem_case(t1, t2, p, ℙ, leq, f)"
unfolding is_mem_case_def
using assms that zero_in_M pair_in_M_iff apply_closed nat_into_M
by (auto simp add:components_abs)
qed
lemma Hfrc_abs:
"⟦fnnc∈M; f∈M⟧ ⟹
is_Hfrc(##M,ℙ,leq,fnnc,f) ⟷ Hfrc(ℙ,leq,fnnc,f)"
unfolding is_Hfrc_def Hfrc_def using pair_in_M_iff zero_in_M
by (auto simp add:components_abs)
lemma Hfrc_at_abs:
"⟦fnnc∈M; f∈M ; z∈M⟧ ⟹
is_Hfrc_at(##M,ℙ,leq,fnnc,f,z) ⟷ z = bool_of_o(Hfrc(ℙ,leq,fnnc,f)) "
unfolding is_Hfrc_at_def using Hfrc_abs
by auto
lemma components_closed :
"x∈M ⟹ (##M)(ftype(x))"
"x∈M ⟹ (##M)(name1(x))"
"x∈M ⟹ (##M)(name2(x))"
"x∈M ⟹ (##M)(cond_of(x))"
unfolding ftype_def name1_def name2_def cond_of_def using fst_snd_closed by simp_all
lemma ecloseN_closed:
"(##M)(A) ⟹ (##M)(ecloseN(A))"
"(##M)(A) ⟹ (##M)(eclose_n(name1,A))"
"(##M)(A) ⟹ (##M)(eclose_n(name2,A))"
unfolding ecloseN_def eclose_n_def
using components_closed eclose_closed singleton_closed Un_closed by auto
lemma eclose_n_abs :
assumes "x∈M" "ec∈M"
shows "is_eclose_n(##M,is_name1,ec,x) ⟷ ec = eclose_n(name1,x)"
"is_eclose_n(##M,is_name2,ec,x) ⟷ ec = eclose_n(name2,x)"
unfolding is_eclose_n_def eclose_n_def
using assms name1_abs name2_abs eclose_abs singleton_closed components_closed
by auto
lemma ecloseN_abs :
"⟦x∈M;ec∈M⟧ ⟹ is_ecloseN(##M,x,ec) ⟷ ec = ecloseN(x)"
unfolding is_ecloseN_def ecloseN_def
using eclose_n_abs Un_closed union_abs ecloseN_closed
by auto
lemma frecR_abs :
"x∈M ⟹ y∈M ⟹ frecR(x,y) ⟷ is_frecR(##M,x,y)"
unfolding frecR_def is_frecR_def
using zero_in_M domain_closed Un_closed components_closed nat_into_M
by (auto simp add: components_abs)
lemma frecrelP_abs :
"z∈M ⟹ frecrelP(##M,z) ⟷ (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y))"
using pair_in_M_iff frecR_abs unfolding frecrelP_def by auto
lemma frecrel_abs:
assumes "A∈M" "r∈M"
shows "is_frecrel(##M,A,r) ⟷ r = frecrel(A)"
proof -
from ‹A∈M›
have "z∈M" if "z∈A×A" for z
using cartprod_closed transitivity that by simp
then
have "Collect(A×A,frecrelP(##M)) = Collect(A×A,λz. (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y)))"
using Collect_cong[of "A×A" "A×A" "frecrelP(##M)"] assms frecrelP_abs by simp
with assms
show ?thesis
unfolding is_frecrel_def def_frecrel using cartprod_closed
by simp
qed
lemma frecrel_closed:
assumes "x∈M"
shows "frecrel(x)∈M"
proof -
have "Collect(x×x,λz. (∃x y. z = ⟨x,y⟩ ∧ frecR(x,y)))∈M"
using Collect_in_M[of "frecrelP_fm(0)" "[]"] arity_frecrelP_fm sats_frecrelP_fm
frecrelP_abs ‹x∈M› cartprod_closed
by simp
then
show ?thesis
unfolding frecrel_def Rrel_def frecrelP_def by simp
qed
lemma field_frecrel : "field(frecrel(names_below(ℙ,x))) ⊆ names_below(ℙ,x)"
unfolding frecrel_def
using field_Rrel by simp
lemma forcerelD : "uv ∈ forcerel(ℙ,x) ⟹ uv∈ names_below(ℙ,x) × names_below(ℙ,x)"
unfolding forcerel_def
using trancl_type field_frecrel by blast
lemma wf_forcerel :
"wf(forcerel(ℙ,x))"
unfolding forcerel_def using wf_trancl wf_frecrel .
lemma restrict_trancl_forcerel:
assumes "frecR(w,y)"
shows "restrict(f,frecrel(names_below(ℙ,x))-``{y})`w
= restrict(f,forcerel(ℙ,x)-``{y})`w"
unfolding forcerel_def frecrel_def using assms restrict_trancl_Rrel[of frecR]
by simp
lemma names_belowI :
assumes "frecR(⟨ft,n1,n2,p⟩,⟨a,b,c,d⟩)" "p∈ℙ"
shows "⟨ft,n1,n2,p⟩ ∈ names_below(ℙ,⟨a,b,c,d⟩)" (is "?x ∈ names_below(_,?y)")
proof -
from assms
have "ft ∈ 2" "a ∈ 2"
unfolding frecR_def by (auto simp add:components_simp)
from assms
consider (eq) "n1 ∈ domain(b) ∪ domain(c) ∧ (n2 = b ∨ n2 =c)"
| (mem) "n1 = b ∧ n2 ∈ domain(c)"
unfolding frecR_def by (auto simp add:components_simp)
then show ?thesis
proof cases
case eq
then
have "n1 ∈ eclose(b) ∨ n1 ∈ eclose(c)"
using Un_iff in_dom_in_eclose by auto
with eq
have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
using ecloseNI components_in_eclose by auto
with ‹ft∈2› ‹p∈ℙ›
show ?thesis
unfolding names_below_def by auto
next
case mem
then
have "n1 ∈ ecloseN(?y)" "n2 ∈ ecloseN(?y)"
using mem_eclose_trans ecloseNI in_dom_in_eclose components_in_eclose
by auto
with ‹ft∈2› ‹p∈ℙ›
show ?thesis
unfolding names_below_def
by auto
qed
qed
lemma names_below_tr :
assumes "x∈ names_below(ℙ,y)" "y∈ names_below(ℙ,z)"
shows "x∈ names_below(ℙ,z)"
proof -
let ?A="λy . names_below(ℙ,y)"
note assms
moreover from this
obtain fx x1 x2 px where "x = ⟨fx,x1,x2,px⟩" "fx∈2" "x1∈ecloseN(y)" "x2∈ecloseN(y)" "px∈ℙ"
unfolding names_below_def by auto
moreover from calculation
obtain fy y1 y2 py where "y = ⟨fy,y1,y2,py⟩" "fy∈2" "y1∈ecloseN(z)" "y2∈ecloseN(z)" "py∈ℙ"
unfolding names_below_def by auto
moreover from calculation
have "x1∈ecloseN(z)" "x2∈ecloseN(z)"
using ecloseN_mono names_simp by auto
ultimately
have "x∈?A(z)"
unfolding names_below_def by simp
then
show ?thesis using subsetI by simp
qed
lemma arg_into_names_below2 :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ,z))"
shows "x ∈ names_below(ℙ,y)"
proof -
from assms
have "x∈names_below(ℙ,z)" "y∈names_below(ℙ,z)" "frecR(x,y)"
unfolding frecrel_def Rrel_def
by auto
obtain f n1 n2 p where "x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈ℙ"
using ‹x∈names_below(ℙ,z)›
unfolding names_below_def by auto
moreover
obtain fy m1 m2 q where "q∈ℙ" "y = ⟨fy,m1,m2,q⟩"
using ‹y∈names_below(ℙ,z)›
unfolding names_below_def by auto
moreover
note ‹frecR(x,y)›
ultimately
show ?thesis
using names_belowI by simp
qed
lemma arg_into_names_below :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ,z))"
shows "x ∈ names_below(ℙ,x)"
proof -
from assms
have "x∈names_below(ℙ,z)"
unfolding frecrel_def Rrel_def
by auto
from ‹x∈names_below(ℙ,z)›
obtain f n1 n2 p where
"x = ⟨f,n1,n2,p⟩" "f∈2" "n1∈ecloseN(z)" "n2∈ecloseN(z)" "p∈ℙ"
unfolding names_below_def by auto
then
have "n1∈ecloseN(x)" "n2∈ecloseN(x)"
using components_in_eclose by simp_all
with ‹f∈2› ‹p∈ℙ› ‹x = ⟨f,n1,n2,p⟩›
show ?thesis
unfolding names_below_def by simp
qed
lemma forcerel_arg_into_names_below :
assumes "⟨x,y⟩ ∈ forcerel(ℙ,z)"
shows "x ∈ names_below(ℙ,x)"
using assms
unfolding forcerel_def
by(rule trancl_induct;auto simp add: arg_into_names_below)
lemma names_below_mono :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ,z))"
shows "names_below(ℙ,x) ⊆ names_below(ℙ,y)"
proof -
from assms
have "x∈names_below(ℙ,y)"
using arg_into_names_below2 by simp
then
show ?thesis
using names_below_tr subsetI by simp
qed
lemma frecrel_mono :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ,z))"
shows "frecrel(names_below(ℙ,x)) ⊆ frecrel(names_below(ℙ,y))"
unfolding frecrel_def
using Rrel_mono names_below_mono assms by simp
lemma forcerel_mono2 :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ,z))"
shows "forcerel(ℙ,x) ⊆ forcerel(ℙ,y)"
unfolding forcerel_def
using trancl_mono frecrel_mono assms by simp
lemma forcerel_mono_aux :
assumes "⟨x,y⟩ ∈ frecrel(names_below(ℙ, w))^+"
shows "forcerel(ℙ,x) ⊆ forcerel(ℙ,y)"
using assms
by (rule trancl_induct,simp_all add: subset_trans forcerel_mono2)
lemma forcerel_mono :
assumes "⟨x,y⟩ ∈ forcerel(ℙ,z)"
shows "forcerel(ℙ,x) ⊆ forcerel(ℙ,y)"
using forcerel_mono_aux assms unfolding forcerel_def by simp
lemma forcerel_eq_aux: "x ∈ names_below(ℙ, w) ⟹ ⟨x,y⟩ ∈ forcerel(ℙ,z) ⟹
(y ∈ names_below(ℙ, w) ⟶ ⟨x,y⟩ ∈ forcerel(ℙ,w))"
unfolding forcerel_def
proof (rule_tac a=x and b=y and
P="λ y . y ∈ names_below(ℙ, w) ⟶ ⟨x,y⟩ ∈ frecrel(names_below(ℙ,w))^+" in trancl_induct,simp)
let ?A="λ a . names_below(ℙ, a)"
let ?R="λ a . frecrel(?A(a))"
let ?fR="λ a .forcerel(a)"
show "u∈?A(w) ⟶ ⟨x,u⟩∈?R(w)^+" if "x∈?A(w)" "⟨x,y⟩∈?R(z)^+" "⟨x,u⟩∈?R(z)" for u
using that frecrelD frecrelI r_into_trancl
unfolding names_below_def by simp
{
fix u v
assume "x ∈ ?A(w)"
"⟨x, y⟩ ∈ ?R(z)^+"
"⟨x, u⟩ ∈ ?R(z)^+"
"⟨u, v⟩ ∈ ?R(z)"
"u ∈ ?A(w) ⟹ ⟨x, u⟩ ∈ ?R(w)^+"
then
have "v ∈ ?A(w) ⟹ ⟨x, v⟩ ∈ ?R(w)^+"
proof -
assume "v ∈?A(w)"
from ‹⟨u,v⟩∈_›
have "u∈?A(v)"
using arg_into_names_below2 by simp
with ‹v ∈?A(w)›
have "u∈?A(w)"
using names_below_tr by simp
with ‹v∈_› ‹⟨u,v⟩∈_›
have "⟨u,v⟩∈ ?R(w)"
using frecrelD frecrelI r_into_trancl unfolding names_below_def by simp
with ‹u ∈ ?A(w) ⟹ ⟨x, u⟩ ∈ ?R(w)^+› ‹u∈?A(w)›
have "⟨x, u⟩ ∈ ?R(w)^+"
by simp
with ‹⟨u,v⟩∈ ?R(w)›
show "⟨x,v⟩∈ ?R(w)^+" using trancl_trans r_into_trancl
by simp
qed
}
then
show "v ∈ ?A(w) ⟶ ⟨x, v⟩ ∈ ?R(w)^+"
if "x ∈ ?A(w)"
"⟨x, y⟩ ∈ ?R(z)^+"
"⟨x, u⟩ ∈ ?R(z)^+"
"⟨u, v⟩ ∈ ?R(z)"
"u ∈ ?A(w) ⟶ ⟨x, u⟩ ∈ ?R(w)^+" for u v
using that
by simp
qed
lemma forcerel_eq :
assumes "⟨z,x⟩ ∈ forcerel(ℙ,x)"
shows "forcerel(ℙ,z) = forcerel(ℙ,x) ∩ names_below(ℙ,z)×names_below(ℙ,z)"
using assms forcerel_eq_aux forcerelD forcerel_mono[of z x x] subsetI
by auto
lemma forcerel_below_aux :
assumes "⟨z,x⟩ ∈ forcerel(ℙ,x)" "⟨u,z⟩ ∈ forcerel(ℙ,x)"
shows "u ∈ names_below(ℙ,z)"
using assms(2)
unfolding forcerel_def
proof(rule trancl_induct)
show "u ∈ names_below(ℙ,y)" if " ⟨u, y⟩ ∈ frecrel(names_below(ℙ, x))" for y
using that vimage_singleton_iff arg_into_names_below2 by simp
next
show "u ∈ names_below(ℙ,z)"
if "⟨u, y⟩ ∈ frecrel(names_below(ℙ, x))^+"
"⟨y, z⟩ ∈ frecrel(names_below(ℙ, x))"
"u ∈ names_below(ℙ, y)"
for y z
using that arg_into_names_below2[of y z x] names_below_tr by simp
qed
lemma forcerel_below :
assumes "⟨z,x⟩ ∈ forcerel(ℙ,x)"
shows "forcerel(ℙ,x) -`` {z} ⊆ names_below(ℙ,z)"
using vimage_singleton_iff assms forcerel_below_aux by auto
lemma relation_forcerel :
shows "relation(forcerel(ℙ,z))" "trans(forcerel(ℙ,z))"
unfolding forcerel_def using relation_trancl trans_trancl by simp_all
lemma Hfrc_restrict_trancl: "bool_of_o(Hfrc(ℙ, leq, y, restrict(f,frecrel(names_below(ℙ,x))-``{y})))
= bool_of_o(Hfrc(ℙ, leq, y, restrict(f,(frecrel(names_below(ℙ,x))^+)-``{y})))"
unfolding Hfrc_def bool_of_o_def eq_case_def mem_case_def
using restrict_trancl_forcerel frecRI1 frecRI2 frecRI3
unfolding forcerel_def
by simp
lemma frc_at_trancl: "frc_at(ℙ,leq,z) = wfrec(forcerel(ℙ,z),z,λx f. bool_of_o(Hfrc(ℙ,leq,x,f)))"
unfolding frc_at_def forcerel_def using wf_eq_trancl Hfrc_restrict_trancl by simp
lemma forcerelI1 :
assumes "n1 ∈ domain(b) ∨ n1 ∈ domain(c)" "p∈ℙ" "d∈ℙ"
shows "⟨⟨1, n1, b, p⟩, ⟨0,b,c,d⟩⟩∈ forcerel(ℙ,⟨0,b,c,d⟩)"
proof -
let ?x="⟨1, n1, b, p⟩"
let ?y="⟨0,b,c,d⟩"
from assms
have "frecR(?x,?y)"
using frecRI1 by simp
then
have "?x∈names_below(ℙ,?y)" "?y ∈ names_below(ℙ,?y)"
using names_belowI assms components_in_eclose
unfolding names_below_def by auto
with ‹frecR(?x,?y)›
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemma forcerelI2 :
assumes "n1 ∈ domain(b) ∨ n1 ∈ domain(c)" "p∈ℙ" "d∈ℙ"
shows "⟨⟨1, n1, c, p⟩, ⟨0,b,c,d⟩⟩∈ forcerel(ℙ,⟨0,b,c,d⟩)"
proof -
let ?x="⟨1, n1, c, p⟩"
let ?y="⟨0,b,c,d⟩"
note assms
moreover from this
have "frecR(?x,?y)"
using frecRI2 by simp
moreover from calculation
have "?x∈names_below(ℙ,?y)" "?y ∈ names_below(ℙ,?y)"
using names_belowI components_in_eclose
unfolding names_below_def by auto
ultimately
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemma forcerelI3 :
assumes "⟨n2, r⟩ ∈ c" "p∈ℙ" "d∈ℙ" "r ∈ ℙ"
shows "⟨⟨0, b, n2, p⟩,⟨1, b, c, d⟩⟩ ∈ forcerel(ℙ,⟨1,b,c,d⟩)"
proof -
let ?x="⟨0, b, n2, p⟩"
let ?y="⟨1, b, c, d⟩"
note assms
moreover from this
have "frecR(?x,?y)"
using frecRI3 by simp
moreover from calculation
have "?x∈names_below(ℙ,?y)" "?y ∈ names_below(ℙ,?y)"
using names_belowI components_in_eclose
unfolding names_below_def by auto
ultimately
show ?thesis
unfolding forcerel_def frecrel_def
using subsetD[OF r_subset_trancl[OF relation_Rrel]] RrelI
by auto
qed
lemmas forcerelI = forcerelI1[THEN vimage_singleton_iff[THEN iffD2]]
forcerelI2[THEN vimage_singleton_iff[THEN iffD2]]
forcerelI3[THEN vimage_singleton_iff[THEN iffD2]]
lemma aux_def_frc_at:
assumes "z ∈ forcerel(ℙ,x) -`` {x}"
shows "wfrec(forcerel(ℙ,x), z, H) = wfrec(forcerel(ℙ,z), z, H)"
proof -
let ?A="names_below(ℙ,z)"
from assms
have "⟨z,x⟩ ∈ forcerel(ℙ,x)"
using vimage_singleton_iff by simp
moreover from this
have "z ∈ ?A"
using forcerel_arg_into_names_below by simp
moreover from calculation
have "forcerel(ℙ,z) = forcerel(ℙ,x) ∩ (?A×?A)"
"forcerel(ℙ,x) -`` {z} ⊆ ?A"
using forcerel_eq forcerel_below
by auto
moreover from calculation
have "wfrec(forcerel(ℙ,x), z, H) = wfrec[?A](forcerel(ℙ,x), z, H)"
using wfrec_trans_restr[OF relation_forcerel(1) wf_forcerel relation_forcerel(2), of x z ?A]
by simp
ultimately
show ?thesis
using wfrec_restr_eq by simp
qed
subsection‹Recursive expression of \<^term>‹frc_at››
lemma def_frc_at :
assumes "p∈ℙ"
shows
"frc_at(ℙ,leq,⟨ft,n1,n2,p⟩) =
bool_of_o( p ∈ℙ ∧
( ft = 0 ∧ (∀s. s∈domain(n1) ∪ domain(n2) ⟶
(∀q. q∈ℙ ∧ q ≼ p ⟶ (frc_at(ℙ,leq,⟨1,s,n1,q⟩) =1 ⟷ frc_at(ℙ,leq,⟨1,s,n2,q⟩) =1)))
∨ ft = 1 ∧ ( ∀v∈ℙ. v ≼ p ⟶
(∃q. ∃s. ∃r. r∈ℙ ∧ q∈ℙ ∧ q ≼ v ∧ ⟨s,r⟩ ∈ n2 ∧ q ≼ r ∧ frc_at(ℙ,leq,⟨0,n1,s,q⟩) = 1))))"
proof -
let ?r="λy. forcerel(ℙ,y)" and ?Hf="λx f. bool_of_o(Hfrc(ℙ,leq,x,f))"
let ?t="λy. ?r(y) -`` {y}"
let ?arg="⟨ft,n1,n2,p⟩"
from wf_forcerel
have wfr: "∀w . wf(?r(w))" ..
with wfrec [of "?r(?arg)" ?arg ?Hf]
have "frc_at(ℙ,leq,?arg) = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. wfrec(?r(?arg), x, ?Hf))"
using frc_at_trancl by simp
also
have " ... = ?Hf( ?arg, λx∈?r(?arg) -`` {?arg}. frc_at(ℙ,leq,x))"
using aux_def_frc_at frc_at_trancl by simp
finally
show ?thesis
unfolding Hfrc_def mem_case_def eq_case_def
using forcerelI assms
by auto
qed
subsection‹Absoluteness of \<^term>‹frc_at››
lemma forcerel_in_M :
assumes "x∈M"
shows "forcerel(ℙ,x)∈M"
unfolding forcerel_def def_frecrel names_below_def
proof -
let ?Q = "2 × ecloseN(x) × ecloseN(x) × ℙ"
have "?Q × ?Q ∈ M"
using ‹x∈M› nat_into_M ecloseN_closed cartprod_closed by simp
moreover
have "separation(##M,λz. frecrelP(##M,z))"
using separation_in_ctm[of "frecrelP_fm(0)",OF _ _ _ sats_frecrelP_fm]
arity_frecrelP_fm frecrelP_fm_type
by auto
moreover from this
have "separation(##M,λz. ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y))"
using separation_cong[OF frecrelP_abs]
by force
ultimately
show "{z ∈ ?Q × ?Q . ∃x y. z = ⟨x, y⟩ ∧ frecR(x, y)}^+ ∈ M"
using separation_closed frecrelP_abs trancl_closed
by simp
qed
lemma relation2_Hfrc_at_abs:
"relation2(##M,is_Hfrc_at(##M,ℙ,leq),λx f. bool_of_o(Hfrc(ℙ,leq,x,f)))"
unfolding relation2_def using Hfrc_at_abs
by simp
lemma Hfrc_at_closed :
"∀x∈M. ∀g∈M. function(g) ⟶ bool_of_o(Hfrc(ℙ,leq,x,g))∈M"
unfolding bool_of_o_def using zero_in_M nat_into_M[of 1] by simp
lemma wfrec_Hfrc_at :
assumes "X∈M"
shows "wfrec_replacement(##M,is_Hfrc_at(##M,ℙ,leq),forcerel(ℙ,X))"
proof -
have 0:"is_Hfrc_at(##M,ℙ,leq,a,b,c) ⟷
sats(M,Hfrc_at_fm(8,9,2,1,0),[c,b,a,d,e,y,x,z,ℙ,leq,forcerel(ℙ,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› forcerel_in_M
Hfrc_at_iff_sats[of concl:M ℙ leq a b c 8 9 2 1 0]
by simp
have 1:"sats(M,is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0),[y,x,z,ℙ,leq,forcerel(ℙ,X)]) ⟷
is_wfrec(##M, is_Hfrc_at(##M,ℙ,leq),forcerel(ℙ,X), x, y)"
if "x∈M" "y∈M" "z∈M" for x y z
using that ‹X∈M› forcerel_in_M sats_is_wfrec_fm[OF 0]
by simp
let
?f="Exists(And(pair_fm(1,0,2),is_wfrec_fm(Hfrc_at_fm(8,9,2,1,0),5,1,0)))"
have satsf:"sats(M, ?f, [x,z,ℙ,leq,forcerel(ℙ,X)]) ⟷
(∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,ℙ,leq),forcerel(ℙ,X), x, y))"
if "x∈M" "z∈M" for x z
using that 1 ‹X∈M› forcerel_in_M by (simp del:pair_abs)
have artyf:"arity(?f) = 5"
using arity_wfrec_replacement_fm[where p="Hfrc_at_fm(8,9,2,1,0)" and i=10]
arity_Hfrc_at_fm ord_simp_union
by simp
moreover
have "?f∈formula" by simp
ultimately
have "strong_replacement(##M,λx z. sats(M,?f,[x,z,ℙ,leq,forcerel(ℙ,X)]))"
using ZF_ground_replacements(1) 1 artyf ‹X∈M› forcerel_in_M
unfolding replacement_assm_def wfrec_Hfrc_at_fm_def by simp
then
have "strong_replacement(##M,λx z.
∃y∈M. pair(##M,x,y,z) & is_wfrec(##M, is_Hfrc_at(##M,ℙ,leq),forcerel(ℙ,X), x, y))"
using repl_sats[of M ?f "[ℙ,leq,forcerel(ℙ,X)]"] satsf by (simp del:pair_abs)
then
show ?thesis unfolding wfrec_replacement_def by simp
qed
lemma names_below_abs :
"⟦Q∈M;x∈M;nb∈M⟧ ⟹ is_names_below(##M,Q,x,nb) ⟷ nb = names_below(Q,x)"
unfolding is_names_below_def names_below_def
using succ_in_M_iff zero_in_M cartprod_closed ecloseN_abs ecloseN_closed
by auto
lemma names_below_closed:
"⟦Q∈M;x∈M⟧ ⟹ names_below(Q,x) ∈ M"
unfolding names_below_def
using zero_in_M cartprod_closed ecloseN_closed succ_in_M_iff
by simp
lemma "names_below_productE" :
assumes "Q ∈ M" "x ∈ M"
"⋀A1 A2 A3 A4. A1 ∈ M ⟹ A2 ∈ M ⟹ A3 ∈ M ⟹ A4 ∈ M ⟹ R(A1 × A2 × A3 × A4)"
shows "R(names_below(Q,x))"
unfolding names_below_def using assms nat_into_M ecloseN_closed[of x] by auto
lemma forcerel_abs :
"⟦x∈M;z∈M⟧ ⟹ is_forcerel(##M,ℙ,x,z) ⟷ z = forcerel(ℙ,x)"
unfolding is_forcerel_def forcerel_def
using frecrel_abs names_below_abs trancl_abs ecloseN_closed names_below_closed
names_below_productE[of concl:"λp. is_frecrel(##M,p,_) ⟷ _ = frecrel(p)"] frecrel_closed
by simp
lemma frc_at_abs:
assumes "fnnc∈M" "z∈M"
shows "is_frc_at(##M,ℙ,leq,fnnc,z) ⟷ z = frc_at(ℙ,leq,fnnc)"
proof -
from assms
have "(∃r∈M. is_forcerel(##M,ℙ,fnnc, r) ∧ is_wfrec(##M, is_Hfrc_at(##M, ℙ, leq), r, fnnc, z))
⟷ is_wfrec(##M, is_Hfrc_at(##M, ℙ, leq), forcerel(ℙ,fnnc), fnnc, z)"
using forcerel_abs forcerel_in_M by simp
then
show ?thesis
unfolding frc_at_trancl is_frc_at_def
using assms wfrec_Hfrc_at[of fnnc] wf_forcerel relation_forcerel forcerel_in_M
Hfrc_at_closed relation2_Hfrc_at_abs
trans_wfrec_abs[of "forcerel(ℙ,fnnc)" fnnc z "is_Hfrc_at(##M,ℙ,leq)" "λx f. bool_of_o(Hfrc(ℙ,leq,x,f))"]
by (simp flip:setclass_iff)
qed
lemma forces_eq'_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq'(##M,ℙ,leq,p,t1,t2) ⟷ forces_eq'(ℙ,leq,p,t1,t2)"
unfolding is_forces_eq'_def forces_eq'_def
using frc_at_abs nat_into_M pair_in_M_iff by (auto simp add:components_abs)
lemma forces_mem'_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem'(##M,ℙ,leq,p,t1,t2) ⟷ forces_mem'(ℙ,leq,p,t1,t2)"
unfolding is_forces_mem'_def forces_mem'_def
using frc_at_abs nat_into_M pair_in_M_iff by (auto simp add:components_abs)
lemma forces_neq'_abs :
assumes "p∈M" "t1∈M" "t2∈M"
shows "is_forces_neq'(##M,ℙ,leq,p,t1,t2) ⟷ forces_neq'(ℙ,leq,p,t1,t2)"
proof -
have "q∈M" if "q∈ℙ" for q
using that transitivity by simp
with assms
show ?thesis
unfolding is_forces_neq'_def forces_neq'_def
using forces_eq'_abs pair_in_M_iff
by (auto simp add:components_abs,blast)
qed
lemma forces_nmem'_abs :
assumes "p∈M" "t1∈M" "t2∈M"
shows "is_forces_nmem'(##M,ℙ,leq,p,t1,t2) ⟷ forces_nmem'(ℙ,leq,p,t1,t2)"
proof -
have "q∈M" if "q∈ℙ" for q
using that transitivity by simp
with assms
show ?thesis
unfolding is_forces_nmem'_def forces_nmem'_def
using forces_mem'_abs pair_in_M_iff
by (auto simp add:components_abs,blast)
qed
lemma leq_abs:
"⟦ l∈M ; q∈M ; p∈M ⟧ ⟹ is_leq(##M,l,q,p) ⟷ ⟨q,p⟩∈l"
unfolding is_leq_def using pair_in_M_iff by simp
subsection‹Forcing for atomic formulas in context›
definition
forces_eq :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ = _')› [36,1,1] 60) where
"forces_eq ≡ forces_eq'(ℙ,leq)"
definition
forces_mem :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ∈ _')› [36,1,1] 60) where
"forces_mem ≡ forces_mem'(ℙ,leq)"
abbreviation is_forces_eq
where "is_forces_eq ≡ is_forces_eq'(##M,ℙ,leq)"
abbreviation
is_forces_mem :: "[i,i,i] ⇒ o" where
"is_forces_mem ≡ is_forces_mem'(##M,ℙ,leq)"
lemma def_forces_eq: "p∈ℙ ⟹ p forces⇩a (t1 = t2) ⟷
(∀s∈domain(t1) ∪ domain(t2). ∀q. q∈ℙ ∧ q ≼ p ⟶
(q forces⇩a (s ∈ t1) ⟷ q forces⇩a (s ∈ t2)))"
unfolding forces_eq_def forces_mem_def forces_eq'_def forces_mem'_def
using def_frc_at[of p 0 t1 t2 ]
unfolding bool_of_o_def
by auto
lemma def_forces_mem: "p∈ℙ ⟹ p forces⇩a (t1 ∈ t2) ⟷
(∀v∈ℙ. v ≼ p ⟶
(∃q. ∃s. ∃r. r∈ℙ ∧ q∈ℙ ∧ q ≼ v ∧ ⟨s,r⟩ ∈ t2 ∧ q ≼ r ∧ q forces⇩a (t1 = s)))"
unfolding forces_eq'_def forces_mem'_def forces_eq_def forces_mem_def
using def_frc_at[of p 1 t1 t2]
unfolding bool_of_o_def
by auto
lemma forces_eq_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_eq(p,t1,t2) ⟷ p forces⇩a (t1 = t2)"
unfolding forces_eq_def
using forces_eq'_abs by simp
lemma forces_mem_abs :
"⟦p∈M ; t1∈M ; t2∈M⟧ ⟹ is_forces_mem(p,t1,t2) ⟷ p forces⇩a (t1 ∈ t2)"
unfolding forces_mem_def
using forces_mem'_abs
by simp
definition
forces_neq :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ≠ _')› [36,1,1] 60) where
"p forces⇩a (t1 ≠ t2) ≡ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩a (t1 = t2))"
definition
forces_nmem :: "[i,i,i] ⇒ o" (‹_ forces⇩a '(_ ∉ _')› [36,1,1] 60) where
"p forces⇩a (t1 ∉ t2) ≡ ¬ (∃q∈ℙ. q≼p ∧ q forces⇩a (t1 ∈ t2))"
lemma forces_neq :
"p forces⇩a (t1 ≠ t2) ⟷ forces_neq'(ℙ,leq,p,t1,t2)"
unfolding forces_neq_def forces_neq'_def forces_eq_def by simp
lemma forces_nmem :
"p forces⇩a (t1 ∉ t2) ⟷ forces_nmem'(ℙ,leq,p,t1,t2)"
unfolding forces_nmem_def forces_nmem'_def forces_mem_def by simp
abbreviation Forces :: "[i, i, i] ⇒ o" (‹_ ⊩ _ _› [36,36,36] 60) where
"p ⊩ φ env ≡ M, ([p,ℙ,leq,𝟭] @ env) ⊨ forces(φ)"
lemma sats_forces_Member :
assumes "x∈nat" "y∈nat" "env∈list(M)"
"nth(x,env)=xx" "nth(y,env)=yy" "q∈M"
shows "q ⊩ ⋅x ∈ y⋅ env ⟷ q ∈ ℙ ∧ is_forces_mem(q, xx, yy)"
unfolding forces_def
using assms
by simp
lemma sats_forces_Equal :
assumes "a∈nat" "b∈nat" "env∈list(M)" "nth(a,env)=x" "nth(b,env)=y" "q∈M"
shows "q ⊩ ⋅a = b⋅ env ⟷ q ∈ ℙ ∧ is_forces_eq(q, x, y)"
unfolding forces_def
using assms
by simp
lemma sats_forces_Nand :
assumes "φ∈formula" "ψ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ ⋅¬(φ ∧ ψ)⋅ env ⟷
p∈ℙ ∧ ¬(∃q∈M. q∈ℙ ∧ is_leq(##M,leq,q,p) ∧ (q ⊩ φ env) ∧ (q ⊩ ψ env))"
unfolding forces_def
using sats_is_leq_fm_auto assms sats_ren_forces_nand zero_in_M
by simp
lemma sats_forces_Neg :
assumes "φ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ ⋅¬φ⋅ env ⟷
(p∈ℙ ∧ ¬(∃q∈M. q∈ℙ ∧ is_leq(##M,leq,q,p) ∧ (q ⊩ φ env)))"
unfolding Neg_def using assms sats_forces_Nand
by simp
lemma sats_forces_Forall :
assumes "φ∈formula" "env∈list(M)" "p∈M"
shows "p ⊩ (⋅∀φ⋅) env ⟷ p ∈ ℙ ∧ (∀x∈M. p ⊩ φ ([x] @ env))"
unfolding forces_def using assms sats_ren_forces_forall
by simp
end
end