section‹The Axiom of Unions in $M[G]$›
theory Union_Axiom
imports Names
begin
context forcing_data
begin
definition Union_name_body :: "[i,i,i,i] ⇒ o" where
"Union_name_body(P',leq',τ,θp) == (∃ σ[##M].
∃ q[##M]. (q∈ P' ∧ (<σ,q> ∈ τ ∧
(∃ r[##M].r∈P' ∧ (<fst(θp),r> ∈ σ ∧ <snd(θp),r> ∈ leq' ∧ <snd(θp),q> ∈ leq')))))"
definition Union_name_fm :: "i" where
"Union_name_fm ==
Exists(
Exists(And(pair_fm(1,0,2),
Exists (
Exists (And(Member(0,7),
Exists (And(And(pair_fm(2,1,0),Member(0,6)),
Exists (And(Member(0,9),
Exists (And(And(pair_fm(6,1,0),Member(0,4)),
Exists (And(And(pair_fm(6,2,0),Member(0,10)),
Exists (And(pair_fm(7,5,0),Member(0,11)))))))))))))))))"
lemma Union_name_fm_type [TC]:
"Union_name_fm ∈formula"
unfolding Union_name_fm_def by simp
lemma arity_Union_name_fm :
"arity(Union_name_fm) = 4"
unfolding Union_name_fm_def upair_fm_def pair_fm_def
by(auto simp add: nat_simp_union)
lemma sats_Union_name_fm :
"⟦ a ∈ M; b ∈ M ; P' ∈ M ; p ∈ M ; θ ∈ M ; τ ∈ M ; leq' ∈ M ⟧ ⟹
sats(M,Union_name_fm,[<θ,p>,τ,leq',P']@[a,b]) ⟷
Union_name_body(P',leq',τ,<θ,p>)"
unfolding Union_name_fm_def Union_name_body_def pairM
by (subgoal_tac "<θ,p> ∈ M", auto simp add : pairM)
lemma domD :
assumes "τ ∈ M" "σ ∈ domain(τ)"
shows "σ ∈ M"
using assms Transset_M trans_M
by (simp flip: setclass_iff)
definition Union_name :: "i ⇒ i" where
"Union_name(τ) ==
{u ∈ domain(⋃(domain(τ))) × P . Union_name_body(P,leq,τ,u)}"
lemma Union_name_M : assumes "τ ∈ M"
shows "{u ∈ domain(⋃(domain(τ))) × P . Union_name_body(P,leq,τ,u)} ∈ M"
unfolding Union_name_def
proof -
let ?P="λ x . sats(M,Union_name_fm,[x,τ,leq]@[P,τ,leq])"
let ?Q="λ x . Union_name_body(P,leq,τ,x)"
from ‹τ∈M› have "domain(⋃(domain(τ)))∈M" (is "?d ∈ _") using domain_closed Union_closed by simp
then have "?d × P ∈ M" using cartprod_closed P_in_M by simp
have "arity(Union_name_fm)≤6" using arity_Union_name_fm by simp
from assms P_in_M leq_in_M arity_Union_name_fm have
"[τ,leq] ∈ list(M)" "[P,τ,leq] ∈ list(M)" by auto
with assms assms P_in_M leq_in_M ‹arity(Union_name_fm)≤6› have
"separation(##M,?P)"
using separation_ax by simp
with ‹?d × P ∈ M› have A:"{ u ∈ ?d × P . ?P(u) } ∈ M"
using separation_iff by force
{fix x
assume "x ∈ ?d×P"
then have "x = <fst(x),snd(x)>" using Pair_fst_snd_eq by simp
with ‹x∈?d×P› ‹?d∈M› have
"fst(x) ∈ M" "snd(x) ∈ M"
using mtrans fst_type snd_type P_in_M unfolding M_trans_def by auto
then have "?P(<fst(x),snd(x)>) ⟷ ?Q(<fst(x),snd(x)>)"
using P_in_M sats_Union_name_fm P_in_M ‹τ∈M› leq_in_M by simp
with ‹x = <fst(x),snd(x)>› have "?P(x) ⟷ ?Q(x)" by simp
}
then have "?P(x)⟷ ?Q(x)" if "x∈ ?d×P" for x using that by simp
then show ?thesis using Collect_cong A by simp
qed
lemma Union_MG_Eq :
assumes "a ∈ M[G]" and "a = val(G,τ)" and "filter(G)" and "τ ∈ M"
shows "⋃ a = val(G,Union_name(τ))"
proof -
{
fix x
assume "x ∈ ⋃ (val(G,τ))"
then obtain i where "i ∈ val(G,τ)" "x ∈ i" by blast
with ‹τ ∈ M› obtain σ q where
"q ∈ G" "<σ,q> ∈ τ" "val(G,σ) = i" "σ ∈ M"
using elem_of_val_pair domD by blast
with ‹x ∈ i› obtain θ r where
"r ∈ G" "<θ,r> ∈ σ" "val(G,θ) = x" "θ ∈ M"
using elem_of_val_pair domD by blast
with ‹<σ,q>∈τ› have "θ ∈ domain(⋃(domain(τ)))" by auto
with ‹filter(G)› ‹q∈G› ‹r∈G› obtain p where
A: "p ∈ G" "<p,r> ∈ leq" "<p,q> ∈ leq" "p ∈ P" "r ∈ P" "q ∈ P"
using low_bound_filter filterD by blast
then have "p ∈ M" "q∈M" "r∈M"
using mtrans P_in_M unfolding M_trans_def by auto
with A ‹<θ,r> ∈ σ› ‹<σ,q> ∈ τ› ‹θ ∈ M› ‹θ ∈ domain(⋃(domain(τ)))› ‹σ∈M› have
"<θ,p> ∈ Union_name(τ)" unfolding Union_name_def Union_name_body_def
by auto
with ‹p∈P› ‹p∈G› have "val(G,θ) ∈ val(G,Union_name(τ))"
using val_of_elem by simp
with ‹val(G,θ)=x› have "x ∈ val(G,Union_name(τ))" by simp
}
with ‹a=val(G,τ)› have 1: "x ∈ ⋃ a ⟹ x ∈ val(G,Union_name(τ))" for x by simp
{
fix x
assume "x ∈ (val(G,Union_name(τ)))"
then obtain θ p where
"p ∈ G" "<θ,p> ∈ Union_name(τ)" "val(G,θ) = x"
using elem_of_val_pair by blast
with ‹filter(G)› have "p∈P" using filterD by simp
from ‹<θ,p> ∈ Union_name(τ)› obtain σ q r where
"σ ∈ domain(τ)" "<σ,q> ∈ τ " "<θ,r> ∈ σ" "r∈P" "q∈P" "<p,r> ∈ leq" "<p,q> ∈ leq"
unfolding Union_name_def Union_name_body_def by force
with ‹p∈G› ‹filter(G)› have "r ∈ G" "q ∈ G"
using filter_leqD by auto
with ‹<θ,r> ∈ σ› ‹<σ,q>∈τ› ‹q∈P› ‹r∈P› have
"val(G,σ) ∈ val(G,τ)" "val(G,θ) ∈ val(G,σ)"
using val_of_elem by simp+
then have "val(G,θ) ∈ ⋃ val(G,τ)" by blast
with ‹val(G,θ)=x› ‹a=val(G,τ)› have
"x ∈ ⋃ a" by simp
}
with ‹a=val(G,τ)› have "x ∈ val(G,Union_name(τ)) ⟹ x ∈ ⋃ a" for x by blast
then show ?thesis using 1 by blast
qed
lemma union_in_MG : assumes "filter(G)"
shows "Union_ax(##M[G])"
proof -
{ fix a
assume "a ∈ M[G]"
then interpret mgtrans : M_trans "##M[G]"
using transitivity_MG by (unfold_locales; auto)
from ‹a∈_› obtain τ where "τ ∈ M" "a=val(G,τ)" using GenExtD by blast
then have "Union_name(τ) ∈ M" (is "?π ∈ _") using Union_name_M unfolding Union_name_def by simp
then have "val(G,?π) ∈ M[G]" (is "?U ∈ _") using GenExtI by simp
with ‹a∈_› have "(##M[G])(a)" "(##M[G])(?U)" by auto
with ‹τ ∈ M› ‹filter(G)› ‹?U ∈ M[G]› ‹a=val(G,τ)›
have "big_union(##M[G],a,?U)"
using Union_MG_Eq Union_abs by simp
with ‹?U ∈ M[G]› have "∃z[##M[G]]. big_union(##M[G],a,z)" by force
}
then have "Union_ax(##M[G])" unfolding Union_ax_def by force
then show ?thesis by simp
qed
theorem Union_MG : "M_generic(G) ⟹ Union_ax(##M[G])"
by (simp add:M_generic_def union_in_MG)
end
end