Theory Arities

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

declare arity_And arity_Or arity_Implies arity_Iff arity_Exists [arity]

declare pred_Un_distrib [arity]

lemma arity_upair_fm [arity] : "⟦  t1∈nat ; t2∈nat ; up∈nat  ⟧ ⟹ 
  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


lemma arity_pair_fm [arity] : "⟦  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 union_abs1 union_abs2 pred_Un
  by auto

lemma arity_composition_fm [arity] :
  "⟦ 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 union_abs1 union_abs2 pred_Un_distrib
  by auto

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

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

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

lemma arity_image_fm [arity] : 
  "⟦ 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  union_abs1 union_abs2 pred_Un_distrib
  by auto

lemma arity_pre_image_fm [arity] : 
  "⟦ 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  union_abs1 union_abs2 pred_Un_distrib
  by auto


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

lemma arity_fun_apply_fm [arity] : 
  "⟦ 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 union_abs2 pred_Un_distrib
  by auto

lemma arity_field_fm [arity] : 
    "⟦ 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 
    union_abs1 union_abs2 pred_Un_distrib
  by auto

lemma arity_empty_fm [arity]: 
    "⟦ r∈nat ⟧ ⟹ arity(empty_fm(r)) = succ(r)"
  unfolding empty_fm_def 
  using union_abs1 union_abs2 pred_Un_distrib
  by simp

lemma arity_cons_fm [arity] :
  "⟦x∈nat;y∈nat;z∈nat⟧ ⟹ arity(cons_fm(x,y,z)) = succ(x) ∪ succ(y) ∪ succ(z)"
  unfolding cons_fm_def
  using arity_upair_fm arity_union_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_succ_fm [arity] :
  "⟦x∈nat;y∈nat⟧ ⟹ arity(succ_fm(x,y)) = succ(x) ∪ succ(y)"
  unfolding succ_fm_def
  using arity_cons_fm
  by auto

lemma arity_number1_fm [arity] : 
    "⟦ r∈nat ⟧ ⟹ arity(number1_fm(r)) = succ(r)"
  unfolding number1_fm_def 
  using arity_empty_fm arity_succ_fm union_abs1 union_abs2 pred_Un_distrib
  by simp

lemma arity_function_fm [arity] : 
    "⟦ r∈nat ⟧ ⟹ arity(function_fm(r)) = succ(r)"
  unfolding function_fm_def 
  using arity_pair_fm union_abs1 union_abs2 pred_Un_distrib
  by simp

lemma arity_relation_fm [arity] : 
    "⟦ r∈nat ⟧ ⟹ arity(relation_fm(r)) = succ(r)"
  unfolding relation_fm_def 
  using arity_pair_fm union_abs1 union_abs2 pred_Un_distrib
  by simp

lemma arity_restriction_fm [arity] : 
    "⟦ 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 union_abs2 pred_Un_distrib
  by auto

lemma arity_typed_function_fm [arity] : 
  "⟦ 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 
    union_abs2 pred_Un_distrib
  by auto


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

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

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

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

lemma arity_finite_ordinal_fm [arity] :
  "⟦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 
    union_abs2 pred_Un_distrib
  by auto

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

lemma arity_cartprod_fm [arity] : 
  "⟦ 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 union_abs2 pred_Un_distrib
  by auto

lemma arity_singleton_fm [arity] :
  "⟦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 union_abs2 pred_Un_distrib
  by auto

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

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

lemma arity_is_recfun_fm [arity] :
  "⟦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
    union_abs2 pred_Un_distrib
  by auto

lemma arity_is_wfrec_fm [arity] :
  "⟦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 
     union_abs2 pred_Un_distrib
  by auto

lemma arity_is_nat_case_fm [arity] :
  "⟦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 
    union_abs2 pred_Un_distrib
  by auto

lemma arity_iterates_MH_fm [arity] :
  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
    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(?φ) = _›] assms pred_succ_eq pred_Un_distrib
    by auto
qed

lemma arity_is_iterates_fm [arity] :
  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 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(?φ) = _›] 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 "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 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 [arity] :
  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 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] :
  "⟦x∈nat ; t∈nat⟧ ⟹ 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" "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

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] :
  "⟦p∈formula ; v∈nat ; n∈nat; i∈nat⟧ ⟹ arity(p) = i ⟹
    arity(Replace_fm(v,p,n)) = succ(n) ∪ (succ(v) ∪ Arith.pred(Arith.pred(i)))"
  unfolding Replace_fm_def
  using union_abs2 pred_Un_distrib
  by simp

lemma arity_lambda_fm [arity] :
  "⟦p∈formula; v∈nat ; n∈nat; i∈nat⟧ ⟹  arity(p) = i ⟹
    arity(lambda_fm(p,v,n)) = succ(n) ∪ (succ(v) ∪ Arith.pred(Arith.pred(Arith.pred(i))))"
  unfolding lambda_fm_def
  using arity_pair_fm pred_Un_distrib union_abs1 union_abs2
  by simp

lemma arity_transrec_fm [arity] :
  "⟦p∈formula ; v∈nat ; n∈nat; i∈nat⟧ ⟹ 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]
  by simp

end