Theory Internal_ZFC_Axioms

section‹The ZFC axioms, internalized›
theory Internal_ZFC_Axioms
  imports 
  Forcing_Data

begin

schematic_goal ZF_union_auto:
    "Union_ax(##A)  (A, []  ?zfunion)"
  unfolding Union_ax_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_union_fm" from_schematic ZF_union_auto

schematic_goal ZF_power_auto:
    "power_ax(##A)  (A, []  ?zfpow)"
  unfolding power_ax_def powerset_def subset_def
  by ((rule sep_rules | simp)+)

synthesize "ZF_power_fm" from_schematic ZF_power_auto

schematic_goal ZF_pairing_auto:
    "upair_ax(##A)  (A, []  ?zfpair)"
  unfolding upair_ax_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_pairing_fm" from_schematic ZF_pairing_auto

schematic_goal ZF_foundation_auto:
    "foundation_ax(##A)  (A, []  ?zfpow)"
  unfolding foundation_ax_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_foundation_fm" from_schematic ZF_foundation_auto

schematic_goal ZF_extensionality_auto:
    "extensionality(##A)  (A, []  ?zfpow)"
  unfolding extensionality_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_extensionality_fm" from_schematic ZF_extensionality_auto

schematic_goal ZF_infinity_auto:
    "infinity_ax(##A)  (A, []  ((i,j,h)))"
  unfolding infinity_ax_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_infinity_fm" from_schematic ZF_infinity_auto

schematic_goal ZF_choice_auto:
    "choice_ax(##A)  (A, []  ((i,j,h)))"
  unfolding choice_ax_def 
  by ((rule sep_rules | simp)+)

synthesize "ZF_choice_fm" from_schematic ZF_choice_auto

syntax
  "_choice" :: "i"  ("AC")
translations
  "AC"  "CONST ZF_choice_fm"

lemmas ZFC_fm_defs = ZF_extensionality_fm_def ZF_foundation_fm_def ZF_pairing_fm_def
              ZF_union_fm_def ZF_infinity_fm_def ZF_power_fm_def ZF_choice_fm_def

lemmas ZFC_fm_sats = ZF_extensionality_auto ZF_foundation_auto ZF_pairing_auto
              ZF_union_auto ZF_infinity_auto ZF_power_auto ZF_choice_auto

definition
  ZF_fin :: "i" where
  "ZF_fin  { ZF_extensionality_fm, ZF_foundation_fm, ZF_pairing_fm,
              ZF_union_fm, ZF_infinity_fm, ZF_power_fm }"

definition
  ZFC_fin :: "i" where
  "ZFC_fin  ZF_fin  {ZF_choice_fm}"

lemma ZFC_fin_type : "ZFC_fin  formula"
  unfolding ZFC_fin_def ZF_fin_def ZFC_fm_defs by (auto)

subsection‹The Axiom of Separation, internalized›
lemma iterates_Forall_type [TC]:
      " n  nat; p  formula   Forall^n(p)  formula"
  by (induct set:nat, auto)

lemma last_init_eq :
  assumes "l  list(A)" "length(l) = succ(n)"
  shows " aA. l'list(A). l = l'@[a]"
proof-
  from l_ length(_) = _
  have "rev(l)  list(A)" "length(rev(l)) = succ(n)"
    by simp_all
  then
  obtain a l' where "aA" "l'list(A)" "rev(l) = Cons(a,l')"
    by (cases;simp)
  then
  have "l = rev(l') @ [a]" "rev(l')  list(A)"
    using rev_rev_ident[OF l_] by auto
  with a_
  show ?thesis by blast
qed

lemma take_drop_eq :
  assumes "llist(M)"
  shows " n . n < succ(length(l))  l = take(n,l) @ drop(n,l)"
  using llist(M)
proof induct
  case Nil
  then show ?case by auto
next
  case (Cons a l)
  then show ?case
  proof -
    {
      fix i
      assume "i<succ(succ(length(l)))"
      with llist(M)
      consider (lt) "i = 0" | (eq) "knat. i = succ(k)  k < succ(length(l))"
        using llist(M)  le_natI nat_imp_quasinat
        by (cases rule:nat_cases[of i];auto)
      then
      have "take(i,Cons(a,l)) @ drop(i,Cons(a,l)) = Cons(a,l)"
        using Cons
        by (cases;auto)
    }
    then show ?thesis using Cons by auto
  qed
qed

lemma list_split :
assumes "n  succ(length(rest))" "rest  list(M)"
shows  "relist(M). stlist(M). rest = re @ st  length(re) = pred(n)"
proof -
  from assms
  have "pred(n)  length(rest)"
    using pred_mono[OF _ n_] pred_succ_eq by auto
  with rest_
  have "pred(n)nat" "rest = take(pred(n),rest) @ drop(pred(n),rest)" (is "_ = ?re @ ?st")
    using take_drop_eq[OF rest_] le_natI by auto
  then
  have "length(?re) = pred(n)" "?relist(M)" "?stlist(M)"
    using length_take[rule_format,OF _ pred(n)_] pred(n)  _ rest_
    unfolding min_def
    by auto
  then
  show ?thesis
    using rev_bexI[of _ _ "λ re. stlist(M). rest = re @ st  length(re) = pred(n)"]
      length(?re) = _ rest = _
    by auto
qed

lemma sats_nForall:
  assumes
    "φ  formula"
  shows
    "nnat  ms  list(M) 
       M, ms  (Forall^n(φ)) 
       (rest  list(M). length(rest) = n  M, rest @ ms  φ)"
proof (induct n arbitrary:ms set:nat)
  case 0
  with assms
  show ?case by simp
next
  case (succ n)
  have "(restlist(M). length(rest) = succ(n)  P(rest,n)) 
        (tM. reslist(M). length(res) = n  P(res @ [t],n))"
    if "nnat" for n P
    using that last_init_eq by force
  from this[of _ "λrest _. (M, rest @ ms  φ)"] nnat
  have "(restlist(M). length(rest) = succ(n)  M, rest @ ms  φ) 
        (tM. reslist(M). length(res) = n   M, (res @ [t]) @ ms  φ)"
    by simp
    with assms succ(1,3) succ(2)[of "Cons(_,ms)"]
  show ?case
    using arity_sats_iff[of φ _ M "Cons(_, ms @ _)"] app_assoc
    by (simp)
qed

definition
  sep_body_fm :: "i  i" where
  "sep_body_fm(p)  Forall(Exists(Forall(
                           Iff(Member(0,1),And(Member(0,2),
                                    incr_bv1^2(p))))))"

lemma sep_body_fm_type [TC]: "p  formula  sep_body_fm(p)  formula"
  by (simp add: sep_body_fm_def)

lemma sats_sep_body_fm: 
  assumes
    "φ  formula" "mslist(M)" "restlist(M)"
  shows
    "M, rest @ ms  sep_body_fm(φ)  
     separation(##M,λx. M, [x] @ rest @ ms  φ)"
  using assms formula_add_params1[of _ 2 _ _ "[_,_]" ]
  unfolding sep_body_fm_def separation_def by simp

definition
  ZF_separation_fm :: "i  i" where
  "ZF_separation_fm(p)  Forall^(pred(arity(p)))(sep_body_fm(p))"

lemma ZF_separation_fm_type [TC]: "p  formula  ZF_separation_fm(p)  formula"
  by (simp add: ZF_separation_fm_def)

lemma sats_ZF_separation_fm_iff:
  assumes
    "φformula"
  shows
  "(M, []  (ZF_separation_fm(φ)))
   
   (envlist(M). arity(φ)  1 #+ length(env)  
      separation(##M,λx. M, [x] @ env  φ))"
proof (intro iffI ballI impI)
  let ?n="Arith.pred(arity(φ))"
  fix env
  assume "M, []  ZF_separation_fm(φ)" 
  assume "arity(φ)  1 #+ length(env)" "envlist(M)"
  moreover from this
  have "arity(φ)  succ(length(env))" by simp
  then
  obtain some rest where "somelist(M)" "restlist(M)" 
    "env = some @ rest" "length(some) = Arith.pred(arity(φ))"
    using list_split[OF arity(φ)  succ(_) env_] by force
  moreover from φ_
  have "arity(φ)  succ(Arith.pred(arity(φ)))"
   using succpred_leI by simp
  moreover
  note assms
  moreover 
  assume "M, []  ZF_separation_fm(φ)" 
  moreover from calculation
  have "M, some  sep_body_fm(φ)"
    using sats_nForall[of "sep_body_fm(φ)" ?n]
    unfolding ZF_separation_fm_def by simp
  ultimately
  show "separation(##M, λx. M, [x] @ env  φ)"
    unfolding ZF_separation_fm_def
    using sats_sep_body_fm[of φ "[]" M some]
      arity_sats_iff[of φ rest M "[_] @ some"]
      separation_cong[of "##M" "λx. M, Cons(x, some @ rest)  φ" _ ]
    by simp
next ― ‹almost equal to the previous implication›
  let ?n="Arith.pred(arity(φ))"
  assume asm:"envlist(M). arity(φ)  1 #+ length(env)  
    separation(##M, λx. M, [x] @ env  φ)"
  {
    fix some
    assume "somelist(M)" "length(some) = Arith.pred(arity(φ))"
    moreover
    note φ_
    moreover from calculation
    have "arity(φ)  1 #+ length(some)" 
      using le_trans[OF succpred_leI] succpred_leI by simp
    moreover from calculation and asm
    have "separation(##M, λx. M, [x] @ some  φ)" by blast
    ultimately
    have "M, some  sep_body_fm(φ)" 
    using sats_sep_body_fm[of φ "[]" M some]
      arity_sats_iff[of φ _ M "[_,_] @ some"]
      strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ _))  φ" _ ]
    by simp
  }
  with φ_
  show "M, []  ZF_separation_fm(φ)"
    using sats_nForall[of "sep_body_fm(φ)" ?n]
    unfolding ZF_separation_fm_def
    by simp
qed

subsection‹The Axiom of Replacement, internalized›
schematic_goal sats_univalent_fm_auto:
  assumes 
    (*    Q_iff_sats:"⋀a b z env aa bb. nth(a,Cons(z,env)) = aa ⟹ nth(b,Cons(z,env)) = bb ⟹ z∈A 
          ⟹ aa ∈ A ⟹ bb ∈ A ⟹ env∈ list(A) ⟹ 
                 Q(aa,bb) ⟷ (A, Cons(z,env) ⊨ (Q_fm(a,b)))" ― ‹using only one formula› *)
    Q_iff_sats:"x y z. x  A  y  A  zA  
                 Q(x,z)  (A,Cons(z,Cons(y,Cons(x,env)))  Q1_fm)"
       "x y z. x  A  y  A  zA  
                 Q(x,y)  (A,Cons(z,Cons(y,Cons(x,env)))  Q2_fm)"
    and 
    asms: "nth(i,env) = B" "i  nat" "env  list(A)"
  shows
    "univalent(##A,B,Q)  A,env  ?ufm(i)"
  unfolding univalent_def 
  by (insert asms; (rule sep_rules Q_iff_sats | simp)+)
  
synthesize_notc "univalent_fm" from_schematic sats_univalent_fm_auto

lemma univalent_fm_type [TC]: "q1 formula  q2formula  inat  
  univalent_fm(q2,q1,i) formula"
  by (simp add:univalent_fm_def)

lemma sats_univalent_fm :
  assumes
    Q_iff_sats:"x y z. x  A  y  A  zA  
                 Q(x,z)  (A,Cons(z,Cons(y,Cons(x,env)))  Q1_fm)"
       "x y z. x  A  y  A  zA  
                 Q(x,y)  (A,Cons(z,Cons(y,Cons(x,env)))  Q2_fm)"
    and 
    asms: "nth(i,env) = B" "i  nat" "env  list(A)"
  shows
    "A,env  univalent_fm(Q1_fm,Q2_fm,i)  univalent(##A,B,Q)"
  unfolding univalent_fm_def using asms sats_univalent_fm_auto[OF Q_iff_sats] by simp

definition
  swap_vars :: "ii" where
  "swap_vars(φ)  
      Exists(Exists(And(Equal(0,3),And(Equal(1,2),iterates(λp. incr_bv(p)`2 , 2, φ)))))" 

lemma swap_vars_type[TC] :
  "φformula  swap_vars(φ) formula" 
  unfolding swap_vars_def by simp

lemma sats_swap_vars :
  "[x,y] @ env  list(M)  φformula  
    M, [x,y] @ env  swap_vars(φ) M,[y,x] @ env  φ"
  unfolding swap_vars_def
  using sats_incr_bv_iff [of _ _ M _ "[y,x]"] by simp

definition
  univalent_Q1 :: "i  i" where
  "univalent_Q1(φ)  incr_bv1(swap_vars(φ))"

definition
  univalent_Q2 :: "i  i" where
  "univalent_Q2(φ)  incr_bv(swap_vars(φ))`0"

lemma univalent_Qs_type [TC]: 
  assumes "φformula"
  shows "univalent_Q1(φ)  formula" "univalent_Q2(φ)  formula"
  unfolding univalent_Q1_def univalent_Q2_def using assms by simp_all

lemma sats_univalent_fm_assm:
  assumes 
    "x  A" "y  A" "zA" "env list(A)" "φ  formula"
  shows 
    "(A, ([x,z] @ env)  φ)  (A, Cons(z,Cons(y,Cons(x,env)))  (univalent_Q1(φ)))"
    "(A, ([x,y] @ env)  φ)  (A, Cons(z,Cons(y,Cons(x,env)))  (univalent_Q2(φ)))"
  unfolding univalent_Q1_def univalent_Q2_def
  using 
    sats_incr_bv_iff[of _ _ A _ "[]"] ― ‹simplifies iterates of termλx. incr_bv(x)`0
    sats_incr_bv1_iff[of _ "Cons(x,env)" A z y] 
    sats_swap_vars  assms 
   by simp_all

definition
  rep_body_fm :: "i  i" where
  "rep_body_fm(p)  Forall(Implies(
        univalent_fm(univalent_Q1(incr_bv(p)`2),univalent_Q2(incr_bv(p)`2),0),
        Exists(Forall(
          Iff(Member(0,1),Exists(And(Member(0,3),incr_bv(incr_bv(p)`2)`2)))))))"

lemma rep_body_fm_type [TC]: "p  formula  rep_body_fm(p)  formula"
  by (simp add: rep_body_fm_def)

lemmas ZF_replacement_simps = formula_add_params1[of φ 2 _ M "[_,_]" ]
  sats_incr_bv_iff[of _ _ M _ "[]"] ― ‹simplifies iterates of termλx. incr_bv(x)`0
  sats_incr_bv_iff[of _ _ M _ "[_,_]"]― ‹simplifies termλx. incr_bv(x)`2
  sats_incr_bv1_iff[of _ _ M] sats_swap_vars for φ M

lemma sats_rep_body_fm:
  assumes
    "φ  formula" "mslist(M)" "restlist(M)"
  shows
    "M, rest @ ms  rep_body_fm(φ)  
     strong_replacement(##M,λx y. M, [x,y] @ rest @ ms  φ)"
  using assms ZF_replacement_simps 
  unfolding rep_body_fm_def strong_replacement_def univalent_def
  unfolding univalent_fm_def univalent_Q1_def univalent_Q2_def
  by simp

definition
  ZF_replacement_fm :: "i  i" where
  "ZF_replacement_fm(p)  Forall^(pred(pred(arity(p))))(rep_body_fm(p))"

lemma ZF_replacement_fm_type [TC]: "p  formula  ZF_replacement_fm(p)  formula"
  by (simp add: ZF_replacement_fm_def)

lemma sats_ZF_replacement_fm_iff:
  assumes
    "φformula"
  shows
  "(M, []  (ZF_replacement_fm(φ)))
   
   (envlist(M). arity(φ)  2 #+ length(env)  
      strong_replacement(##M,λx y. M,[x,y] @ env  φ))"
proof (intro iffI ballI impI)
  let ?n="Arith.pred(Arith.pred(arity(φ)))"
  fix env
  assume "M, []  ZF_replacement_fm(φ)" "arity(φ)  2 #+ length(env)" "envlist(M)"
  moreover from this
  have "arity(φ)  succ(succ(length(env)))" by (simp)
  moreover from calculation 
  have "pred(arity(φ))  succ(length(env))"
    using pred_mono[OF _ arity(φ)succ(_)] pred_succ_eq by simp
  moreover from calculation
  obtain some rest where "somelist(M)" "restlist(M)" 
    "env = some @ rest" "length(some) = Arith.pred(Arith.pred(arity(φ)))" 
    using list_split[OF pred(_)  _ env_] by auto
  moreover
  note φ_
  moreover from this
  have "arity(φ)  succ(succ(Arith.pred(Arith.pred(arity(φ)))))"
    using le_trans[OF succpred_leI] succpred_leI by simp
  moreover from calculation
  have "M, some  rep_body_fm(φ)"
    using sats_nForall[of "rep_body_fm(φ)" ?n]
    unfolding ZF_replacement_fm_def
    by simp
  ultimately
  show "strong_replacement(##M, λx y. M, [x, y] @ env  φ)"
    using sats_rep_body_fm[of φ "[]" M some]
      arity_sats_iff[of φ rest M "[_,_] @ some"]
      strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ rest))  φ" _ ]
    by simp
next ― ‹almost equal to the previous implication›
  let ?n="Arith.pred(Arith.pred(arity(φ)))"
  assume asm:"envlist(M). arity(φ)  2 #+ length(env)  
    strong_replacement(##M, λx y. M, [x, y] @ env  φ)"
  {
    fix some
    assume "somelist(M)" "length(some) = Arith.pred(Arith.pred(arity(φ)))"
    moreover
    note φ_
    moreover from calculation
    have "arity(φ)  2 #+ length(some)" 
      using le_trans[OF succpred_leI] succpred_leI by simp
    moreover from calculation and asm
    have "strong_replacement(##M, λx y. M, [x, y] @ some  φ)" by blast
    ultimately
    have "M, some  rep_body_fm(φ)" 
    using sats_rep_body_fm[of φ "[]" M some]
      arity_sats_iff[of φ _ M "[_,_] @ some"]
      strong_replacement_cong[of "##M" "λx y. M, Cons(x, Cons(y, some @ _))  φ" _ ]
    by simp
  }
  with φ_
  show "M, []  ZF_replacement_fm(φ)"
    using sats_nForall[of "rep_body_fm(φ)" ?n]
    unfolding ZF_replacement_fm_def
    by simp
qed

definition
  ZF_inf :: "i" where
  "ZF_inf  {ZF_separation_fm(p) . p  formula }  {ZF_replacement_fm(p) . p  formula }"
              
lemma Un_subset_formula: "Aformula  Bformula  AB  formula"
  by auto
  
lemma ZF_inf_subset_formula : "ZF_inf  formula"
  unfolding ZF_inf_def by auto
    
definition
  ZFC :: "i" where
  "ZFC  ZF_inf  ZFC_fin"

definition
  ZF :: "i" where
  "ZF  ZF_inf  ZF_fin"

definition 
  ZF_minus_P :: "i" where
  "ZF_minus_P  ZF - { ZF_power_fm }"

lemma ZFC_subset_formula: "ZFC  formula"
  by (simp add:ZFC_def Un_subset_formula ZF_inf_subset_formula ZFC_fin_type)
  
txt‹Satisfaction of a set of sentences›
definition
  satT :: "[i,i]  o"  ("_  _" [36,36] 60) where
  "A  Φ    φΦ. (A,[]  φ)"

lemma satTI [intro!]: 
  assumes "φ. φΦ  A,[]  φ"
  shows "A  Φ"
  using assms unfolding satT_def by simp

lemma satTD [dest] :"A  Φ   φΦ  A,[]  φ"
  unfolding satT_def by simp

lemma sats_ZFC_iff_sats_ZF_AC: 
  "(N  ZFC)  (N  ZF)  (N, []  AC)"
    unfolding ZFC_def ZFC_fin_def ZF_def by auto

lemma M_ZF_iff_M_satT: "M_ZF(M)  (M  ZF)"
proof
  assume "M  ZF"
  then
  have fin: "upair_ax(##M)" "Union_ax(##M)" "power_ax(##M)"
    "extensionality(##M)" "foundation_ax(##M)" "infinity_ax(##M)"
    unfolding ZF_def ZF_fin_def ZFC_fm_defs satT_def
    using ZFC_fm_sats[of M] by simp_all
  {
    fix φ env
    assume "φ  formula" "envlist(M)" 
    moreover from M  ZF
    have "pformula. (M, []  (ZF_separation_fm(p)))" 
         "pformula. (M, []  (ZF_replacement_fm(p)))"
      unfolding ZF_def ZF_inf_def by auto
    moreover from calculation
    have "arity(φ)  succ(length(env))  separation(##M, λx. (M, Cons(x, env)  φ))"
      "arity(φ)  succ(succ(length(env)))  strong_replacement(##M,λx y. sats(M,φ,Cons(x,Cons(y, env))))"
      using sats_ZF_separation_fm_iff sats_ZF_replacement_fm_iff by simp_all  
  }
  with fin
  show "M_ZF(M)"
    unfolding M_ZF_def by simp
next
  assume M_ZF(M)
  then
  have "M  ZF_fin" 
    unfolding M_ZF_def ZF_fin_def ZFC_fm_defs satT_def
    using ZFC_fm_sats[of M] by blast
  moreover from M_ZF(M)
  have "pformula. (M, []  (ZF_separation_fm(p)))" 
       "pformula. (M, []  (ZF_replacement_fm(p)))"
    unfolding M_ZF_def using sats_ZF_separation_fm_iff 
      sats_ZF_replacement_fm_iff by simp_all
  ultimately
  show "M  ZF"
    unfolding ZF_def ZF_inf_def by blast
qed

end