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 :
"⟦ env ∈ list(M); P' ∈ M ; p ∈ M ; θ ∈ M ; τ ∈ M ; leq' ∈ M ⟧ ⟹
sats(M,Union_name_fm,[⟨θ,p⟩,τ,leq',P']@env) ⟷
Union_name_body(P',leq',τ,⟨θ,p⟩)"
unfolding Union_name_fm_def Union_name_body_def tuples_in_M
by (subgoal_tac "⟨θ,p⟩ ∈ M", auto simp add : tuples_in_M)
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 "Union_name(τ) ∈ M"
proof -
let ?P="λ x . sats(M,Union_name_fm,[x,τ,leq,P])"
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)≤4" using arity_Union_name_fm by simp
with ‹τ∈M› P_in_M leq_in_M
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
have "?P(x)⟷ ?Q(x)" if "x∈?d×P" for x
proof -
from ‹x∈?d×P›
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 transitivity fst_type snd_type P_in_M 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)⟩›
show "?P(x) ⟷ ?Q(x)" using ‹x∈_› by simp
qed
then show ?thesis using Collect_cong A unfolding Union_name_def by simp
qed
lemma Union_MG_Eq :
assumes "a ∈ M[G]" and "a = val(P,G,τ)" and "filter(G)" and "τ ∈ M"
shows "⋃ a = val(P,G,Union_name(τ))"
proof -
{
fix x
assume "x ∈ ⋃ (val(P,G,τ))"
then obtain i where "i ∈ val(P,G,τ)" "x ∈ i" by blast
with ‹τ ∈ M› obtain σ q where
"q ∈ G" "⟨σ,q⟩ ∈ τ" "val(P,G,σ) = i" "σ ∈ M"
using elem_of_val_pair domain_trans[OF trans_M] by blast
with ‹x ∈ i› obtain θ r where
"r ∈ G" "⟨θ,r⟩ ∈ σ" "val(P,G,θ) = x" "θ ∈ M"
using elem_of_val_pair domain_trans[OF trans_M] 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 P_in_M by (auto dest:transM)
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(P,G,θ) ∈ val(P,G,Union_name(τ))"
using val_of_elem by simp
with ‹val(P,G,θ)=x›
have "x ∈ val(P,G,Union_name(τ))" by simp
}
with ‹a=val(P,G,τ)›
have 1: "x ∈ ⋃ a ⟹ x ∈ val(P,G,Union_name(τ))" for x by simp
{
fix x
assume "x ∈ (val(P,G,Union_name(τ)))"
then obtain θ p where
"p ∈ G" "⟨θ,p⟩ ∈ Union_name(τ)" "val(P,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(P,G,σ) ∈ val(P,G,τ)" "val(P,G,θ) ∈ val(P,G,σ)"
using val_of_elem by simp+
then have "val(P,G,θ) ∈ ⋃ val(P,G,τ)" by blast
with ‹val(P,G,θ)=x› ‹a=val(P,G,τ)› have
"x ∈ ⋃ a" by simp
}
with ‹a=val(P,G,τ)›
have "x ∈ val(P,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(P,G,τ)" using GenExtD by blast
then
have "Union_name(τ) ∈ M" (is "?π ∈ _") using Union_name_M unfolding Union_name_def by simp
then
have "val(P,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(P,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 auto
}
then
show ?thesis unfolding Union_ax_def by simp
qed
theorem Union_MG : "M_generic(G) ⟹ Union_ax(##M[G])"
by (simp add:M_generic_def union_in_MG)
end
end