Theory Arities

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

lemma arity_upair_fm : "  t1nat ; t2nat ; upnat    
  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 : "  t1nat ; t2nat ; pnat    
  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 :
  " rnat ; snat ; tnat   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 : 
    " rnat ; znat   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 : 
    " rnat ; znat   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 : 
  " xnat ; ynat ; znat   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 : 
  " xnat ; ynat ; znat   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 : 
  " xnat ; ynat ; znat   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 : 
  " xnat ; ynat   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 : 
  " xnat ; ynat ; fnat   
    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 : 
    " rnat ; znat   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 : 
    " rnat   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 :
  "xnat;ynat  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 : 
    " rnat   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 : 
    " rnat   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 : 
    " rnat   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 : 
    " rnat ; znat ; Anat   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 : 
  " xnat ; ynat ; fnat   
    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 : 
  "xnat ; ynat  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 :
  "xnat  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 :
  "xnat  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 :
  "xnat  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 :
  "xnat  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 :
  "xnat  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 : 
  " Anat ; Bnat ; znat   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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  arity(ftype_fm(x,t)) = succ(x)  succ(t)"
  unfolding ftype_fm_def
  using arity_fst_fm 
  by auto

lemma name1arity__fm :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat  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 :
  "pformula ; vnat ; nnat; Znat;inat   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 :
  "pformula ; vnat ; nnat; Znat ; inat  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 :
  "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 
    nat_union_abs2 pred_Un_distrib
  by auto

lemma arity_iterates_MH_fm :
  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(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 "pformula" "vnat" "nnat" "Znat" "inat" 
    "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 "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 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 "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 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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "xnat ; tnat  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 :
  "anat;bnat  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" "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

end