Theory Interface

theory Interface 
  imports Forcing_Data Relative Internalizations Renaming
begin

lemma Transset_intf :
  "Transset(M) ⟹  y∈x ⟹ x ∈ M ⟹ y ∈ M"
  by (simp add: Transset_def,auto)

lemma TranssetI :
  "(⋀y x. y∈x ⟹ x∈M ⟹ y∈M) ⟹ Transset(M)"
  by (auto simp add: Transset_def)
    
lemma empty_intf :
  "infinity_ax(M) ⟹
  (∃z[M]. empty(M,z))"
  by (auto simp add: empty_def infinity_ax_def)

lemma (in forcing_data) zero_in_M:  "0 ∈ M"
proof -
  from infinity_ax have
        "(∃z[##M]. empty(##M,z))"
    by (rule empty_intf)
  then obtain z where
        zm: "empty(##M,z)"  "z∈M"
    by auto
  with trans_M have "z=0"
    by (simp  add: empty_def, blast intro: Transset_intf )
  with zm show ?thesis 
      by simp
qed
    
(* Interface with M_trivial *)
    
lemma (in forcing_data) mtriv :  
  "M_trivial(##M)"
  apply (insert trans_M upair_ax Union_ax)
  apply (rule M_trivial.intro)
  apply (simp_all add: zero_in_M)
  apply (rule Transset_intf,simp+)
done

sublocale forcing_data ⊆ M_trivial "##M"
  by (rule mtriv)
  
(* tupling *)
abbreviation
 dec10  :: i   ("10") where "10 == succ(9)"
    
abbreviation
 dec11  :: i   ("11") where "11 == succ(10)"

abbreviation
 dec12  :: i   ("12") where "12 == succ(11)"

abbreviation
 dec13  :: i   ("13") where "13 == succ(12)"

lemma uniq_dec_2p: "<C,D> ∈ M ⟹ 
             ∀A∈M. ∀B∈M. <C,D> = ⟨A, B⟩ ⟶ P(x, A, B)
            ⟷
              P(x, C, D)"
  by simp
    
lemma (in forcing_data) tupling_sep_2p :
    "(∀v∈M. separation(##M,λx. (∀A∈M. ∀B∈M. pair(##M,A,B,v) ⟶ Q(x,A,B))))
    ⟷
     (∀A∈M. ∀B∈M. separation(##M,λx. Q(x,A,B)))"
  apply (simp add: separation_def)
proof (intro ballI iffI)
  fix A B z
  assume
        Eq1:  "∀v∈M. ∀z∈M. ∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧ (∀A∈M. ∀B∈M. v = ⟨A, B⟩ ⟶ Q(x, A, B))"
     and
        Eq2:  "A∈M" "B∈M" "z∈M"  (* no puedo poner la conjunción *)
  then have 
        Eq3:  "<A,B>∈M"
    by (simp del:setclass_iff add:setclass_iff[symmetric])
  with Eq1 have 
              "∀z∈M. ∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧ (∀C∈M. ∀D∈M. <A,B> = ⟨C, D⟩ ⟶ Q(x, C, D))"
    by (rule bspec)
  with uniq_dec_2p and Eq3 and Eq2 show
              "∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧  Q(x, A, B)"
    by simp
next
  fix v z
  assume
       asms:  "v∈M"   "z∈M"
              "∀A∈M. ∀B∈M. ∀z∈M. ∃y∈M. ∀x∈M. x ∈ y ⟷ x ∈ z ∧ Q(x, A, B)"
  consider (a) "∃A∈M. ∃B∈M. v = ⟨A, B⟩" | (b) "∀A∈M. ∀B∈M. v ≠ ⟨A, B⟩" by auto
  then show                (* "then" is important here *)
              "∃y∈M. ∀x∈M. x ∈ y ⟷ x ∈ z ∧ 
                    (∀A∈M. ∀B∈M. v = ⟨A, B⟩ ⟶ Q(x, A, B))"
  proof cases
    case a
    then obtain A B where  (* also here *)
        Eq4:  "A∈M" "B∈M" "v = ⟨A, B⟩"
      by auto
    then have
              "∃y∈M. ∀x∈M. x ∈ y ⟷ x ∈ z ∧ Q(x, A, B)"
      using asms by simp
    then show ?thesis using Eq4 and uniq_dec_2p by simp
  next
    case b
    then have
              "∀x∈M. x ∈ z ⟷ x ∈ z ∧ (∀A∈M. ∀B∈M. v = ⟨A, B⟩ ⟶ Q(x, A, B))"
      by simp
    then show ?thesis using b and asms by auto
  qed
qed
  

lemma (in forcing_data) tuples_in_M: "A∈M ⟹ B∈M ⟹ <A,B>∈M" 
   by (simp del:setclass_iff add:setclass_iff[symmetric])

(* Five-parameter separation auxiliary results *)
     
lemma uniq_dec_5p: "<A',B',C',D',E'> ∈ M ⟹ 
             ∀A∈M. ∀B∈M. ∀C∈M. ∀D∈M. ∀E∈M. <A',B',C',D',E'> = <A,B,C,D,E> ⟶ 
                  P(x,A,B,C,D,E)
                ⟷
                  P(x,A',B',C',D',E')"
  by simp

lemma (in forcing_data) tupling_sep_5p_aux :
              "(∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
                ⟨A4, A5⟩ ∈ M ∧ ⟨A3, A4, A5⟩ ∈ M ∧ ⟨A2, A3, A4, A5⟩ ∈ M ∧ 
                v = ⟨A1, A2, A3, A4, A5⟩ ⟶
                Q(x, A1, A2, A3, A4, A5))
               ⟷
               (∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M.
                v = ⟨A1, A2, A3, A4, A5⟩ ⟶
                Q(x, A1, A2, A3, A4, A5))" for x v
 by (auto simp add:tuples_in_M)


lemma (in forcing_data) tupling_sep_5p : 
"(∀v∈M. separation(##M,λx. (∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M. 
                  v = ⟨A1, ⟨A2, ⟨A3, ⟨A4, A5⟩⟩⟩⟩ ⟶ Q(x,A1,A2,A3,A4,A5))))
    ⟷
 (∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M. separation(##M,λx. Q(x,A1,A2,A3,A4,A5)))"
proof (simp add: separation_def, intro ballI iffI)
  fix A B C D E z
  assume
        Eq1:  "∀v∈M. ∀z∈M. ∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧ (∀A∈M. ∀B∈M.  ∀C∈M. ∀D∈M. ∀E∈M. v = ⟨A, B,C,D,E⟩ 
                   ⟶ Q(x, A, B, C, D, E))"
     and
        Eq2:  "A∈M" "B∈M" "C∈M" "D∈M" "E∈M" "z∈M"  (* no puedo poner la conjunción *)
  then have 
        Eq3:  "<A,B,C,D,E>∈M"
    by (simp del:setclass_iff add:setclass_iff[symmetric])
  with Eq1 have 
              "∀z∈M. ∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧ (∀A'∈M. ∀B'∈M.  ∀C'∈M. ∀D'∈M. ∀E'∈M. <A,B,C,D,E> = ⟨A',B',C',D',E'⟩ 
                   ⟶ Q(x, A', B', C', D', E'))"
    by (rule bspec)
  with uniq_dec_5p and Eq3 and Eq2 show
              "∃y∈M. ∀x∈M. x ∈ y ⟷ 
               x ∈ z ∧  Q(x,A,B,C,D,E)"
    by simp
next
  fix v z
  assume
       asms:  "v∈M"   "z∈M"
              "∀A∈M. ∀B∈M. ∀C∈M. ∀D∈M. ∀E∈M. ∀z∈M. ∃y∈M. 
                  ∀x∈M. x ∈ y ⟷ x ∈ z ∧ Q(x, A,B,C,D,E)"
  consider (a) "∃A∈M. ∃B∈M. ∃C∈M. ∃D∈M. ∃E∈M. v = ⟨A,B,C,D,E⟩" | 
           (b) "∀A∈M. ∀B∈M. ∀C∈M. ∀D∈M. ∀E∈M. v ≠ ⟨A,B,C,D,E⟩" by blast
  then show               
              "∃y∈M. ∀x∈M. x ∈ y ⟷ x ∈ z ∧ 
                    (∀A∈M. ∀B∈M. ∀C∈M. ∀D∈M. ∀E∈M. v = ⟨A,B,C,D,E⟩ ⟶ Q(x,A,B,C,D,E))"
  proof cases
    case a
    then obtain A B C D E where 
        Eq4:  "A∈M" "B∈M" "C∈M" "D∈M" "E∈M" "v = ⟨A,B,C,D,E⟩"
      by auto
    then have
              "∃y∈M. ∀x∈M. x ∈ y ⟷ x ∈ z ∧ Q(x,A,B,C,D,E)"
      using asms by simp
    then show ?thesis using Eq4 by simp
  next
    case b
    then have
              "∀x∈M. x ∈ z ⟷ x ∈ z ∧ 
                (∀A∈M. ∀B∈M.  ∀C∈M. ∀D∈M. ∀E∈M. v = ⟨A,B,C,D,E⟩ ⟶ Q(x,A,B,C,D,E))"
      by simp
    then show ?thesis using b and asms by auto
  qed
qed

   
lemma (in forcing_data) tupling_sep_5p_rel : 
"(∀v∈M. separation(##M,λx. (∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. 
                    ∀B1∈M. ∀B2∈M. ∀B3∈M.   
                    pair(##M,A4,A5,B1) & 
                    pair(##M,A3,B1,B2) & 
                    pair(##M,A2,B2,B3) & 
                    pair(##M,A1,B3,v)  
               ⟶ Q(x,A1,A2,A3,A4,A5))))
    ⟷
 (∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. separation(##M,λx. Q(x,A1,A2,A3,A4,A5)))"
proof (simp)
  have
      "(∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
        ⟨A4, A5⟩ ∈ M ∧ ⟨A3, A4, A5⟩ ∈ M ∧ ⟨A2, A3, A4, A5⟩ ∈ M ∧ v = ⟨A1, A2, A3, A4, A5⟩ ⟶
        Q(x, A1, A2, A3, A4, A5))
      ⟷
      (∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M.
        v = ⟨A1, A2, A3, A4, A5⟩ ⟶
        Q(x, A1, A2, A3, A4, A5))" for x v
    by (rule tupling_sep_5p_aux)
  then have
      "(∀v∈M. separation
             (##M,
              λx. ∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
        ⟨A4, A5⟩ ∈ M ∧ ⟨A3, A4, A5⟩ ∈ M ∧ ⟨A2, A3, A4, A5⟩ ∈ M ∧ v = ⟨A1, A2, A3, A4, A5⟩ ⟶
        Q(x, A1, A2, A3, A4, A5)))
      ⟷
      (∀v∈M. separation
             (##M,
              λx. ∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M.
        v = ⟨A1, A2, A3, A4, A5⟩ ⟶
        Q(x, A1, A2, A3, A4, A5)))"
    by simp
  also have
     "...   ⟷
 (∀A1∈M. ∀A2∈M. ∀A3∈M. ∀A4∈M. ∀A5∈M. separation(##M,λx. Q(x,A1,A2,A3,A4,A5)))"
    using tupling_sep_5p by simp
  finally  show
    "(∀v∈M. separation
             (##M,
              λx. ∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
⟨A4, A5⟩ ∈ M ∧ ⟨A3, A4, A5⟩ ∈ M ∧ ⟨A2, A3, A4, A5⟩ ∈ M ∧ v = ⟨A1, A2, A3, A4, A5⟩ ⟶
Q(x, A1, A2, A3, A4, A5))) ⟷
    (∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. separation(##M, λx. Q(x, A1, A2, A3, A4, A5)))"
    by auto
qed

lemma (in forcing_data) tupling_sep_5p_rel2 : 
"(∀v∈M. separation(##M,λx. (∀B3∈M. ∀B2∈M. ∀B1∈M. 
                    ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. ∀A1∈M.  
                    pair(##M,A4,A5,B1) & 
                    pair(##M,A3,B1,B2) & 
                    pair(##M,A2,B2,B3) & 
                    pair(##M,A1,B3,v)  
               ⟶ Q(x,A1,A2,A3,A4,A5))))
    ⟷
 (∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. ∀A1∈M. separation(##M,λx. Q(x,A1,A2,A3,A4,A5)))"
proof -
  have
        "(∀B3∈M. ∀B2∈M. ∀B1∈M. 
                    ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. ∀A1∈M.  
                    pair(##M,A4,A5,B1) & 
                    pair(##M,A3,B1,B2) & 
                    pair(##M,A2,B2,B3) & 
                    pair(##M,A1,B3,v)  
               ⟶ Q(x,A1,A2,A3,A4,A5))
          ⟷
         (∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. 
                    ∀B1∈M. ∀B2∈M. ∀B3∈M.   
                    pair(##M,A4,A5,B1) & 
                    pair(##M,A3,B1,B2) & 
                    pair(##M,A2,B2,B3) & 
                    pair(##M,A1,B3,v)  
               ⟶ Q(x,A1,A2,A3,A4,A5))" 
        (is "?P⟷?Q") for x v 
    by auto
  then have
        "separation(##M,λx. ?P(x,v)) ⟷ separation(##M,λx. ?Q(x,v))" for v
    by auto
  then have
        "(∀v∈M. separation(##M,λx. ?P(x,v)))
         ⟷ 
         (∀v∈M. separation(##M,λx. ?Q(x,v)))"
    by blast
  also have
    " ... ⟷ (∀A1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M. separation(##M,λx. Q(x,A1,A2,A3,A4,A5)))"
    using tupling_sep_5p_rel by simp
  finally show ?thesis by auto
qed

(* Internalized tupling *) 
definition 
  tupling_fm_2p :: "i ⇒ i" where
  "tupling_fm_2p(φ) = Forall(Forall(Implies(pair_fm(1,0,3),φ)))"
  
lemma [TC] :  "⟦ φ ∈ formula ⟧ ⟹ tupling_fm_2p(φ) ∈ formula"
  by (simp add: tupling_fm_2p_def)
    
lemma arity_tup2p :  
  "⟦ φ ∈ formula ; arity(φ) = 3 ⟧ ⟹ arity(tupling_fm_2p(φ)) = 2"
  by (simp add: tupling_fm_2p_def arity_incr_bv_lemma pair_fm_def 
                upair_fm_def Un_commute nat_union_abs1)

definition
  tupling_fm_5p :: "i ⇒ i" where
  "tupling_fm_5p(φ) = 
      Forall(Forall(Forall(Forall(Forall(Forall(Forall(Forall(
        Implies(And(pair_fm(3,4,5),
                And(pair_fm(2,5,6),
                And(pair_fm(1,6,7),
                    pair_fm(0,7,9)))),φ)))))))))"

  
lemma [TC] :  "⟦ φ ∈ formula ⟧ ⟹ tupling_fm_5p(φ) ∈ formula"
  by (simp add: tupling_fm_5p_def)

lemma arity_tup5p :
  "⟦ φ ∈ formula ; arity(φ) = 9 ⟧ ⟹ arity(tupling_fm_5p(φ)) = 2"
  by (simp add: tupling_fm_5p_def arity_incr_bv_lemma pair_fm_def 
                upair_fm_def Un_commute nat_union_abs1)

lemma leq_9:
  "n≤9 ⟹ n=0 | n=1 | n=2 | n=3 | n=4 | n=5 | n=6| n=7 | n=8 | n=9"
  by (clarsimp simp add:not_lt_iff_le, auto simp add:lt_def)

lemma arity_tup5p_leq :
  "⟦ φ ∈ formula ; arity(φ) ≤ 9 ⟧ ⟹ arity(tupling_fm_5p(φ)) = 2"
  by (drule leq_9, elim disjE, simp_all add:tupling_fm_5p_def arity_incr_bv_lemma pair_fm_def 
                upair_fm_def Un_commute nat_union_abs1)

(* end tupling *)

(* Instances of separation of M_basic *)

(* Inter_separation: "M(A) ==> separation(M, λx. ∀y[M]. y∈A ⟶ x∈y)" *)
              
lemma arity_inter_fm :
  "arity(Forall(Implies(Member(0,2),Member(1,0)))) = 2"
  by (simp add: Un_commute nat_union_abs1)
  
lemma (in forcing_data) inter_sep_intf :
  assumes
      "A∈M"
  shows
      "separation(##M,λx . ∀y∈M . y∈A ⟶ x∈y)"
proof -
    from separation_ax arity_inter_fm have 
        "∀a∈M. separation(##M, λx. sats(M, Forall(Implies(Member(0,2),Member(1,0))), [x, a]))"
    by simp
  with ‹A∈M› have 
        "separation(##M, λx. sats(M, Forall(Implies(Member(0,2),Member(1,0))), [x, A]))"
    by simp
  with ‹A∈M› show ?thesis unfolding separation_def by simp
qed

  
(* Diff_separation: "M(B) ==> separation(M, λx. x ∉ B)" *)
lemma arity_diff_fm: 
  "arity(Neg(Member(0,1))) = 2"
by (simp add: nat_union_abs1)
    
lemma (in forcing_data) diff_sep_intf :
  assumes
      "B∈M"
  shows
      "separation(##M,λx . x∉B)"
proof -
  from separation_ax arity_diff_fm have 
        "∀a∈M. separation(##M, λx. sats(M, Neg(Member(0,1)), [x, a]))"
    by simp
  with ‹B∈M› have 
        "separation(##M, λx. sats(M, Neg(Member(0,1)), [x, B]))"
    by simp
  with ‹B∈M› show ?thesis unfolding separation_def by simp
qed
  
  
(* cartprod_separation: 
   "[| M(A); M(B) |] ==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. y∈B & pair(M,x,y,z)))" *)
definition
  cartprod_sep_fm :: "i" where
  "cartprod_sep_fm == 
              Exists(And(Member(0,2),
                     Exists(And(Member(0,2),pair_fm(1,0,4)))))"

lemma cartprof_sep_fm_type [TC] : 
  "cartprod_sep_fm ∈ formula"
  by (simp add: cartprod_sep_fm_def)
    
lemma arity_cartprod_fm [simp] : "arity(cartprod_sep_fm) = 3" 
  by (simp add: cartprod_sep_fm_def pair_fm_def upair_fm_def 
                Un_commute nat_union_abs1)
              
lemma (in forcing_data) cartprod_sep_intf :
  assumes
            "A∈M"
            and
            "B∈M"
   shows
            "separation(##M,λz. ∃x∈M. x∈A ∧ (∃y∈M. y∈B ∧ pair(##M,x,y,z)))"
proof -
  from separation_ax arity_tup2p have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_2p(cartprod_sep_fm),[x,v])))"
  by simp
  then have
    "(∀v∈M. separation(##M, λx. ∀A∈M. ∀B∈M. pair(##M, A, B, v) ⟶ 
                      (∃xa∈M. xa ∈ A ∧ (∃y∈M. y ∈ B ∧ pair(##M, xa, y, x)))))"
  unfolding separation_def tupling_fm_2p_def cartprod_sep_fm_def by (simp del: pair_abs)
  with tupling_sep_2p have 
    "(∀A∈M. ∀B∈M. separation(##M, λz. ∃x∈M. x ∈ A ∧ (∃y∈M. y ∈ B ∧ pair(##M, x, y, z))))"
  by simp
  with ‹A∈M› ‹B∈M› show ?thesis by simp
qed

(*image_separation: 
   "[| M(A); M(r) |] ==> separation(M, λy. ∃p[M]. p∈r & (∃x[M]. x∈A & pair(M,x,y,p)))" *)
definition
  image_sep_fm :: "i" where
  "image_sep_fm == 
    Exists(And(Member(0,1),
          Exists(And(Member(0,3),pair_fm(0,4,1)))))"
  
lemma image_sep_fm_type [TC] : 
  "image_sep_fm ∈ formula"
  by (simp add: image_sep_fm_def)

    
lemma [simp] : "arity(image_sep_fm) = 3" 
  by (simp add: image_sep_fm_def pair_fm_def upair_fm_def 
                Un_commute nat_union_abs1)
  
lemma (in forcing_data) image_sep_intf :
  assumes
            "A∈M"
            and
            "r∈M"
   shows
            "separation(##M, λy. ∃p∈M. p∈r & (∃x∈M. x∈A & pair(##M,x,y,p)))"
proof -
  from separation_ax arity_tup2p have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_2p(image_sep_fm),[x,v])))"
  by simp
  then have
    "(∀v∈M. separation(##M, λx. ∀A∈M. ∀B∈M. pair(##M, A, B, v) ⟶ 
          (∃p∈M. p ∈ B ∧ (∃xa∈M. xa ∈ A ∧ pair(##M, xa, x, p)))))"
  unfolding separation_def tupling_fm_2p_def image_sep_fm_def by (simp del: pair_abs)
  with tupling_sep_2p have 
    "(∀A∈M. ∀r∈M. separation(##M, λy. ∃p∈M. p∈r & (∃x∈M. x∈A & pair(##M,x,y,p))))"
  by simp
  with ‹A∈M› ‹r∈M› show ?thesis by simp
qed
   
(* converse_separation:
 "M(r) ==> separation(M,λz. ∃p[M]. p∈r & (∃x[M]. ∃y[M]. pair(M,x,y,p) & pair(M,y,x,z)))" *)
definition
  converse_sep_fm :: "i" where
  "converse_sep_fm == 
    Exists(And(Member(0,2),
      Exists(Exists(And(pair_fm(1,0,2),pair_fm(0,1,3))))))"
  
lemma converse_sep_fm_type [TC] : "converse_sep_fm ∈ formula"
  by (simp add: converse_sep_fm_def)

lemma [simp] : "arity(converse_sep_fm) = 2"
  by (simp add: converse_sep_fm_def pair_fm_def upair_fm_def 
                Un_commute nat_union_abs1)
       
lemma (in forcing_data) converse_sep_intf :
  assumes
         "R∈M"
  shows
         "separation(##M,λz. ∃p∈M. p∈R & (∃x∈M.∃y∈M. pair(##M,x,y,p) & pair(##M,y,x,z)))"
proof -
  from separation_ax have 
        "∀r∈M. separation(##M, λx. sats(M,converse_sep_fm, [x, r]))"
    by simp
  with ‹R∈M› have 
        "separation(##M, λx. sats(M,converse_sep_fm, [x, R]))"
    by simp
  with ‹R∈M› show ?thesis unfolding separation_def converse_sep_fm_def  by (simp del: pair_abs)
qed
              
(* restrict_separation:
     "M(A) ==> separation(M, λz. ∃x[M]. x∈A & (∃y[M]. pair(M,x,y,z)))" *)
definition
  restrict_sep_fm :: "i" where
  "restrict_sep_fm == Exists(And(Member(0,2),Exists(pair_fm(1,0,2))))"

lemma restrict_sep_fm_type [TC] : "restrict_sep_fm ∈ formula"
  by (simp add: restrict_sep_fm_def)
    
lemma [simp] : "arity(restrict_sep_fm) = 2"
  by (simp add: restrict_sep_fm_def pair_fm_def upair_fm_def 
                Un_commute nat_union_abs1)

lemma (in forcing_data) restrict_sep_intf :
  assumes
         "A∈M"
  shows
         "separation(##M,λz. ∃x∈M. x∈A & (∃y∈M. pair(##M,x,y,z)))"
proof -
  from separation_ax have 
        "∀a∈M. separation(##M, λx. sats(M,restrict_sep_fm, [x, a]))"
    by simp
  with ‹A∈M› have 
        "separation(##M, λx. sats(M,restrict_sep_fm, [x, A]))"
    by simp
  with ‹A∈M› show ?thesis unfolding separation_def restrict_sep_fm_def by (simp del: pair_abs)
qed
  
(* comp_separation:
    "[| M(r); M(s) |]
      ==> separation(M, λxz. ∃x[M]. ∃y[M]. ∃z[M]. ∃xy[M]. ∃yz[M].
                  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & xy∈s & yz∈r)"*)
definition 
  comp_sep_fm :: "i" where
  "comp_sep_fm ==
    Exists(Exists(Exists(Exists(Exists
      (And(pair_fm(4,2,7),And(pair_fm(4,3,1),
          And(pair_fm(3,2,0),And(Member(1,5),Member(0,6))))))))))"

lemma comp_sep_fm_type [TC] : "comp_sep_fm ∈ formula"
  by (simp add: comp_sep_fm_def)

lemma [simp] : "arity(comp_sep_fm) = 3"
  by (simp add: comp_sep_fm_def pair_fm_def upair_fm_def Un_commute nat_union_abs1)

lemma (in forcing_data) comp_sep_intf :
  assumes
    "R∈M"
    and
    "S∈M"
  shows
    "separation(##M,λxz. ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M.
              pair(##M,x,z,xz) & pair(##M,x,y,xy) & pair(##M,y,z,yz) & xy∈S & yz∈R)"
proof -
  from separation_ax arity_tup2p have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_2p(comp_sep_fm),[x,v])))"
    by simp
  then have
    "(∀v∈M. separation
             (##M, λx. ∀A∈M. ∀B∈M. pair(##M, A, B, v) ⟶
                                    (∃xa∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M. pair(##M, xa, z, x) ∧
              pair(##M, xa, y, xy) ∧ pair(##M, y, z, yz) ∧ xy ∈ B ∧ yz ∈ A)))"
  unfolding separation_def tupling_fm_2p_def comp_sep_fm_def by (simp del: pair_abs)
  with tupling_sep_2p have 
    "(∀r∈M. ∀s∈M. separation
         (##M, λxz. ∃x∈M. ∃y∈M. ∃z∈M. ∃xy∈M. ∃yz∈M. pair(##M, x, z, xz) ∧
                                    pair(##M, x, y, xy) ∧ pair(##M, y, z, yz) ∧ xy ∈ s ∧ yz ∈ r))"
    by simp
  with ‹S∈M› ‹R∈M› show ?thesis by simp
qed
 
(* pred_separation:
   "[| M(r); M(x) |] ==> separation(M, λy. ∃p[M]. p∈r & pair(M,y,x,p))"
*)
  
lemma arity_pred_fm [simp] : 
  "arity(Exists(And(Member(0,2),pair_fm(3,1,0)))) = 3"
  by (simp add: pair_fm_def upair_fm_def Un_commute nat_union_abs1)

lemma (in forcing_data) pred_sep_intf:
    assumes
      "R∈M"
    and
      "X∈M"
    shows
      "separation(##M, λy. ∃p∈M. p∈R & pair(##M,y,X,p))"
proof -
  from separation_ax arity_tup2p arity_pred_fm have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_2p(Exists(And(Member(0,2),
                                                                  pair_fm(3,1,0)))),[x,v])))"
  by simp
  then have
    "(∀v∈M. separation(##M, λx. ∀A∈M. ∀B∈M. pair(##M, A, B, v) ⟶ 
                                                        (∃p∈M. p ∈ A ∧ pair(##M, x, B, p))))"
  unfolding separation_def tupling_fm_2p_def by (simp del: pair_abs)
  with tupling_sep_2p have
    "∀r∈M. ∀x∈M. separation(##M, λy. ∃p∈M. p∈r & pair(##M,y,x,p))"
  by simp
  with ‹R∈M› ‹X∈M› show ?thesis by simp
qed
  
  
   
(* Memrel_separation:
     "separation(M, λz. ∃x[M]. ∃y[M]. pair(M,x,y,z) & x ∈ y)"
*)
definition
  memrel_fm :: "i" where
  "memrel_fm == Exists(Exists(And(pair_fm(1,0,2),Member(1,0))))"
    
lemma [TC] : "memrel_fm ∈ formula"
  by (simp add: memrel_fm_def)
  
lemma [simp] : "arity(memrel_fm) = 1"
  by (simp add: memrel_fm_def pair_fm_def upair_fm_def Un_commute nat_union_abs1)

lemma (in forcing_data) memrel_sep_intf:
  "separation(##M, λz. ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y)"
proof -
  from separation_ax have
    "(∀v∈M. separation(##M,λx. sats(M,memrel_fm,[x,v])))"
    by simp
  then have      
    "(∀v∈M. separation(##M, λz. ∃x∈M. ∃y∈M. pair(##M,x,y,z) & x ∈ y))"
    unfolding separation_def memrel_fm_def by (simp del: pair_abs)
  with zero_in_M show ?thesis by auto
qed

(*is_recfun_separation:
     ―‹for well-founded recursion: used to prove ‹is_recfun_equal››
     "[| M(r); M(f); M(g); M(a); M(b) |]
     ==> separation(M,
            λx. ∃xa[M]. ∃xb[M].
                pair(M,x,a,xa) & xa ∈ r & pair(M,x,b,xb) & xb ∈ r &
                (∃fx[M]. ∃gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
                                   fx ≠ gx))"
*)
  
definition
  is_recfun_sep_fm :: "i" where
  "is_recfun_sep_fm == 
  Exists(Exists(And(pair_fm(10,3,1),And(Member(1,6),And(pair_fm(10,2,0),And(Member(0,6),
                Exists(Exists(And(fun_apply_fm(7,12,1),
                And(fun_apply_fm(6,12,0),Neg(Equal(1,0))))))))))))"
  
lemma is_recfun_sep_fm [TC] : "is_recfun_sep_fm ∈ formula"
  by (simp add: is_recfun_sep_fm_def)

lemma [simp] : "arity(is_recfun_sep_fm) = 9"
  by (simp add: is_recfun_sep_fm_def fun_apply_fm_def upair_fm_def
                image_fm_def big_union_fm_def pair_fm_def Un_commute nat_union_abs1)


lemma (in forcing_data) is_recfun_sep_intf :
  assumes
        "r∈M" "f∈M" "g∈M" "a∈M" "b∈M"
   shows
      "separation(##M,λx. ∃xa∈M. ∃xb∈M.
                    pair(##M,x,a,xa) & xa ∈ r & pair(##M,x,b,xb) & xb ∈ r &
                    (∃fx∈M. ∃gx∈M. fun_apply(##M,f,x,fx) & fun_apply(##M,g,x,gx) &
                                     fx ≠ gx))"
proof -
  from separation_ax arity_tup5p have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_5p(is_recfun_sep_fm),[x,v])))"
    by simp
  then have
      "(∀v∈M. separation
             (##M, λx. ∀B3∈M. ∀B2∈M. ∀B1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
                    ∀A1∈M. pair(##M, A4, A5, B1) ∧ pair(##M, A3, B1, B2) ∧ pair(##M, A2, B2, B3) ∧ 
                            pair(##M, A1, B3, v) ⟶
         (∃xa∈M. ∃xb∈M. pair(##M, x, A2, xa) ∧ xa ∈ A5 ∧ pair(##M, x, A1, xb) ∧ xb ∈ A5 ∧ 
              (∃fx∈M. ∃gx∈M. fun_apply(##M, A4, x, fx) ∧ fun_apply(##M, A3, x, gx) ∧ fx ≠ gx))))" 
    unfolding separation_def tupling_fm_5p_def is_recfun_sep_fm_def by (simp del: pair_abs)
  with tupling_sep_5p_rel2 have
    "(∀r∈M. ∀f∈M. ∀g∈M. ∀a∈M. ∀b∈M. 
    separation(##M,λx. ∃xa∈M. ∃xb∈M.
                    pair(##M,x,a,xa) & xa ∈ r & pair(##M,x,b,xb) & xb ∈ r &
                    (∃fx∈M. ∃gx∈M. fun_apply(##M,f,x,fx) & fun_apply(##M,g,x,gx) &
                                     fx ≠ gx)))"
  by simp 
  with ‹r∈M› ‹f∈M› ‹g∈M› ‹a∈M› ‹b∈M› show ?thesis by simp
qed

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

lemma sixp_perm_ftc : "sixp_sep_perm ∈ 6 -||> 9"
  by(unfold sixp_sep_perm_def,(rule consI,auto)+,rule emptyI)

lemma dom_sixp_perm : "domain(sixp_sep_perm) = 6"
  by(unfold sixp_sep_perm_def,auto)
  
lemma sixp_perm_tc : "sixp_sep_perm ∈ 6 → 9"
  by(subst dom_sixp_perm[symmetric],rule FiniteFun_is_fun,rule sixp_perm_ftc)

lemma apply_fun: "f ∈ Pi(A,B) ==> <a,b>: f ⟹ f`a = b"
  by(auto simp add: apply_iff)

lemma sixp_perm_env : 
  "{x,a1,a2,a3,a4,a5} ⊆ A ⟹ j<6 ⟹
  nth(j,[x,a1,a2,a3,a4,a5]) = nth(sixp_sep_perm`j,[a1,a2,a3,a4,a5,b1,b2,b3,x,v])"
  apply(subgoal_tac "j∈nat")
  apply(rule natE,simp,subst apply_fun,rule sixp_perm_tc,simp add:sixp_sep_perm_def,simp+)+
  apply(subst apply_fun,rule sixp_perm_tc,simp add:sixp_sep_perm_def,simp+,drule ltD,auto)
  done

lemma (in forcing_data) sixp_sep: 
  assumes
    "φ ∈ formula" "arity(φ)≤6" "a1∈M" "a2∈M" "a3∈M" "a4∈M" "a5∈M"
  shows 
    "separation(##M,λx. sats(M,φ,[x,a1,a2,a3,a4,a5]))"
proof -
  let 
    ?f="sixp_sep_perm"
  let
    ?φ'="ren(φ)`6`9`?f"
  from assms have
    "arity(?φ')≤9" "?φ' ∈ formula"
    using sixp_perm_tc ren_arity ren_tc by simp_all
  then have
    "(∀v∈M. separation(##M,λx. sats(M,tupling_fm_5p(?φ'),[x,v])))"
    using separation_ax arity_tup5p_leq by simp
  then have
    Eq1: "(∀v∈M. separation
             (##M, λx. ∀B3∈M. ∀B2∈M. ∀B1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
                    ∀A1∈M. pair(##M, A4, A5, B1) ∧ pair(##M, A3, B1, B2) ∧ pair(##M, A2, B2, B3) ∧ 
                            pair(##M, A1, B3, v) ⟶
               sats(M,?φ',[A1,A2,A3,A4,A5,B1,B2,B3,x,v])))" 
    (is "∀v∈M. separation(_ , λx. ?P(x,v))")
    unfolding separation_def tupling_fm_5p_def by (simp del: pair_abs)
  {
    fix B1 B2 B3 A1 A2 A3 A4 A5 x v
    assume
      "x∈M" "v∈M"
      "B3∈M" "B2∈M" "B1∈M" "A5∈M" "A4∈M" "A3∈M" "A2∈M" "A1∈M"
    with assms have
      "sats(M,?φ',[A1,A2,A3,A4,A5,B1,B2,B3,x,v]) ⟷ sats(M,φ,[x,A1,A2,A3,A4,A5])" 
      (is "sats(_,_,?env1) ⟷ sats(_,_,?env2)")
      using sats_iff_sats_ren[of φ 6 9 ?env2 M ?env1 ?f] sixp_perm_tc sixp_perm_env [of _ _ _ _ _ _ "M"]  
      by auto
  }
  then have
    Eq2: "x∈M ⟹ v∈M ⟹ ?P(x,v) ⟷ (∀B3∈M. ∀B2∈M. ∀B1∈M. ∀A5∈M. ∀A4∈M. ∀A3∈M. ∀A2∈M.
                    ∀A1∈M. pair(##M, A4, A5, B1) ∧ pair(##M, A3, B1, B2) ∧ pair(##M, A2, B2, B3) ∧ 
                            pair(##M, A1, B3, v) ⟶
               sats(M,φ,[x,A1,A2,A3,A4,A5]))" (is "_ ⟹ _⟹ _ ⟷ ?Q(x,v)") for x v 
    by (simp del: pair_abs)
  define PP where "PP ≡ ?P"
  define QQ where "QQ ≡ ?Q"
  from Eq2 have
      "x∈M ⟹ v∈M ⟹ PP(x,v) ⟷ QQ(x,v)" for x v 
      unfolding PP_def QQ_def .
  then have
    "v∈M ⟹ 
     (∀z[##M]. ∃y[##M]. ∀x[##M]. x ∈ y ⟷ x ∈ z ∧ PP(x,v)) ⟷
     (∀z[##M]. ∃y[##M]. ∀x[##M]. x ∈ y ⟷ x ∈ z ∧ QQ(x,v))" for v by (simp del: pair_abs)
  with Eq1 have
    "(∀v∈M. separation (##M, λx. QQ(x,v)))"
    unfolding separation_def PP_def by (simp del: pair_abs)
  with assms show ?thesis unfolding QQ_def using tupling_sep_5p_rel2  by simp
qed 
  
(* Instance of Replacement for M_basic *)
  
(* funspace_succ_replacement:
     "M(n) ==>
      strong_replacement(M, λp z. ∃f[M]. ∃b[M]. ∃nb[M]. ∃cnbf[M].
                pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
                upair(M,cnbf,cnbf,z))" 
*)
definition 
  is_cons_fm :: "i ⇒ i ⇒ i ⇒ i" where
 "is_cons_fm(a,b,z) == Exists(And(upair_fm(succ(a),succ(a),0),union_fm(0,succ(b),succ(z))))"

lemma is_cons_type [TC]:
     "[| x ∈ nat; y ∈ nat; z ∈ nat |] ==> is_cons_fm(x,y,z) ∈ formula"
by (simp add: is_cons_fm_def)

lemma is_cons_fm [simp] :
  "⟦ a ∈ nat ; b ∈ nat ; z ∈ nat ; env ∈ list(A) ⟧ ⟹ 
    sats(A,is_cons_fm(a,b,z),env) ⟷ 
    is_cons(##A,nth(a,env),nth(b,env),nth(z,env))"
  by (simp add: is_cons_fm_def is_cons_def)

definition 
  funspace_succ_fm :: "i" where
  "funspace_succ_fm == 
    Exists(Exists(Exists(Exists(And(pair_fm(3,2,4),And(pair_fm(6,2,1),
        And(is_cons_fm(1,3,0),upair_fm(0,0,5))))))))"
  
lemma funspace_succ_fm_type [TC] : 
  "funspace_succ_fm ∈ formula"
  by (simp add: funspace_succ_fm_def)

lemma [simp] : "arity(funspace_succ_fm) = 3" 
  by (simp add: funspace_succ_fm_def pair_fm_def upair_fm_def is_cons_fm_def 
                    union_fm_def Un_commute nat_union_abs1)

lemma (in forcing_data) funspace_succ_rep_intf :
  assumes
      "n∈M"
  shows
     "strong_replacement(##M,
          λp z. ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M.
                pair(##M,f,b,p) & pair(##M,n,b,nb) & is_cons(##M,nb,f,cnbf) &
                upair(##M,cnbf,cnbf,z))"
proof -
  from replacement_ax have 
       "(∀a∈M. strong_replacement(##M,λx y. sats(M,funspace_succ_fm,[x,y,a])))"      
    by simp
  then have
    "(∀n∈M. strong_replacement(##M,
          λp z. ∃f∈M. ∃b∈M. ∃nb∈M. ∃cnbf∈M.
                pair(##M,f,b,p) & pair(##M,n,b,nb) & is_cons(##M,nb,f,cnbf) &
                upair(##M,cnbf,cnbf,z)))"
    unfolding funspace_succ_fm_def strong_replacement_def univalent_def by (simp del: pair_abs)
  with ‹n∈M› show ?thesis by simp
qed


(* Interface with M_basic *)
  
lemmas (in forcing_data) M_basic_sep_instances = 
                inter_sep_intf diff_sep_intf cartprod_sep_intf
                image_sep_intf converse_sep_intf restrict_sep_intf
                pred_sep_intf memrel_sep_intf comp_sep_intf is_recfun_sep_intf
  
sublocale forcing_data ⊆ M_basic "##M"
  apply (insert trans_M zero_in_M power_ax)
  apply (rule M_basic.intro,rule mtriv)
  apply (rule M_basic_axioms.intro)
  apply (insert M_basic_sep_instances funspace_succ_rep_intf)
  apply (simp_all)
done
  
end