Theory Regular_Tree_Relations.Term_Context

section ‹Preliminaries›

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

subsection ‹Additional functionality on @{type term} and @{type ctxt}›
 
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 ‹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_both f ≡ map_prod f f"

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

definition adapt_vars_ctxt :: "('f,'q)ctxt ⇒ ('f,'v)ctxt" where
  "adapt_vars_ctxt = map_vars_ctxt (λ_. undefined)"


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

lemma subst_at_ctxt_of_pos_term_eq_termD:
  assumes "s = t" "p ∈ poss t"
  shows "s |_ p = t |_ p ∧ ctxt_of_pos_term p s = ctxt_of_pos_term p t" using assms
  by 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 ⟹ replace_at 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
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 Hole = Hole"
  "adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"
  by (simp_all add: adapt_vars_ctxt_def adapt_vars_def)

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 empty_pos_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_of_pos_term p s = ctxt_of_pos_term p t" 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_of_pos_term p (ss ! i) = ctxt_of_pos_term p (ts ! i)" 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 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