Theory Term_Aux

section ‹Auxiliaries›

theory Term_Aux
  imports
    Subterm_and_Context
    "HOL-Library.Multiset"
begin

text ‹
  This theory contains material about terms that is required for KBO, 
  but does not belong to @{theory Knuth_Bendix_Order.Subterm_and_Context}.

  We plan to merge this material into the theory @{theory First_Order_Terms.Term}
  at some point.
›

text ‹The variables of a term as multiset.›
fun vars_term_ms :: "('f, 'v) term ⇒ 'v multiset"
  where
    "vars_term_ms (Var x) = {#x#}" |
    "vars_term_ms (Fun f ts) = ⋃# (mset (map vars_term_ms ts))"

lemma vars_term_ms_subst [simp]:
  "vars_term_ms (t ⋅ σ) =
    ⋃# (image_mset (λ x. vars_term_ms (σ x)) (vars_term_ms t))" (is "_ = ?V t")
proof (induct t)
  case (Fun f ts)
  have IH: "map (λ t. vars_term_ms (t ⋅ σ)) ts = map (λ t. ?V t) ts"
    by (rule map_cong[OF refl Fun])
  show ?case by (simp add: o_def IH, induct ts, auto)
qed simp

lemma vars_term_ms_subst_mono:
  assumes "vars_term_ms s ⊆# vars_term_ms t"
  shows "vars_term_ms (s ⋅ σ) ⊆# vars_term_ms (t ⋅ σ)"
proof -
  from assms[unfolded mset_subset_eq_exists_conv] obtain u where t: "vars_term_ms t = vars_term_ms s + u" by auto
  show ?thesis unfolding vars_term_ms_subst unfolding t by auto
qed

lemma set_mset_vars_term_ms [simp]:
  "set_mset (vars_term_ms t) = vars_term t"
  by (induct t) auto

text ‹A term is called ∗‹ground› if it does not contain any variables.›
fun ground :: "('f, 'v) term ⇒ bool"
  where
    "ground (Var x) ⟷ False" |
    "ground (Fun f ts) ⟷ (∀t ∈ set ts. ground t)"

lemma ground_vars_term_empty:
  "ground t ⟷ vars_term t = {}"
  by (induct t) simp_all

lemma ground_subst [simp]:
  "ground (t ⋅ σ) ⟷ (∀x ∈ vars_term t. ground (σ x))"
  by (induct t) simp_all

lemma ground_subst_apply:
  assumes "ground t"
  shows "t ⋅ σ = t"
proof -
  have "t = t ⋅ Var" by simp
  also have "… = t ⋅ σ"
    by (rule term_subst_eq, insert assms[unfolded ground_vars_term_empty], auto)
  finally show ?thesis by simp
qed

text ‹
  A ∗‹signature› is a set of function symbol/arity pairs, where the arity of a function symbol,
  denotes the number of arguments it expects.
›
type_synonym 'f sig = "('f × nat) set"

text ‹The set of all function symbol/ arity pairs occurring in a term.›
fun funas_term :: "('f, 'v) term ⇒ 'f sig"
  where
    "funas_term (Var _) = {}" |
    "funas_term (Fun f ts) = {(f, length ts)} ∪ ⋃(set (map funas_term ts))"


lemma supt_imp_funas_term_subset:
  assumes "s ⊳ t"
  shows "funas_term t ⊆ funas_term s"
  using assms by (induct) auto

lemma supteq_imp_funas_term_subset[simp]:
  assumes "s ⊵ t"
  shows "funas_term t ⊆ funas_term s"
  using assms by (induct) auto

text ‹The set of all function symbol/arity pairs occurring in a context.›
fun funas_ctxt :: "('f, 'v) ctxt ⇒ 'f sig"
  where
    "funas_ctxt Hole = {}" |
    "funas_ctxt (More f ss1 D ss2) = {(f, Suc (length (ss1 @ ss2)))}
     ∪ funas_ctxt D ∪ ⋃(set (map funas_term (ss1 @ ss2)))"

lemma funas_term_ctxt_apply [simp]:
  "funas_term (C⟨t⟩) = funas_ctxt C ∪ funas_term t"
proof (induct t)
  case (Var x) show ?case by (induct C) auto
next
  case (Fun f ts) show ?case by (induct C arbitrary: f ts) auto
qed

lemma funas_term_subst:
  "funas_term (t ⋅ σ) = funas_term t ∪ ⋃(funas_term ` σ ` vars_term t)"
  by (induct t) auto

lemma funas_ctxt_compose [simp]:
  "funas_ctxt (C ∘⇩c D) = funas_ctxt C ∪ funas_ctxt D"
  by (induct C) auto

lemma funas_ctxt_subst [simp]:
  "funas_ctxt (C ⋅⇩c σ) = funas_ctxt C ∪ ⋃(funas_term ` σ ` vars_ctxt C)"
  by (induct C, auto simp: funas_term_subst)

end