Theory First_Order_Clause.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 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 = smaller_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"
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
  is_var_subterms [simp]: "⋀t. is_var t ⟹ subterms t = []" 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)

inductive is_subterm_eq :: "'t ⇒ 't ⇒ bool" (infix ‹⊴› 55) where
  subterm_refl [simp, intro]: "is_subterm_eq t t" |
  subterm [intro]: "t' ∈ set (subterms t) ⟹ is_subterm_eq t'' t' ⟹ is_subterm_eq t'' t"

function all_subterms_eq :: "'t ⇒ 't set" where
  "all_subterms_eq t = {t} ∪ ⋃(all_subterms_eq ` set (subterms t))"
  by auto

termination
proof (relation "measure size")
  fix t t'
  assume "t' ∈ set (subterms t)"

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

declare all_subterms_eq.simps [simp del]

lemmas term_induct = all_subterms_eq.induct

lemma all_subterms_eq_refl [simp]: "t ∈ all_subterms_eq t"
  by (subst all_subterms_eq.simps) simp

lemma all_subterms_eq_is_var [simp]: "is_var t ⟹ all_subterms_eq t = {t}"
  by (subst all_subterms_eq.simps) simp

lemma all_subterms_eq_Fun [simp]: 
  "all_subterms_eq (Fun f e ts) = {Fun f e ts} ∪ ⋃(all_subterms_eq ` set ts)"
  by (subst all_subterms_eq.simps) simp

lemma all_subterms_eq_is_subterm_eq: "all_subterms_eq t = {t'. t' ⊴ t}"
proof -

  have "t' ∈ all_subterms_eq t ⟹ t' ⊴ t" for t'
    by 
      (induction t rule: all_subterms_eq.induct)
      (metis (mono_tags, opaque_lifting) UN_iff Un_insert_left all_subterms_eq.simps insert_iff 
        subterm_refl subterm sup_bot_left)

  moreover have "t' ⊴ t ⟹ t' ∈ all_subterms_eq t" for t'
  proof (induction t' t rule: is_subterm_eq.induct)
    case (subterm_refl t)

    then show ?case
      by simp
  next
    case (subterm t' t t'')
    
    then show ?case
      by (metis UN_I UnCI all_subterms_eq.elims)
  qed

  ultimately show ?thesis
    by blast
qed

end

end