Theory Internal_ZFC_Axioms

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

begin

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

synthesize "ZF_union" from_schematic ZF_union_auto
notation ZF_union_fm (⋅Union Ax⋅)

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" from_schematic ZF_power_auto
notation ZF_power_fm (⋅Powerset Ax⋅)

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

synthesize "ZF_pairing" from_schematic ZF_pairing_auto
notation ZF_pairing_fm (⋅Pairing⋅)

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

synthesize "ZF_foundation" from_schematic ZF_foundation_auto
notation ZF_foundation_fm (⋅Foundation⋅)

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

synthesize "ZF_extensionality" from_schematic ZF_extensionality_auto
notation ZF_extensionality_fm (⋅Extensionality⋅)

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

synthesize "ZF_infinity" from_schematic ZF_infinity_auto
notation ZF_infinity_fm (⋅Infinity⋅)

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

synthesize "ZF_choice" from_schematic ZF_choice_auto
notation ZF_choice_fm (⋅AC⋅)

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  {⋅Extensionality⋅, ⋅Foundation⋅, ⋅Pairing⋅,
              ⋅Union Ax⋅, ⋅Infinity⋅, ⋅Powerset Ax⋅}"

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)  (⋅∀(⋅∃(⋅∀0  1  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" (⋅Separation'(_')⋅) 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, []  ⋅Separation(φ)⋅)
   
   (envlist(M). arity(φ)  1 +ω length(env) 
      separation(##M,λx. M, [x] @ env  φ))"
proof (intro iffI ballI impI)
  let ?n="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) = pred(arity(φ))"
    using list_split[OF arity(φ)  succ(_) env_] by force
  moreover from φ_
  have "arity(φ)  succ(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="pred(arity(φ))"
  assume asm:"envlist(M). arity(φ)  1 +ω length(env) 
    separation(##M, λx. M, [x] @ env  φ)"
  {
    fix some
    assume "somelist(M)" "length(some) = 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 𝟭 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" 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" (⋅Replacement'(_')⋅) 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, []  ⋅Replacement(φ)⋅)  (env. replacement_assm(M,env,φ))"
  unfolding replacement_assm_def
proof (intro iffI allI impI)
  let ?n="pred(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) = pred(pred(arity(φ)))"
    using list_split[OF pred(_)  _ env_] by auto
  moreover
  note φ_
  moreover from this
  have "arity(φ)  succ(succ(pred(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="pred(pred(arity(φ)))"
  assume asm:"env. φ  formula 
          env  list(M)  arity(φ)  2 +ω length(env) 
    strong_replacement(##M, λx y. M, [x, y] @ env  φ)"
  {
    fix some
    assume "somelist(M)" "length(some) = pred(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_schemes :: "i" where
  "ZF_schemes  {⋅Separation(p)⋅ . p  formula }  {⋅Replacement(p)⋅ . p  formula }"

lemma Un_subset_formula [TC]: "Aformula  Bformula  AB  formula"
  by auto

lemma ZF_schemes_subset_formula [TC]: "ZF_schemes  formula"
  unfolding ZF_schemes_def by auto

lemma ZF_fin_subset_formula [TC]: "ZF_fin  formula"
  unfolding ZF_fin_def by simp

definition
  ZF :: "i" where
  "ZF  ZF_schemes  ZF_fin"

lemma ZF_subset_formula [TC]: "ZF  formula"
  unfolding ZF_def by auto

definition
  ZFC :: "i" where
  "ZFC  ZF  {⋅AC⋅}"

definition
  ZF_minus_P :: "i" where
  "ZF_minus_P  ZF - { ⋅Powerset Ax⋅ }"

definition
  Zermelo_fms :: "i" (⋅Z⋅) where
  "Zermelo_fms  ZF_fin  {⋅Separation(p)⋅ . p  formula }"

definition
  ZC :: "i" where
  "ZC  Zermelo_fms  {⋅AC⋅}"

lemma ZFC_subset_formula: "ZFC  formula"
  by (simp add:ZFC_def Un_subset_formula)

text‹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 satT_mono: "A  Φ  Ψ  Φ  A  Ψ"
  by blast

lemma satT_Un_iff: "M  Φ  Ψ  M  Φ  M  Ψ" by auto

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

lemma satT_ZF_imp_satT_Z: "M  ZF  M  ⋅Z⋅"
  unfolding ZF_def ZF_schemes_def Zermelo_fms_def ZF_fin_def by auto

lemma satT_ZFC_imp_satT_ZC: "M  ZFC  M  ZC"
  unfolding ZFC_def ZF_def ZF_schemes_def ZC_def Zermelo_fms_def by auto

lemma satT_Z_ZF_replacement_imp_satT_ZF: "N  ⋅Z⋅  N  {⋅Replacement(x)⋅ . x  formula}  N  ZF"
  unfolding ZF_def ZF_schemes_def Zermelo_fms_def ZF_fin_def by auto

lemma satT_ZC_ZF_replacement_imp_satT_ZFC: "N  ZC  N  {⋅Replacement(x)⋅ . x  formula}  N  ZFC"
  unfolding ZFC_def ZF_def ZF_schemes_def ZC_def Zermelo_fms_def  by auto

lemma ground_repl_fm_sub_ZF: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ  formula}  ZF"
   unfolding ZF_def ZF_schemes_def by auto

lemma ZF_replacement_fms_sub_ZFC: "{⋅Replacement(φ)⋅ . φ  formula}  ZFC"
   unfolding ZFC_def ZF_def ZF_schemes_def by auto

lemma ground_repl_fm_sub_ZFC: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ  formula}  ZFC"
   unfolding ZFC_def ZF_def ZF_schemes_def by auto

lemma ZF_replacement_ground_repl_fm_type: "{⋅Replacement(ground_repl_fm(φ))⋅ . φ  formula}  formula"
  by auto

end