Theory List_Extra

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: List_Extra.thy                                                       *)
(* Authors: Simon Foster and Frank Zeyda                                      *)
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
(******************************************************************************)

section ‹ Lists: extra functions and properties ›

theory List_Extra
  imports
  "HOL-Library.Sublist"
  "HOL-Library.Monad_Syntax"
  "HOL-Library.Prefix_Order"
  "Optics.Lens_Instances"
begin

subsection ‹ Useful Abbreviations ›

abbreviation "list_sum xs ≡ foldr (+) xs 0"

subsection ‹ Folds ›

context abel_semigroup
begin

  lemma foldr_snoc: "foldr (❙*) (xs @ [x]) k = (foldr (❙*) xs k) ❙* x"
    by (induct xs, simp_all add: commute left_commute)
  
end

subsection ‹ List Lookup ›

text ‹
  The following variant of the standard ‹nth› function returns ‹⊥› if the index is 
  out of range.
›

primrec
  nth_el :: "'a list ⇒ nat ⇒ 'a option" (‹_⟨_⟩⇩_l› [90, 0] 91)
where
  "[]⟨i⟩⇩_l = None"
| "(x # xs)⟨i⟩⇩_l = (case i of 0 ⇒ Some x | Suc j ⇒ xs ⟨j⟩⇩_l)"

lemma nth_el_appendl[simp]: "i < length xs ⟹ (xs @ ys)⟨i⟩⇩_l = xs⟨i⟩⇩_l"
  apply (induct xs arbitrary: i)
   apply simp
  apply (case_tac i)
   apply simp_all
  done

lemma nth_el_appendr[simp]: "length xs ≤ i ⟹ (xs @ ys)⟨i⟩⇩_l = ys⟨i - length xs⟩⇩_l"
  apply (induct xs arbitrary: i)
   apply simp
  apply (case_tac i)
   apply simp_all
  done

subsection ‹ Extra List Theorems ›

subsubsection ‹ Map ›

lemma map_nth_Cons_atLeastLessThan:
  "map (nth (x # xs)) [Suc m..<n] = map (nth xs) [m..<n - 1]"
proof -
  have "nth xs = nth (x # xs) ∘ Suc"
    by auto
  hence "map (nth xs) [m..<n - 1] = map (nth (x # xs) ∘ Suc) [m..<n - 1]"
    by simp
  also have "... = map (nth (x # xs)) (map Suc [m..<n - 1])"
    by simp
  also have "... = map (nth (x # xs)) [Suc m..<n]"
    by (metis Suc_diff_1 le_0_eq length_upt list.simps(8) list.size(3) map_Suc_upt not_less upt_0)
  finally show ?thesis ..
qed

subsubsection ‹ Sorted Lists ›

lemma sorted_last [simp]: "⟦ x ∈ set xs; sorted xs ⟧ ⟹ x ≤ last xs"
  by (induct xs, auto)

lemma sorted_prefix:
  assumes "xs ≤ ys" "sorted ys"
  shows "sorted xs"
proof -
  obtain zs where "ys = xs @ zs"
    using Prefix_Order.prefixE assms(1) by auto
  thus ?thesis
    using assms(2) sorted_append by blast
qed

lemma sorted_map: "⟦ sorted xs; mono f ⟧ ⟹ sorted (map f xs)"
  by (simp add: monoD sorted_iff_nth_mono)

lemma sorted_distinct [intro]: "⟦ sorted (xs); distinct(xs) ⟧ ⟹ (∀ i<length xs - 1. xs!i < xs!(i + 1))"
  apply (induct xs)
   apply (auto)
  apply (metis (no_types, opaque_lifting) Suc_leI Suc_less_eq Suc_pred gr0_conv_Suc not_le not_less_iff_gr_or_eq nth_Cons_Suc nth_mem nth_non_equal_first_eq)
  done

text ‹ Is the given list a permutation of the given set? ›

definition is_sorted_list_of_set :: "('a::ord) set ⇒ 'a list ⇒ bool" where
"is_sorted_list_of_set A xs = ((∀ i<length(xs) - 1. xs!i < xs!(i + 1)) ∧ set(xs) = A)"

lemma sorted_is_sorted_list_of_set:
  assumes "is_sorted_list_of_set A xs"
  shows "sorted(xs)" and "distinct(xs)"
using assms proof (induct xs arbitrary: A)
  show "sorted []"
    by auto
next
  show "distinct []"
    by auto
next
  fix A :: "'a set"
  case (Cons x xs) note hyps = this
  assume isl: "is_sorted_list_of_set A (x # xs)"
  hence srt: "(∀i<length xs - Suc 0. xs ! i < xs ! Suc i)"
    using less_diff_conv by (auto simp add: is_sorted_list_of_set_def)
  with hyps(1) have srtd: "sorted xs"
    by (simp add: is_sorted_list_of_set_def)
  with isl show "sorted (x # xs)"
    apply (auto simp add: is_sorted_list_of_set_def)
    apply (metis (mono_tags, lifting) all_nth_imp_all_set less_le_trans linorder_not_less not_less_iff_gr_or_eq nth_Cons_0 sorted_iff_nth_mono zero_order(3))
    done
  from srt hyps(2) have "distinct xs"
    by (simp add: is_sorted_list_of_set_def)
  then have False if "x ∈ set xs"
    using distinct_Ex1 [OF _ that] isl unfolding is_sorted_list_of_set_def
    by (metis add.commute add_diff_cancel_left' leD length_Cons less_le not_gr_zero nth_Cons' plus_1_eq_Suc sorted_iff_nth_mono srtd)
  with isl ‹distinct xs› show "distinct (x # xs)"
    by force
qed

lemma is_sorted_list_of_set_alt_def:
  "is_sorted_list_of_set A xs ⟷ sorted (xs) ∧ distinct (xs) ∧ set(xs) = A"
  apply (auto intro: sorted_is_sorted_list_of_set)
    apply (auto simp add: is_sorted_list_of_set_def)
  apply (metis Nat.add_0_right One_nat_def add_Suc_right sorted_distinct)
  done

definition sorted_list_of_set_alt :: "('a::ord) set ⇒ 'a list" where
"sorted_list_of_set_alt A =
  (if (A = {}) then [] else (THE xs. is_sorted_list_of_set A xs))"

lemma is_sorted_list_of_set:
  "finite A ⟹ is_sorted_list_of_set A (sorted_list_of_set A)"
  by (simp add: is_sorted_list_of_set_alt_def)

lemma sorted_list_of_set_other_def:
  "finite A ⟹ sorted_list_of_set(A) = (THE xs. sorted(xs) ∧ distinct(xs) ∧ set xs = A)"
  apply (rule sym)
  apply (rule the_equality)
   apply (auto)
  apply (simp add: sorted_distinct_set_unique)
  done

lemma sorted_list_of_set_alt [simp]:
  "finite A ⟹ sorted_list_of_set_alt(A) = sorted_list_of_set(A)"
  apply (rule sym)
  apply (auto simp add: sorted_list_of_set_alt_def is_sorted_list_of_set_alt_def sorted_list_of_set_other_def)
  done

text ‹ Sorting lists according to a relation ›

definition is_sorted_list_of_set_by :: "'a rel ⇒ 'a set ⇒ 'a list ⇒ bool" where
"is_sorted_list_of_set_by R A xs = ((∀ i<length(xs) - 1. (xs!i, xs!(i + 1)) ∈ R) ∧ set(xs) = A)"

definition sorted_list_of_set_by :: "'a rel ⇒ 'a set ⇒ 'a list" where
"sorted_list_of_set_by R A = (THE xs. is_sorted_list_of_set_by R A xs)"

definition fin_set_lexord :: "'a rel ⇒ 'a set rel" where
"fin_set_lexord R = {(A, B). finite A ∧ finite B ∧
                             (∃ xs ys. is_sorted_list_of_set_by R A xs ∧ is_sorted_list_of_set_by R B ys
                              ∧ (xs, ys) ∈ lexord R)}"

lemma is_sorted_list_of_set_by_mono:
  "⟦ R ⊆ S; is_sorted_list_of_set_by R A xs ⟧ ⟹ is_sorted_list_of_set_by S A xs"
  by (auto simp add: is_sorted_list_of_set_by_def)

lemma lexord_mono':
  "⟦ (⋀ x y. f x y ⟶ g x y); (xs, ys) ∈ lexord {(x, y). f x y} ⟧ ⟹ (xs, ys) ∈ lexord {(x, y). g x y}"
  by (metis case_prodD case_prodI lexord_take_index_conv mem_Collect_eq)

lemma fin_set_lexord_mono [mono]:
  "(⋀ x y. f x y ⟶ g x y) ⟹ (xs, ys) ∈ fin_set_lexord {(x, y). f x y} ⟶ (xs, ys) ∈ fin_set_lexord {(x, y). g x y}"
proof
  assume
    fin: "(xs, ys) ∈ fin_set_lexord {(x, y). f x y}" and
    hyp: "(⋀ x y. f x y ⟶ g x y)"

  from fin have "finite xs" "finite ys"
    using fin_set_lexord_def by fastforce+

  with fin hyp show "(xs, ys) ∈ fin_set_lexord {(x, y). g x y}"
    apply (auto simp add: fin_set_lexord_def)
    apply (rename_tac xs' ys')
    apply (rule_tac x="xs'" in exI)
    apply (auto)
     apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def mem_Collect_eq)
    apply (metis case_prodD case_prodI is_sorted_list_of_set_by_def lexord_mono' mem_Collect_eq)
    done
qed

definition distincts :: "'a set ⇒ 'a list set" where
"distincts A = {xs ∈ lists A. distinct(xs)}"

lemma tl_element:
  "⟦ x ∈ set xs; x ≠ hd(xs) ⟧ ⟹ x ∈ set(tl(xs))"
  by (metis in_set_insert insert_Nil list.collapse list.distinct(2) set_ConsD)

subsubsection ‹ List Update ›

lemma listsum_update:
  fixes xs :: "'a::ring list"
  assumes "i < length xs"
  shows "list_sum (xs[i := v]) = list_sum xs - xs ! i + v"
using assms proof (induct xs arbitrary: i)
  case Nil
  then show ?case by (simp)
next
  case (Cons a xs)
  then show ?case
  proof (cases i)
    case 0
    thus ?thesis
      by (simp add: add.commute) 
  next
    case (Suc i')
    with Cons show ?thesis
      by (auto)
  qed
qed

subsubsection ‹ Drop While and Take While ›


lemma dropWhile_sorted_le_above:
  "⟦ sorted xs; x ∈ set (dropWhile (λ x. x ≤ n) xs) ⟧ ⟹ x > n"
  apply (induct xs)
   apply (auto)
  apply (rename_tac a xs)
  apply (case_tac "a ≤ n")
   apply (auto)
done

lemma set_dropWhile_le:
  "sorted xs ⟹ set (dropWhile (λ x. x ≤ n) xs) = {x∈set xs. x > n}"
  apply (induct xs)
   apply (simp)
  apply (rename_tac x xs)
  apply (subgoal_tac "sorted xs")
   apply (simp)
   apply (safe)
     apply (auto)
done

lemma set_takeWhile_less_sorted:
  "⟦ sorted I; x ∈ set I; x < n ⟧ ⟹ x ∈ set (takeWhile (λx. x < n) I)"
proof (induct I arbitrary: x)
  case Nil thus ?case
    by (simp)
next
  case (Cons a I) thus ?case
    by auto
qed

lemma nth_le_takeWhile_ord: "⟦ sorted xs; i ≥ length (takeWhile (λ x. x ≤ n) xs); i < length xs ⟧ ⟹ n ≤ xs ! i"
  apply (induct xs arbitrary: i, auto)
  apply (rename_tac x xs i)
  apply (case_tac "x ≤ n")
   apply (auto)
  apply (metis One_nat_def Suc_eq_plus1 le_less_linear le_less_trans less_imp_le list.size(4) nth_mem set_ConsD)
  done

lemma length_takeWhile_less:
  "⟦ a ∈ set xs; ¬ P a ⟧ ⟹ length (takeWhile P xs) < length xs"
  by (metis in_set_conv_nth length_takeWhile_le nat_neq_iff not_less set_takeWhileD takeWhile_nth)

lemma nth_length_takeWhile_less:
  "⟦ sorted xs; distinct xs; (∃ a ∈ set xs. a ≥ n) ⟧ ⟹ xs ! length (takeWhile (λx. x < n) xs) ≥ n"
  by (induct xs, auto)

subsubsection ‹ Last and But Last ›

lemma length_gt_zero_butlast_concat:
  assumes "length ys > 0"
  shows "butlast (xs @ ys) = xs @ (butlast ys)"
  using assms by (metis butlast_append length_greater_0_conv)

lemma length_eq_zero_butlast_concat:
  assumes "length ys = 0"
  shows "butlast (xs @ ys) = butlast xs"
  using assms by (metis append_Nil2 length_0_conv)

lemma butlast_single_element:
  shows "butlast [e] = []"
  by (metis butlast.simps(2))

lemma last_single_element:
  shows "last [e] = e"
  by (metis last.simps)

lemma length_zero_last_concat:
  assumes "length t = 0"
  shows "last (s @ t) = last s"
  by (metis append_Nil2 assms length_0_conv)

lemma length_gt_zero_last_concat:
  assumes "length t > 0"
  shows "last (s @ t) = last t"
  by (metis assms last_append length_greater_0_conv)

subsubsection ‹ Prefixes and Strict Prefixes ›

lemma prefix_length_eq:
  "⟦ length xs = length ys; prefix xs ys ⟧ ⟹ xs = ys"
  by (metis not_equal_is_parallel parallel_def)

lemma prefix_Cons_elim [elim]:
  assumes "prefix (x # xs) ys"
  obtains ys' where "ys = x # ys'" "prefix xs ys'"
  using assms
  by (metis append_Cons prefix_def)

lemma prefix_map_inj:
  "⟦ inj_on f (set xs ∪ set ys); prefix (map f xs) (map f ys) ⟧ ⟹
   prefix xs ys"
  apply (induct xs arbitrary:ys)
   apply (simp_all)
  apply (erule prefix_Cons_elim)
  apply (auto)
  apply (metis image_insert insertI1 insert_Diff_if singletonE)
  done

lemma prefix_map_inj_eq [simp]:
  "inj_on f (set xs ∪ set ys) ⟹
   prefix (map f xs) (map f ys) ⟷ prefix xs ys"
  using map_mono_prefix prefix_map_inj by blast

lemma strict_prefix_Cons_elim [elim]:
  assumes "strict_prefix (x # xs) ys"
  obtains ys' where "ys = x # ys'" "strict_prefix xs ys'"
  using assms
  by (metis Sublist.strict_prefixE' Sublist.strict_prefixI' append_Cons)

lemma strict_prefix_map_inj:
  "⟦ inj_on f (set xs ∪ set ys); strict_prefix (map f xs) (map f ys) ⟧ ⟹
   strict_prefix xs ys"
  apply (induct xs arbitrary:ys)
  apply auto
   apply (simp flip: prefix_bot.bot_less)
  apply (erule strict_prefix_Cons_elim)
  apply (auto)
  apply (metis image_eqI insert_Diff_single insert_iff)
  done

lemma strict_prefix_map_inj_eq [simp]:
  "inj_on f (set xs ∪ set ys) ⟹
   strict_prefix (map f xs) (map f ys) ⟷ strict_prefix xs ys"
  by (simp add: inj_on_map_eq_map strict_prefix_def)

lemma prefix_drop:
  "⟦ drop (length xs) ys = zs; prefix xs ys ⟧
   ⟹ ys = xs @ zs"
  by (metis append_eq_conv_conj prefix_def)

lemma list_append_prefixD [dest]: "x @ y ≤ z ⟹ x ≤ z"
  using append_prefixD less_eq_list_def by blast

lemma prefix_not_empty:
  assumes "strict_prefix xs ys" and "xs ≠ []"
  shows "ys ≠ []"
  using Sublist.strict_prefix_simps(1) assms(1) by blast

lemma prefix_not_empty_length_gt_zero:
  assumes "strict_prefix xs ys" and "xs ≠ []"
  shows "length ys > 0"
  using assms prefix_not_empty by auto

lemma butlast_prefix_suffix_not_empty:
  assumes "strict_prefix (butlast xs) ys"
  shows "ys ≠ []"
  using assms prefix_not_empty_length_gt_zero by fastforce

lemma prefix_and_concat_prefix_is_concat_prefix:
  assumes "prefix s t" "prefix (e @ t) u"
  shows "prefix (e @ s) u"
  using Sublist.same_prefix_prefix assms(1) assms(2) prefix_order.dual_order.trans by blast

lemma prefix_eq_exists:
  "prefix s t ⟷ (∃xs . s @ xs = t)"
  using prefix_def by auto

lemma strict_prefix_eq_exists:
  "strict_prefix s t ⟷ (∃xs . s @ xs = t ∧ (length xs) > 0)"
  using prefix_def strict_prefix_def by auto

lemma butlast_strict_prefix_eq_butlast:
  assumes "length s = length t" and "strict_prefix (butlast s) t"
  shows "strict_prefix (butlast s) t ⟷ (butlast s) = (butlast t)"
  by (metis append_butlast_last_id append_eq_append_conv assms(1) assms(2) length_0_conv length_butlast strict_prefix_eq_exists)

lemma butlast_eq_if_eq_length_and_prefix:
  assumes "length s > 0" "length z > 0"
          "length s = length z" "strict_prefix (butlast s) t" "strict_prefix (butlast z) t"
  shows   "(butlast s) = (butlast z)"
  using assms by (auto simp add:strict_prefix_eq_exists)

lemma butlast_prefix_imp_length_not_gt:
  assumes "length s > 0" "strict_prefix (butlast s) t"
  shows "¬ (length t < length s)"
  using assms prefix_length_less by fastforce

lemma length_not_gt_iff_eq_length:
  assumes "length s > 0" and "strict_prefix (butlast s) t"
  shows "(¬ (length s < length t)) = (length s = length t)"
proof -
  have "(¬ (length s < length t)) = ((length t < length s) ∨ (length s = length t))"
      by (metis not_less_iff_gr_or_eq)
  also have "... = (length s = length t)"
      using assms
      by (simp add:butlast_prefix_imp_length_not_gt)

  finally show ?thesis .
qed

text ‹ Greatest common prefix ›

fun gcp :: "'a list ⇒ 'a list ⇒ 'a list" where
"gcp [] ys = []" |
"gcp (x # xs) (y # ys) = (if (x = y) then x # gcp xs ys else [])" |
"gcp _ _ = []"

lemma gcp_right [simp]: "gcp xs [] = []"
  by (induct xs, auto)

lemma gcp_append [simp]: "gcp (xs @ ys) (xs @ zs) = xs @ gcp ys zs"
  by (induct xs, auto)

lemma gcp_lb1: "prefix (gcp xs ys) xs"
  apply (induct xs arbitrary: ys, auto)
  apply (case_tac ys, auto)
  done

lemma gcp_lb2: "prefix (gcp xs ys) ys"
  apply (induct ys arbitrary: xs, auto)
  apply (case_tac xs, auto)
  done

interpretation prefix_semilattice: semilattice_inf gcp prefix strict_prefix
proof
  fix xs ys :: "'a list"
  show "prefix (gcp xs ys) xs"
    by (induct xs arbitrary: ys, auto, case_tac ys, auto)
  show "prefix (gcp xs ys) ys"
    by (induct ys arbitrary: xs, auto, case_tac xs, auto)
next
  fix xs ys zs :: "'a list"
  assume "prefix xs ys" "prefix xs zs"
  thus "prefix xs (gcp ys zs)"
    by (simp add: prefix_def, auto)
qed

subsubsection ‹ Lexicographic Order ›

lemma lexord_append:
  assumes "(xs⇩₁ @ ys⇩₁, xs⇩₂ @ ys⇩₂) ∈ lexord R" "length(xs⇩₁) = length(xs⇩₂)"
  shows "(xs⇩₁, xs⇩₂) ∈ lexord R ∨ (xs⇩₁ = xs⇩₂ ∧ (ys⇩₁, ys⇩₂) ∈ lexord R)"
using assms
proof (induct xs⇩₂ arbitrary: xs⇩₁)
  case (Cons x⇩₂ xs⇩₂') note hyps = this
  from hyps(3) obtain x⇩₁ xs⇩₁' where xs⇩₁: "xs⇩₁ = x⇩₁ # xs⇩₁'" "length(xs⇩₁') = length(xs⇩₂')"
    by (auto, metis Suc_length_conv)
  with hyps(2) have xcases: "(x⇩₁, x⇩₂) ∈ R ∨ (xs⇩₁' @ ys⇩₁, xs⇩₂' @ ys⇩₂) ∈ lexord R"
    by (auto)
  show ?case
  proof (cases "(x⇩₁, x⇩₂) ∈ R")
    case True with xs⇩₁ show ?thesis
      by (auto)
  next
    case False
    with xcases have "(xs⇩₁' @ ys⇩₁, xs⇩₂' @ ys⇩₂) ∈ lexord R"
      by (auto)
    with hyps(1) xs⇩₁ have dichot: "(xs⇩₁', xs⇩₂') ∈ lexord R ∨ (xs⇩₁' = xs⇩₂' ∧ (ys⇩₁, ys⇩₂) ∈ lexord R)"
      by (auto)
    have "x⇩₁ = x⇩₂"
      using False hyps(2) xs⇩₁(1) by auto
    with dichot xs⇩₁ show ?thesis
      by (simp)
  qed
next
  case Nil thus ?case
    by auto
qed

lemma strict_prefix_lexord_rel:
  "strict_prefix xs ys ⟹ (xs, ys) ∈ lexord R"
  by (metis Sublist.strict_prefixE' lexord_append_rightI)

lemma strict_prefix_lexord_left:
  assumes "trans R" "(xs, ys) ∈ lexord R" "strict_prefix xs' xs"
  shows "(xs', ys) ∈ lexord R"
  by (metis assms lexord_trans strict_prefix_lexord_rel)

lemma prefix_lexord_right:
  assumes "trans R" "(xs, ys) ∈ lexord R" "strict_prefix ys ys'"
  shows "(xs, ys') ∈ lexord R"
  by (metis assms lexord_trans strict_prefix_lexord_rel)

lemma lexord_eq_length:
  assumes "(xs, ys) ∈ lexord R" "length xs = length ys"
  shows "∃ i. (xs!i, ys!i) ∈ R ∧ i < length xs ∧ (∀ j<i. xs!j = ys!j)"
using assms proof (induct xs arbitrary: ys)
  case (Cons x xs) note hyps = this
  then obtain y ys' where ys: "ys = y # ys'" "length ys' = length xs"
    by (metis Suc_length_conv)
  show ?case
  proof (cases "(x, y) ∈ R")
    case True with ys show ?thesis
      by (rule_tac x="0" in exI, simp)
  next
    case False
    with ys hyps(2) have xy: "x = y" "(xs, ys') ∈ lexord R"
      by auto
    with hyps(1,3) ys obtain i where "(xs!i, ys'!i) ∈ R" "i < length xs" "(∀ j<i. xs!j = ys'!j)"
      by force
    with xy ys show ?thesis
      apply (rule_tac x="Suc i" in exI)
      apply (auto simp add: less_Suc_eq_0_disj)
    done
  qed
next
  case Nil thus ?case by (auto)
qed

lemma lexord_intro_elems:
  assumes "length xs > i" "length ys > i" "(xs!i, ys!i) ∈ R" "∀ j<i. xs!j = ys!j"
  shows "(xs, ys) ∈ lexord R"
using assms proof (induct i arbitrary: xs ys)
  case 0 thus ?case
    by (auto, metis lexord_cons_cons list.exhaust nth_Cons_0)
next
  case (Suc i) note hyps = this
  then obtain x' y' xs' ys' where "xs = x' # xs'" "ys = y' # ys'"
    by (metis Suc_length_conv Suc_lessE)
  moreover with hyps(5) have "∀j<i. xs' ! j = ys' ! j"
    by (auto)
  ultimately show ?case using hyps
    by (auto)
qed

subsection ‹ Distributed Concatenation ›

definition uncurry :: "('a ⇒ 'b ⇒  'c) ⇒ ('a × 'b ⇒ 'c)" where
[simp]: "uncurry f = (λ(x, y). f x y)"

definition dist_concat ::
  "'a list set ⇒ 'a list set ⇒ 'a list set" (infixr ‹⇧^⌢› 100) where
"dist_concat ls1 ls2 = (uncurry (@) ` (ls1 × ls2))"

lemma dist_concat_left_empty [simp]:
  "{} ⇧^⌢ ys = {}"
  by (simp add: dist_concat_def)

lemma dist_concat_right_empty [simp]:
  "xs ⇧^⌢ {} = {}"
  by (simp add: dist_concat_def)

lemma dist_concat_insert [simp]:
"insert l ls1 ⇧^⌢ ls2 = ((@) l ` ( ls2)) ∪ (ls1 ⇧^⌢ ls2)"
  by (auto simp add: dist_concat_def)

subsection ‹ List Domain and Range ›

abbreviation seq_dom :: "'a list ⇒ nat set" (‹dom⇩_l›) where
"seq_dom xs ≡ {0..<length xs}"

abbreviation seq_ran :: "'a list ⇒ 'a set" (‹ran⇩_l›) where
"seq_ran xs ≡ set xs"

subsection ‹ Extracting List Elements ›

definition seq_extract :: "nat set ⇒ 'a list ⇒ 'a list" (infix ‹↿⇩_l› 80) where
"seq_extract A xs = nths xs A"

lemma seq_extract_Nil [simp]: "A ↿⇩_l [] = []"
  by (simp add: seq_extract_def)

lemma seq_extract_Cons:
  "A ↿⇩_l (x # xs) = (if 0 ∈ A then [x] else []) @ {j. Suc j ∈ A} ↿⇩_l xs"
  by (simp add: seq_extract_def nths_Cons)

lemma seq_extract_empty [simp]: "{} ↿⇩_l xs = []"
  by (simp add: seq_extract_def)

lemma seq_extract_ident [simp]: "{0..<length xs} ↿⇩_l xs = xs"
  unfolding list_eq_iff_nth_eq
  by (auto simp add: seq_extract_def length_nths atLeast0LessThan)

lemma seq_extract_split:
  assumes "i ≤ length xs"
  shows "{0..<i} ↿⇩_l xs @ {i..<length xs} ↿⇩_l xs = xs"
using assms
proof (induct xs arbitrary: i)
  case Nil thus ?case by (simp add: seq_extract_def)
next
  case (Cons x xs) note hyp = this
  have "{j. Suc j < i} = {0..<i - 1}"
    by (auto)
  moreover have "{j. i ≤ Suc j ∧ j < length xs} = {i - 1..<length xs}"
    by (auto)
  ultimately show ?case
    using hyp by (force simp add: seq_extract_def nths_Cons)
qed

lemma seq_extract_append:
  "A ↿⇩_l (xs @ ys) = (A ↿⇩_l xs) @ ({j. j + length xs ∈ A} ↿⇩_l ys)"
  by (simp add: seq_extract_def nths_append)

lemma seq_extract_range: "A ↿⇩_l xs = (A ∩ dom⇩_l(xs)) ↿⇩_l xs"
  apply (auto simp add: seq_extract_def nths_def)
  apply (metis (no_types, lifting) atLeastLessThan_iff filter_cong in_set_zip nth_mem set_upt)
done

lemma seq_extract_out_of_range:
  "A ∩ dom⇩_l(xs) = {} ⟹ A ↿⇩_l xs = []"
  by (metis seq_extract_def seq_extract_range nths_empty)

lemma seq_extract_length [simp]:
  "length (A ↿⇩_l xs) = card (A ∩ dom⇩_l(xs))"
proof -
  have "{i. i < length(xs) ∧ i ∈ A} = (A ∩ {0..<length(xs)})"
    by (auto)
  thus ?thesis
    by (simp add: seq_extract_def length_nths)
qed

lemma seq_extract_Cons_atLeastLessThan:
  assumes "m < n"
  shows "{m..<n} ↿⇩_l (x # xs) = (if (m = 0) then x # ({0..<n-1} ↿⇩_l xs) else {m-1..<n-1} ↿⇩_l xs)"
proof -
  have "{j. Suc j < n} = {0..<n - Suc 0}"
    by (auto)
  moreover have "{j. m ≤ Suc j ∧ Suc j < n} = {m - Suc 0..<n - Suc 0}"
    by (auto)

  ultimately show ?thesis using assms
    by (auto simp add: seq_extract_Cons)
qed

lemma seq_extract_singleton:
  assumes "i < length xs"
  shows "{i} ↿⇩_l xs = [xs ! i]"
  using assms
  apply (induct xs arbitrary: i)
  apply (auto simp add: seq_extract_Cons)
  apply (rename_tac xs i)
  apply (subgoal_tac "{j. Suc j = i} = {i - 1}")
  apply (auto)
done

lemma seq_extract_as_map:
  assumes "m < n" "n ≤ length xs"
  shows "{m..<n} ↿⇩_l xs = map (nth xs) [m..<n]"
using assms proof (induct xs arbitrary: m n)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  have "[m..<n] = m # [m+1..<n]"
    using Cons.prems(1) upt_eq_Cons_conv by blast
  moreover have "map (nth (x # xs)) [Suc m..<n] = map (nth xs) [m..<n-1]"
    by (simp add: map_nth_Cons_atLeastLessThan)
  ultimately show ?case
    using Cons upt_rec
    by (auto simp add: seq_extract_Cons_atLeastLessThan)
qed

lemma seq_append_as_extract:
  "xs = ys @ zs ⟷ (∃ i≤length(xs). ys = {0..<i} ↿⇩_l xs ∧ zs = {i..<length(xs)} ↿⇩_l xs)"
proof
  assume xs: "xs = ys @ zs"
  moreover have "ys = {0..<length ys} ↿⇩_l (ys @ zs)"
    by (simp add: seq_extract_append)
  moreover have "zs = {length ys..<length ys + length zs} ↿⇩_l (ys @ zs)"
  proof -
    have "{length ys..<length ys + length zs} ∩ {0..<length ys} = {}"
      by auto
    moreover have s1: "{j. j < length zs} = {0..<length zs}"
      by auto
    ultimately show ?thesis
      by (simp add: seq_extract_append seq_extract_out_of_range)
  qed
  ultimately show "(∃ i≤length(xs). ys = {0..<i} ↿⇩_l xs ∧ zs = {i..<length(xs)} ↿⇩_l xs)"
    by (rule_tac x="length ys" in exI, auto)
next
  assume "∃i≤length xs. ys = {0..<i} ↿⇩_l xs ∧ zs = {i..<length xs} ↿⇩_l xs"
  thus "xs = ys @ zs"
    by (auto simp add: seq_extract_split)
qed

subsection ‹ Filtering a list according to a set ›

definition seq_filter :: "'a list ⇒ 'a set ⇒ 'a list" (infix ‹↾⇩_l› 80) where
"seq_filter xs A = filter (λ x. x ∈ A) xs"

lemma seq_filter_Cons_in [simp]: 
  "x ∈ cs ⟹ (x # xs) ↾⇩_l cs = x # (xs ↾⇩_l cs)"
  by (simp add: seq_filter_def)

lemma seq_filter_Cons_out [simp]: 
  "x ∉ cs ⟹ (x # xs) ↾⇩_l cs = (xs ↾⇩_l cs)"
  by (simp add: seq_filter_def)

lemma seq_filter_Nil [simp]: "[] ↾⇩_l A = []"
  by (simp add: seq_filter_def)

lemma seq_filter_empty [simp]: "xs ↾⇩_l {} = []"
  by (simp add: seq_filter_def)

lemma seq_filter_append: "(xs @ ys) ↾⇩_l A = (xs ↾⇩_l A) @ (ys ↾⇩_l A)"
  by (simp add: seq_filter_def)

lemma seq_filter_UNIV [simp]: "xs ↾⇩_l UNIV = xs"
  by (simp add: seq_filter_def)

lemma seq_filter_twice [simp]: "(xs ↾⇩_l A) ↾⇩_l B = xs ↾⇩_l (A ∩ B)"
  by (simp add: seq_filter_def)

subsection ‹ Minus on lists ›

instantiation list :: (type) minus
begin

text ‹ We define list minus so that if the second list is not a prefix of the first, then an arbitrary
        list longer than the combined length is produced. Thus we can always determined from the output
        whether the minus is defined or not. ›

definition "xs - ys = (if (prefix ys xs) then drop (length ys) xs else [])"

instance ..
end

lemma minus_cancel [simp]: "xs - xs = []"
  by (simp add: minus_list_def)

lemma append_minus [simp]: "(xs @ ys) - xs = ys"
  by (simp add: minus_list_def)

lemma minus_right_nil [simp]: "xs - [] = xs"
  by (simp add: minus_list_def)

lemma list_concat_minus_list_concat: "(s @ t) - (s @ z) = t - z"
  by (simp add: minus_list_def)

lemma length_minus_list: "y ≤ x ⟹ length(x - y) = length(x) - length(y)"
  by (simp add: less_eq_list_def minus_list_def)

lemma map_list_minus:
  "xs ≤ ys ⟹ map f (ys - xs) = map f ys - map f xs"
  by (simp add: drop_map less_eq_list_def map_mono_prefix minus_list_def)

lemma list_minus_first_tl [simp]: 
  "[x] ≤ xs ⟹ (xs - [x]) = tl xs"
  by (metis Prefix_Order.prefixE append.left_neutral append_minus list.sel(3) not_Cons_self2 tl_append2)

text ‹ Extra lemmas about @{term prefix} and @{term strict_prefix} ›

lemma prefix_concat_minus:
  assumes "prefix xs ys"
  shows "xs @ (ys - xs) = ys"
  using assms by (metis minus_list_def prefix_drop)

lemma prefix_minus_concat:
  assumes "prefix s t"
  shows "(t - s) @ z = (t @ z) - s"
  using assms by (simp add: Sublist.prefix_length_le minus_list_def)

lemma strict_prefix_minus_not_empty:
  assumes "strict_prefix xs ys"
  shows "ys - xs ≠ []"
  using assms by (metis append_Nil2 prefix_concat_minus strict_prefix_def)

lemma strict_prefix_diff_minus:
  assumes "prefix xs ys" and "xs ≠ ys"
  shows "(ys - xs) ≠ []"
  using assms by (simp add: strict_prefix_minus_not_empty)

lemma length_tl_list_minus_butlast_gt_zero:
  assumes "length s < length t" and "strict_prefix (butlast s) t" and "length s > 0"
  shows "length (tl (t - (butlast s))) > 0"
  using assms
  by (metis Nitpick.size_list_simp(2) butlast_snoc hd_Cons_tl length_butlast length_greater_0_conv length_tl less_trans nat_neq_iff strict_prefix_minus_not_empty prefix_order.dual_order.strict_implies_order prefix_concat_minus)

lemma list_minus_butlast_eq_butlast_list:
  assumes "length t = length s" and "strict_prefix (butlast s) t"
  shows "t - (butlast s) = [last t]"
  using assms
  by (metis append_butlast_last_id append_eq_append_conv butlast.simps(1) length_butlast less_numeral_extra(3) list.size(3) prefix_order.dual_order.strict_implies_order prefix_concat_minus prefix_length_less)

lemma butlast_strict_prefix_length_lt_imp_last_tl_minus_butlast_eq_last:
  assumes "length s > 0" "strict_prefix (butlast s) t" "length s < length t"
  shows "last (tl (t - (butlast s))) = (last t)"
  using assms by (metis last_append last_tl length_tl_list_minus_butlast_gt_zero less_numeral_extra(3) list.size(3) append_minus strict_prefix_eq_exists)

lemma tl_list_minus_butlast_not_empty:
  assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t > length s"
  shows "tl (t - (butlast s)) ≠ []"
  using assms length_tl_list_minus_butlast_gt_zero by fastforce

lemma tl_list_minus_butlast_empty:
  assumes "strict_prefix (butlast s) t" and "length s > 0" and "length t = length s"
  shows "tl (t - (butlast s)) = []"
  using assms by (simp add: list_minus_butlast_eq_butlast_list)

lemma tl_list_minus_butlast_eq_empty:
  assumes "strict_prefix (butlast s) t" and "length s = length t"
  shows "tl (t - (butlast s)) = []"
  using assms by (metis list.sel(3) list_minus_butlast_eq_butlast_list)

lemma length_list_minus:
  assumes "strict_prefix s t"
  shows "length(t - s) = length(t) - length(s)"
  using assms by (simp add: minus_list_def prefix_order.dual_order.strict_implies_order)

subsection ‹ Laws on @{term take}, @{term drop}, and @{term nths} ›

lemma take_prefix: "m ≤ n ⟹ take m xs ≤ take n xs"
  by (metis Prefix_Order.prefixI append_take_drop_id min_absorb2 take_append take_take)

lemma nths_atLeastAtMost_0_take: "nths xs {0..m} = take (Suc m) xs"
  by (metis atLeast0AtMost lessThan_Suc_atMost nths_upt_eq_take)

lemma nths_atLeastLessThan_0_take: "nths xs {0..<m} = take m xs"
  by (simp add: atLeast0LessThan)

lemma nths_atLeastAtMost_prefix: "m ≤ n ⟹ nths xs {0..m} ≤ nths xs {0..n}"
  by (simp add: nths_atLeastAtMost_0_take take_prefix)

lemma sorted_nths_atLeastAtMost_0: "⟦ m ≤ n; sorted (nths xs {0..n}) ⟧ ⟹ sorted (nths xs {0..m})"
  using nths_atLeastAtMost_prefix sorted_prefix by blast

lemma sorted_nths_atLeastLessThan_0: "⟦ m ≤ n; sorted (nths xs {0..<n}) ⟧ ⟹ sorted (nths xs {0..<m})"
  by (metis atLeast0LessThan nths_upt_eq_take sorted_prefix take_prefix)

lemma list_augment_as_update: 
  "k < length xs ⟹ list_augment xs k x = list_update xs k x"
  by (metis list_augment_def list_augment_idem list_update_overwrite)

lemma nths_list_update_out: "k ∉ A ⟹ nths (list_update xs k x) A = nths xs A"
  apply (induct xs arbitrary: k x A)
   apply (auto)
  apply (rename_tac a xs k x A)
  apply (case_tac k)
   apply (auto simp add: nths_Cons)
  done

lemma nths_list_augment_out: "⟦ k < length xs; k ∉ A ⟧ ⟹ nths (list_augment xs k x) A = nths xs A"
  by (simp add: list_augment_as_update nths_list_update_out)

end