Theory Term_Auxx

theory Term_Auxx
  imports TRS.Term_More TRS.Multihole_Context
begin

(* List functions *)
fun countWhile :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"  where
  "countWhile P [] = 0"
| "countWhile P (x # xs) = (if P x then 1 + countWhile P xs else 0)"

fun insert_at where
  "insert_at 0 x ys = x # ys"
| "insert_at n x [] = [x]"
| "insert_at (Suc n) x (y # ys) = y # insert_at n x ys"

lemma insert_at_empty [simp]: "insert_at n x [] = [x]"
  by (cases n) auto

lemma insert_at_length [simp]:
  "length (insert_at n x xs) = Suc (length xs)"
proof (induct n arbitrary: xs)
  case (Suc n) then show ?case
    by (cases xs) auto
qed auto

lemma insert_at_set [simp]:
  "set (insert_at n x xs) = insert x (set xs)"
proof (induct n arbitrary: xs)
  case (Suc n) then show ?case
    by (cases xs) auto
qed auto


lemma insert_at_nth_gr_length [simp]:
  "length xs ≤ n ⟹ insert_at n x xs = xs @ [x]"
proof (induct n arbitrary: xs)
  case (Suc n) then show ?case
    by (cases xs) auto
qed auto

lemma insert_at_nth_less_length [simp]:
  "¬ n < length xs ⟹ insert_at n x xs = xs @ [x]"
  by (auto simp: not_less)

lemma insert_at_take_drop_conv:
  "insert_at n x xs = take n xs @ x # drop n xs"
proof (induct n arbitrary: xs)
  case (Suc n) then show ?case
    by (cases xs) auto
qed auto

lemma insert_at_nth:
  assumes "i < Suc (length xs)" "n ≤ length xs"
  shows "insert_at n x xs ! i =
     (if i < n then xs ! i else if i = n then x else xs ! (i - Suc 0))"
  using assms unfolding insert_at_take_drop_conv
  by (auto simp: nth_append_Cons min_def)

lemma set_zip_insert_at_nth [simp]:
  "length xs = length ys ⟹ set (zip (insert_at n x xs) (insert_at n y ys)) = insert (x, y) (set (zip xs ys))"
proof (induct n arbitrary: xs ys)
  case (Suc n) then show ?case
    by (cases xs; cases ys) auto
qed auto

lemma map_insert_at_dist:
  "map f (insert_at n x xs) = insert_at n (f x) (map f xs)"
proof (induct n arbitrary: xs)
  case (Suc n) then show ?case
    by (cases xs) auto
qed auto

lemma countWhile_length_takeWhile:
  "countWhile P xs = length (takeWhile P xs)"
  by (induct xs) auto

lemma countWhile_append:
  "(⋀x. x ∈ set xs ⟹ P x) ⟹ countWhile P (xs @ ys) = length xs + countWhile P ys"
  by (induct xs) auto

lemma countWhile_in_rangeI:
  "x ∈ set xs ⟹ ¬ P x ⟹ countWhile P xs < length xs"
  by (induct xs) auto

lemma takeWhile_nle_length_P:
  "¬ length (takeWhile P ss) < length ss ⟹ (∀ x ∈ set ss. P x)"
  by (metis not_le_imp_less set_takeWhileD takeWhile_eq_take take_all)

lemma takeWhile_append3:
  "(⋀ y. y ∈ set ys ⟹ ¬ P y) ⟹ takeWhile P (xs @ ys) = takeWhile P xs"
  by (cases ys) (auto simp add: takeWhile_tail)

lemma dropWhile_append4:
  "(⋀ y. y ∈ set ys ⟹ ¬ P y) ⟹ dropWhile P (xs @ ys) = dropWhile P xs @ ys"
  by (cases ys) (auto simp add: dropWhile_append3)

lemma take_countWhile_takeWhile:
  "take (countWhile P xs) xs = takeWhile P xs" unfolding countWhile_length_takeWhile
  by (metis takeWhile_eq_take)

lemma drop_countWhile_dropWhile:
  "drop (countWhile P xs) xs = dropWhile P xs"
  by (simp add: countWhile_length_takeWhile dropWhile_eq_drop)


lemma countWhile_length_less_eq: "countWhile P xs < length xs ∨ countWhile P xs = length xs"
  by (auto simp: countWhile_length_takeWhile le_neq_implies_less length_takeWhile_le)

lemma countWhile_length_less_eq' [simp]: "countWhile P xs ≤ length xs ⟷ True"
  by (auto simp: countWhile_length_takeWhile le_neq_implies_less length_takeWhile_le)

lemma countWhile_gre_lenght [simp]: "length xs < countWhile P xs ⟷ False"
  using countWhile_length_less_eq dual_order.asym by fastforce

lemma countWhile_nless [dest!]:
  "¬ countWhile P xs < length xs ⟹ countWhile P xs = length xs"
  using countWhile_length_less_eq by blast


lemma countWhile_eq_lengthE [elim!]:
  assumes "countWhile P xs = length xs"
  shows "((⋀ x. x ∈ set xs ⟹ P x) ⟹ R) ⟹ R"
  using assms nat_less_le takeWhile_nle_length_P
  unfolding countWhile_length_takeWhile
  by metis

lemma countWhile_eq_length_conv: "countWhile P xs = length xs ⟷ (∀ x ∈ set xs. P x)"
  by auto (metis countWhile_length_takeWhile takeWhile_eq_all_conv)

lemma countWhile_less_length:
  assumes "countWhile P xs < length xs"
  shows "(⋀ x. x ∈ set (take (countWhile P xs) xs) ⟹ P x)" "¬ P (xs ! countWhile P xs)"
  using assms unfolding countWhile_length_takeWhile
  by (induct xs) (auto split: if_splits)

lemma countWhile_less_lengthE:
  assumes "countWhile P xs < length xs"
  obtains ys x zs where "xs = ys @ x # zs" "(⋀ x. x ∈ set ys ⟹ P x)" "¬ P x" "countWhile P xs = length ys"
  using countWhile_less_length[OF assms] assms
  using id_take_nth_drop[OF assms]
  by auto

lemma list_update_append_Cons:
  "(xs @ y # ys)[i:=x] = (if i < length xs then xs[i := x] @ y # ys
     else if i = length xs then xs @ x # ys else xs @ y # ys[(i - Suc (length xs)) := x])"
  by (induct xs arbitrary: i)(auto split:nat.split)

lemma remove_prefix_Cons [simp]:
  "remove_prefix (i # xs) (i # ys) = remove_prefix xs ys"
  by auto

lemma remove_prefix_append [simp]:
  "remove_prefix (xs @ ys) (xs @ zs) = remove_prefix ys zs"
  by (induct xs) auto

― ‹Replacing terms at given position›

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)"

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 nth_append_Cons intro!: nth_equalityI)
qed

lemma replace_term_at_replace_at_conv:
  "p ∈ poss s ⟹ s[p ← t] = replace_at 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 simp: parallel_pos)
  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[the (remove_prefix p q) ← 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_hole [simp]:
  "p = hole_pos C ⟹ C⟨s⟩[p ← t] = C⟨t⟩"
  by (induct C arbitrary: p) auto

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

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

fun replace_term_at_ctxt where
  "replace_term_at_ctxt C [] t = C"
| "replace_term_at_ctxt (More f ss C ts) (i # ps) t =
    (if i < length ss then More f (ss[i:=(replace_term_at (ss ! i) ps t)]) C ts
     else if i = length ss then More f ss (replace_term_at_ctxt C ps t) ts
     else if i - (Suc (length ss)) < length ts
       then More f ss C (ts[(i - (Suc (length ss))) := (replace_term_at (ts ! (i - (Suc (length ss)))) ps t)])
     else More f ss C ts)"
| "replace_term_at_ctxt □ _ _ = □"


lemma replace_parallel_ctxt [simp]:
  "hole_pos C ⊥ p ⟹ C⟨s⟩[p ← t] = (replace_term_at_ctxt C p t)⟨s⟩"
proof (induct p arbitrary: C)
  case (Cons i p) then show ?case
    by (cases C) (auto simp: nth_append_Cons list_update_append_Cons)
qed (auto simp: parallel_pos)

― ‹replacing function distribution over substitutions of linear terms›

lemma poss_subt_at_Var:
  "p ∈ poss s ⟹ s |_ p = Var x ⟹ x ∈ vars_term s"
  using subt_at_imp_supteq subteq_Var_imp_in_vars_term by fastforce

lemma replace_term_under_subst:
  "linear_term s ⟹ q ∈ varposs s ⟹ q ≤⇩p p ⟹
    (s ⋅ σ)[p ← t] = s ⋅ (λ x. if x = the_Var (s |_ q) then (σ x)[the (remove_prefix q p) ← t] else (σ x))"
proof (induct s arbitrary: p q)
  case (Fun f ts)
  obtain i qs ps where *: "q = i # qs" "p = i # ps" using Fun(3, 4)
    by (cases p; cases q) force+
  show ?case using Fun(1)[OF nth_mem, of i qs ps] Fun(2-) unfolding *
    apply (auto simp: nth_list_update is_partition_def varposs_iff intro!: nth_equalityI term_subst_eq)
    using nat_neq_iff poss_subt_at_Var by fastforce
qed (auto simp: varposs_iff)

― ‹replace term at position function symbol space›

lemma replace_term_funas:
  "funas_term s[p ← t] ⊆ funas_term s ∪ funas_term t"
proof (induct s arbitrary: p)
  case (Var x) then show ?case
    by (cases p) auto
next
  case (Fun f ts)
  show ?case using Fun[OF nth_mem, of "hd p" "tl p"]
    by (cases p) (auto simp: in_set_conv_nth nth_list_update split: if_splits, auto)
qed

lemma replace_term_at_ctxt_funas:
  "funas_ctxt (replace_term_at_ctxt C p t) ⊆ funas_ctxt C ∪ funas_term t"
proof (induct C arbitrary: p)
  case Hole
  then show ?case by (cases p) auto
next
  case (More f ss C ts) show ?case
  proof (cases p)
    case [simp]: (Cons i q)
    have "i < length ss ⟹ ?thesis" using replace_term_funas[of "ss ! i" q t]
      by (auto dest!: subsetD[OF set_update_subset_insert])
    moreover have "¬ i < length ss ⟹ i ≠ length ss ⟹ i < Suc (length ss + length ts) ⟹ ?thesis"
      using replace_term_funas[of "ts ! (i - Suc (length ss))" q t]
      by (auto dest!: subsetD[OF set_update_subset_insert])
    moreover have "i = length ss ⟹ ?thesis" using More[of q] by auto
    moreover have "¬ i < Suc (length ss + length ts) ⟹ ?thesis" by auto
    ultimately show ?thesis by linarith 
  qed auto
qed

― ‹Replace term at position subterm at position›

lemma replace_term_at_subt_at_subt_at [simp]:
  "p ∈ poss s ⟹ s[p ← u] |_ p = u"
proof (induct p arbitrary: s)
  case (Cons a p) then show ?case
    by (cases s) auto
qed auto

lemma replace_term_at_subt_at_parallel [simp]:
  "p ∈ poss s ⟹ q ∈ poss s ⟹ p ⊥ q ⟹ s[p ← u] |_ q = s |_ q"
  by (induct s arbitrary: p q) (auto simp: nth_list_update)

lemma replace_term_at_subt_at_above [simp]:
  "p ∈ poss s ⟹ q ∈ poss s ⟹ q <⇩p p ⟹ s[p ← u] |_ q = (s |_ q)[the (remove_prefix q p) ← u]"
  by (metis ctxt_supt_id hole_pos_ctxt_of_pos_term order_pos.order.strict_implies_order replace_at_subt_at replace_term_below_hole)

― ‹Replace term at position changes in position set›

lemma replace_with_subterm_at [simp]:
  "s[p ← s |_ p] = s"
proof (induct s arbitrary: p)
  case (Var x) then show ?case
    by (cases p) auto
next
  case (Fun f ts) then show ?case
    by (cases p) auto
qed

lemma replace_term_at_poss:
  "p ∈ poss s ⟹ poss s[p ← u] = {q. q ∈ poss s ∧ (q <⇩p p ∨ p ⊥ q)} ∪ {p @ q | q. q ∈ poss u}"
proof (induct p arbitrary: s)
  case (Cons i p)
  show ?case using Cons(1)[of "args s ! i"] Cons(2-)
    by (cases s) (auto 0 0 simp add: less_pos_def' nth_list_update, blast+)
qed auto

― ‹recovering substitution via replace terms at position›

abbreviation "poss_args f ts ≡ map (λ i. map ((#) i) (f (ts ! i))) [0 ..< length ts]"

fun varposs_list :: "('f, 'v) term ⇒ pos list" where
  "varposs_list (Var x) = [[]]" |
  "varposs_list (Fun f ts) = concat (poss_args varposs_list ts)"

lemma varposs_list_varposs_conv:
  "set (varposs_list s) = varposs s" by (induct s) auto

lemma varposs_parallel_or_eq:
  "p ∈ varposs s ⟹ q ∈ varposs s ⟹ p ⊥ q ∨ p = q"
  by (metis append_Nil2 less_pos_def' pos_cases prefix_pos_diff var_pos_maximal varposs_iff)

lemma varposs_list_var_terms_length:
  "length (varposs_list t) = length (vars_term_list t)"
  by (induct t) (auto simp: vars_term_list.simps intro: eq_length_concat_nth)

lemma map_cons_presv_distinct:
  "distinct t ⟹ distinct (map ((#) i) t)"
  by (simp add: distinct_conv_nth)

lemma varposs_listE [elim]:
  assumes "p ∈ set (varposs_list s) ⟹ P"
  shows "p ∈ varposs s ⟹ P" using assms
  by (auto simp: varposs_list_varposs_conv)

lemma varposs_empty_gound:
  "varposs s = {} ⟷ ground s"
  by (induct s) (auto simp: lessThan_def dest: all_nth_imp_all_set)

lemma ground_subt_at_Var_False [dest]:
  "ground u ⟹ q ∈ poss u ⟹ u |_ q = Var x ⟹ False"
  using varposs_empty_gound varposs_iff by fastforce

lemma varposs_ground_replace:
  assumes "p ∈ varposs s" "ground u"
  shows "varposs s[p ← u] = varposs s - {p}" 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_list_update lessThan_def split: if_splits)
qed (auto simp: equals0D varposs_empty_gound dest: varposs_parallel_or_eq)

lemma varposs_list_Nil_ground:
  "varposs_list s = [] ⟹ ground s"
  using varposs_empty_gound
  using varposs_list_varposs_conv by force

declare vars_term_list.simps [simp del]

― ‹Positions of a concrete variable›


lemma length_takeWhile_eq_P_nth:
  assumes "⋀i. i < j ⟹ P (xs ! i)" and "j < length xs" and "¬ P (xs ! j)"
  shows "length (takeWhile P xs) = j" using assms
  using length_takeWhile_less_P_nth[of j P xs]
  by auto (metis nat_less_le nth_mem set_takeWhileD takeWhile_nth)

fun first_varposs_of :: "'v ⇒ ('f, 'v) term  ⇒ pos option" where
  "first_varposs_of y (Var x) = (if x = y then Some [] else None)"
| "first_varposs_of y (Fun f ts) = (let n = length (takeWhile (λ t. y ∉ vars_term t) ts) in 
    if n < length ts then Some (n # the (first_varposs_of y (ts ! n))) else None)"

lemma first_varposs_of_poss:
  "x ∈ vars_term s ⟹ the (first_varposs_of x s) ∈ poss s"
  using takeWhile_nle_length_P
  by (induct s) (auto simp: Let_def, metis (mono_tags) nth_length_takeWhile nth_mem)

lemma first_varposs_of_complete:
  "x ∈ vars_term s ⟹ first_varposs_of x s ≠ None"
  using takeWhile_nle_length_P
  by (induct s) (auto simp: Let_def)

lemma first_varposs_of_sound [simp]:
  "x ∈ vars_term s ⟹ s |_ the (first_varposs_of x s) = Var x"
  apply (induct s) apply (auto simp: Let_def)
  using nth_length_takeWhile nth_mem apply blast
  using takeWhile_nle_length_P by blast

lemma first_varposs_of_varposs:
  "x ∈ vars_term s ⟹ the (first_varposs_of x s) ∈ varposs s"
  using first_varposs_of_poss first_varposs_of_sound unfolding varposs_iff
  by fast

lemma first_varposs_of_neq_or_par: 
  "x ∈ vars_term s ⟹ y ∈ vars_term s ⟹ x ≠ y ⟹ the (first_varposs_of x s) ⊥ the (first_varposs_of y s)"
  apply (induct s) apply (auto simp: Let_def dest: takeWhile_nle_length_P)
  apply (metis nth_length_takeWhile nth_mem)
  done

lemma linear_term_fist_varposs_of_simp:
  assumes "linear_term (Fun f ts)" "i < length ts" "x ∈ vars_term (ts ! i)"
  shows "the (first_varposs_of x (Fun f ts)) = i # the (first_varposs_of x (ts ! i))" using assms
  by (auto simp: Let_def is_partition_def dest: takeWhile_nle_length_P intro: length_takeWhile_eq_P_nth)
    (metis IntI empty_iff nat_neq_iff nth_length_takeWhile)

lemma vars_term_first_varposs_subst [simp]:
  "x ∈ vars_term l ⟹ l ⋅ σ |_ the (first_varposs_of x l) = σ x"
  apply (induct l) apply (auto simp: Let_def dest: takeWhile_nle_length_P)
  using nth_length_takeWhile nth_mem by blast


― ‹Cutting a context n times›
fun cut_ctxt where
  "cut_ctxt n Hole = Hole"
|  "cut_ctxt 0 C = C"
|  "cut_ctxt (Suc n) (More f ss C ts)= cut_ctxt n C"

lemma cut_ctxt_pos_id:
  assumes "hole_pos C ≤⇩p p"
  shows "cut_ctxt (length p) C = Hole" using assms
proof (induct C arbitrary: p)
  case (More f ss C ts)
  then show ?case by (cases p) (auto simp: Let_def)
qed auto

lemma cut_ctxt_apply_ctxt:
  assumes "p ≤⇩p hole_pos C"
  shows "(cut_ctxt (length p) C)⟨s⟩ = C⟨s⟩ |_ p" using assms
proof (induct C arbitrary: p)
  case (More f ss C ts)
  then show ?case by (cases p) (auto simp: map_nth)
qed simp

lemma cut_ctxt_funas:
  "funas_ctxt (cut_ctxt n C) ⊆ funas_ctxt C"
proof (induct C arbitrary: n)
  case (More f ss C ts)
  then show ?case by (cases n) auto
qed simp



end