Theory Powerset_Axiom

theory Powerset_Axiom 
  imports Separation_Axiom Pairing_Axiom Union_Axiom 
begin

definition 
  perm_pow :: "i" where
  "perm_pow == {<0,3>,<1,4>,<2,5>,<3,1>,<4,0>,<5,6>}"  

lemma perm_pow_ftc : "perm_pow ∈ 6 -||> 7" "domain(perm_pow) = 6"
  unfolding perm_pow_def
  by (blast intro: consI emptyI,auto)
  
lemma perm_pow_tc : "perm_pow ∈ 6 → 7"
  using  FiniteFun_is_fun perm_pow_ftc
  by force

lemma perm_pow_env : 
   "{p,l,o,ss,fs,χ} ⊆ A ⟹ j<6 ⟹
  nth(j,[p,l,o,ss,fs,χ]) = nth(perm_pow`j,[fs,ss,sp,p,l,o,χ])" 
  apply(subgoal_tac "j∈nat")
  apply(rule natE,simp,subst apply_fun,rule perm_pow_tc,simp add:perm_pow_def,simp_all)+
   apply(subst apply_fun,rule perm_pow_tc,simp add:perm_pow_def,simp_all,drule ltD,auto)
  done

  
lemma (in M_trivial) powerset_subset_Pow:
  assumes 
    "powerset(M,x,y)" "⋀z. z∈y ⟹ M(z)"
  shows 
    "y ⊆ Pow(x)"
  using assms unfolding powerset_def
  by (auto)
    
lemma (in M_trivial) powerset_abs: 
  assumes
    "M(x)" "⋀z. z∈y ⟹ M(z)"
  shows
    "powerset(M,x,y) ⟷ y = {a∈Pow(x) . M(a)}"
proof (intro iffI equalityI)
  (* First show the converse implication by double inclusion *)
  assume 
    "powerset(M,x,y)"
  with assms have
    "y ⊆ Pow(x)" 
    using powerset_subset_Pow by simp
  with assms show
    "y ⊆ {a∈Pow(x) . M(a)}"
    by blast
  {
    fix a
    assume 
      "a ⊆ x" "M(a)"
    then have 
      "subset(M,a,x)" by simp
    with ‹M(a)› ‹powerset(M,x,y)› have
      "a ∈ y"
      unfolding powerset_def by simp
  }
  then show 
    "{a∈Pow(x) . M(a)} ⊆ y"
    by auto
next (* we show the direct implication *)
  assume 
    "y = {a ∈ Pow(x) . M(a)}"
  then show
    "powerset(M, x, y)"
    unfolding powerset_def
    by simp
qed
  
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 trans_M  Transset_intf[of _ "<σ,p>"] by simp
  moreover from calculation have
    "a∈M" 
    using trans_M  Transset_intf[of _ _ "<σ,p>"] by simp
  ultimately show
    "σ∈M" "p∈M" 
    using trans_M  Transset_intf[of _ _ "a"] 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,φ,[p,l,o,snd(sq),fst(sq),χ])} ∈ M" 
    (is "?θ ∈ M")
proof -
  have "6∈nat" "7∈nat" by simp_all
  let ?φ' = "ren(φ)`6`7`perm_pow"
  from ‹A∈M› ‹B∈M› have
    "A×B ∈ M" 
    using cartprod_closed by simp
  from  ‹arity(φ) ≤ 6› ‹φ∈ formula› have
    "?φ' ∈ formula" "arity(?φ')≤7" 
    using perm_pow_tc ren_arity ren_tc by simp_all
  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› 
      by (simp_all add: trans_M Transset_intf)    
    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
      "sats(M,?ψ,[sp,p,l,o,χ]@[p]) ⟷ sats(M,?ψ,[sp,p,l,o,χ])" (is "sats(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,φ,[p,l,o,snd(sp),fst(sp),χ])" 
      (is "sats(_,_,?env1) ⟷ sats(_,_,?env2)")
      using sats_iff_sats_ren[of φ 6 7 ?env2 M ?env1 perm_pow] perm_pow_tc perm_pow_env [of _ _ _ _ _ _ "M"]
      by simp
    finally have
      "sats(M,?ψ,[sp,p,l,o,χ,p]) ⟷ 
       sats(M,φ,[p,l,o,snd(sp),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 sixp_sep Collect_abs 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 blast
  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 Transset_intf trans_M by blast
    ultimately have
      "Q = {a∈Pow(domain(τ)×P) . a∈M}"
      using ‹domain(τ)×P ∈ M› powerset_abs[of "domain(τ)×P" Q]     
      by (simp del:setclass_iff add:setclass_iff[symmetric])
    also have
      " ... = ?Q"
      by auto
    finally show
      "?Q ∈ M" 
      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 Transset_intf transM  
    by (simp del:setclass_iff add:setclass_iff[symmetric])
  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 blast
    let
      ?θ="{sp ∈domain(τ)×P . sats(M,forces(Member(0,1)),[P,leq,one,snd(sp),fst(sp),χ])}"
    have
      "arity(forces(Member(0,1))) = 6"
      using arity_forces 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
      (* val(G,?θ) ⊆ c *)
      {
        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 ‹<σ,p>∈?θ› ‹?θ ∈ M› have
          "σ∈M"
          using name_components_in_M[of _ _ ?θ]  by auto
        moreover from 1 have
          "sats(M,forces(Member(0,1)),[P,leq,one,p,σ,χ])" "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_forces
          by auto
        moreover have
          "x∈M[G]" 
          using ‹val(G,σ) =  x› ‹σ∈M› GenExtI by blast
        ultimately have
          "x∈c"
          using ‹c∈M[G]› by simp
      }
      then show 
        "val(G,?θ) ⊆ c"
        by auto
    next
      (* val(G,?θ) ⊇ c *)
      {
        fix x
        assume 
          "x ∈ c"
        with ‹c ∈ Pow(a) ∩ M[G]› have
          "x ∈ a" "c∈M[G]" "x∈M[G]"
          by (auto simp add:Transset_intf Transset_MG)
        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" "sats(M,forces(Member(0,1)),[P,leq,one,p,σ,χ])"
          using generic truth_lemma[of "Member(0,1)" "[σ,χ]" "G"] 
          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› have
          "x∈val(G,?θ)"
          using val_of_elem [of _ _ "?θ"] by auto
      }
      then show
        "c ⊆ val(G,?θ)"
        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 have
    " ... ∈ M[G]"
  proof -
    have
      "arity(subset_fm(0,1)) ≤ 2"
      by (simp add:  not_lt_iff_le leI nat_union_abs1)
    moreover note
      ‹?π∈M› ‹τ∈M› ‹val(G,τ) = a›
    ultimately show ?thesis
      using Collect_sats_in_MG by auto
  qed
  finally show ?thesis .
qed
end
  
sublocale G_generic ⊆ M_trivial"##M[G]"
  using generic Union_MG pairing_in_MG zero_in_MG Transset_intf Transset_MG
  unfolding M_trivial_def by simp 
 
context G_generic begin
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∈M[G] there exists some x∈M[G] with powerset(##M[G],a,x)
  *)
  fix a
  assume 
    "a ∈ M[G]"
  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]› have
    "powerset(##M[G], a, {x∈Pow(a) . x ∈ M[G]})"
    using powerset_abs[of a "{x∈Pow(a) . x ∈ M[G]}"]
    by simp
  ultimately show 
    "∃x∈M[G] . powerset(##M[G], a, x)"
    by auto
qed
end
end