Theory 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

subsection ‹Properties on @{const adapt_vars} and @{const adapt_vars_ctxt}›

lemma adapt_vars2:
  "adapt_vars (adapt_vars t) = adapt_vars t"
  by (induct t) (auto simp add: adapt_vars_def)

lemma adapt_vars_simps[code, simp]: "adapt_vars (Fun f ts) = Fun f (map adapt_vars ts)"
  by (induct ts, auto simp: adapt_vars_def)

lemma adapt_vars_reverse: "ground t ⟹ adapt_vars t' = t ⟹ adapt_vars t = t'"
  unfolding 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

lemma ground_adapt_vars [simp]: "ground (adapt_vars t) = ground t"
  by (simp add: adapt_vars_def)
lemma funas_term_adapt_vars[simp]: "funas_term (adapt_vars t) = funas_term t" by (simp add: adapt_vars_def)

lemma adapt_vars_adapt_vars[simp]: fixes t :: "('f,'v)term"
  assumes g: "ground t"
  shows "adapt_vars (adapt_vars t :: ('f,'w)term) = 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

lemma adapt_vars_inj:
  assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
  shows "x = y"
  using adapt_vars_adapt_vars assms by metis

lemma adapt_vars_ctxt_simps[simp, code]: 
  "adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"
  "adapt_vars_ctxt Hole = Hole" unfolding adapt_vars_ctxt_def adapt_vars_def by auto

lemma adapt_vars_ctxt[simp]: "adapt_vars (C ⟨ t ⟩ ) = (adapt_vars_ctxt C) ⟨ adapt_vars t ⟩"
  by (induct C, auto)

lemma adapt_vars_subst[simp]: "adapt_vars (l ⋅ σ) = l ⋅ (λ x. adapt_vars (σ x))"
  unfolding adapt_vars_def
  by (induct l) auto

lemma adapt_vars_gr_map_vars [simp]:
  "ground t ⟹ map_vars_term f t = adapt_vars t"
  by (induct t) auto


lemma adapt_vars_gr_ctxt_of_map_vars [simp]:
  "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