Theory List_Extra

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 ‹ Sets ›

lemma set_Fpow [simp]: "set xs ∈ Fpow A ⟷ set xs ⊆ A"
  by (auto simp add: Fpow_def)

lemma Fpow_as_Pow: "finite A ⟹ Fpow A = Pow A"
  by (auto simp add: Pow_def Fpow_def finite_subset)

lemma Fpow_set [code]:
  "Fpow (set []) = {{}}"
  "Fpow (set (x # xs)) = (let A = Fpow (set xs) in A ∪ insert x ` A)"
  by (simp_all add: Fpow_as_Pow Pow_set del: set_simps)

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 @{text nth} function returns @{text "⊥"} 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"
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
    then show ?thesis by simp
  next
    case (Suc nat)
    with Cons show ?thesis by simp
  qed
qed

lemma nth_el_appendr[simp]: "length xs ≤ i ⟹ (xs @ ys)⟨i⟩⇩_l = ys⟨i - length xs⟩⇩_l"
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
    with Cons show ?thesis
      by fastforce
  next
    case (Suc nat)
    with Cons show ?thesis by simp
  qed
qed

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 (simp_all)
  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 ‹ The concatenation of two lists is sorted provided (1) both the lists are sorted, and (2) 
  the final and first elements are ordered. ›

lemma sorted_append_middle:
  "sorted(xs@ys) = (sorted xs ∧ sorted ys ∧ (xs ≠ [] ∧ ys ≠ [] ⟶ xs!(length xs - 1) ≤ ys!0))"
proof -
  have "⋀x y. ⟦ sorted xs; sorted ys; xs ! (length xs - Suc 0) ≤ ys ! 0 ⟧ ⟹ x ∈ set xs ⟹ y ∈ set ys ⟹ x ≤ y"
  proof -
    fix x y
    assume "sorted xs" "sorted ys" "xs ! (length xs - Suc 0) ≤ ys ! 0" "x ∈ set xs" "y ∈ set ys"
    moreover then obtain i j where i: "x = xs!i" "i < length xs" and j: "y = ys!j" "j < length ys"
      by (auto simp add: in_set_conv_nth)
    moreover have "xs ! i ≤ xs!(length xs - 1)"
      by (metis One_nat_def Suc_diff_Suc Suc_leI Suc_le_mono ‹i < length xs› ‹sorted xs› diff_less diff_zero gr_implies_not_zero nat.simps(3) sorted_iff_nth_mono zero_less_iff_neq_zero)
    moreover have "ys!0 ≤ ys ! j"
      by (simp add: calculation(2) calculation(9) sorted_nth_mono)
    ultimately have "xs ! i ≤ ys ! j"
      by (metis One_nat_def dual_order.trans) 
    thus "x ≤ y"
      by (simp add: i j)
  qed
  thus ?thesis
    by (auto simp add: sorted_append)
qed

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 (simp_all 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)
  with isl show "distinct (x # xs)"
  proof -
    have "(∀n. ¬ n < length (x # xs) - 1 ∨ (x # xs) ! n < (x # xs) ! (n + 1)) ∧ set (x # xs) = A"
      by (meson ‹is_sorted_list_of_set A (x # xs)› is_sorted_list_of_set_def)
  then show ?thesis
    by (metis ‹distinct xs› add.commute add_diff_cancel_left' distinct.simps(2) leD length_Cons length_greater_0_conv length_pos_if_in_set less_le nth_Cons_0 nth_Cons_Suc plus_1_eq_Suc set_ConsD sorted_wrt.elims(2) srtd)    
  qed
qed

lemma is_sorted_list_of_set_alt_def:
  "is_sorted_list_of_set A xs ⟷ sorted (xs) ∧ distinct (xs) ∧ set(xs) = A"
  by (metis is_sorted_list_of_set_def sorted_distinct sorted_is_sorted_list_of_set(1,2))

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)"
  using sorted_distinct sorted_list_of_set(2) by (fastforce simp add: is_sorted_list_of_set_def)

lemma sorted_list_of_set_other_def:
  "finite A ⟹ sorted_list_of_set(A) = (THE xs. sorted(xs) ∧ distinct(xs) ∧ set xs = A)"
  by (metis (mono_tags, lifting) sorted_list_of_set.distinct_sorted_key_list_of_set
      sorted_list_of_set.idem_if_sorted_distinct sorted_list_of_set.set_sorted_key_list_of_set
      sorted_list_of_set.sorted_sorted_key_list_of_set the_equality)

lemma sorted_list_of_set_alt [simp]:
  "finite A ⟹ sorted_list_of_set_alt(A) = sorted_list_of_set(A)"
  by (metis is_sorted_list_of_set is_sorted_list_of_set_def sorted_is_sorted_list_of_set(1,2)
      sorted_list_of_set.idem_if_sorted_distinct sorted_list_of_set_alt_def sorted_list_of_set_eq_Nil_iff
      the_equality)

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}"
    by (simp add: fin_set_lexord_def, metis case_prod_conv is_sorted_list_of_set_by_def lexord_mono' mem_Collect_eq)

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"
proof (induct xs)
  case Nil
  then show ?case
    by simp 
next
  case (Cons a xs)
  then show ?case
  proof (cases "a ≤ n")
    case True
    with Cons show ?thesis by simp
  next
    case False
    with Cons show ?thesis
      by force 
  qed
qed

lemma set_dropWhile_le:
  "sorted xs ⟹ set (dropWhile (λ x. x ≤ n) xs) = {x∈set xs. x > n}"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  hence "sorted xs"
    using sorted_simps(2) by blast
  with Cons show ?case 
    by force
qed

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"
proof (induct xs arbitrary: i)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
    by (meson dual_order.trans nle_le nth_length_takeWhile order_le_less_trans sorted_iff_nth_mono) 
qed

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"
proof (induct xs arbitrary:ys)
  case Nil
  then show ?case
    by simp 
next
  case (Cons x xs)
  obtain ys' where "map f ys = f x # ys'" "prefix (map f xs) ys'"
    using Cons.prems(2) by auto 
  with Cons show ?case
    by (simp, safe, metis Diff_iff Sublist.Cons_prefix_Cons Un_insert_right empty_iff image_eqI inj_on_insert insert_iff list.simps(15))
qed

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 (simp_all)
  using prefix_bot.not_eq_extremum apply fastforce
  apply (erule strict_prefix_Cons_elim)
  apply (safe)
  apply (metis Diff_iff Sublist.strict_prefix_simps(3) Un_insert_right empty_iff imageI inj_on_insert insert_iff
      list.simps(15))
  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 prefix_imp_length_lteq:
  assumes "prefix s t"
  shows "length s ≤ length t"
  using assms by (simp add: Sublist.prefix_length_le)

lemma prefix_imp_length_not_gt:
  assumes "prefix s t"
  shows "¬ length t < length s"
  using assms by (simp add: Sublist.prefix_length_le leD)

lemma prefix_and_eq_length_imp_eq_list:
  assumes "prefix s t" and "length t = length s"
  shows "s=t"
  using assms by (simp add: prefix_length_eq)

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

lemma list_prefix_iff:
  "(prefix xs ys ⟷ (length xs ≤ length ys ∧ (∀ i<length xs. xs!i = ys!i)))"
  apply (safe)
    apply (simp add: prefix_imp_length_lteq)
   apply (metis nth_append prefix_def)
  apply (metis nth_take_lemma order_refl take_all take_is_prefix)
  done

lemma list_le_prefix_iff:
  "(xs ≤ ys ⟷ (length xs ≤ length ys ∧ (∀ i<length xs. xs!i = ys!i)))"
  by (simp add: less_eq_list_def list_prefix_iff)

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"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof (cases ys)
    case Nil
    then show ?thesis by simp
  next
    case (Cons a list)
    then show ?thesis
      by (simp add: Cons.hyps)
  qed
qed

lemma gcp_lb2: "prefix (gcp xs ys) ys"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case
  proof (cases ys)
    case Nil
    then show ?thesis by simp
  next
    case (Cons a list)
    then show ?thesis
      by (simp add: Cons.hyps)
  qed
qed

interpretation prefix_semilattice: semilattice_inf gcp prefix strict_prefix
proof
  fix xs ys :: "'a list"
  show "prefix (gcp xs ys) xs"
  proof (induct xs arbitrary: ys)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then show ?case
      by (simp add: gcp_lb1) 
  qed
  show "prefix (gcp xs ys) ys"
  proof (induct xs arbitrary: ys)
    case Nil
    then show ?case by simp
  next
    case (Cons a xs)
    then show ?case
      by (simp add: gcp_lb2) 
  qed
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 (simp, 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 force
  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 have "((x # xs) ! Suc i, ys ! Suc i) ∈ R ∧ Suc i < length (x # xs) ∧ (∀j<Suc i. (x # xs) ! j = ys ! j) "
      by (auto simp add: less_Suc_eq_0_disj)
    thus ?thesis
      by blast 
  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 (simp, 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 (input) 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 (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 (simp_all add: seq_extract_Cons)
  apply safe
  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)"
    using le_iff_add by 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 concat_minus_list_concat_butlast_eq_list_minus_butlast:
  assumes "prefix (butlast u) s"
  shows "(t @ s) - (t @ (butlast u)) = s - (butlast u)"
  using assms by (metis append_assoc prefix_concat_minus append_minus)

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)

(* this can be shown using length_tl, but care is needed when list is empty? *)
lemma prefix_length_tl_minus:
  assumes "strict_prefix s t"
  shows "length (tl (t-s)) = (length (t-s)) - 1"
  by (auto)

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)

lemma length_minus_le: "length (ys - xs) ≤ length ys"
  by (simp add: minus_list_def)

lemma length_minus_less: "⟦ xs ≤ ys; xs ≠ [] ⟧ ⟹ length (ys - xs) < length ys"
  by (simp add: minus_list_def less_eq_list_def)
     (metis diff_less length_greater_0_conv prefix_bot.extremum_uniqueI)

lemma filter_minus [simp]: "ys ≤ xs ⟹ filter P (xs - ys) = filter P xs - filter P ys"
  by (simp add: minus_list_def less_eq_list_def filter_mono_prefix)
     (metis filter_append filter_mono_prefix prefix_drop same_append_eq)

subsection ‹ Laws on @{term list_update} ›

lemma list_update_0: "length(xs) > 0 ⟹ xs[0 := x] = x # tl xs"
  by (metis length_0_conv list.collapse list_update_code(2) nat_less_le)

lemma tl_list_update: "⟦ length xs > 0; k > 0 ⟧ ⟹ tl(xs[k := v]) = (tl xs)[k-1 := v]"
  by (metis One_nat_def Suc_pred length_greater_0_conv list.collapse list.sel(3) list_update_code(3))

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"
proof (induct xs arbitrary: k x A)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (cases k, auto simp add: nths_Cons)
qed

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)

lemma nths_none: 
  assumes "∀i ∈ I. i ≥ length xs"
  shows "nths xs I = []"
proof -
  from assms have "∀x∈set (zip xs [0..<length xs]). snd x ∉ I"
    by (metis atLeastLessThan_iff in_set_zip leD nth_mem set_upt)
  thus ?thesis
    by (simp add: nths_def)
qed

lemma nths_uptoLessThan:
  "⟦ m ≤ n; n < length xs ⟧ ⟹ nths xs {m..n} = xs ! m # nths xs {Suc m..n}"
proof (induct xs arbitrary: m n)
case Nil
  then show ?case by (simp)
next
  case (Cons a xs)
  have l1: "⋀ m n. ⟦ 0 < m; m ≤ n ⟧ ⟹ {j. m ≤ Suc j ∧ Suc j ≤ n} = {m-1..n-1}"
    by (auto)
  have l2: "⋀ m n. ⟦ 0 < m; m ≤ n ⟧ ⟹ {j. m ≤ j ∧ Suc j ≤ n} = {m..n-1}"
    by (auto)
  from Cons show ?case by (auto simp add: nths_Cons l1 l2)
qed

lemma nths_upt_nth: "⟦ j < i; i < length xs ⟧ ⟹ (nths xs {0..<i}) ! j = xs ! j"
  by (metis lessThan_atLeast0 nth_take nths_upt_eq_take)


lemma nths_upt_length: "⟦ m ≤ n; n ≤ length xs ⟧ ⟹ length (nths xs {m..<n}) = n-m"
  by (metis atLeastLessThan_empty diff_is_0_eq length_map length_upt list.size(3) not_less nths_empty seq_extract_as_map seq_extract_def)

lemma nths_upt_le_length: 
  "⟦ m ≤ n; Suc n ≤ length xs ⟧ ⟹ length (nths xs {m..n}) = Suc n - m"
  by (metis atLeastLessThanSuc_atLeastAtMost le_SucI nths_upt_length)

lemma sl1: "n > 0 ⟹ {j. Suc j ≤ n} = {0..n-1}"
  by (auto)

lemma sl2: "⟦ 0 < m; m ≤ n ⟧ ⟹ {j. m ≤ Suc j ∧ Suc j ≤ n} = {m-1..n-1}"
  by auto

lemma nths_upt_le_nth: "⟦ m ≤ n; Suc n ≤ length xs; i < Suc n - m ⟧ 
  ⟹ (nths xs {m..n}) ! i = xs ! (i + m)"
proof (induct xs arbitrary: m n i)
  case Nil
  then show ?case by (simp)
next
  case (Cons a xs)
  then show ?case   
  proof (cases "i = 0")
    case True
    with Cons show ?thesis by (auto simp add: nths_Cons sl2)
  next
    case False
    with Cons show ?thesis by (auto simp add: nths_Cons sl1 sl2)
  qed
qed    

lemma nths_split_union:
  assumes "⋀x y. x ∈ A ⟹ y ∈ B ⟹ x < y"
  shows "nths l A @ nths l B = nths l (A ∪ B)"
proof (induct l rule: rev_induct)
  case Nil
  then show ?case by simp
next
  case (snoc x xs)
  { assume *: "length xs ∉ (A ∪ B)"
    then have L: "nths (xs @ [x]) (A ∪ B) = nths xs (A ∪ B)"
      by (simp add: nths_append)
    from * have R: "nths (xs @ [x]) A = nths xs A" "nths (xs @ [x]) B = nths xs B"
      by (simp add: nths_append)+
    have ?case
      using L R snoc by presburger
  } note length_notin = this

  { assume *: "length xs ∈ (A ∪ B)"
    then have new_nths: "nths (xs @ [x]) (A ∪ B) = nths xs (A ∪ B) @ [x]"
      by (simp add: nths_append)
    from * consider (A) "length xs ∈ A" | (B) "length xs ∈ B"
      using assms by auto
    then have ?case
    proof cases
      case A
      then have "i ∈ B ⟹ i > length xs" for i
        using assms by force
      then have nths_B: "nths (xs @ [x]) B = []"
        by (metis Suc_less_eq le_simps(2) length_Cons length_rotate1 nths_none rotate1.simps(2))
      from A have "nths (xs @ [x]) A = nths xs A @ [x]"
        by (simp add: nths_append)
      then have "nths (xs @ [x]) A @ nths (xs @ [x]) B = (nths xs A @ nths xs B) @ [x]"
        by (metis append_is_Nil_conv nths_B nths_append self_append_conv)
      then show ?thesis
        using snoc new_nths by presburger
    next
      case B
      then have "length xs ∉ A"
        using assms by blast
      then have "nths (xs @ [x]) A = nths xs A"
        by (simp add: nths_append)
      moreover have "nths (xs @ [x]) B = nths xs B @ [x]"
        by (simp add: B nths_append)
      ultimately show ?thesis
        by (simp add: new_nths snoc)
    qed
  } note length_in=this
   
  show ?case
    using length_in length_notin by blast
qed

corollary nths_upt_le_append_split:
  "j ≤ i ⟹ nths xs {0..<j} @ nths xs {j..i} = nths xs {0..i}"
proof -
  assume "j ≤ i"
  have "⋀x y. x ∈ {0..<j} ⟹ y ∈ {j..i} ⟹ x < y"
    by auto
  then have "nths xs {0..<j} @ nths xs {j..i} = nths xs ({0..<j} ∪ {j..i})"
    by (rule nths_split_union)
  moreover have "{0..<j} ∪ {j..i} = {0..i}"
    by (simp add: ivl_disj_un_two(7) ‹j ≤ i›)
  ultimately show ?thesis
    using ‹j ≤ i› by presburger
qed

lemma nths_Cons_atLeastAtMost: "n > m ⟹ nths (x # xs) {m..n} = (if m = 0 then x # nths xs {0..n-1} else nths xs {m-1..n-1})"
  apply (simp add: nths_Cons)
  apply safe
  using One_nat_def sl1 apply presburger
  using One_nat_def le_eq_less_or_eq sl2 apply presburger
  done

lemma nths_atLeastAtMost_eq_drop_take: "nths xs {m..n} = drop m (take (n+1) xs)"
  by (induct xs rule: rev_induct, simp_all split: nat_diff_split add: nths_append, linarith)

lemma drop_as_map: "drop m xs = map (nth xs) [m..<length xs]"
  by (metis add.commute add.right_neutral drop_map drop_upt map_nth)

lemma take_as_map: "take m xs = map (nth xs) [0..<min m (length xs)]"
  by (metis (no_types, lifting) add_0 map_nth min.cobounded2 min.commute min_def take_all_iff take_map take_upt)

lemma nths_atLeastAtMost_as_map: "nths xs {m..n} = map (λ i. xs ! i) [m..<min (n+1) (length xs)]"
  by (simp add: nths_atLeastAtMost_eq_drop_take drop_as_map take_as_map)

lemma nths_single: "nths xs {k} = (if k < length xs then [xs ! k] else [])"
  using nths_atLeastAtMost_as_map[of xs k k] by simp 

lemma nths_list_update_in_range: "k ∈ {m..n} ⟹ nths (list_update xs k x) {m..n} = list_update (nths xs {m..n}) (k - m) x"
proof (induct xs arbitrary: k x m n)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case
  proof (cases k)
    case 0
    then show ?thesis apply (simp)
      by (smt (verit, best) Cons.prems append_Cons list_update_code(2) nths_Cons)
  next
    case (Suc nat)
    with Cons show ?thesis
    proof (cases n m rule: linorder_cases)
      case less
      then show ?thesis
        by force
    next
      case equal
      with Suc show ?thesis 
        by (cases k, force)
           (metis (no_types, opaque_lifting) Cons.prems nths_single atLeastAtMost_singleton diff_is_0_eq' length_list_update list_update_code(2) list_update_code(3) list_update_nonempty nle_le nth_list_update_eq singletonD)
    next
      case greater
      with Suc Cons(1)[of nat "m - Suc 0" "n - Suc 0" x] show ?thesis
        by (cases k, simp_all add: nths_Cons_atLeastAtMost nths_atLeastAtMost_0_take take_update_swap, safe)
           (metis Cons.prems Suc_le_mono Suc_pred atLeastAtMost_iff diff_Suc_Suc le_zero_eq not_gr_zero)
    qed
  qed
qed

lemma length_nths_atLeastAtMost [simp]: "length (nths xs {m..n}) = min (Suc n) (length xs) - m"
  by (simp add: nths_atLeastAtMost_as_map)

lemma hd_nths_atLeastAtMost: "⟦ m < length xs; m ≤ n ⟧ ⟹ hd (nths xs {m..n}) = xs ! m"
  by (simp add: nths_atLeastAtMost_as_map upt_conv_Cons)

lemma tl_nths_atLeastAtMost: "tl (nths xs {m..n}) = nths xs {Suc m..n}"
  by (simp add: nths_atLeastAtMost_as_map, metis map_tl tl_upt)

lemma set_nths_atLeastAtMost: "set (nths xs {m..n}) = {xs!i | i. m ≤ i ∧ i ≤ n ∧ i < length xs}"
  by (auto simp add: nths_atLeastAtMost_as_map)

lemma nths_atLeastAtMost_neq_Nil [simp]: "⟦ m ≤ n; length xs > m ⟧ ⟹ nths xs {m..n} ≠ []"
  by (force simp add: nths_atLeastAtMost_as_map)

lemma nths_atLeastAtMost_head: "⟦ m ≤ n; m < length xs ⟧ ⟹ nths xs {m..n} = xs ! m # (nths xs {Suc m..n})"
  by (simp add: nths_atLeastAtMost_as_map upt_conv_Cons)

lemma sorted_hd_le_all: "⟦ xs ≠ []; sorted xs; x ∈ set xs ⟧ ⟹ hd xs ≤ x"
  by (metis Orderings.order_eq_iff list.sel(1) list.set_cases sorted_simps(2))

subsection ‹ List power ›

overloading
  listpow ≡ "compow :: nat ⇒ 'a list ⇒ 'a list"
begin

fun listpow :: "nat ⇒ 'a list ⇒ 'a list" where
  "listpow 0 xs = []" 
| "listpow (Suc n) xs = xs @ listpow n xs"

end

lemma listpow_Nil [simp]: "[] ^^ n = []"
  by (induct n) simp_all

lemma listpow_Suc_right: "xs ^^ Suc n = xs ^^ n @ xs"
  by (induct n) simp_all

lemma listpow_add: "xs ^^ (m + n) = xs ^^ m @ xs ^^ n"
  by (induct m) simp_all

subsection ‹ Alternative List Lexicographic Order ›

text ‹ Since we can't instantiate the order class twice for lists, and we often want prefix as
  the default order, we here add syntax for the lexicographic order relation. ›

definition list_lex_less :: "'a::linorder list ⇒ 'a list ⇒ bool" (infix "<⇩_l" 50)
where "xs <⇩_l ys ⟷ (xs, ys) ∈ lexord {(u, v). u < v}"

lemma list_lex_less_neq [simp]: "x <⇩_l y ⟹ x ≠ y"
  apply (simp add: list_lex_less_def)
  apply (meson case_prodD less_irrefl lexord_irreflexive mem_Collect_eq)
  done

lemma not_less_Nil [simp]: "¬ x <⇩_l []"
  by (simp add: list_lex_less_def)

lemma Nil_less_Cons [simp]: "[] <⇩_l a # x"
  by (simp add: list_lex_less_def)

lemma Cons_less_Cons [simp]: "a # x <⇩_l b # y ⟷ a < b ∨ a = b ∧ x <⇩_l y"
  by (simp add: list_lex_less_def)

subsection ‹ Bounded List Universe ›

text ‹ Analogous to @{const List.n_lists}, but includes all lists with a length up to the given number. ›

definition b_lists :: "nat ⇒ 'a list ⇒ 'a list list" where
"b_lists n xs = concat (map (λ n. List.n_lists n xs) [0..<Suc n])"

lemma b_lists_Nil [simp]: "b_lists n [] = [[]]"
  unfolding b_lists_def by (induct n) simp_all 

lemma length_b_lists_elem: "ys ∈ set (b_lists n xs) ⟹ length ys ≤ n"
  unfolding b_lists_def
  by (auto simp add: length_n_lists_elem)

lemma b_lists_in_lists: "ys ∈ set (b_lists n xs) ⟹ ys ∈ lists (set xs)"
  by (auto simp add: b_lists_def in_mono set_n_lists)

lemma in_blistsI: 
  assumes "length xs ≤ n" "xs ∈ lists (set A)"
  shows "xs ∈ set (b_lists n A)"
proof -
  have "xs ∉ set (List.n_lists n A) ⟹ xs ∈ set (List.n_lists (length xs) A)"
    using assms(2) in_lists_conv_set set_n_lists by fastforce
  with assms show ?thesis
  by (force simp add: set_n_lists subsetI b_lists_def)
qed

lemma ex_list_nonempty_carrier:
  assumes "A ≠ {}"
  obtains xs where "length xs = n" "set xs ⊆ A"
proof -
  obtain a where a: "a ∈ A"
    using assms by blast
  hence "set (replicate n a) ⊆ A"
    by (simp add: set_replicate_conv_if)
  with that show ?thesis
    by (meson length_replicate)
qed

lemma n_lists_inj:
  assumes "xs ≠ []" "List.n_lists m xs = List.n_lists n xs"
  shows "m = n"
proof (rule ccontr)
  assume mn: "m ≠ n"
  hence "m < n ∨ m > n"
    by auto
  moreover have "m < n ⟶ False"
  proof
    assume "m < n"
    then obtain ys where ys: "length ys = n" "set ys ⊆ set xs"
      by (metis all_not_in_conv assms(1) ex_list_nonempty_carrier length_0_conv neq0_conv nth_mem)
    hence "ys ∈ set (List.n_lists n xs)"
      by (simp add: set_n_lists)
    moreover have "ys ∉ set (List.n_lists m xs)"
      using length_n_lists_elem mn ys(1) by blast
    ultimately show False
      by (simp add: assms(2))
  qed
  moreover have "m > n ⟶ False"
  proof
    assume "n < m"
    then obtain ys where ys: "length ys = m" "set ys ⊆ set xs"
      by (metis all_not_in_conv assms(1) ex_list_nonempty_carrier length_0_conv neq0_conv nth_mem)
    hence "ys ∈ set (List.n_lists m xs)"
      by (simp add: set_n_lists)
    moreover have "ys ∉ set (List.n_lists n xs)"
      using length_n_lists_elem mn ys(1) by blast
    ultimately show False
      by (simp add: assms(2))
  qed
  ultimately show False
    by blast
qed 

lemma distinct_b_lists: "distinct xs ⟹ distinct (b_lists n xs)"
  apply (cases "xs = []")
   apply (simp)
  apply (simp add: b_lists_def, safe)
    apply (rule distinct_concat)
      apply (simp add: distinct_map)
      apply (simp add: inj_onI n_lists_inj)
  using distinct_n_lists apply auto[1]
    apply (safe)
    apply (metis ex_map_conv length_n_lists_elem)
   apply (simp add: distinct_n_lists)
  apply (metis atLeastLessThan_iff length_n_lists_elem order_less_irrefl)
  done

definition bounded_lists :: "nat ⇒ 'a set ⇒ 'a list set" where
  "bounded_lists n A = {xs∈lists A. length xs ≤ n}"

lemma bounded_lists_b_lists [code]: "bounded_lists n (set xs) = set (b_lists n xs)"
  apply (simp add: bounded_lists_def in_blistsI in_listsI, safe)
  using in_blistsI apply blast
  apply (meson b_lists_in_lists in_lists_conv_set)
  apply (meson length_b_lists_elem)
  done

subsection ‹ Disjointness and Partitions ›

definition list_disjoint :: "'a set list ⇒ bool" where
"list_disjoint xs = (∀ i < length xs. ∀ j < length xs. i ≠ j ⟶ xs!i ∩ xs!j = {})"

definition list_partitions :: "'a set list ⇒ 'a set ⇒ bool" where
"list_partitions xs T = (list_disjoint xs ∧ ⋃ (set xs) = T)"

lemma list_disjoint_Nil [simp]: "list_disjoint []"
  by (simp add: list_disjoint_def)

lemma list_disjoint_Cons [simp]: "list_disjoint (A # Bs) = ((∀ B ∈ set Bs. A ∩ B = {}) ∧ list_disjoint Bs)"
  apply (simp add: list_disjoint_def disjoint_iff)
  apply (safe)
    apply (metis Suc_less_eq in_set_conv_nth nat.distinct(1) neq0_conv nth_Cons_0 nth_Cons_Suc)
   apply (metis lessI lift_Suc_mono_less_iff nat.inject nth_Cons_Suc)
  apply (metis less_Suc_eq_0_disj[of _ "length Bs"] nth_Cons_0[of A Bs] nth_Cons_Suc[of A Bs] nth_mem[of _ Bs])
  done

subsection ‹ Code Generation ›

lemma set_singleton_iff: "set xs = {x} ⟷ remdups xs = [x]"
  apply (safe)
    apply (metis card_set empty_set insert_not_empty length_0_conv length_Suc_conv list.simps(15) remdups.simps(1) remdups.simps(2) set_remdups the_elem_set)
   apply (metis empty_iff empty_set set_ConsD set_remdups)
  apply (metis list.set_intros(1) set_remdups)
  done

lemma list_singleton_iff: "(∃ x. xs = [x]) ⟷ (length xs = 1)"
  by (auto simp add: length_Suc_conv)

end