Theory Union_Axiom

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 tuples_in_M
  by (subgoal_tac "⟨θ,p⟩ ∈ M", auto simp add : tuples_in_M)


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
  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 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)⟩›
    show "?P(x) ⟷ ?Q(x)" using that by simp
  qed
  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 (* forcing_data *)
end