Theory FrecR_Arities

theory FrecR_Arities
  imports
    FrecR
begin

context
  notes FOL_arities[simp]
begin

arity_theorem intermediate for "fst_fm"
lemma arity_fst_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(fst_fm(x,t)) = succ(x) ∪ succ(t)"
  using arity_fst_fm'
  by auto

arity_theorem intermediate for "snd_fm"
lemma arity_snd_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(snd_fm(x,t)) = succ(x) ∪ succ(t)"
  using arity_snd_fm'
  by auto

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

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

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

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

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

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

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

lemma arity_ecloseN_fm [arity] :
  "⟦x∈nat ; t∈nat⟧ ⟹ arity(ecloseN_fm(x,t)) = succ(x) ∪ succ(t)"
  unfolding ecloseN_fm_def
  using arity_eclose_n1_fm arity_eclose_n2_fm arity_union_fm union_abs2 pred_Un_distrib
  by auto

lemma arity_frecR_fm [arity]:
  "⟦a∈nat;b∈nat⟧ ⟹ arity(frecR_fm(a,b)) = succ(a) ∪ succ(b)"
  unfolding frecR_fm_def
  using arity_ftype_fm arity_name1_fm arity_name2_fm arity_domain_fm
      arity_empty_fm arity_union_fm pred_Un_distrib arity_succ_fm
  by auto

end ― ‹@{thm [source] FOL_arities}›

end