Quelle  Choice_Axiom.thy

section‹The Axiom of Choice in $M[G]$›
theory Choice_Axiom
  imports Powerset_Axiom Pairing_Axiom Union_Axiom Extensionality_Axiom 
          Foundation_Axiom Powerset_Axiom Separation_Axiom 
          Replacement_Axiom Interface Infinity_Axiom
begin

definition 
  induced_surj :: "i==>i==>i==>i" where
  "induced_surj(f,a,e) ≡ f-``(range(f)-a)×{e} ∪ restrict(f,f-``a)"
  
lemma domain_induced_surj: "domain(induced_surj(f,a,e)) = domain(f)"
  unfolding induced_surj_def using domain_restrict domain_of_prod by auto
    
lemma range_restrict_vimage: 
  assumes "function(f)"
  shows "range(restrict(f,f-``a)) ⊆ a"
proof
  from assms 
  have "function(restrict(f,f-``a))" 
    using function_restrictI by simp
  fix y
  assume "y ∈ range(restrict(f,f-``a))"
  then 
  obtain x where "⟨x,y⟩ ∈ restrict(f,f-``a)"  "x ∈ f-``a" "x∈domain(f)"
    using domain_restrict domainI[of _ _ "restrict(f,f-``a)"] by auto
  moreover 
  note ‹function(restrict(f,f-``a))›
  ultimately 
  have "y = restrict(f,f-``a)`x" 
    using function_apply_equality by blast
  also from ‹x ∈ f-``a›
  have "restrict(f,f-``a)`x = f`x" 
    by simp
  finally 
  have "y=f`x" .
  moreover from assms ‹x∈domain(f)›
  have "⟨x,f`x⟩ ∈ f" 
    using function_apply_Pair by auto 
  moreover 
  note assms ‹x ∈ f-``a›
  ultimately 
  show "y∈a"
    using function_image_vimage[of f a] by auto
qed
  
lemma induced_surj_type: 
  assumes
    "function(f)" (* "relation(f)" (* a function can contain nonpairs *) *)
  shows 
    "induced_surj(f,a,e): domain(f) → {e} ∪ a"
    and
    "x ∈ f-``a ==> induced_surj(f,a,e)`x = f`x" 
proof -
  let ?f1="f-``(range(f)-a) × {e}" and ?f2="restrict(f, f-``a)"
  have "domain(?f2) = domain(f) ∩ f-``a"
    using domain_restrict by simp
  moreover from assms 
  have 1: "domain(?f1) = f-``(range(f))-f-``a"
    using domain_of_prod function_vimage_Diff by simp
  ultimately 
  have "domain(?f1) ∩ domain(?f2) = 0"
    by auto
  moreover 
  have "function(?f1)" "relation(?f1)" "range(?f1) ⊆ {e}"
    unfolding function_def relation_def range_def by auto
  moreover from this and assms 
  have "?f1: domain(?f1) → range(?f1)"
    using function_imp_Pi by simp
  moreover from assms 
  have "?f2: domain(?f2) → range(?f2)"
    using function_imp_Pi[of "restrict(f, f -`` a)"] function_restrictI by simp
  moreover from assms 
  have "range(?f2) ⊆ a" 
    using range_restrict_vimage by simp
  ultimately 
  have "induced_surj(f,a,e): domain(?f1) ∪ domain(?f2) → {e} ∪ a"
    unfolding induced_surj_def using fun_is_function fun_disjoint_Un fun_weaken_type by simp
  moreover 
  have "domain(?f1) ∪ domain(?f2) = domain(f)"
    using domain_restrict domain_of_prod by auto 
  ultimately
  show "induced_surj(f,a,e): domain(f) → {e} ∪ a"
    by simp
  assume "x ∈ f-``a"
  then 
  have "?f2`x = f`x"
    using restrict by simp
  moreover from ‹x ∈ f-``a› and 1 
  have "x ∉ domain(?f1)"
    by simp
  ultimately 
  show "induced_surj(f,a,e)`x = f`x" 
    unfolding induced_surj_def using fun_disjoint_apply2[of x ?f1 ?f2] by simp
qed
  
lemma induced_surj_is_surj : 
  assumes 
    "e∈a" "function(f)" "domain(f) = α" "∧y. y ∈ a ==> ∃x∈α. f ` x = y" 
  shows
    "induced_surj(f,a,e) ∈ surj(α,a)"
  unfolding surj_def
proof (intro CollectI ballI)
  from assms 
  show "induced_surj(f,a,e): α → a"
    using induced_surj_type[of f a e] cons_eq cons_absorb by simp
  fix y
  assume "y ∈ a"
  with assms 
  have "∃x∈α. f ` x = y" 
    by simp
  then
  obtain x where "x∈α" "f ` x = y" by auto
  with ‹y∈a› assms
  have "x∈f-``a" 
    using vimage_iff function_apply_Pair[of f x] by auto
  with ‹f ` x = y› assms
  have "induced_surj(f, a, e) ` x = y"
    using induced_surj_type by simp
  with ‹x∈α› show
    "∃x∈α. induced_surj(f, a, e) ` x = y" by auto
qed
  
context G_generic 
begin

definition
  upair_name :: "i ==> i ==> i" where
  "upair_name(τ,ρ) ≡ {⟨τ,one⟩,⟨ρ,one⟩}"

definition
  is_upair_name :: "[i,i,i] ==> o" where
  "is_upair_name(x,y,z) ≡ ∃xo∈M. ∃yo∈M. pair(##M,x,one,xo) ∧ pair(##M,y,one,yo) ∧
                                       upair(##M,xo,yo,z)"

lemma upair_name_abs : 
  assumes "x∈M" "y∈M" "z∈M" 
  shows "is_upair_name(x,y,z) ⟷ z = upair_name(x,y)" 
  unfolding is_upair_name_def upair_name_def using assms one_in_M pair_in_M_iff by simp

lemma upair_name_closed :
  "[ x∈M; y∈M ] ==> upair_name(x,y)∈M" 
  unfolding upair_name_def using upair_in_M_iff pair_in_M_iff one_in_M by simp

definition
  upair_name_fm :: "[i,i,i,i] ==> i" where
  "upair_name_fm(x,y,o,z) ≡ Exists(Exists(And(pair_fm(x#+2,o#+2,1),
                                          And(pair_fm(y#+2,o#+2,0),upair_fm(1,0,z#+2)))))" 

lemma upair_name_fm_type[TC] :
    "[ s∈nat;x∈nat;y∈nat;o∈nat] ==> upair_name_fm(s,x,y,o)∈formula"
  unfolding upair_name_fm_def by simp

lemma sats_upair_name_fm :
  assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)""nth(o,env)=one" 
  shows 
    "sats(M,upair_name_fm(x,y,o,z),env) ⟷ is_upair_name(nth(x,env),nth(y,env),nth(z,env))"
  unfolding upair_name_fm_def is_upair_name_def using assms by simp

definition
  opair_name :: "i ==> i ==> i" where
  "opair_name(τ,ρ) ≡ upair_name(upair_name(τ,τ),upair_name(τ,ρ))"

definition
  is_opair_name :: "[i,i,i] ==> o" where
  "is_opair_name(x,y,z) ≡ ∃upxx∈M. ∃upxy∈M. is_upair_name(x,x,upxx) ∧ is_upair_name(x,y,upxy)
                                          ∧ is_upair_name(upxx,upxy,z)" 

lemma opair_name_abs : 
  assumes "x∈M" "y∈M" "z∈M" 
  shows "is_opair_name(x,y,z) ⟷ z = opair_name(x,y)" 
  unfolding is_opair_name_def opair_name_def using assms upair_name_abs upair_name_closed by simp

lemma opair_name_closed :
  "[ x∈M; y∈M ] ==> opair_name(x,y)∈M" 
  unfolding opair_name_def using upair_name_closed by simp

definition
  opair_name_fm :: "[i,i,i,i] ==> i" where
  "opair_name_fm(x,y,o,z) ≡ Exists(Exists(And(upair_name_fm(x#+2,x#+2,o#+2,1),
                    And(upair_name_fm(x#+2,y#+2,o#+2,0),upair_name_fm(1,0,o#+2,z#+2)))))" 

lemma opair_name_fm_type[TC] :
    "[ s∈nat;x∈nat;y∈nat;o∈nat] ==> opair_name_fm(s,x,y,o)∈formula"
  unfolding opair_name_fm_def by simp

lemma sats_opair_name_fm :
  assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)""nth(o,env)=one" 
  shows 
    "sats(M,opair_name_fm(x,y,o,z),env) ⟷ is_opair_name(nth(x,env),nth(y,env),nth(z,env))"
  unfolding opair_name_fm_def is_opair_name_def using assms sats_upair_name_fm by simp

lemma val_upair_name : "val(G,upair_name(τ,ρ)) = {val(G,τ),val(G,ρ)}"
  unfolding upair_name_def using val_Upair  generic one_in_G one_in_P by simp
    
lemma val_opair_name : "val(G,opair_name(τ,ρ)) = ⟨val(G,τ),val(G,ρ)⟩"
  unfolding opair_name_def Pair_def using val_upair_name  by simp
    
lemma val_RepFun_one: "val(G,{⟨f(x),one⟩ . x∈a}) = {val(G,f(x)) . x∈a}"
proof -
  let ?A = "{f(x) . x ∈ a}"
  let ?Q = "λ⟨x,p⟩ . p = one"
  have "one ∈ P∩G" using generic one_in_G one_in_P by simp
  have "{⟨f(x),one⟩ . x ∈ a} = {t ∈ ?A × P . ?Q(t)}" 
    using one_in_P by force
  then
  have "val(G,{⟨f(x),one⟩ . x ∈ a}) = val(G,{t ∈ ?A × P . ?Q(t)})"
    by simp
  also
  have "... = {val(G,t) .. t ∈ ?A , ∃p∈P∩G . ?Q(⟨t,p⟩)}"
    using val_of_name_alt by simp
  also
  have "... = {val(G,t) . t ∈ ?A }"
    using ‹one∈P∩G› by force
  also
  have "... = {val(G,f(x)) . x ∈ a}"
    by auto
  finally show ?thesis by simp
qed

subsection‹$M[G]$ is a transitive model of ZF›

interpretation mgzf: M_ZF_trans "M[G]"
  using Transset_MG generic pairing_in_MG Union_MG 
    extensionality_in_MG power_in_MG foundation_in_MG  
    strong_replacement_in_MG separation_in_MG infinity_in_MG
  by unfold_locales simp_all

(* y = opair_name(check(\<beta>),s`\<beta>) *)
definition
  is_opname_check :: "[i,i,i] ==> o" where
  "is_opname_check(s,x,y) ≡ ∃chx∈M. ∃sx∈M. is_check(x,chx) ∧ fun_apply(##M,s,x,sx) ∧
                             is_opair_name(chx,sx,y)" 

definition
  opname_check_fm :: "[i,i,i,i] ==> i" where
  "opname_check_fm(s,x,y,o) ≡ Exists(Exists(And(check_fm(2#+x,2#+o,1),
                              And(fun_apply_fm(2#+s,2#+x,0),opair_name_fm(1,0,2#+o,2#+y)))))"

lemma opname_check_fm_type[TC] :
  "[ s∈nat;x∈nat;y∈nat;o∈nat] ==> opname_check_fm(s,x,y,o)∈formula"
  unfolding opname_check_fm_def by simp

lemma sats_opname_check_fm:
  assumes "x∈nat" "y∈nat" "z∈nat" "o∈nat" "env∈list(M)" "nth(o,env)=one" 
          "y<length(env)"
  shows 
    "sats(M,opname_check_fm(x,y,z,o),env) ⟷ is_opname_check(nth(x,env),nth(y,env),nth(z,env))"
  unfolding opname_check_fm_def is_opname_check_def 
  using assms sats_check_fm sats_opair_name_fm one_in_M by simp


lemma opname_check_abs :
  assumes "s∈M" "x∈M" "y∈M" 
  shows "is_opname_check(s,x,y) ⟷ y = opair_name(check(x),s`x)" 
  unfolding is_opname_check_def  
  using assms check_abs check_in_M opair_name_abs apply_abs apply_closed by simp

lemma repl_opname_check :
  assumes
    "A∈M" "f∈M" 
  shows
   "{opair_name(check(x),f`x). x∈A}∈M"
proof -
  have "arity(opname_check_fm(3,0,1,2))= 4" 
    unfolding opname_check_fm_def opair_name_fm_def upair_name_fm_def
          check_fm_def rcheck_fm_def trans_closure_fm_def is_eclose_fm_def mem_eclose_fm_def
         is_Hcheck_fm_def Replace_fm_def PHcheck_fm_def finite_ordinal_fm_def is_iterates_fm_def
             is_wfrec_fm_def is_recfun_fm_def restriction_fm_def pre_image_fm_def eclose_n_fm_def
        is_nat_case_fm_def quasinat_fm_def Memrel_fm_def singleton_fm_def fm_defs iterates_MH_fm_def
    by (simp add:nat_simp_union)
  moreover
  have "x∈A ==> opair_name(check(x), f ` x)∈M" for x
    using assms opair_name_closed apply_closed transitivity check_in_M
    by simp
  ultimately
  show ?thesis using assms opname_check_abs[of f] sats_opname_check_fm
        one_in_M
        Repl_in_M[of "opname_check_fm(3,0,1,2)" "[one,f]" "is_opname_check(f)" 
                    "λx. opair_name(check(x),f`x)"] 
    by simp
qed



theorem choice_in_MG: 
  assumes "choice_ax(##M)"
  shows "choice_ax(##M[G])"
proof -
  {
    fix a
    assume "a∈M[G]"
    then
    obtain τ where "τ∈M" "val(G,τ) = a" 
      using GenExt_def by auto
    with ‹τ∈M›
    have "domain(τ)∈M"
      using domain_closed by simp
    then
    obtain s α where "s∈surj(α,domain(τ))" "Ord(α)" "s∈M" "α∈M"
      using assms choice_ax_abs by auto
    then
    have "α∈M[G]"         
      using M_subset_MG generic one_in_G subsetD by blast
    let ?A="domain(τ)×P"
    let ?g = "{opair_name(check(β),s`β). β∈α}"
    have "?g ∈ M" using ‹s∈M› ‹α∈M› repl_opname_check by simp
    let ?f_dot="{⟨opair_name(check(β),s`β),one⟩. β∈α}"
    have "?f_dot = ?g × {one}" by blast
    from one_in_M have "{one} ∈ M" using singletonM by simp
    define f where
      "f ≡ val(G,?f_dot)" 
    from ‹{one}∈M› ‹?g∈M› ‹?f_dot = ?g×{one}›
    have "?f_dot∈M" 
      using cartprod_closed by simp
    then
    have "f ∈ M[G]"
      unfolding f_def by (blast intro:GenExtI)
    have "f = {val(G,opair_name(check(β),s`β)) . β∈α}"
      unfolding f_def using val_RepFun_one by simp
    also
    have "... = {⟨β,val(G,s`β)⟩ . β∈α}"
      using val_opair_name valcheck generic one_in_G one_in_P by simp
    finally
    have "f = {⟨β,val(G,s`β)⟩ . β∈α}" .
    then
    have 1: "domain(f) = α" "function(f)"
      unfolding function_def by auto
    have 2: "y ∈ a ==> ∃x∈α. f ` x = y" for y
    proof -
      fix y
      assume
        "y ∈ a"
      with ‹val(G,τ) = a›
      obtain σ where  "σ∈domain(τ)" "val(G,σ) = y"
        using elem_of_val[of y _ τ] by blast
      with ‹s∈surj(α,domain(τ))›
      obtain β where "β∈α" "s`β = σ" 
        unfolding surj_def by auto
      with ‹val(G,σ) = y›
      have "val(G,s`β) = y" 
        by simp
      with ‹f = {⟨β,val(G,s`β)⟩ . β∈α}› ‹β∈α›
      have "⟨β,y⟩∈f" 
        by auto
      with ‹function(f)›
      have "f`β = y"
        using function_apply_equality by simp
      with ‹β∈α› show
        "∃β∈α. f ` β = y" 
        by auto
    qed
    then
    have "∃α∈(M[G]). ∃f'∈(M[G]). Ord(α) ∧ f' ∈ surj(α,a)"
    proof (cases "a=0")
      case True
      then
      have "0∈surj(0,a)" 
        unfolding surj_def by simp
      then
      show ?thesis using zero_in_MG by auto
    next
      case False
      with ‹a∈M[G]›
      obtain e where "e∈a" "e∈M[G]" 
        using transitivity_MG by blast
      with 1 and 2
      have "induced_surj(f,a,e) ∈ surj(α,a)"
        using induced_surj_is_surj by simp
      moreover from ‹f∈M[G]› ‹a∈M[G]› ‹e∈M[G]›
      have "induced_surj(f,a,e) ∈ M[G]"
        unfolding induced_surj_def 
        by (simp flip: setclass_iff)
      moreover note
        ‹α∈M[G]› ‹Ord(α)›
      ultimately show ?thesis by auto
    qed
  }
  then
  show ?thesis using mgzf.choice_ax_abs by simp
qed
  
end (* G_generic_extra_repl *)
  
end