Theory Names

(*
----------------------------------------------
First steps towards a formalization of Forcing
---------------------------------------------

Definition of Generic extension of a model M of ZFC: M[G].
Definition of function val and check, and properties about them.
Proof that G belongs to M[G] and that the latter is	a transitive 
set.

*)

theory Names imports Forcing_data begin

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

definition
  SepReplace :: "[i, i⇒i, i⇒ o] ⇒i" where
  "SepReplace(A,b,Q) == {y . x∈A, y=b(x) ∧ Q(x)}"
  
syntax
  "_SepReplace"  :: "[i, pttrn, i, o] => i"  ("(1{_ ../ _ ∈ _, _})")
translations
  "{b .. x∈A, Q}" => "CONST SepReplace(A, λx. b, λx. Q)"

lemma Sep_and_Replace: "{b(x) .. x∈A, P(x) } = {b(x) . x∈{y∈A. P(y)}}"
  by (auto simp add:SepReplace_def)

lemma SepReplace_subset : "A⊆A'⟹ {b .. x∈A, Q}⊆{b .. x∈A', Q}"
  by (auto simp add:SepReplace_def)

    
lemma SepReplace_dom_implies :
   "∀x∈A. b(x) = b'(x)⟹ {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (simp add:SepReplace_def)
    
lemma SepReplace_pred_implies :
   "∀x. Q(x)⟶ b(x) = b'(x)⟹ {b(x) .. x∈A, Q(x)}={b'(x) .. x∈A, Q(x)}"
  by  (force simp add:SepReplace_def)
   
text‹The well founded relation on which @{term val} is defined›

definition
  ed :: "[i,i] ⇒ o" where
  "ed(x,y) == x ∈ domain(y)"
  
definition
  edrel :: "i ⇒ i" where
  "edrel(A) == {<x,y> ∈ A*A . x ∈ domain(y)}"

lemma edrelI [intro!]: "x∈A ⟹ y∈A ⟹ x ∈ domain(y) ⟹ <x,y>∈edrel(A)"
  by (simp add:edrel_def)
    
lemma edrelD [dest] : "<x,y>∈edrel(A)⟹ x ∈ domain(y)"
  by (simp add:edrel_def)
    
lemma edrel_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ <x,y>∈edrel(A)"
   by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)

lemma edrel_trans_iff: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟷ <x,y>∈edrel(A)"
  by (auto simp add: edrel_trans, auto simp add:Transset_def Pair_def)

lemma edrel_domain: "x∈ M ⟹ edrel(eclose(M)) -`` {x} = domain(x)"
  apply (rule equalityI, auto , subgoal_tac "Transset(eclose(M))", rule vimageI)
    apply (auto simp add: edrelI Transset_eclose)
   apply (rename_tac y z)
   apply (rule_tac A="{y}" in ecloseD)
    apply (rule_tac A="⟨y, z⟩" in ecloseD)
    apply (rule_tac A="x" in ecloseD)
     apply (tactic {* distinct_subgoals_tac *})
    apply (auto simp add: Pair_def arg_into_eclose)
  done

lemma domain_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ x∈A"
  by (auto simp add: Transset_def domain_def Pair_def)
    
lemma edrel_sub_memrel: "edrel(A) ⊆ trancl(Memrel(eclose(A)))" 
proof
  let
              ?r="trancl(Memrel(eclose(A)))"
  fix z
  assume
              "z∈edrel(A)"
  then obtain x y where
              "x∈A" "y∈A" "z=<x,y>" "x∈domain(y)"
    unfolding edrel_def by (auto)
  then obtain u v where
       Eq1:   "x∈u" "u∈v" "v∈y"
    unfolding domain_def Pair_def by auto
  with ‹x∈A› ‹y∈A› have
              "x∈eclose(A)" "y∈eclose(A)" 
    using  arg_into_eclose by auto
  moreover with  ‹v∈y› have
              "v∈eclose(A)" 
    using  ecloseD by simp
  moreover with  ‹u∈v› have
              "u∈eclose(A)" 
    using  ecloseD arg_into_eclose by simp
  ultimately have
              "<x,u>∈?r" "<u,v>∈?r" "<v,y>∈?r"
    using Eq1 r_into_trancl by auto
  then have
              "<x,y>∈?r"
    by (rule_tac trancl_trans; simp)+
  with ‹z=<x,y>› show 
              "z∈?r" by simp
qed
  
lemma wf_edrel : "wf(edrel(A))"
  apply (rule_tac wf_subset [of "trancl(Memrel(eclose(A)))"])
  apply (auto simp add:edrel_sub_memrel wf_trancl wf_Memrel)
  done
    
lemma eq_sub_trans :  "x=y ⟹ y⊆z ⟹ x⊆z"
                "x⊆y ⟹ y=z ⟹ x⊆z"
  by simp_all
    
    
lemma SepReplace_iff [simp]: "y∈{b(x) .. x∈A, P(x)} ⟷ (∃x∈A. y=b(x) & P(x))"
   by (auto simp add:SepReplace_def)

    
context forcing_data
begin  (*************** CONTEXT: forcing_data *****************)

definition 
  Hcheck :: "[i,i] ⇒ i" where
  "Hcheck(z,f)  == { <f`y,one> . y ∈ z}"

definition
  check :: "i ⇒ i" where
  "check(x) == wfrec(Memrel(eclose({x})), x , Hcheck)"

lemma  aux_def_check:
  "(λx∈y. wfrec(Memrel(eclose({y})), x, Hcheck)) = 
   (λx∈y. wfrec(Memrel(eclose({x})), x, Hcheck))"
  apply (rule lam_cong)
   defer 1 apply (rule wfrec_eclose_eq)
    defer 1 apply (rule ecloseD, auto simp add: arg_into_eclose)
  done
    
lemma def_check : "check(y) = { <check(w),one> . w ∈ y}"
proof -
  let 
              ?r="λy. Memrel(eclose({y}))"
  from wf_Memrel have
       wfr:   "∀w . wf(?r(w))" ..
  with wfrec [of "?r(y)" y "Hcheck"] have
              "check(y)= 
               Hcheck( y, λx∈?r(y) -`` {y}. wfrec(?r(y), x, Hcheck))"
    by (simp add:check_def)
  also have 
              " ... = Hcheck( y, λx∈y. wfrec(?r(y), x, Hcheck))"
    by (simp add:under_Memrel_eclose arg_into_eclose)
  also have 
              " ... = Hcheck( y, λx∈y. check(x))"
    using aux_def_check by (simp add:check_def)
  finally show ?thesis by (simp add:Hcheck_def)
qed

definition
  Hv :: "i⇒i⇒i⇒i" where
  "Hv(G,x,f) == { f`y .. y∈ domain(x), ∃p∈P. <y,p> ∈ x ∧ p ∈ G }"

definition
  val :: "i⇒i⇒i" where
  "val(G,τ) == wfrec(edrel(eclose(M)), τ ,Hv(G))"

definition
  GenExt :: "i⇒i"     ("M[_]")
  where "GenExt(G)== {val(G,τ). τ ∈ M}"
  
lemma def_val:  "x∈M ⟹ val(G,x) = {val(G,t) .. t∈domain(x) , ∃p∈P .  ⟨t, p⟩∈x ∧ p ∈ G }"
proof -
  assume
      asm:  "x∈M"
  let
            ?r="edrel(eclose(M))"
  let
            ?f="λz∈?r-``{x}. wfrec(?r,z,Hv(G))"
  have
            "∀τ. wf(?r)"
    by (simp add: wf_edrel)
  with wfrec [of "?r" x "Hv(G)"] have
            "val(G,x) = Hv(G,x,?f)"
    by (simp add:val_def)
  also have
            " ... = Hv(G,x,λz∈domain(x). wfrec(?r,z,Hv(G)))"
    using asm and edrel_domain by (simp) 
  also have
            " ... = Hv(G,x,λz∈domain(x). val(G,z))"
    by (simp add:val_def)
  finally show ?thesis by (simp add:Hv_def SepReplace_def)
qed

lemma elem_of_val: "⟦ x∈val(G,π) ; π ∈ M ⟧ ⟹ ∃θ∈domain(π). val(G,θ) = x"
  by (subst (asm) def_val,auto)

lemma elem_of_val_pair: "⟦ x∈val(G,π) ; π ∈ M ⟧ ⟹ ∃θ. ∃p∈G.  <θ,p>∈π ∧ val(G,θ) = x"
  by (subst (asm) def_val,auto)
  
lemma GenExtD: 
  "x ∈ M[G] ⟹ ∃τ∈M. x = val(G,τ)"
  by (simp add:GenExt_def)
    
lemma GenExtI: 
  "x ∈ M ⟹ val(G,x) ∈ M[G]"
  by (auto simp add: GenExt_def)
  
lemma val_of_name : 
  "{x∈A×P. Q(x)} ∈ M ⟹
   val(G,{x∈A×P. Q(x)}) = {val(G,t) .. t∈A , ∃p∈P .  Q(<t,p>) ∧ p ∈ G }"
proof -
  let
              ?n="{x∈A×P. Q(x)}" and
              ?r="edrel(eclose(M))"
  assume
        asm:  "?n ∈ M"
  let
              ?f="λz∈?r-``{?n}. val(G,z)"
  have
              "∀τ. wf(?r)"
    by (simp add: wf_edrel)
  with val_def have
              "val(G,?n) = Hv(G,?n,?f)"
    by (rule_tac def_wfrec [of _ "?r" "Hv(G)"], simp_all)
  also have
              "... = {?f`t .. t∈domain(?n), ∃p∈P . <t,p>∈?n ∧ p∈G}"
    unfolding Hv_def by simp
  also have
              "... = { (if t∈?r-``{?n} then val(G,t) else 0) .. t∈domain(?n), ∃p∈P . <t,p>∈?n ∧ p∈G}"
    by (simp)
  also have
        Eq1:  "... = { val(G,t) .. t∈domain(?n), ∃p∈P . <t,p>∈?n ∧ p∈G}"
  proof -
    from edrel_domain and asm have
              "domain(?n) ⊆ ?r-``{?n}" 
      by simp
    then have
              "∀t∈domain(?n). (if t∈?r-``{?n} then val(G,t) else 0) = val(G,t)"
      by auto
    then show 
              "{ (if t∈?r-``{?n} then val(G,t) else 0) .. t∈domain(?n), ∃p∈P . <t,p>∈?n ∧ p∈G} =
               { val(G,t) .. t∈domain(?n), ∃p∈P . <t,p>∈?n ∧ p∈G}"
      by auto
  qed
  also have
              " ... = { val(G,t) .. t∈A, ∃p∈P . <t,p>∈?n ∧ p∈G}"
   by force 
  finally show
              " val(G,?n)  = { val(G,t) .. t∈A, ∃p∈P . Q(<t,p>) ∧ p∈G}"
    by auto
qed

lemma valcheck : "y ∈ M ⟹ one ∈ G ⟹ ∀x∈M. check(x) ∈ M ⟹ val(G,check(y))  = y"
proof (induct rule:eps_induct)
  case (1 y)
  then show ?case
  proof -
    from def_check have
          Eq1: "check(y) = { ⟨check(w), one⟩ . w ∈ y}"  (is "_ = ?C") .
    with 1 have
          Eq2: "?C∈M" 
      by auto
    with 1 transD subsetD trans_M have 
        w_in_M : "∀ w ∈ y . w ∈ M" by force
    from Eq1 have
               "val(G,check(y)) = val(G, {⟨check(w), one⟩ . w ∈ y})"
      by simp
    also have
                " ...  = {val(G,t) .. t∈domain(?C) , ∃p∈P .  ⟨t, p⟩∈?C ∧ p ∈ G }"
      using def_val and Eq2 by simp
    also have
                " ... =  {val(G,t) .. t∈domain(?C) , ∃w∈y. t=check(w) }"
      using 1 and one_in_P by simp
    also have
                " ... = {val(G,check(w)) . w∈y }"
      by force
    also have
                " ... = y"
      using 1 and w_in_M by simp        
    finally show "val(G,check(y)) = y" 
      using 1 by simp
  qed
qed
  
(* M[G] is transitive *)
lemma trans_Gen_Ext' :
  assumes "vc ∈ M[G]"
    "y ∈ vc" 
  shows
    "y ∈ M[G]" 
proof -
  from ‹vc∈M[G]› have
    "∃c∈M. vc = val(G,c)"
    by (blast dest:GenExtD)
  then obtain c where
    "c∈M" "vc = val(G,c)" by auto
  with ‹vc ∈ M[G]› have
    "val(G,c)∈M[G]" by simp
  from ‹y ∈ vc› and ‹vc = val(G,c)› have
    "y ∈ val(G,c)" by simp
  with ‹c∈M› and elem_of_val have
    "∃θ∈domain(c). val(G,θ) = y" by simp
  then obtain θ where
    "θ∈domain(c)" "val(G,θ) = y" by auto
  from ‹θ∈domain(c)› trans_M ‹c∈M› domain_trans have
    "θ∈M" by simp
  then have
    "val(G,θ) ∈ M[G]" 
    by (blast intro:GenExtI)
  with ‹val(G,θ) = y› show ?thesis by simp
qed
  
lemma trans_Gen_Ext:
  "Transset(M[G])"
  by (auto simp add: Transset_def trans_Gen_Ext')

lemma val_of_elem: 
  assumes 
    "<θ,p> ∈ π" "π∈M" "p∈G" "p∈P"
  shows
    "val(G,θ) ∈ val(G,π)"
proof - 
  from ‹π∈M› have 
    1:"val(G,π) = {val(G,t) .. t∈domain(π) , ∃p∈P .  ⟨t, p⟩∈π ∧ p ∈ G }"
    using def_val by simp
  from ‹<θ,p> ∈ π› have "θ∈domain(π)" by auto
  with ‹p∈G› ‹p∈P› ‹θ∈domain(π)› ‹<θ,p> ∈ π› have
    "val(G,θ) ∈ {val(G,t) .. t∈domain(π) , ∃p∈P .  ⟨t, p⟩∈π ∧ p ∈ G }"
    by auto
  with 1 show ?thesis by simp
qed

end    (*************** CONTEXT: forcing_data *****************)

(* definitions from Relative by Paulson *)
definition
  upair :: "[i=>o,i,i,i] => o" where
    "upair(M,a,b,z) == a ∈ z & b ∈ z & (∀x[M]. x∈z ⟶ x = a | x = b)"
  
definition
  upair_ax :: "(i=>o) => o" where
    "upair_ax(M) == ∀x[M]. ∀y[M]. ∃z[M]. upair(M,x,y,z)"

definition
  univalent :: "[i=>o, i, [i,i]=>o] => o" where
    "univalent(M,A,P) ==
        ∀x[M]. x∈A ⟶ (∀y[M]. ∀z[M]. P(x,y) & P(x,z) ⟶ y=z)"

definition
  strong_replacement :: "[i=>o, [i,i]=>o] => o" where
    "strong_replacement(M,P) ==
      ∀A[M]. univalent(M,A,P) ⟶
      (∃Y[M]. ∀b[M]. b ∈ Y ⟷ (∃x[M]. x∈A & P(x,b)))"

lemma univalent_triv [intro,simp]:
     "univalent(M, A, λx y. y = f(x))"
by (simp add: univalent_def)

    
(* G ∈ M[G] *)
locale M_extra_assms = forcing_data +
  assumes
        check_in_M : "⋀x. x ∈ M ⟹ check(x) ∈ M"
    and upair_ax:         "upair_ax(##M)"
    and repl_check_pair : "strong_replacement(##M,λp y. y =<check(p),p>)"
    
begin  (*************** CONTEXT: M_extra_assms *****************)
  
(* The next lemma is needed to provide an interface between 
   Paulson's lemmas for classes and our set models *)
lemma Transset_intf :
  "Transset(M) ⟹  y∈x ⟹ x ∈ M ⟹ y ∈ M"
  by (simp add: Transset_def,auto)

(* The following five lemmas are extracted from Relative by Paulson.
   upairM and pairM are variants of upair_in_M_iff and pair_in_M_iff,
   respectively, written for the set model M instead of the class ##M 
*)
lemma upair_abs [simp]:
     "z∈M ==> upair(##M,a,b,z) ⟷ z={a,b}"
  apply (simp add: upair_def)
  apply (insert trans_M)
  apply (blast intro: Transset_intf)
done

lemma upairM : "x ∈ M ⟹ y ∈ M ⟹ {x,y} ∈ M"
  by(insert upair_ax, auto simp add: upair_ax_def)
    
lemma pairM : "x ∈  M ⟹ y ∈ M ⟹ <x,y> ∈ M"
  by(unfold Pair_def, rule upairM,(rule upairM,simp+)+)

lemma univalent_Replace_iff:
     "[| A∈M; univalent(##M,A,Q);
         !!x y. [| x∈A; Q(x,y) |] ==> y∈M |]
      ==> u ∈ Replace(A,Q) ⟷ (∃x. x∈A & Q(x,u))"
  apply (simp add: Replace_iff univalent_def)
  apply (insert trans_M)
  apply (blast dest: Transset_intf)
done

lemma strong_replacement_closed [intro,simp]:
     "[| strong_replacement(##M,Q); A∈M; univalent(##M,A,Q);
         !!x y. [| x∈A; Q(x,y) |] ==> y∈M |] ==> (Replace(A,Q)∈M)"
  apply (simp add: strong_replacement_def)
  apply (drule_tac x=A in bspec, safe)
  apply (subgoal_tac "Replace(A,Q) = Y")
   apply simp
  apply (rule equality_iffI)
  apply (simp add: univalent_Replace_iff)
  apply (insert trans_M)
  apply (blast dest: Transset_intf)
done
    
lemma P_sub_M : "P ⊆ M"
  by (simp add: P_in_M trans_M transD)

    
definition
  G_dot :: "i" where
  "G_dot == {<check(p),p> . p∈P}"
  
lemma G_dot_in_M :
    "G_dot ∈ M" 
proof -
  have 0:"G_dot = { y . p∈P , y = <check(p),p> }"
    unfolding G_dot_def by auto
  from P_in_M check_in_M pairM P_sub_M have "⋀ p . p∈P ⟹ <check(p),p> ∈ M" 
    by auto
  then have
    1:"⋀x y. ⟦ x∈P ; y = <check(x),x> ⟧ ⟹ y∈M"
    by simp
  then have
    "∀A∈M.(∃Y∈M. ∀b∈M. b ∈ Y ⟷ (∃x∈M. x∈A & b = <check(x),x>))"
    using repl_check_pair unfolding strong_replacement_def by simp
  then have
    "(∃Y∈M. ∀b∈M. b ∈ Y ⟷ (∃x∈M. x∈P & b = <check(x),x>))"
    using P_in_M by simp
  with 1 repl_check_pair P_in_M strong_replacement_closed have
    "{ y . p∈P , y = <check(p),p> } ∈ M" by simp
  then show ?thesis using 0 by simp
qed
  
lemma val_G_dot :
  assumes "G ⊆ P"
    "one ∈ G" 
  shows "val(G,G_dot) = G"
proof (intro equalityI subsetI) 
  fix x
  assume "x∈val(G,G_dot)"
  then have 
      "∃θ. ∃p∈G.  <θ,p>∈G_dot ∧ val(G,θ) = x"
    using G_dot_in_M elem_of_val_pair by simp
  then obtain r p where 
    "p∈G" "<r,p> ∈ G_dot" "val(G,r) = x" 
    by auto
  then have
    "r = check(p)" 
    unfolding G_dot_def by simp
  with ‹one∈G› ‹G⊆P› ‹p∈G› ‹val(G,r) = x› show
      "x ∈ G" 
    using valcheck P_sub_M  check_in_M by auto
next
  fix p
  assume "p∈G" 
  have "∀q∈P. <check(q),q> ∈ G_dot" 
    unfolding G_dot_def by simp
  with ‹p∈G› ‹G⊆P› have
    "val(G,check(p)) ∈ val(G,G_dot)"
    using val_of_elem G_dot_in_M by blast
  with ‹p∈G› ‹G⊆P› ‹one∈G› show
    "p ∈ val(G,G_dot)" 
    using P_sub_M check_in_M valcheck by auto
qed
  
  
lemma G_in_Gen_Ext :
  assumes "G ⊆ P"
    "one ∈ G"
  shows   "G ∈ M[G]" 
proof -
  from G_dot_in_M have
    "val(G,G_dot) ∈ M[G]" 
    by (auto intro:GenExtI)
  with assms val_G_dot 
  show ?thesis by simp
qed

  
end    (*************** CONTEXT: M_extra_assms *****************)

end