Quelle  Forcing_Data.thy

section‹Transitive set models of ZF›
text‹This theory defines the locale term‹M_ZF_trans› for
  models of ZF, and the associated term‹forcing_data›
 that adds a forcing notion›
theory Forcing_Data
  imports  
    Forcing_Notions 
    Interface

begin

lemma Transset_M :
  "Transset(M) ==> y∈x ==> x ∈ M ==> y ∈ M"
  by (simp add: Transset_def,auto)  


locale M_ZF = 
  fixes M 
  assumes 
    upair_ax:         "upair_ax(##M)"
    and Union_ax:         "Union_ax(##M)"
    and power_ax:         "power_ax(##M)"
    and extensionality:   "extensionality(##M)"
    and foundation_ax:    "foundation_ax(##M)"
    and infinity_ax:      "infinity_ax(##M)"
    and separation_ax:    "φ∈formula ==> env∈list(M) ==> arity(φ) ≤ 1 #+ length(env) ==>
                    separation(##M,λx. sats(M,φ,[x] @ env))" 
    and replacement_ax:   "φ∈formula ==> env∈list(M) ==> arity(φ) ≤ 2 #+ length(env) ==>
                    strong_replacement(##M,λx y. sats(M,φ,[x,y] @ env))" 

locale M_ctm = M_ZF +
  fixes enum
  assumes M_countable:      "enum∈bij(nat,M)"
    and trans_M:          "Transset(M)"

begin
interpretation intf: M_ZF_trans "M"
  using M_ZF_trans.intro
    trans_M upair_ax Union_ax power_ax extensionality
    foundation_ax infinity_ax separation_ax[simplified] 
    replacement_ax[simplified]
  by simp


lemmas transitivity = Transset_intf[OF trans_M]

lemma zero_in_M:  "0 ∈ M" 
  by (rule intf.zero_in_M)

lemma tuples_in_M: "A∈M ==> B∈M ==> ⟨A,B⟩∈M" 
  by (simp flip:setclass_iff)

lemma nat_in_M : "nat ∈ M"
  by (rule intf.nat_in_M)

lemma n_in_M : "n∈nat ==> n∈M"
  using nat_in_M transitivity by simp

lemma mtriv: "M_trivial(##M)" 
  by (rule intf.mtriv)

lemma mtrans: "M_trans(##M)"
  by (rule intf.mtrans)

lemma mbasic: "M_basic(##M)"
  by (rule intf.mbasic)

lemma mtrancl: "M_trancl(##M)"
  by (rule intf.mtrancl)

lemma mdatatypes: "M_datatypes(##M)"
  by (rule intf.mdatatypes)

lemma meclose: "M_eclose(##M)"
  by (rule intf.meclose)

lemma meclose_pow: "M_eclose_pow(##M)"
  by (rule intf.meclose_pow)



end (* M_ctm *)

(* M_ctm interface *)
sublocale M_ctm ⊆ M_trivial "##M"
  by  (rule mtriv)

sublocale M_ctm ⊆ M_trans "##M"
  by  (rule mtrans)

sublocale M_ctm ⊆ M_basic "##M"
  by  (rule mbasic)

sublocale M_ctm ⊆ M_trancl "##M"
  by  (rule mtrancl)

sublocale M_ctm ⊆ M_datatypes "##M"
  by  (rule mdatatypes)

sublocale M_ctm ⊆ M_eclose "##M"
  by  (rule meclose)

sublocale M_ctm ⊆ M_eclose_pow "##M"
  by  (rule meclose_pow)

(* end interface *)

context M_ctm
begin

subsection‹term‹Collects› in $M$›
lemma Collect_in_M_0p :
  assumes
    Qfm : "Q_fm ∈ formula" and
    Qarty : "arity(Q_fm) = 1" and
    Qsats : "∧x. x∈M ==> sats(M,Q_fm,[x]) ⟷ is_Q(##M,x)" and
    Qabs  : "∧x. x∈M ==> is_Q(##M,x) ⟷ Q(x)" and
    "A∈M"
  shows
    "Collect(A,Q)∈M" 
proof -
  have "z∈A ==> z∈M" for z
    using ‹A∈M› transitivity[of z A] by simp
  then
  have 1:"Collect(A,is_Q(##M)) = Collect(A,Q)" 
    using Qabs Collect_cong[of "A" "A" "is_Q(##M)" "Q"] by simp
  have "separation(##M,is_Q(##M))"
    using separation_ax Qsats Qarty Qfm
      separation_cong[of "##M" "λy. sats(M,Q_fm,[y])" "is_Q(##M)"]
    by simp
  then 
  have "Collect(A,is_Q(##M))∈M"
    using separation_closed ‹A∈M› by simp 
  then
  show ?thesis using 1 by simp
qed

lemma Collect_in_M_2p :
  assumes
    Qfm : "Q_fm ∈ formula" and
    Qarty : "arity(Q_fm) = 3" and
    params_M : "y∈M" "z∈M" and
    Qsats : "∧x. x∈M ==> sats(M,Q_fm,[x,y,z]) ⟷ is_Q(##M,x,y,z)" and
    Qabs  : "∧x. x∈M ==> is_Q(##M,x,y,z) ⟷ Q(x,y,z)" and
    "A∈M"
  shows
    "Collect(A,λx. Q(x,y,z))∈M" 
proof -
  have "z∈A ==> z∈M" for z
    using ‹A∈M› transitivity[of z A] by simp
  then
  have 1:"Collect(A,λx. is_Q(##M,x,y,z)) = Collect(A,λx. Q(x,y,z))" 
    using Qabs Collect_cong[of "A" "A" "λx. is_Q(##M,x,y,z)" "λx. Q(x,y,z)"] by simp
  have "separation(##M,λx. is_Q(##M,x,y,z))"
    using separation_ax Qsats Qarty Qfm params_M
      separation_cong[of "##M" "λx. sats(M,Q_fm,[x,y,z])" "λx. is_Q(##M,x,y,z)"]
    by simp
  then 
  have "Collect(A,λx. is_Q(##M,x,y,z))∈M"
    using separation_closed ‹A∈M› by simp 
  then
  show ?thesis using 1 by simp
qed

lemma Collect_in_M_4p :
  assumes
    Qfm : "Q_fm ∈ formula" and
    Qarty : "arity(Q_fm) = 5" and
    params_M : "a1∈M" "a2∈M" "a3∈M" "a4∈M" and
    Qsats : "∧x. x∈M ==> sats(M,Q_fm,[x,a1,a2,a3,a4]) ⟷ is_Q(##M,x,a1,a2,a3,a4)" and
    Qabs  : "∧x. x∈M ==> is_Q(##M,x,a1,a2,a3,a4) ⟷ Q(x,a1,a2,a3,a4)" and
    "A∈M"
  shows
    "Collect(A,λx. Q(x,a1,a2,a3,a4))∈M" 
proof -
  have "z∈A ==> z∈M" for z
    using ‹A∈M› transitivity[of z A] by simp
  then
  have 1:"Collect(A,λx. is_Q(##M,x,a1,a2,a3,a4)) = Collect(A,λx. Q(x,a1,a2,a3,a4))" 
    using Qabs Collect_cong[of "A" "A" "λx. is_Q(##M,x,a1,a2,a3,a4)" "λx. Q(x,a1,a2,a3,a4)"] 
    by simp
  have "separation(##M,λx. is_Q(##M,x,a1,a2,a3,a4))"
    using separation_ax Qsats Qarty Qfm params_M
      separation_cong[of "##M" "λx. sats(M,Q_fm,[x,a1,a2,a3,a4])" 
        "λx. is_Q(##M,x,a1,a2,a3,a4)"]
    by simp
  then 
  have "Collect(A,λx. is_Q(##M,x,a1,a2,a3,a4))∈M"
    using separation_closed ‹A∈M› by simp 
  then
  show ?thesis using 1 by simp
qed

lemma Repl_in_M :
  assumes
    f_fm:  "f_fm ∈ formula" and
    f_ar:  "arity(f_fm)≤ 2 #+ length(env)" and
    fsats: "∧x y. x∈M ==> y∈M ==> sats(M,f_fm,[x,y]@env) ⟷ is_f(x,y)" and
    fabs:  "∧x y. x∈M ==> y∈M ==> is_f(x,y) ⟷ y = f(x)" and
    fclosed: "∧x. x∈A ==> f(x) ∈ M"  and
    "A∈M" "env∈list(M)" 
  shows "{f(x). x∈A}∈M"
proof -
  have "strong_replacement(##M, λx y. sats(M,f_fm,[x,y]@env))"
    using replacement_ax f_fm f_ar ‹env∈list(M)› by simp
  then
  have "strong_replacement(##M, λx y. y = f(x))"
    using fsats fabs 
      strong_replacement_cong[of "##M" "λx y. sats(M,f_fm,[x,y]@env)" "λx y. y = f(x)"]
    by simp
  then
  have "{ y . x∈A , y = f(x) } ∈ M" 
    using ‹A∈M› fclosed strong_replacement_closed by simp
  moreover
  have "{f(x). x∈A} = { y . x∈A , y = f(x) }"
    by auto
  ultimately show ?thesis by simp
qed

end (* M_ctm *)      

subsection‹A forcing locale and generic filters›
locale forcing_data = forcing_notion + M_ctm +
  assumes P_in_M:           "P ∈ M"
    and leq_in_M:         "leq ∈ M"

begin

lemma transD : "Transset(M) ==> y ∈ M ==> y ⊆ M" 
  by (unfold Transset_def, blast) 

(* P \<subseteq> M *)
lemmas P_sub_M = transD[OF trans_M P_in_M]

definition
  M_generic :: "i==>o" where
  "M_generic(G) ≡ filter(G) ∧ (∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"

lemma M_genericD [dest]: "M_generic(G) ==> x∈G ==> x∈P"
  unfolding M_generic_def by (blast dest:filterD)

lemma M_generic_leqD [dest]: "M_generic(G) ==> p∈G ==> q∈P ==> p⪯q ==> q∈G"
  unfolding M_generic_def by (blast dest:filter_leqD)

lemma M_generic_compatD [dest]: "M_generic(G) ==> p∈G ==> r∈G ==> ∃q∈G. q⪯p ∧ q⪯r"
  unfolding M_generic_def by (blast dest:low_bound_filter)

lemma M_generic_denseD [dest]: "M_generic(G) ==> dense(D) ==> D⊆P ==> D∈M ==> ∃q∈G. q∈D"
  unfolding M_generic_def by blast

lemma G_nonempty: "M_generic(G) ==> G≠0"
proof -
  have "P⊆P" ..
  assume
    "M_generic(G)"
  with P_in_M P_dense ‹P⊆P› show
    "G ≠ 0"
    unfolding M_generic_def by auto
qed

lemma one_in_G : 
  assumes "M_generic(G)"
  shows  "one ∈ G" 
proof -
  from assms have "G⊆P" 
    unfolding M_generic_def and filter_def by simp
  from ‹M_generic(G)› have "increasing(G)" 
    unfolding M_generic_def and filter_def by simp
  with ‹G⊆P› and ‹M_generic(G)›
  show ?thesis 
    using G_nonempty and one_in_P and one_max 
    unfolding increasing_def by blast
qed

lemma G_subset_M: "M_generic(G) ==> G ⊆ M"
  using transitivity[OF _ P_in_M] by auto

declare iff_trans [trans]

lemma generic_filter_existence: 
  "p∈P ==> ∃G. p∈G ∧ M_generic(G)"
proof -
  assume "p∈P"
  let ?D="λn∈nat. (if (enum`n⊆P ∧ dense(enum`n)) then enum`n else P)"
  have "∀n∈nat. ?D`n ∈ Pow(P)"
    by auto
  then 
  have "?D:nat→Pow(P)"
    using lam_type by auto
  have Eq4: "∀n∈nat. dense(?D`n)"
  proof(intro ballI)
    fix n
    assume "n∈nat"
    then
    have "dense(?D`n) ⟷ dense(if enum`n ⊆ P ∧ dense(enum`n) then enum`n else P)"
      by simp
    also 
    have "... ⟷ (¬(enum`n ⊆ P ∧ dense(enum`n)) ⟶ dense(P)) "
      using split_if by simp
    finally
    show "dense(?D`n)"
      using P_dense ‹n∈nat› by auto
  qed
  from ‹?D∈_› and Eq4 
  interpret cg: countable_generic P leq one ?D 
    by (unfold_locales, auto)
  from ‹p∈P›
  obtain G where Eq6: "p∈G ∧ filter(G) ∧ (∀n∈nat.(?D`n)∩G≠0)"
    using cg.countable_rasiowa_sikorski[where M="λ_. M"]  P_sub_M
      M_countable[THEN bij_is_fun] M_countable[THEN bij_is_surj, THEN surj_range] 
    unfolding cg.D_generic_def by blast
  then 
  have Eq7: "(∀D∈M. D⊆P ∧ dense(D)⟶D∩G≠0)"
  proof (intro ballI impI)
    fix D
    assume "D∈M" and Eq9: "D ⊆ P ∧ dense(D) " 
    have "∀y∈M. ∃x∈nat. enum`x= y"
      using M_countable and  bij_is_surj unfolding surj_def by (simp)
    with ‹D∈M› obtain n where Eq10: "n∈nat ∧ enum`n = D" 
      by auto
    with Eq9 and if_P
    have "?D`n = D" by (simp)
    with Eq6 and Eq10 
    show "D∩G≠0" by auto
  qed
  with Eq6 
  show ?thesis unfolding M_generic_def by auto
qed

(* Compatibility lemmas *)
lemma compat_in_abs :
  assumes
    "A∈M" "r∈M" "p∈M" "q∈M" 
  shows
    "is_compat_in(##M,A,r,p,q) ⟷ compat_in(A,r,p,q)" 
proof -
  have "d∈A ==> d∈M" for d
    using transitivity ‹A∈M› by simp
  moreover from this
  have "d∈A ==> ⟨d, t⟩ ∈ M" if "t∈M" for t d
    using that pair_in_M_iff by simp
  ultimately 
  show ?thesis
    unfolding is_compat_in_def compat_in_def 
    using assms pair_in_M_iff transitivity by auto
qed

definition
  compat_in_fm :: "[i,i,i,i] ==> i" where
  "compat_in_fm(A,r,p,q) ≡
    Exists(And(Member(0,succ(A)),Exists(And(pair_fm(1,p#+2,0),
                                        And(Member(0,r#+2),
                                 Exists(And(pair_fm(2,q#+3,0),Member(0,r#+3))))))))" 

lemma compat_in_fm_type[TC] : 
  "[ A∈nat;r∈nat;p∈nat;q∈nat] ==> compat_in_fm(A,r,p,q)∈formula" 
  unfolding compat_in_fm_def by simp

lemma sats_compat_in_fm:
  assumes
    "A∈nat" "r∈nat"  "p∈nat" "q∈nat" "env∈list(M)"  
  shows
    "sats(M,compat_in_fm(A,r,p,q),env) ⟷
            is_compat_in(##M,nth(A, env),nth(r, env),nth(p, env),nth(q, env))"
  unfolding compat_in_fm_def is_compat_in_def using assms by simp

end (* forcing_data *)

end