Quelle  Powerset_Axiom.thy

section‹The Powerset Axiom in $M[G]$›
theory Powerset_Axiom
  imports Renaming_Auto Separation_Axiom Pairing_Axiom Union_Axiom
begin

simple_rename "perm_pow" src "[ss,p,l,o,fs,χ]" tgt "[fs,ss,sp,p,l,o,χ]"

lemma Collect_inter_Transset:
  assumes
    "Transset(M)" "b ∈ M"
  shows
    "{x∈b . P(x)} = {x∈b . P(x)} ∩ M"
  using assms unfolding Transset_def
  by (auto)

context G_generic  begin

lemma name_components_in_M:
  assumes "<σ,p>∈θ" "θ ∈ M"
  shows   "σ∈M" "p∈M"
proof -
  from assms obtain a where
    "σ ∈ a" "p ∈ a" "a∈<σ,p>"
    unfolding Pair_def by auto
  moreover from assms
  have "<σ,p>∈M"
    using transitivity by simp
  moreover from calculation
  have "a∈M"
    using transitivity by simp
  ultimately
  show "σ∈M" "p∈M"
    using transitivity by simp_all
qed

lemma sats_fst_snd_in_M:
  assumes
    "A∈M" "B∈M" "φ ∈ formula" "p∈M" "l∈M" "o∈M" "χ∈M"
    "arity(φ) ≤ 6"
  shows
    "{sq ∈A×B . sats(M,φ,[snd(sq),p,l,o,fst(sq),χ])} ∈ M"
    (is "?θ ∈ M")
proof -
  have "6∈nat" "7∈nat" by simp_all
  let ?φ' = "ren(φ)`6`7`perm_pow_fn"
  from ‹A∈M› ‹B∈M› have
    "A×B ∈ M"
    using cartprod_closed by simp
  from ‹arity(φ) ≤ 6› ‹φ∈ formula› ‹6∈_› ‹7∈_›
  have "?φ' ∈ formula" "arity(?φ')≤7"
    unfolding perm_pow_fn_def
    using  perm_pow_thm  arity_ren ren_tc Nil_type
    by auto
  with ‹?φ' ∈ formula›
  have 1: "arity(Exists(Exists(And(pair_fm(0,1,2),?φ'))))≤5"     (is "arity(?ψ)≤5")
    unfolding pair_fm_def upair_fm_def
    using nat_simp_union pred_le arity_type by auto
  {
    fix sp
    note ‹A×B ∈ M›
    moreover
    assume "sp ∈ A×B"
    moreover from calculation
    have "fst(sp) ∈ A" "snd(sp) ∈ B"
      using fst_type snd_type by simp_all
    ultimately
    have "sp ∈ M" "fst(sp) ∈ M" "snd(sp) ∈ M"
      using  ‹A∈M› ‹B∈M› transitivity
      by simp_all
    note inM = ‹A∈M› ‹B∈M› ‹p∈M› ‹l∈M› ‹o∈M› ‹χ∈M›
      ‹sp∈M› ‹fst(sp)∈M› ‹snd(sp)∈M›
    with 1 ‹sp ∈ M› ‹?φ' ∈ formula›
    have "M, [sp,p,l,o,χ]@[p] ⊨ ?ψ ⟷ M,[sp,p,l,o,χ] ⊨ ?ψ" (is "M,?env0@ _⊨_ ⟷ _")
      using arity_sats_iff[of ?ψ "[p]" M ?env0] by auto
    also from inM ‹sp ∈ A×B›
    have "... ⟷ sats(M,?φ',[fst(sp),snd(sp),sp,p,l,o,χ])"
      by auto
    also from inM ‹φ ∈ formula› ‹arity(φ) ≤ 6›
    have "... ⟷ sats(M,φ,[snd(sp),p,l,o,fst(sp),χ])"
      (is "sats(_,_,?env1) ⟷ sats(_,_,?env2)")
      using sats_iff_sats_ren[of φ 6 7 ?env2 M ?env1 perm_pow_fn] perm_pow_thm
      unfolding perm_pow_fn_def by simp
    finally
    have "sats(M,?ψ,[sp,p,l,o,χ,p]) ⟷ sats(M,φ,[snd(sp),p,l,o,fst(sp),χ])"
      by simp
  }
  then have
    "?θ = {sp∈A×B . sats(M,?ψ,[sp,p,l,o,χ,p])}"
    by auto
  also from assms ‹A×B∈M› have
    " ... ∈ M"
  proof -
    from 1
    have "arity(?ψ) ≤ 6"
      using leI by simp
    moreover from ‹?φ' ∈ formula›
    have "?ψ ∈ formula"
      by simp
    moreover note assms ‹A×B∈M›
    ultimately 
    show "{x ∈ A×B . sats(M, ?ψ, [x, p, l, o, χ, p])} ∈ M"
      using separation_ax separation_iff
      by simp
  qed
  finally show ?thesis .
qed

lemma Pow_inter_MG:
  assumes
    "a∈M[G]"
  shows
    "Pow(a) ∩ M[G] ∈ M[G]"
proof -
  from assms obtain τ where
    "τ ∈ M" "val(G, τ) = a"
    using GenExtD by auto
  let ?Q="Pow(domain(τ)×P) ∩ M"
  from ‹τ∈M›
  have "domain(τ)×P ∈ M" "domain(τ) ∈ M"
    using domain_closed cartprod_closed P_in_M
    by simp_all
  then 
  have "?Q ∈ M"
  proof -
    from power_ax ‹domain(τ)×P ∈ M› obtain Q where
      "powerset(##M,domain(τ)×P,Q)" "Q ∈ M"
      unfolding power_ax_def by auto
    moreover from calculation 
    have "z∈Q ==> z∈M" for z
      using transitivity by blast
    ultimately
    have "Q = {a∈Pow(domain(τ)×P) . a∈M}"
      using ‹domain(τ)×P ∈ M› powerset_abs[of "domain(τ)×P" Q]
      by (simp flip: setclass_iff)
    also 
    have " ... = ?Q"
      by auto
    finally 
    show ?thesis using ‹Q∈M› by simp
  qed
  let
    ?π="?Q×{one}"
  let
    ?b="val(G,?π)"
  from ‹?Q∈M›
  have "?π∈M"
    using one_in_P P_in_M transitivity
    by (simp flip: setclass_iff)
  from ‹?π∈M›
  have "?b ∈ M[G]"
    using GenExtI by simp
  have "Pow(a) ∩ M[G] ⊆ ?b"
  proof
    fix c
    assume "c ∈ Pow(a) ∩ M[G]"
    then obtain χ where
      "c∈M[G]" "χ ∈ M" "val(G,χ) = c"
      using GenExtD by auto
    let ?θ="{sp ∈domain(τ)×P . snd(sp) ⊨!!! (Member(0,1)) [fst(sp),χ] }"
    have "arity(forces(Member(0,1))) = 6"
      using arity_forces_at by auto
    with ‹domain(τ) ∈ M› ‹χ ∈ M›
    have "?θ ∈ M"
      using P_in_M one_in_M leq_in_M sats_fst_snd_in_M
      by simp
    then 
    have "?θ ∈ ?Q"
      by auto
    then 
    have "val(G,?θ) ∈ ?b"
      using one_in_G one_in_P generic val_of_elem [of ?θ one ?π G]
      by auto
    have "val(G,?θ) = c"
    proof(intro equalityI subsetI)
      fix x
      assume "x ∈ val(G,?θ)"
      then obtain σ p where
        1: "<σ,p>∈?θ" "p∈G" "val(G,σ) = x"
        using elem_of_val_pair
        by blast
      moreover from ‹<\<sigma>,p>∈?θ› ‹?θ ∈ M›
      have "σ∈M"
        using name_components_in_M[of _ _ ?θ] by auto
      moreover from 1 
      have "(p ⊨!!! (Member(0,1)) [σ,χ])" "p∈P"
        by simp_all
      moreover 
      note ‹val(G,χ) = c›
      ultimately 
      have "sats(M[G],Member(0,1),[x,c])"
        using ‹χ ∈ M› generic definition_of_forcing nat_simp_union
        by auto
      moreover 
      have "x∈M[G]"
        using ‹val(G,σ) = x› ‹σ∈M›  ‹χ∈M› GenExtI by blast
      ultimately 
      show "x∈c"
        using ‹c∈M[G]› by simp
    next
      fix x
      assume "x ∈ c"
      with ‹c ∈ Pow(a) ∩ M[G]›
      have "x ∈ a" "c∈M[G]" "x∈M[G]"
        using transitivity_MG
        by auto
      with ‹val(G, τ) = a›
      obtain σ where
        "σ∈domain(τ)" "val(G,σ) = x"
        using elem_of_val
        by blast
      moreover note ‹x∈c› ‹val(G,χ) = c›
      moreover from calculation 
      have "val(G,σ) ∈ val(G,χ)"
        by simp
      moreover note ‹c∈M[G]› ‹x∈M[G]›
      moreover from calculation 
      have "sats(M[G],Member(0,1),[x,c])"
        by simp
      moreover 
      have "Member(0,1)∈formula" by simp
      moreover 
      have "σ∈M"
      proof -
        from ‹σ∈domain(τ)›
        obtain p where "<σ,p> ∈ τ"
          by auto
        with ‹τ∈M›
        show ?thesis
          using name_components_in_M by blast
      qed
      moreover note ‹χ ∈ M›
      ultimately 
      obtain p where "p∈G" "(p ⊨!!! Member(0,1) [σ,χ])"
        using generic truth_lemma[of "Member(0,1)" "G" "[σ,χ]" ] nat_simp_union
        by auto
      moreover from ‹p∈G›
      have "p∈P"
        using generic unfolding M_generic_def filter_def by blast
      ultimately
      have "<σ,p>∈?θ"
        using ‹σ∈domain(τ)› by simp
      with ‹val(G,σ) = x› ‹p∈G›
      show "x∈val(G,?θ)"
        using val_of_elem [of _ _ "?θ"] by auto
    qed
    with ‹val(G,?θ) ∈ ?b›
    show "c∈?b" by simp
  qed
  then 
  have "Pow(a) ∩ M[G] = {x∈?b . x⊆a & x∈M[G]}"
    by auto
  also from ‹a∈M[G]›
  have " ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a]) & x∈M[G]}"
    using Transset_MG by force
  also 
  have " ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a])} ∩ M[G]"
    by auto
  also from ‹?b∈M[G]›
  have " ... = {x∈?b . sats(M[G],subset_fm(0,1),[x,a])}"
    using Collect_inter_Transset Transset_MG
    by simp
  also from ‹?b∈M[G]› ‹a∈M[G]›
  have " ... ∈ M[G]"
    using Collect_sats_in_MG GenExtI nat_simp_union by simp
  finally show ?thesis .
qed
end (* context: G_generic *)


context G_generic begin

interpretation mgtriv: M_trivial "##M[G]"
  using generic Union_MG pairing_in_MG zero_in_MG transitivity_MG
  unfolding M_trivial_def M_trans_def M_trivial_axioms_def by (simp; blast)


theorem power_in_MG : "power_ax(##(M[G]))"
  unfolding power_ax_def
proof (intro rallI, simp only:setclass_iff rex_setclass_is_bex)
  (* After simplification, we have to show that for every
     a\<in>M[G] there exists some x\<in>M[G] with powerset(##M[G],a,x)
  *)
  fix a
  assume "a ∈ M[G]"
  then
  have "(##M[G])(a)" by simp
  have "{x∈Pow(a) . x ∈ M[G]} = Pow(a) ∩ M[G]"
    by auto
  also from ‹a∈M[G]›
  have " ... ∈ M[G]"
    using Pow_inter_MG by simp
  finally 
  have "{x∈Pow(a) . x ∈ M[G]} ∈ M[G]" .
  moreover from ‹a∈M[G]› ‹{x∈Pow(a) . x ∈ M[G]} ∈ _›
  have "powerset(##M[G], a, {x∈Pow(a) . x ∈ M[G]})"
    using mgtriv.powerset_abs[OF ‹(##M[G])(a)›]
    by simp
  ultimately 
  show "∃x∈M[G] . powerset(##M[G], a, x)"
    by auto
qed
end (* context: G_generic *)
end