# Theory Regular_Tree_Relations.Term_Context

```section ‹Preliminaries›

theory Term_Context
imports First_Order_Terms.Term
First_Order_Terms.Subterm_and_Context
Polynomial_Factorization.Missing_List
begin

subsection ‹Additional functionality on @{type term} and @{type ctxt}›
subsubsection ‹Positions›

type_synonym pos = "nat list"
context
notes conj_cong [fundef_cong]
begin

fun poss :: "('f, 'v) term ⇒ pos set" where
"poss (Var x) = {[]}"
| "poss (Fun f ss) = {[]} ∪ {i # p | i p. i < length ss ∧ p ∈ poss (ss ! i)}"
end

fun hole_pos where
"hole_pos □ = []"
| "hole_pos (More f ss D ts) = length ss # hole_pos D"

definition position_less_eq (infixl "≤⇩p" 67) where
"p ≤⇩p q ⟷ (∃ r. p @ r = q)"

abbreviation position_less (infixl "<⇩p" 67) where
"p <⇩p q ≡ p ≠ q ∧ p ≤⇩p q"

definition position_par  (infixl "⊥" 67) where
"p ⊥ q ⟷ ¬ (p ≤⇩p q) ∧ ¬ (q ≤⇩p p)"

fun remove_prefix where
"remove_prefix (x # xs) (y # ys) = (if x = y then remove_prefix xs ys else None)"
| "remove_prefix [] ys = Some ys"
| "remove_prefix xs [] = None"

definition pos_diff  (infixl "-⇩p" 67) where
"p -⇩p q = the (remove_prefix q p)"

fun subt_at :: "('f, 'v) term ⇒ pos ⇒ ('f, 'v) term" (infixl "|'_" 67) where
"s |_ [] = s"
| "Fun f ss |_ (i # p) = (ss ! i) |_ p"
| "Var x |_ _ = undefined"

fun ctxt_at_pos where
"ctxt_at_pos s [] = □"
| "ctxt_at_pos (Fun f ss) (i # p) = More f (take i ss) (ctxt_at_pos (ss ! i) p) (drop (Suc i) ss)"
| "ctxt_at_pos (Var x) _ = undefined"

fun replace_term_at ("_[_ ← _]" [1000, 0, 0] 1000) where
"replace_term_at s [] t = t"
| "replace_term_at (Var x) ps t = (Var x)"
| "replace_term_at (Fun f ts) (i # ps) t =
(if i < length ts then Fun f (ts[i:=(replace_term_at (ts ! i) ps t)]) else Fun f ts)"

fun fun_at :: "('f, 'v) term ⇒ pos ⇒ ('f + 'v) option" where
"fun_at (Var x) [] = Some (Inr x)"
| "fun_at (Fun f ts) [] = Some (Inl f)"
| "fun_at (Fun f ts) (i # p) = (if i < length ts then fun_at (ts ! i) p else None)"
| "fun_at _ _ = None"

subsubsection ‹Computing the signature›

fun funas_term where
"funas_term (Var x) = {}"
| "funas_term (Fun f ts) = insert (f, length ts) (⋃ (set (map funas_term ts)))"

fun funas_ctxt where
"funas_ctxt □ = {}"
| "funas_ctxt (More f ss C ts) = (⋃ (set (map funas_term ss))) ∪
insert (f, Suc (length ss + length ts)) (funas_ctxt C) ∪ (⋃ (set (map funas_term ts)))"

subsubsection ‹Groundness›

fun ground where
"ground (Var x) = False"
| "ground (Fun f ts) = (∀ t ∈ set ts. ground t)"

fun ground_ctxt where
"ground_ctxt □ ⟷ True"
| "ground_ctxt (More f ss C ts) ⟷ (∀ t ∈ set ss. ground t) ∧ ground_ctxt C ∧ (∀ t ∈ set ts. ground t)"

subsubsection ‹Depth›
fun depth where
"depth (Var x) = 0"
| "depth (Fun f []) = 0"
| "depth (Fun f ts) = Suc (Max (depth ` set ts))"

subsubsection ‹Type conversion›

text ‹We require a function which adapts the type of variables of a term,
so that states of the automaton and variables in the term language can be
chosen independently.›

abbreviation "map_funs_term f ≡ map_term f (λ x. x)"
abbreviation "map_both f ≡ map_prod f f"

definition adapt_vars :: "('f, 'q) term ⇒ ('f,'v)term" where
[code del]: "adapt_vars ≡ map_vars_term (λ_. undefined)"

abbreviation "map_vars_ctxt f ≡ map_ctxt (λx. x) f"
definition adapt_vars_ctxt :: "('f,'q)ctxt ⇒ ('f,'v)ctxt" where
[code del]: "adapt_vars_ctxt = map_vars_ctxt (λ_. undefined)"

subsection ‹Properties of @{type pos}›

lemma position_less_eq_induct [consumes 1]:
assumes "p ≤⇩p q" and "⋀ p. P p p"
and "⋀ p q r. p ≤⇩p q ⟹ P p q ⟹ P p (q @ r)"
shows "P p q" using assms
proof (induct p arbitrary: q)
case Nil then show ?case
by (metis append_Nil position_less_eq_def)
next
case (Cons a p)
then show ?case
by (metis append_Nil2 position_less_eq_def)
qed

text ‹We show the correspondence between the function @{const remove_prefix} and
the order on positions @{const position_less_eq}. Moreover how it can be used to
compute the difference of positions.›

lemma remove_prefix_Nil [simp]:
"remove_prefix xs xs = Some []"
by (induct xs) auto

lemma remove_prefix_Some:
assumes "remove_prefix xs ys = Some zs"
shows "ys = xs @ zs" using assms
proof (induct xs arbitrary: ys)
case (Cons x xs)
show ?case using Cons(1)[of "tl ys"] Cons(2)
by (cases ys) (auto split: if_splits)
qed auto

lemma remove_prefix_append:
"remove_prefix xs (xs @ ys) = Some ys"
by (induct xs) auto

lemma remove_prefix_iff:
"remove_prefix xs ys = Some zs ⟷ ys = xs @ zs"
using remove_prefix_Some remove_prefix_append
by blast

lemma position_less_eq_remove_prefix:
"p ≤⇩p q ⟹ remove_prefix p q ≠ None"
by (induct rule: position_less_eq_induct) (auto simp: remove_prefix_iff)

text ‹Simplification rules on @{const position_less_eq}, @{const pos_diff},
and @{const position_par}.›

lemma position_less_refl [simp]: "p ≤⇩p p"
by (auto simp: position_less_eq_def)

lemma position_less_eq_Cons [simp]:
"(i # ps) ≤⇩p (j # qs) ⟷ i = j ∧ ps ≤⇩p qs"
by (auto simp: position_less_eq_def)

lemma position_less_Nil_is_bot [simp]: "[] ≤⇩p p"
by (auto simp: position_less_eq_def)

lemma position_less_Nil_is_bot2 [simp]: "p ≤⇩p [] ⟷ p = []"
by (auto simp: position_less_eq_def)

lemma position_diff_Nil [simp]: "q -⇩p [] = q"
by (auto simp: pos_diff_def)

lemma position_diff_Cons [simp]:
"(i # ps) -⇩p (i # qs) = ps -⇩p qs"
by (auto simp: pos_diff_def)

lemma Nil_not_par [simp]:
"[] ⊥ p ⟷ False"
"p ⊥ [] ⟷ False"
by (auto simp: position_par_def)

lemma par_not_refl [simp]: "p ⊥ p ⟷ False"
by (auto simp: position_par_def)

lemma par_Cons_iff:
"(i # ps) ⊥ (j # qs) ⟷ (i ≠ j ∨ ps ⊥ qs)"
by (auto simp: position_par_def)

text ‹Simplification rules on @{const poss}.›

lemma Nil_in_poss [simp]: "[] ∈ poss t"
by (cases t) auto

lemma poss_Cons [simp]:
"i # p ∈ poss t ⟹ [i] ∈ poss t"
by (cases t) auto

lemma poss_Cons_poss:
"i # q ∈ poss t ⟷ i < length (args t) ∧ q ∈ poss (args t ! i)"
by (cases t) auto

lemma poss_append_poss:
"p @ q ∈ poss t ⟷ p ∈ poss t ∧ q ∈ poss (t |_ p)"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons[of "args t ! i"] show ?case
by (cases t) auto
qed auto

text ‹Simplification rules on @{const hole_pos}›

lemma hole_pos_map_vars [simp]:
"hole_pos (map_vars_ctxt f C) = hole_pos C"
by (induct C) auto

lemma hole_pos_in_ctxt_apply [simp]: "hole_pos C ∈ poss C⟨u⟩"
by (induct C) auto

subsection ‹Properties of @{const ground} and @{const ground_ctxt}›

lemma ground_vars_term_empty [simp]:
"ground t ⟹ vars_term t = {}"
by (induct t) auto

lemma ground_map_term [simp]:
"ground (map_term f h t) = ground t"
by (induct t) auto

lemma ground_ctxt_apply [simp]:
"ground C⟨t⟩ ⟷ ground_ctxt C ∧ ground t"
by (induct C) auto

lemma ground_ctxt_comp [intro]:
"ground_ctxt C ⟹ ground_ctxt D ⟹ ground_ctxt (C ∘⇩c D)"
by (induct C) auto

lemma ctxt_comp_n_pres_ground [intro]:
"ground_ctxt C ⟹ ground_ctxt (C^n)"
by (induct n arbitrary: C) auto

lemma subterm_eq_pres_ground:
assumes "ground s" and "s ⊵ t"
shows "ground t" using assms(2,1)
by (induct) auto

lemma ground_substD:
"ground (l ⋅ σ) ⟹ x ∈ vars_term l ⟹ ground (σ x)"
by (induct l) auto

lemma ground_substI:
"(⋀ x. x ∈ vars_term s ⟹ ground (σ x)) ⟹ ground (s ⋅ σ)"
by (induct s) auto

subsection ‹Properties on signature induced by a term @{type term}/context @{type ctxt}›

lemma funas_ctxt_apply [simp]:
"funas_term C⟨t⟩ = funas_ctxt C ∪ funas_term t"
by (induct C) auto

lemma funas_term_map [simp]:
"funas_term (map_term f h t) = (λ (g, n). (f g, n)) ` funas_term t"
by (induct t) auto

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

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

lemma ctxt_comp_n_funas [simp]:
"(f, v) ∈ funas_ctxt (C^n) ⟹ (f, v) ∈ funas_ctxt C"
by (induct n arbitrary: C) auto

lemma ctxt_comp_n_pres_funas [intro]:
"funas_ctxt C ⊆ ℱ ⟹ funas_ctxt (C^n) ⊆ ℱ"
by (induct n arbitrary: C) auto

subsection ‹Properties on subterm at given position @{const subt_at}›

lemma subt_at_Cons_comp:
"i # p ∈ poss s ⟹ (s |_ [i]) |_ p = s |_ (i # p)"
by (cases s) auto

lemma ctxt_at_pos_subt_at_pos:
"p ∈ poss t ⟹ (ctxt_at_pos t p)⟨u⟩ |_ p = u"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) (auto simp: nth_append)
qed auto

lemma ctxt_at_pos_subt_at_id:
"p ∈ poss t ⟹ (ctxt_at_pos t p)⟨t |_ p⟩ = t"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) force+
qed auto

lemma subst_at_ctxt_at_eq_termD:
assumes "s = t" "p ∈ poss t"
shows "s |_ p = t |_ p ∧ ctxt_at_pos s p = ctxt_at_pos t p" using assms
by auto

lemma subst_at_ctxt_at_eq_termI:
assumes "p ∈ poss s" "p ∈ poss t"
and "s |_p = t |_ p"
and "ctxt_at_pos s p = ctxt_at_pos t p"
shows "s = t" using assms
by (metis ctxt_at_pos_subt_at_id)

lemma subt_at_subterm_eq [intro!]:
"p ∈ poss t ⟹ t ⊵ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto

lemma subt_at_subterm [intro!]:
"p ∈ poss t ⟹ p ≠ [] ⟹  t ⊳ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto

lemma ctxt_at_pos_hole_pos [simp]: "ctxt_at_pos C⟨s⟩ (hole_pos C) = C"
by (induct C) auto

subsection ‹Properties on replace terms at a given position
@{const replace_term_at}›

lemma replace_term_at_not_poss [simp]:
"p ∉ poss s ⟹ s[p ← t] = s"
proof (induct s arbitrary: p)
case (Var x) then show ?case by (cases p) auto
next
case (Fun f ts) show ?case using Fun(1)[OF nth_mem] Fun(2)
by (cases p) (auto simp: min_def intro!: nth_equalityI)
qed

lemma replace_term_at_replace_at_conv:
"p ∈ poss s ⟹ (ctxt_at_pos s p)⟨t⟩ = s[p ← t]"
by (induct s arbitrary: p) (auto simp: upd_conv_take_nth_drop)

lemma parallel_replace_term_commute [ac_simps]:
"p ⊥ q ⟹ s[p ← t][q ← u] = s[q ← u][p ← t]"
proof (induct s arbitrary: p q)
case (Var x) then show ?case
by (cases p; cases q) auto
next
case (Fun f ts)
from Fun(2) have "p ≠ []" "q ≠ []" by auto
then obtain i j ps qs where [simp]: "p = i # ps" "q = j # qs"
by (cases p; cases q) auto
have "i ≠ j ⟹ (Fun f ts)[p ← t][q ← u] = (Fun f ts)[q ← u][p ← t]"
by (auto simp: list_update_swap)
then show ?case using Fun(1)[OF nth_mem, of j ps qs] Fun(2)
by (cases "i = j") (auto simp: par_Cons_iff)
qed

lemma replace_term_at_above [simp]:
"p ≤⇩p q ⟹ s[q ← t][p ← u] = s[p ← u]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma replace_term_at_below [simp]:
"p <⇩p q ⟹ s[p ← t][q ← u] = s[p ← t[q -⇩p p ← u]]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto

lemma replace_at_hole_pos [simp]: "C⟨s⟩[hole_pos C ← t] = C⟨t⟩"
by (induct C) auto

by (induct ts, auto simp: adapt_vars_def)

proof (induct t arbitrary: t')
case (Fun f ts)
then show ?case by (cases t') (auto simp add: map_idI)
qed auto

assumes g: "ground t"
proof -
let ?t' = "adapt_vars t :: ('f,'w)term"
have gt': "ground ?t'" using g by auto
from adapt_vars_reverse[OF gt', of t] show ?thesis by blast
qed

shows "x = y"

by (induct C, auto)

by (induct l) auto

"ground t ⟹ map_vars_term f t = adapt_vars t"
by (induct t) auto

"ground_ctxt C ⟹ map_vars_ctxt f C = adapt_vars_ctxt C"
by (induct C) auto

subsubsection ‹Equality on ground terms/contexts by positions and symbols›

lemma fun_at_def':
"fun_at t p = (if p ∈ poss t then
(case t |_ p of Var x ⇒ Some (Inr x) | Fun f ts ⇒ Some (Inl f)) else None)"
by (induct t p rule: fun_at.induct) auto

lemma fun_at_None_nposs_iff:
"fun_at t p = None ⟷ p ∉ poss t"
by (auto simp: fun_at_def') (meson term.case_eq_if)

lemma eq_term_by_poss_fun_at:
assumes "poss s = poss t" "⋀p. p ∈ poss s ⟹ fun_at s p = fun_at t p"
shows "s = t"
using assms
proof (induct s arbitrary: t)
case (Var x) then show ?case
by (cases t) simp_all
next
case (Fun f ss) note Fun' = this
show ?case
proof (cases t)
case (Var x) show ?thesis using Fun'(3)[of "[]"] by (simp add: Var)
next
case (Fun g ts)
have *: "length ss = length ts"
using Fun'(3) arg_cong[OF Fun'(2), of "λP. card {i |i p. i # p ∈ P}"]
by (auto simp: Fun exI[of "λx. x ∈ poss _", OF Nil_in_poss])
then have "i < length ss ⟹ poss (ss ! i) = poss (ts ! i)" for i
using arg_cong[OF Fun'(2), of "λP. {p. i # p ∈ P}"] by (auto simp: Fun)
then show ?thesis using * Fun'(2) Fun'(3)[of "[]"] Fun'(3)[of "_ # _ :: pos"]
by (auto simp: Fun intro!: nth_equalityI Fun'(1)[OF nth_mem, of n "ts ! n" for n])
qed
qed

lemma eq_ctxt_at_pos_by_poss:
assumes "p ∈ poss s" "p ∈ poss t"
and "⋀ q. ¬ (p ≤⇩p q) ⟹ q ∈ poss s ⟷ q ∈ poss t"
and "(⋀ q. q ∈ poss s ⟹ ¬ (p ≤⇩p q) ⟹ fun_at s q = fun_at t q)"
shows "ctxt_at_pos s p = ctxt_at_pos t p" using assms
proof (induct p arbitrary: s t)
case (Cons i p)
from Cons(2, 3) Cons(4, 5)[of "[]"] obtain f ss ts where [simp]: "s = Fun f ss" "t = Fun f ts"
by (cases s; cases t) auto
have flt: "j < i ⟹ j # q ∈ poss s ⟹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have fgt: "i < j ⟹ j # q ∈ poss s ⟹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have lt: "j < i ⟹ j # q ∈ poss s ⟷ j # q ∈ poss t" for j q by (intro Cons(4)) auto
have gt: "i < j ⟹ j # q ∈ poss s ⟷ j # q ∈ poss t" for j q by (intro Cons(4)) auto
from this[of _ "[]"] have "i < j ⟹ j < length ss ⟷ j < length ts" for j by auto
from this Cons(2, 3) have l: "length ss = length ts" by auto (meson nat_neq_iff)
have "ctxt_at_pos (ss ! i) p = ctxt_at_pos (ts ! i) p" using Cons(2, 3) Cons(4-)[of "i # q" for q]
by (intro Cons(1)[of "ss ! i" "ts ! i"]) auto
moreover have "take i ss = take i ts" using l lt Cons(2, 3) flt
by (intro nth_equalityI) (auto intro!: eq_term_by_poss_fun_at)
moreover have "drop (Suc i) ss = drop (Suc i) ts" using l Cons(2, 3) fgt gt[of "Suc i + j" for j]
by (intro nth_equalityI) (auto simp: nth_map intro!: eq_term_by_poss_fun_at, fastforce+)
ultimately show ?case by auto
qed auto

subsection ‹Misc›

lemma fun_at_hole_pos_ctxt_apply [simp]:
"fun_at C⟨t⟩ (hole_pos C) = fun_at t []"
by (induct C) auto

lemma vars_term_ctxt_apply [simp]:
"vars_term C⟨t⟩ = vars_ctxt C ∪ vars_term t"
by (induct C arbitrary: t) auto

lemma map_vars_term_ctxt_apply:
"map_vars_term f C⟨t⟩ = (map_vars_ctxt f C)⟨map_vars_term f t⟩"
by (induct C) auto

lemma map_term_replace_at_dist:
"p ∈ poss s ⟹ (map_term f g s)[p ← (map_term f g t)] = map_term f g (s[p ← t])"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) (auto simp: nth_list_update intro!: nth_equalityI)
qed auto

end
```