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 Cu"
  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 Ct  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 Ct = 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 Cs (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]: "Cs[hole_pos C  t] = Ct"
  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 Ct (hole_pos C) = fun_at t []"
  by (induct C) auto

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

lemma map_vars_term_ctxt_apply:
  "map_vars_term f Ct = (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