Theory Generic_Term

theory Generic_Term
  imports Main
begin

type_synonym position = "nat list"

locale subterms = 
  fixes subterms :: "'t ⇒ 't list"
begin

primrec subterm_at :: "'t ⇒ position ⇒ 't" (infixl ‹!⇩t› 64) where
  "t !⇩t [] = t" 
| "t !⇩t i # p = subterms t ! i !⇩t p"

end

locale smaller_subterms = subterms where subterms = subterms 
  for subterms :: "'t ⇒ 't list" +
  notes conj_cong [fundef_cong]
  fixes size  :: "'t ⇒ nat" and is_var :: "'t ⇒ bool"
  assumes subterms_smaller: "⋀t' t. t' ∈ set (subterms t) ⟹ size t' < size t"
begin

function positions :: "'t ⇒ position set" where
  "positions t =
     {[]} ∪ {i # p | i p.
              ¬is_var t ∧
              i < length (subterms t) ∧
              p ∈ positions ((subterms t) ! i)}"
  by pat_completeness auto

termination
proof (relation "measure size")
  fix t p i p'
  assume "p = i # p'" "i < length (subterms t)"

  then show "(subterms t ! i, t) ∈ measure size"
    using subterms_smaller
    by simp  
qed auto

declare positions.simps [simp del]

lemma empty_positions [simp]: "[] ∈ positions t"
  by (subst positions.simps) blast

lemma nonempty_positions [simp]:
  "i # p ∈ positions t ⟷ ¬is_var t ∧ i < length (subterms t) ∧ p ∈ positions ((subterms t) ! i)"
  by (subst positions.simps) auto

end

locale term_interpretation = 
  subterms where subterms = subterms
for subterms :: "'t ⇒ 't list" +
fixes 
  Fun :: "'f ⇒ 'e ⇒ 't list ⇒ 't" and
  fun_sym :: "'t ⇒ 'f" and 
  extra :: "'t ⇒ 'e" and
  is_var :: "'t ⇒ bool"
assumes
  term_fun_sym [simp]: "⋀f e ts. fun_sym (Fun f e ts) = f" and
  term_extra [simp]: "⋀f e ts. extra (Fun f e ts) = e" and
  subterms [simp]: "⋀f e ts. subterms (Fun f e ts) = ts" and
  term_destruct: "⋀t. ¬is_var t ⟷ (∃f e ts. t = Fun f e ts)" and
  term_inject [intro]:
    "⋀f⇩1 e⇩1 ts⇩1 f⇩2 e⇩2 ts⇩2. Fun f⇩1 e⇩1 ts⇩1 = Fun f⇩2 e⇩2 ts⇩2 ⟹ f⇩1 = f⇩2 ∧ e⇩1 = e⇩2 ∧ ts⇩1 = ts⇩2"
begin

lemma interpret_term [simp]: 
  assumes "¬is_var t"
  shows "Fun (fun_sym t) (extra t) (subterms t) = t"
  by (metis assms subterms term_destruct term_extra term_fun_sym)

end

end