Theory Terms_Positions

section ‹Preliminaries›
theory Terms_Positions
  imports 
    Regular_Tree_Relations.Ground_Terms
    First_Order_Rewriting.Trs
begin
subsection ‹Additional operations on terms and positions›

subsubsection ‹Linearity›
abbreviation "linear_sys ℛ ≡ ∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r"

subsubsection ‹Positions by given subterms›
definition "poss_of_term u t = {p. p ∈ poss t ∧ t |_ p = u}"

lemma var_poss_def: "var_poss s = {p | p. p ∈ poss s ∧ is_Var (s |_ p)}" 
  by (induct s, auto)


subsubsection ‹Replacing functions symbols that aren't specified in the signature by variables›

abbreviation "funas_rel ≡ funas_trs" 

lemma funas_rel_def: "funas_rel ℛ = (⋃ (l, r) ∈ ℛ. funas_term l ∪ funas_term r)"
  unfolding funas_trs_def funas_rule_def by auto

fun term_to_sig where
  "term_to_sig ℱ v (Var x) = Var x"
| "term_to_sig ℱ v (Fun f ts) =
    (if (f, length ts) ∈ ℱ then Fun f (map (term_to_sig ℱ v) ts) else Var v)"

fun ctxt_well_def_hole_path where
  "ctxt_well_def_hole_path ℱ Hole ⟷ True"
| "ctxt_well_def_hole_path ℱ (More f ss C ts) ⟷ (f, Suc (length ss + length ts)) ∈ ℱ ∧ ctxt_well_def_hole_path ℱ C"

fun inv_const_ctxt where
  "inv_const_ctxt ℱ v Hole = Hole"
| "inv_const_ctxt ℱ v ((More f ss C ts)) 
              = (More f (map (term_to_sig ℱ v) ss) (inv_const_ctxt ℱ v C) (map (term_to_sig ℱ v) ts))"

fun inv_const_ctxt' where
  "inv_const_ctxt' ℱ v Hole = Var v"
| "inv_const_ctxt' ℱ v ((More f ss C ts)) 
              = (if (f, Suc (length ss + length ts)) ∈ ℱ then Fun f (map (term_to_sig ℱ v) ss @ inv_const_ctxt' ℱ v C # map (term_to_sig ℱ v) ts) else Var v)"


subsubsection ‹Replace term at a given position in contexts›

fun replace_term_context_at :: "('f, 'v) ctxt ⇒ pos ⇒ ('f, 'v) term ⇒ ('f, 'v) ctxt"
  (‹_[_ ← _]⇩C› [1000, 0] 1000) where
  "replace_term_context_at □ p u = □"
| "replace_term_context_at (More f ss C ts) (i # ps) u =
    (if i < length ss then More f (ss[i := (ss ! i)[ps ← u]]) C ts
     else if i = length ss then More f ss (replace_term_context_at C ps u) ts
     else More f ss C (ts[(i - Suc (length ss)) := (ts ! (i - Suc (length ss)))[ps ← u]]))"

abbreviation "constT c ≡ Fun c []"


subsection ‹Lemmas for @{const poss} and ordering of positions›

lemma subst_poss_mono: "poss s ⊆ poss (s ⋅ σ)"
  by (induct s) force+

lemma par_pos_prefix [simp]:
  "(i # p) ⊥ (i # q) ⟹ p ⊥ q"
  by simp

lemma pos_diff_itself [simp]: "p -⇩p p = []"
  by (simp add: pos_diff_def)

lemma pos_diff_append_itself [simp]: "(p @ q) -⇩p p = q"
  by (simp add: pos_diff_def)

lemma poss_pos_diffI:
  "p ≤⇩p q ⟹ q ∈ poss s ⟹ q -⇩p p ∈ poss (s |_ p)"
  using poss_append_poss by fastforce

declare hole_pos_poss_conv[simp]

lemma pos_replace_at_pres:
  "p ∈ poss s ⟹ p ∈ poss s[p ← t]"
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"] Cons(2-)
    by (cases s) auto
qed auto

lemma par_pos_replace_pres:
  "p ∈ poss s ⟹ p ⊥ q ⟹ p ∈ poss s[q ← t]"
proof (induct p arbitrary: s q)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
    by (cases s; cases q) (auto simp add: nth_list_update)
qed auto

lemma poss_of_termE [elim]:
  assumes "p ∈ poss_of_term u s"
    and "p ∈ poss s ⟹ s |_ p = u ⟹ P"
  shows "P" using assms unfolding poss_of_term_def
  by blast

lemma poss_of_term_Cons:
  "i # p ∈ poss_of_term u (Fun f ts) ⟹ p ∈ poss_of_term u (ts ! i)"
  unfolding poss_of_term_def by auto

lemma poss_of_term_const_ctxt_apply:
  assumes "p ∈ poss_of_term (constT c) C⟨s⟩"
  shows "p ⊥ (hole_pos C) ∨ (hole_pos C) ≤⇩p p" using assms
proof (induct p arbitrary: C)
  case Nil then show ?case
    by (cases C) auto
next
  case (Cons i p) then show ?case
    by (cases C) (fastforce dest!: poss_of_term_Cons)+
qed


subsection ‹Lemmas for @{const subt_at} and @{const replace_term_at}›

lemma subt_at_append_dist:
  "p @ q ∈ poss s ⟹ s |_ (p @ q) = (s |_ p) |_ q" 
  by simp

lemma ctxt_apply_term_subt_at_hole_pos [simp]:
  "C⟨s⟩ |_ (hole_pos C @ q) = s |_ q" by simp

lemma replace_term_at_subt_at_id [simp]: "s[p ← (s |_ p)] = s"
proof (induct p arbitrary: s)
  case (Cons i p) then show ?case
    by (cases s) auto
qed auto


lemma replace_term_at_same_pos [simp]:
  "s[p ← u][p ← t] = s[p ← t]"
  using replace_term_at_above by blast

― ‹Replacement at under substitution›
lemma subt_at_vars_term:
  "p ∈ poss s ⟹ s |_ p = Var x ⟹ x ∈ vars_term s"
  by (metis var_poss_iff vars_term_var_poss_iff)

lemma linear_term_var_poss_subst_replace_term:
  "linear_term s ⟹ p ∈ var_poss s ⟹ p ≤⇩p q ⟹
     (s ⋅ σ)[q ← u] = s ⋅ (λ x. if Var x = s |_ p then (σ x)[q -⇩p p ← u] else (σ x))"
proof (induct q arbitrary: s p)
  case (Cons i q)
  show ?case using Cons(1)[of "args s ! i" "tl p"] Cons(2-)
    by (cases s) (auto simp: var_poss_def nth_list_update term_subst_eq_conv
      is_partition_alt is_partition_alt_def disjoint_iff subt_at_vars_term intro!: nth_equalityI)
qed (auto simp: var_poss_def)

― ‹Replacement at context parallel to the hole position›
lemma par_hole_pos_replace_term_context_at:
  "p ⊥ hole_pos C ⟹ C⟨s⟩[p ← u] = (C[p ← u]⇩C)⟨s⟩"
proof (induct p arbitrary: C)
  case (Cons i p)
  from Cons(2) obtain f ss D ts where [simp]: "C = More f ss D ts" by (cases C) auto 
  show ?case using Cons(1)[of D] Cons(2)
    by (auto simp: list_update_beyond list_update_append nth_append_Cons minus_nat.simps(2) split: nat.splits)
qed auto

lemma par_pos_replace_term_at:
  "p ∈ poss s ⟹ p ⊥ q ⟹ s[q ← t] |_ p = s |_ p"
proof (induct p arbitrary: s q)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
    by (cases s; cases q) (auto, metis nth_list_update)
qed auto


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


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

lemma replace_subterm_at_itself [simp]:
  "s[p ← (s |_ p)[q ← t]] = s[p @ q ← t]"
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"]
    by (cases s) auto
qed auto


lemma hole_pos_replace_term_at [simp]:
  "hole_pos C ≤⇩p p ⟹ C⟨s⟩[p ← u] = C⟨s[p -⇩p hole_pos C ← u]⟩"
proof (induct C arbitrary: p)
  case (More f ss C ts) then show ?case
    by (cases p) auto
qed auto

lemmas ctxt_of_pos_term_apply_replace_at_ident = replace_term_at_replace_at_conv

lemma ctxt_apply_term_replace_term_hole_pos [simp]:
  "C⟨s⟩[hole_pos C @ q  ← u] = C⟨s[q  ← u]⟩"
  by (simp add: pos_diff_def)


subsection ‹@{const term_to_sig} invariants and distributions›

lemma fuans_term_term_to_sig [simp]: "funas_term (term_to_sig ℱ v t) ⊆ ℱ"
  by (induct t) auto

lemma term_to_sig_id [simp]:
  "funas_term t ⊆ ℱ ⟹ term_to_sig ℱ v t = t"
  by (induct t) (auto simp add: UN_subset_iff map_idI)

lemma term_to_sig_subst_sig [simp]:
  "funas_term t ⊆ ℱ ⟹ term_to_sig ℱ v (t ⋅ σ) = t ⋅ (λ x.  term_to_sig ℱ v (σ x))"
  by (induct t) auto

lemma funas_ctxt_ctxt_inv_const_ctxt_ind [simp]:
  "funas_ctxt C ⊆ ℱ ⟹ inv_const_ctxt ℱ v C = C"
  by (induct C) (auto simp add: UN_subset_iff intro!: nth_equalityI)

lemma term_to_sig_ctxt_apply [simp]:
  "ctxt_well_def_hole_path ℱ C ⟹ term_to_sig ℱ v C⟨s⟩ = (inv_const_ctxt ℱ v C)⟨term_to_sig ℱ v s⟩"
  by (induct C) auto

lemma term_to_sig_ctxt_apply' [simp]:
  "¬ ctxt_well_def_hole_path ℱ C ⟹ term_to_sig ℱ v C⟨s⟩ = inv_const_ctxt' ℱ v C"
  by (induct C) auto

lemma funas_ctxt_ctxt_well_def_hole_path:
  "funas_ctxt C ⊆ ℱ ⟹ ctxt_well_def_hole_path ℱ C"
  by (induct C) auto


subsection ‹Misc›

lemma funas_term_subt_at:
  "(f, n) ∈ funas_term t ⟹ (∃ p ts. p ∈ poss t ∧ t |_ p = Fun f ts ∧ length ts = n)"
  unfolding funas_term_poss_conv by force

declare ground_substI[intro, simp]
lemma ground_ctxt_substI:
  "(⋀ x. x ∈ vars_ctxt C ⟹ ground (σ x)) ⟹ ground_ctxt (C ⋅⇩c σ)"
  by (induct C) auto

lemma var_poss_Fun[simp]:
  "var_poss (Fun f ts) = { i # p| i p. i < length ts ∧ p ∈ var_poss (ts ! i)}"
  by auto

lemma vars_term_empty_ground:
  "vars_term s = {} ⟹ ground s"
  unfolding ground_vars_term_empty .

lemma var_poss_empty_gound:
 "var_poss s = {} ⟷ ground s"
  by (induct s) (fastforce simp: in_set_conv_nth)+

lemma funas_term_subterm_atI [intro]:
  "p ∈ poss s ⟹ funas_term s ⊆ ℱ ⟹ funas_term (s |_ p) ⊆ ℱ"
  by (meson subset_trans subt_at_imp_supteq' supteq_imp_funas_term_subset)

lemma var_poss_ground_replace_at:
  "p ∈ var_poss s ⟹ ground u ⟹ var_poss s[p ← u] = var_poss s - {p}"
proof (induct p arbitrary: s)
  case Nil then show ?case
    by (cases s) (auto simp: var_poss_empty_gound)
next
  case (Cons i p)
  from Cons(2) obtain f ts where [simp]: "s = Fun f ts" by (cases s) auto
  from Cons(2) have var: "p ∈ var_poss (ts ! i)" by auto
  from Cons(1)[OF var Cons(3)] have "j < length ts ⟹ {j # q| q. q ∈ var_poss (ts[i := (ts ! i)[p ← u]] ! j)} =
           {j # q |q. q ∈ var_poss (ts ! j)} - {i # p}" for j
    by (cases "j = i") (auto simp add: nth_list_update)
  then show ?case by auto 
qed

lemma funas_term_replace_at_upper:
  "funas_term s[p ← t] ⊆ funas_term s ∪ funas_term t"
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"]
    by (cases s) (fastforce simp: in_set_conv_nth nth_list_update split!: if_splits)+
qed simp

lemma funas_term_replace_at_lower:
  "p ∈ poss s ⟹ funas_term t ⊆ funas_term (s[p ← t])"
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"] Cons(2-)
    by (cases s) (fastforce simp: in_set_conv_nth nth_list_update split!: if_splits)+
qed simp

lemma poss_of_term_possI [intro!]:
  "p ∈ poss s ⟹ s |_ p = u ⟹ p ∈ poss_of_term u s"
  unfolding poss_of_term_def by blast

lemma poss_of_term_replace_term_at:
  "p ∈ poss s ⟹ p ∈ poss_of_term u s[p ← u]"
proof (induct p arbitrary: s)
  case (Cons i p) then show ?case
    by (cases s) (auto simp: poss_of_term_def)
qed auto

lemma constT_nfunas_term_poss_of_term_empty:
  "(c, 0) ∉ funas_term t ⟷ poss_of_term (constT c) t = {}"
  unfolding poss_of_term_def
  using funas_term_subt_at[of c 0 t]
  using funas_term_subterm_atI[where ?ℱ ="funas_term t" and ?s = t, THEN subsetD]
  by auto

lemma poss_of_term_poss_emptyD:
  assumes "poss_of_term u s = {}"
  shows "p ∈ poss s ⟹ s |_ p ≠ u" using assms
  unfolding poss_of_term_def by blast

lemma possc_subt_at_ctxt_apply:
  "p ∈ possc C ⟹ p ⊥ hole_pos C ⟹ C⟨s⟩ |_ p = C⟨t⟩ |_ p"
  by (metis par_pos_replace_term_at poss_imp_possc replace_at_hole_pos)

end