Theory Arities

section‹Arities of internalized formulas›
theory Arities
  imports
    Discipline_Base
begin

lemmas FOL_arities [simp del, arity] = arity_And arity_Or arity_Implies arity_Iff arity_Exists

declare pred_Un_distrib[arity_aux]

context
  notes FOL_arities[simp]
begin

lemma arity_upair_fm [arity] : "  t1nat ; t2nat ; upnat   
  arity(upair_fm(t1,t2,up)) =  {succ(t1),succ(t2),succ(up)}"
  unfolding  upair_fm_def
  using union_abs1 union_abs2 pred_Un
  by auto

end

lemma Un_trasposition_aux1: "r  s  r = r  s" by auto

lemma Un_trasposition_aux2:
  "r  (s  (r  u))= r  (s  u)"
  "r  (s  (t  (r  u)))= r  (s  (t  u))" by auto

text‹We use the previous lemmas to guide automatic arity calculations.›

context
  notes Un_assoc[symmetric,simp] Un_trasposition_aux1[simp]
begin

arity_theorem for "pair_fm"
arity_theorem for "composition_fm"
arity_theorem for "domain_fm"
arity_theorem for "range_fm"
arity_theorem for "union_fm"
arity_theorem for "image_fm"
arity_theorem for "pre_image_fm"
arity_theorem for "big_union_fm"
arity_theorem for "fun_apply_fm"
arity_theorem for "field_fm"
arity_theorem for "empty_fm"
arity_theorem for "cons_fm"
arity_theorem for "succ_fm"
arity_theorem for "number1_fm"
arity_theorem for "function_fm"
arity_theorem for "relation_fm"
arity_theorem for "restriction_fm"
arity_theorem for "typed_function_fm"
arity_theorem for "subset_fm"
arity_theorem for "transset_fm"
arity_theorem for "ordinal_fm"
arity_theorem for "limit_ordinal_fm"
arity_theorem for "finite_ordinal_fm"
arity_theorem for "omega_fm"
arity_theorem for "cartprod_fm"
arity_theorem for "singleton_fm"
arity_theorem for "Memrel_fm"
arity_theorem for "quasinat_fm"

end ― ‹context›

context
  notes FOL_arities[simp]
begin

lemma arity_is_recfun_fm [arity]:
  "pformula ; vnat ; nnat; Znat;inat   arity(p) = i 
  arity(is_recfun_fm(p,v,n,Z)) = succ(v)  succ(n)  succ(Z)  (pred^4(i))"
  unfolding is_recfun_fm_def
  using arity_upair_fm arity_pair_fm arity_pre_image_fm arity_restriction_fm
    union_abs2 pred_Un_distrib
  by auto

lemma arity_is_wfrec_fm [arity]:
  "pformula ; vnat ; nnat; Znat ; inat  arity(p) = i 
    arity(is_wfrec_fm(p,v,n,Z)) = succ(v)  succ(n)  succ(Z)  (pred^5(i))"
  unfolding is_wfrec_fm_def
  using arity_succ_fm  arity_is_recfun_fm
    union_abs2 pred_Un_distrib
  by auto

lemma arity_is_nat_case_fm [arity]:
  "pformula ; vnat ; nnat; Znat; inat  arity(p) = i 
    arity(is_nat_case_fm(v,p,n,Z)) = succ(v)  succ(n)  succ(Z)  pred(pred(i))"
  unfolding is_nat_case_fm_def
  using arity_succ_fm arity_empty_fm arity_quasinat_fm
    union_abs2 pred_Un_distrib
  by auto

lemma arity_iterates_MH_fm [arity]:
  assumes "isFformula" "vnat" "nnat" "gnat" "znat" "inat"
    "arity(isF) = i"
  shows "arity(iterates_MH_fm(isF,v,n,g,z)) =
           succ(v)  succ(n)  succ(g)  succ(z)  (pred^4(i))"
proof -
  let  = "(⋅∃g +ω 3`2 is 0  (⋅∀0 = 2  isF⋅)⋅)"
  let ?ar = "(g +ω 3)  pred(pred(i))"
  from assms
  have "arity() =?ar" "formula"
    using arity_fun_apply_fm
      union_abs1 union_abs2 pred_Un_distrib succ_Un_distrib Un_assoc[symmetric]
    by simp_all
  then
  show ?thesis
    unfolding iterates_MH_fm_def
    using arity_is_nat_case_fm[OF _ _ _ _ _ arity() = ?ar] assms pred_succ_eq pred_Un_distrib
    by auto
qed

lemma arity_is_iterates_fm [arity]:
  assumes "pformula" "vnat" "nnat" "Znat" "inat"
    "arity(p) = i"
  shows "arity(is_iterates_fm(p,v,n,Z)) = succ(v)  succ(n)  succ(Z) 
          (pred^11(i))"
proof -
  let  = "iterates_MH_fm(p, 7+ωv, 2, 1, 0)"
  let  = "is_wfrec_fm(, 0, n +ω 2, Z +ω 2)"
  from v_
  have "arity() = (8+ωv)  (pred^4(i))" "formula"
    using assms arity_iterates_MH_fm union_abs2
    by simp_all
  then
  have "arity() = n +ω 3  (Z +ω 3)  (3+ωv)  (pred^9(i))"
    using assms arity_is_wfrec_fm[OF _ _ _ _ _ arity() = _] union_abs1 pred_Un_distrib
    by auto
  then
  show ?thesis
    unfolding is_iterates_fm_def
    using arity_Memrel_fm arity_succ_fm assms union_abs1 pred_Un_distrib
    by auto
qed

lemma arity_eclose_n_fm [arity]:
  assumes "Anat" "xnat" "tnat"
  shows "arity(eclose_n_fm(A,x,t)) = succ(A)  succ(x)  succ(t)"
proof -
  let  = "big_union_fm(1,0)"
  have "arity() = 2" "formula"
    using arity_big_union_fm union_abs2
    by auto
  with assms
  show ?thesis
    unfolding eclose_n_fm_def
    using arity_is_iterates_fm[OF _ _ _ _,of _ _ _ 2]
    by auto
qed

lemma arity_mem_eclose_fm [arity]:
  assumes "xnat" "tnat"
  shows "arity(mem_eclose_fm(x,t)) = succ(x)  succ(t)"
proof -
  let ="eclose_n_fm(x +ω 2, 1, 0)"
  from xnat
  have "arity() = x+ω3"
    using arity_eclose_n_fm union_abs2
    by simp
  with assms
  show ?thesis
    unfolding mem_eclose_fm_def
    using arity_finite_ordinal_fm union_abs2 pred_Un_distrib
    by simp
qed

lemma arity_is_eclose_fm [arity]:
  "xnat ; tnat  arity(is_eclose_fm(x,t)) = succ(x)  succ(t)"
  unfolding is_eclose_fm_def
  using arity_mem_eclose_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_Collect_fm [arity]:
  assumes "x  nat" "y  nat" "pformula"
  shows "arity(Collect_fm(x,p,y)) = succ(x)  succ(y)  pred(arity(p))"
  unfolding Collect_fm_def
  using assms pred_Un_distrib
  by auto

schematic_goal arity_least_fm':
  assumes
    "i  nat" "q  formula"
  shows
    "arity(least_fm(q,i))  ?ar"
  unfolding least_fm_def
  using assms pred_Un_distrib arity_And arity_Or arity_Neg arity_Implies arity_ordinal_fm
    arity_empty_fm Un_assoc[symmetric] Un_commute
  by auto

lemma arity_least_fm [arity]:
  assumes
    "i  nat" "q  formula"
  shows
    "arity(least_fm(q,i)) = succ(i)  pred(arity(q))"
  using assms arity_least_fm'
  by auto

lemma arity_Replace_fm [arity]:
  "pformula ; vnat ; nnat; inat  arity(p) = i 
    arity(Replace_fm(v,p,n)) = succ(n)  succ(v)  pred(pred(i))"
  unfolding Replace_fm_def
  using union_abs2 pred_Un_distrib
  by auto

lemma arity_lambda_fm [arity]:
  "pformula; vnat ; nnat; inat   arity(p) = i 
    arity(lambda_fm(p,v,n)) = succ(n)  (succ(v)  (pred^3(i)))"
  unfolding lambda_fm_def
  using arity_pair_fm pred_Un_distrib union_abs1 union_abs2
  by simp

lemma arity_transrec_fm [arity]:
  "pformula ; vnat ; nnat; inat  arity(p) = i 
     arity(is_transrec_fm(p,v,n)) = succ(v)  succ(n)  (pred^8(i))"
  unfolding is_transrec_fm_def
  using arity Un_assoc[symmetric] pred_Un_distrib
  by simp

lemma arity_wfrec_replacement_fm :
  "pformula ; vnat ; nnat; Znat ; inat  arity(p) = i 
    arity(Exists(And(pair_fm(1,0,2),is_wfrec_fm(p,v,n,Z))))
   = 2  v  n  Z  (pred^6(i))"
  unfolding is_wfrec_fm_def
  using arity_succ_fm  arity_is_recfun_fm union_abs2 pred_Un_distrib arity_pair_fm
  by auto

end ― ‹@{thm [source] FOL_arities}

declare arity_subset_fm [simp del] arity_ordinal_fm[simp del, arity] arity_transset_fm[simp del]

context
  notes Un_assoc[symmetric,simp] Un_trasposition_aux1[simp]
begin
arity_theorem for "rtran_closure_mem_fm"
arity_theorem for "rtran_closure_fm"
arity_theorem for "tran_closure_fm"
end

context
  notes Un_assoc[simp] Un_trasposition_aux2[simp]
begin
arity_theorem for "injection_fm"
arity_theorem for "surjection_fm"
arity_theorem for "bijection_fm"
arity_theorem for "order_isomorphism_fm"
end

arity_theorem for "Inl_fm"
arity_theorem for "Inr_fm"
arity_theorem for "pred_set_fm"

end