Theory Arities

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

lemma arity_upair_fm : "⟦  t1∈nat ; t2∈nat ; up∈nat  ⟧ ⟹ 
  arity(upair_fm(t1,t2,up)) = ⋃ {succ(t1),succ(t2),succ(up)}"
  unfolding  upair_fm_def
  using nat_union_abs1 nat_union_abs2 pred_Un   
  by auto


lemma arity_pair_fm : "⟦  t1∈nat ; t2∈nat ; p∈nat  ⟧ ⟹ 
  arity(pair_fm(t1,t2,p)) = ⋃ {succ(t1),succ(t2),succ(p)}"
  unfolding pair_fm_def 
  using arity_upair_fm nat_union_abs1 nat_union_abs2 pred_Un
  by auto

lemma arity_composition_fm :
  "⟦ r∈nat ; s∈nat ; t∈nat ⟧ ⟹ arity(composition_fm(r,s,t)) = ⋃ {succ(r), succ(s), succ(t)}"
  unfolding composition_fm_def    
  using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_domain_fm : 
    "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(domain_fm(r,z)) = succ(r) ∪ succ(z)"
  unfolding domain_fm_def 
  using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_range_fm : 
    "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(range_fm(r,z)) = succ(r) ∪ succ(z)"
  unfolding range_fm_def 
  using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_union_fm : 
  "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(union_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}"
  unfolding union_fm_def
  using  nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_image_fm : 
  "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(image_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}"
  unfolding image_fm_def
  using arity_pair_fm  nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_pre_image_fm : 
  "⟦ x∈nat ; y∈nat ; z∈nat ⟧ ⟹ arity(pre_image_fm(x,y,z)) = ⋃ {succ(x), succ(y), succ(z)}"
  unfolding pre_image_fm_def
  using arity_pair_fm  nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto


lemma arity_big_union_fm : 
  "⟦ x∈nat ; y∈nat ⟧ ⟹ arity(big_union_fm(x,y)) = succ(x) ∪ succ(y)"
  unfolding big_union_fm_def
  using nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_fun_apply_fm : 
  "⟦ x∈nat ; y∈nat ; f∈nat ⟧ ⟹ 
    arity(fun_apply_fm(f,x,y)) =  succ(f) ∪ succ(x) ∪ succ(y)"
  unfolding fun_apply_fm_def
  using arity_upair_fm arity_image_fm arity_big_union_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_field_fm : 
    "⟦ r∈nat ; z∈nat ⟧ ⟹ arity(field_fm(r,z)) = succ(r) ∪ succ(z)"
  unfolding field_fm_def 
  using arity_pair_fm arity_domain_fm arity_range_fm arity_union_fm 
    nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_empty_fm : 
    "⟦ r∈nat ⟧ ⟹ arity(empty_fm(r)) = succ(r)"
  unfolding empty_fm_def 
  using nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by simp

lemma arity_succ_fm :
  "⟦x∈nat;y∈nat⟧ ⟹ arity(succ_fm(x,y)) = succ(x) ∪ succ(y)"
  unfolding succ_fm_def cons_fm_def 
  using arity_upair_fm arity_union_fm nat_union_abs2 pred_Un_distrib
  by auto


lemma number1arity__fm : 
    "⟦ r∈nat ⟧ ⟹ arity(number1_fm(r)) = succ(r)"
  unfolding number1_fm_def 
  using arity_empty_fm arity_succ_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by simp


lemma arity_function_fm : 
    "⟦ r∈nat ⟧ ⟹ arity(function_fm(r)) = succ(r)"
  unfolding function_fm_def 
  using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by simp

lemma arity_relation_fm : 
    "⟦ r∈nat ⟧ ⟹ arity(relation_fm(r)) = succ(r)"
  unfolding relation_fm_def 
  using arity_pair_fm nat_union_abs1 nat_union_abs2 pred_Un_distrib
  by simp

lemma arity_restriction_fm : 
    "⟦ r∈nat ; z∈nat ; A∈nat ⟧ ⟹ arity(restriction_fm(A,z,r)) = succ(A) ∪ succ(r) ∪ succ(z)"
  unfolding restriction_fm_def 
  using arity_pair_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_typed_function_fm : 
  "⟦ x∈nat ; y∈nat ; f∈nat ⟧ ⟹ 
    arity(typed_function_fm(f,x,y)) = ⋃ {succ(f), succ(x), succ(y)}"
  unfolding typed_function_fm_def
  using arity_pair_fm arity_relation_fm arity_function_fm arity_domain_fm 
    nat_union_abs2 pred_Un_distrib
  by auto


lemma arity_subset_fm : 
  "⟦x∈nat ; y∈nat⟧ ⟹ arity(subset_fm(x,y)) = succ(x) ∪ succ(y)"
  unfolding subset_fm_def 
  using nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_transset_fm :
  "⟦x∈nat⟧ ⟹ arity(transset_fm(x)) = succ(x)"
  unfolding transset_fm_def 
  using arity_subset_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_ordinal_fm :
  "⟦x∈nat⟧ ⟹ arity(ordinal_fm(x)) = succ(x)"
  unfolding ordinal_fm_def 
  using arity_transset_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_limit_ordinal_fm :
  "⟦x∈nat⟧ ⟹ arity(limit_ordinal_fm(x)) = succ(x)"
  unfolding limit_ordinal_fm_def 
  using arity_ordinal_fm arity_succ_fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_finite_ordinal_fm :
  "⟦x∈nat⟧ ⟹ arity(finite_ordinal_fm(x)) = succ(x)"
  unfolding finite_ordinal_fm_def 
  using arity_ordinal_fm arity_limit_ordinal_fm arity_succ_fm arity_empty_fm 
    nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_omega_fm :
  "⟦x∈nat⟧ ⟹ arity(omega_fm(x)) = succ(x)"
  unfolding omega_fm_def 
  using arity_limit_ordinal_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_cartprod_fm : 
  "⟦ A∈nat ; B∈nat ; z∈nat ⟧ ⟹ arity(cartprod_fm(A,B,z)) = succ(A) ∪ succ(B) ∪ succ(z)"
  unfolding cartprod_fm_def
  using arity_pair_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_fst_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(fst_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding fst_fm_def
  using arity_pair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_snd_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding snd_fm_def
  using arity_pair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_snd_snd_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_snd_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding snd_snd_fm_def hcomp_fm_def
  using arity_snd_fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_ftype_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(ftype_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding ftype_fm_def
  using arity_fst_fm 
  by auto

lemma name1arity__fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(name1_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding name1_fm_def hcomp_fm_def
  using arity_fst_fm arity_snd_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma name2arity__fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(name2_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding name2_fm_def hcomp_fm_def
  using arity_fst_fm arity_snd_snd_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_cond_of_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(cond_of_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding cond_of_fm_def hcomp_fm_def
  using arity_snd_fm arity_snd_snd_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_singleton_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(singleton_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding singleton_fm_def cons_fm_def
  using arity_union_fm arity_upair_fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_Memrel_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(Memrel_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding Memrel_fm_def 
  using  arity_pair_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_quasinat_fm :
  "⟦x∈nat⟧ ⟹ arity(quasinat_fm(x)) = succ(x)"
  unfolding quasinat_fm_def cons_fm_def 
  using arity_succ_fm arity_empty_fm
    nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_is_recfun_fm :
  "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat;i∈nat⟧ ⟹  arity(p) = i ⟹ 
  arity(is_recfun_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(pred(pred(i))))"
  unfolding is_recfun_fm_def
  using arity_upair_fm arity_pair_fm arity_pre_image_fm arity_restriction_fm
    nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_is_wfrec_fm :
  "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat ; i∈nat⟧ ⟹ arity(p) = i ⟹ 
    arity(is_wfrec_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ pred(pred(pred(pred(pred(i)))))"
  unfolding is_wfrec_fm_def
  using arity_succ_fm  arity_is_recfun_fm 
     nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_is_nat_case_fm :
  "⟦p∈formula ; v∈nat ; n∈nat; Z∈nat; i∈nat⟧ ⟹ 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 
    nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_iterates_MH_fm :
  assumes "isF∈formula" "v∈nat" "n∈nat" "g∈nat" "z∈nat" "i∈nat" 
      "arity(isF) = i"
    shows "arity(iterates_MH_fm(isF,v,n,g,z)) = 
           succ(v) ∪ succ(n) ∪ succ(g) ∪ succ(z) ∪ pred(pred(pred(pred(i))))"
proof -
  let ?φ = "Exists(And(fun_apply_fm(succ(succ(succ(g))), 2, 0), Forall(Implies(Equal(0, 2), isF))))"
  let ?ar = "succ(succ(succ(g))) ∪ pred(pred(i))"
  from assms
  have "arity(?φ) =?ar" "?φ∈formula" 
    using arity_fun_apply_fm
    nat_union_abs1 nat_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(?φ) = _›] assms pred_succ_eq pred_Un_distrib
    by auto
qed

lemma arity_is_iterates_fm :
  assumes "p∈formula" "v∈nat" "n∈nat" "Z∈nat" "i∈nat" 
    "arity(p) = i"
  shows "arity(is_iterates_fm(p,v,n,Z)) = succ(v) ∪ succ(n) ∪ succ(Z) ∪ 
          pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(pred(i)))))))))))"
proof -
  let ?φ = "iterates_MH_fm(p, 7#+v, 2, 1, 0)"
  let ?ψ = "is_wfrec_fm(?φ, 0, succ(succ(n)),succ(succ(Z)))"
  from ‹v∈_›
  have "arity(?φ) = (8#+v) ∪ pred(pred(pred(pred(i))))" "?φ∈formula"
    using assms arity_iterates_MH_fm nat_union_abs2
    by simp_all
  then
  have "arity(?ψ) = succ(succ(succ(n))) ∪ succ(succ(succ(Z))) ∪ (3#+v) ∪ 
      pred(pred(pred(pred(pred(pred(pred(pred(pred(i)))))))))"
    using assms arity_is_wfrec_fm[OF ‹?φ∈_› _ _ _ _ ‹arity(?φ) = _›] nat_union_abs1 pred_Un_distrib
    by auto
  then
  show ?thesis
    unfolding is_iterates_fm_def 
    using arity_Memrel_fm arity_succ_fm assms nat_union_abs1 pred_Un_distrib
    by auto
qed

lemma arity_eclose_n_fm :
  assumes "A∈nat" "x∈nat" "t∈nat" 
  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 nat_union_abs2
    by simp_all
  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 :
  assumes "x∈nat" "t∈nat"
  shows "arity(mem_eclose_fm(x,t)) = succ(x) ∪ succ(t)"
proof -  
  let ?φ="eclose_n_fm(x #+ 2, 1, 0)"
  from ‹x∈nat›
  have "arity(?φ) = x#+3" 
    using arity_eclose_n_fm nat_union_abs2 
    by simp
  with assms
  show ?thesis
    unfolding mem_eclose_fm_def 
    using arity_finite_ordinal_fm nat_union_abs2 pred_Un_distrib
    by simp
qed

lemma arity_is_eclose_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(is_eclose_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding is_eclose_fm_def 
  using arity_mem_eclose_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma eclose_n1arity__fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n1_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding eclose_n1_fm_def 
  using arity_is_eclose_fm arity_singleton_fm name1arity__fm nat_union_abs2 pred_Un_distrib
  by auto

lemma eclose_n2arity__fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(eclose_n2_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding eclose_n2_fm_def 
  using arity_is_eclose_fm arity_singleton_fm name2arity__fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_ecloseN_fm :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(ecloseN_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding ecloseN_fm_def 
  using eclose_n1arity__fm eclose_n2arity__fm arity_union_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_frecR_fm :
  "⟦a∈nat;b∈nat⟧ ⟹ arity(frecR_fm(a,b)) = succ(a) ∪ succ(b)"
  unfolding frecR_fm_def
  using arity_ftype_fm name1arity__fm name2arity__fm arity_domain_fm 
      number1arity__fm arity_empty_fm nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_Collect_fm :
  assumes "x ∈ nat" "y ∈ nat" "p∈formula" 
  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

end