section ‹Preliminaries›
theory Terms_Positions
  imports Regular_Tree_Relations.Ground_Terms
begin

subsection ‹Additional operations on terms and positions›

subsubsection ‹Linearity›
fun linear_term :: "('f, 'v) term ⇒ bool" where
  "linear_term (Var _) = True" |
  "linear_term (Fun _ ts) = (is_partition (map vars_term ts) ∧ (∀t∈set ts. linear_term t))"
abbreviation "linear_sys ℛ ≡ ∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r"

subsubsection ‹Positions induced by contexts, by variables and by given subterms›

definition "possc C = {p | p t. p ∈ poss C⟨t⟩}"
definition "varposs s = {p | p. p ∈ poss s ∧ is_Var (s |_ p)}"
definition "poss_of_term u t = {p. p ∈ poss t ∧ t |_ p = u}"


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

definition "funas_rel ℛ = (⋃ (l, r) ∈ ℛ. funas_term l ∪ funas_term r)"

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 []"

subsubsection ‹Multihole context closure of a term relation as inductive set›

definition all_ctxt_closed where
  "all_ctxt_closed F r ⟷ (∀f ts ss. (f, length ss) ∈ F ⟶ length ts = length ss ⟶
    (∀i. i < length ts ⟶ (ts ! i, ss ! i) ∈ r) ⟶
    (∀ i. i < length ts ⟶ funas_term (ts ! i) ∪ funas_term (ss ! i) ⊆ F) ⟶ (Fun f ts, Fun f ss) ∈ r) ∧
    (∀ x. (Var x, Var x) ∈ r)"



subsection ‹Destruction and introduction of @{const all_ctxt_closed}›

lemma all_ctxt_closedD: "all_ctxt_closed F r ⟹ (f,length ss) ∈ F ⟹ length ts = length ss
  ⟹ ⟦⋀ i. i < length ts ⟹ (ts ! i, ss ! i) ∈ r ⟧
  ⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ts ! i) ⊆ F ⟧
  ⟹ ⟦⋀ i. i < length ts ⟹ funas_term (ss ! i) ⊆ F ⟧
  ⟹ (Fun f ts, Fun f ss) ∈ r"
  unfolding all_ctxt_closed_def by auto

lemma trans_ctxt_sig_imp_all_ctxt_closed: assumes tran: "trans r"
  and refl: "⋀ t. funas_term t ⊆ F ⟹ (t,t) ∈ r"
  and ctxt: "⋀ C s t. funas_ctxt C ⊆ F ⟹ funas_term s ⊆ F ⟹ funas_term t ⊆ F ⟹ (s,t) ∈ r ⟹ (C ⟨ s ⟩, C ⟨ t ⟩) ∈ r"
  shows "all_ctxt_closed F r" unfolding all_ctxt_closed_def
proof (rule, intro allI impI)
  fix f ts ss
  assume f: "(f,length ss) ∈ F" and
         l: "length ts = length ss" and
         steps: "∀ i < length ts. (ts ! i, ss ! i) ∈ r" and
         sig: "∀ i < length ts. funas_term (ts ! i) ∪  funas_term (ss ! i) ⊆ F"
  from sig have sig_ts: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ F"  unfolding set_conv_nth by auto
  let ?p = "λ ss. (Fun f ts, Fun f ss) ∈ r ∧ funas_term (Fun f ss) ⊆ F"
  let ?r = "λ xsi ysi. (xsi, ysi) ∈ r ∧ funas_term ysi ⊆ F"
  have init: "?p ts" by (rule conjI[OF refl], insert f sig_ts l, auto)
  have "?p ss"
  proof (rule parallel_list_update[where p = ?p and r = ?r, OF _ HOL.refl init l[symmetric]])
    fix xs i y
    assume len: "length xs = length ts"
       and i: "i < length ts"
       and r: "?r (xs ! i) y"
       and p: "?p xs"
    let ?C = "More f (take i xs) Hole (drop (Suc i) xs)"
    have id1: "Fun f xs = ?C ⟨ xs ! i⟩" using id_take_nth_drop[OF i[folded len]] by simp
    have id2: "Fun f (xs[i := y]) = ?C ⟨ y ⟩" using upd_conv_take_nth_drop[OF i[folded len]] by simp
    from p[unfolded id1] have C: "funas_ctxt ?C ⊆ F" and xi: "funas_term (xs ! i) ⊆ F" by auto
    from r have "funas_term y ⊆ F" "(xs ! i, y) ∈ r" by auto
    with ctxt[OF C xi this] C have r: "(Fun f xs, Fun f (xs[i := y])) ∈ r"
      and f: "funas_term (Fun f (xs[i := y])) ⊆ F" unfolding id1 id2 by auto
    from p r tran have "(Fun f ts, Fun f (xs[i := y])) ∈ r" unfolding trans_def by auto
    with f
    show "?p (xs[i := y])"  by auto
  qed (insert sig steps, auto)
  then show "(Fun f ts, Fun f ss) ∈ r" ..
qed (insert refl, auto)



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 add: par_Cons_iff)

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

lemma pos_les_eq_append_diff [simp]:
  "p ≤⇩p q ⟹ p @ (q -⇩p p) = q"
  by (metis option.sel pos_diff_def position_less_eq_def remove_prefix_append)

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

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

lemma less_eq_poss_append_itself [simp]: "p ≤⇩p (p @ q)"
  using position_less_eq_def by blast

lemma poss_ctxt_apply [simp]:
  "hole_pos C @ p ∈ poss C⟨s⟩ ⟷ p ∈ poss s"
  by (induct C) auto

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 par_Cons_iff)
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 simp add: par_Cons_iff 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"
proof (induct p arbitrary: s)
  case (Cons i p) then show ?case
    by (cases s) auto
qed auto

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

lemma subst_subt_at_dist:
  "p ∈ poss s ⟹ s ⋅ σ |_ p = s |_ p ⋅ σ"
proof (induct p arbitrary: s)
  case (Cons i p) then show ?case
    by (cases s) auto
qed auto

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 position_less_refl 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 UnCI ctxt_at_pos_subt_at_id term.set_intros(3) vars_term_ctxt_apply)

lemma linear_term_varposs_subst_replace_term:
  "linear_term s ⟹ p ∈ varposs 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: varposs_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: varposs_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_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 par_Cons_iff)
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

lemma ctxt_of_pos_term_apply_replace_at_ident:
  assumes "p ∈ poss s"
  shows "(ctxt_at_pos s p)⟨t⟩ = s[p ← t]"
  using assms
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"] Cons(2-)
    by (cases s) (auto simp: nth_append_Cons intro!: nth_equalityI)
qed auto

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 position_less_eq_def remove_prefix_append)

lemma ctxt_apply_subt_at_hole_pos [simp]: "C⟨s⟩ |_ hole_pos C = s"
  by (induct C) auto

lemma subt_at_imp_supteq':
  assumes "p ∈ poss s" and "s|_p = t" shows "s ⊵ t" using assms
proof (induct p arbitrary: s)
  case (Cons i p)
  from Cons(2-) show ?case using Cons(1)[of "args s ! i"]
    by (cases s) force+
qed auto

lemma subt_at_imp_supteq:
  assumes "p ∈ poss s" shows "s ⊵ s|_p"
proof -
 have "s|_p = s|_p" by auto
 with assms show ?thesis by (rule subt_at_imp_supteq')
qed


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)"
proof (induct t)
  case (Fun g ts) note IH = this
  show ?case
  proof (cases "g = f ∧ length ts = n")
    case False
    then obtain i where i: "i < length ts" "(f, n) ∈ funas_term (ts ! i)" using IH(2)
      using in_set_idx by force
    from IH(1)[OF nth_mem[OF this(1)] this(2)] show ?thesis using i(1)
      by (metis poss_Cons_poss subt_at.simps(2) term.sel(4))
  qed auto
qed simp

lemma finite_poss: "finite (poss s)"
proof (induct s)
  case (Fun f ts)
  have "poss (Fun f ts) = insert [] (⋃ (set (map2 (λ i p. ((#) i) ` p) [0..< length ts] (map poss ts))))"
    by (auto simp: image_iff set_zip split: prod.splits)
  then show ?case using Fun
    by (auto simp del: poss.simps dest!: set_zip_rightD)
qed simp

lemma finite_varposs: "finite (varposs s)"
  by (intro finite_subset[of "varposs s" "poss s"]) (auto simp: varposs_def finite_poss)

lemma gound_linear [simp]: "ground t ⟹ linear_term t"
  by (induct t) (auto simp: is_partition_alt is_partition_alt_def)

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 funas_ctxt_subst_apply_ctxt:
  "funas_ctxt (C ⋅⇩c σ) = funas_ctxt C ∪ (⋃ (funas_term ` σ ` vars_ctxt C))"
proof (induct C)
  case (More f ss C ts)
  then show ?case
    by (fastforce simp add: funas_term_subst)
qed simp

lemma varposs_Var[simp]:
  "varposs (Var x) = {[]}"
  by (auto simp: varposs_def)

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

lemma vars_term_varposs_iff:
  "x ∈ vars_term s ⟷ (∃ p ∈ varposs s. s |_ p = Var x)"
proof (induct s)
  case (Fun f ts)
  show ?case using Fun[OF nth_mem]
    by (force simp: in_set_conv_nth Bex_def)
qed auto

lemma vars_term_empty_ground:
  "vars_term s = {} ⟹ ground s"
  by (metis equals0D ground_substI subst_ident)

lemma ground_subst_apply: "ground t ⟹ t ⋅ σ = t"
  by (induct t) (auto intro: nth_equalityI)

lemma varposs_imp_poss:
  "p ∈ varposs s ⟹ p ∈ poss s" by (auto simp: varposs_def)

lemma varposs_empty_gound:
 "varposs 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 (metis ctxt_at_pos_subt_at_id funas_ctxt_apply le_sup_iff)

lemma varposs_ground_replace_at:
  "p ∈ varposs s ⟹ ground u ⟹ varposs s[p ← u] = varposs s - {p}"
proof (induct p arbitrary: s)
  case Nil then show ?case
    by (cases s) (auto simp: varposs_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 ∈ varposs (ts ! i)" by auto
  from Cons(1)[OF var Cons(3)] have "j < length ts ⟹ {j # q| q. q ∈ varposs (ts[i := (ts ! i)[p ← u]] ! j)} =
           {j # q |q. q ∈ varposs (ts ! j)} - {i # p}" for j
    by (cases "j = i") (auto simp add: nth_list_update)
  then show ?case by auto blast
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"
proof (induct p arbitrary: C)
  case (Cons i p)
  have [dest]: "length ss # p ∈ possc (More f ss D ts) ⟹ p ∈ possc D" for f ss D ts
    by (auto simp: possc_def)
  show ?case using Cons
    by (cases C) (auto simp: nth_append_Cons)
qed simp

end