Theory HOL-Library.More_List

(* Author: Andreas Lochbihler, ETH Zürich
   Author: Florian Haftmann, TU Muenchen  *)

section ‹Less common functions on lists›

theory More_List
imports Main
begin

definition strip_while :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list"
where
  "strip_while P = rev ∘ dropWhile P ∘ rev"

lemma strip_while_rev [simp]:
  "strip_while P (rev xs) = rev (dropWhile P xs)"
  by (simp add: strip_while_def)
  
lemma strip_while_Nil [simp]:
  "strip_while P [] = []"
  by (simp add: strip_while_def)

lemma strip_while_append [simp]:
  "¬ P x ⟹ strip_while P (xs @ [x]) = xs @ [x]"
  by (simp add: strip_while_def)

lemma strip_while_append_rec [simp]:
  "P x ⟹ strip_while P (xs @ [x]) = strip_while P xs"
  by (simp add: strip_while_def)

lemma strip_while_Cons [simp]:
  "¬ P x ⟹ strip_while P (x # xs) = x # strip_while P xs"
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)

lemma strip_while_eq_Nil [simp]:
  "strip_while P xs = [] ⟷ (∀x∈set xs. P x)"
  by (simp add: strip_while_def)

lemma strip_while_eq_Cons_rec:
  "strip_while P (x # xs) = x # strip_while P xs ⟷ ¬ (P x ∧ (∀x∈set xs. P x))"
  by (induct xs rule: rev_induct) (simp_all add: strip_while_def)

lemma split_strip_while_append:
  fixes xs :: "'a list"
  obtains ys zs :: "'a list"
  where "strip_while P xs = ys" and "∀x∈set zs. P x" and "xs = ys @ zs"
proof (rule that)
  show "strip_while P xs = strip_while P xs" ..
  show "∀x∈set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric])
  have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))"
    by (simp add: strip_while_def)
  then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))"
    by (simp only: rev_is_rev_conv)
qed

lemma strip_while_snoc [simp]:
  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
  by (simp add: strip_while_def)

lemma strip_while_map:
  "strip_while P (map f xs) = map f (strip_while (P ∘ f) xs)"
  by (simp add: strip_while_def rev_map dropWhile_map)

lemma strip_while_dropWhile_commute:
  "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
proof (induct xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  show ?case
  proof (cases "∀y∈set xs. P y")
    case True
    with dropWhile_append2 [of "rev xs"] show ?thesis
      by (auto simp add: strip_while_def dest: set_dropWhileD)
  next
    case False
    then obtain y where "y ∈ set xs" and "¬ P y"
      by blast
    with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
      by (simp add: strip_while_def)
  qed
qed

lemma dropWhile_strip_while_commute:
  "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
  by (simp add: strip_while_dropWhile_commute)


definition no_leading :: "('a ⇒ bool) ⇒ 'a list ⇒ bool"
where
  "no_leading P xs ⟷ (xs ≠ [] ⟶ ¬ P (hd xs))"

lemma no_leading_Nil [iff]:
  "no_leading P []"
  by (simp add: no_leading_def)

lemma no_leading_Cons [iff]:
  "no_leading P (x # xs) ⟷ ¬ P x"
  by (simp add: no_leading_def)

lemma no_leading_append [simp]:
  "no_leading P (xs @ ys) ⟷ no_leading P xs ∧ (xs = [] ⟶ no_leading P ys)"
  by (induct xs) simp_all

lemma no_leading_dropWhile [simp]:
  "no_leading P (dropWhile P xs)"
  by (induct xs) simp_all

lemma dropWhile_eq_obtain_leading:
  assumes "dropWhile P xs = ys"
  obtains zs where "xs = zs @ ys" and "⋀z. z ∈ set zs ⟹ P z" and "no_leading P ys"
proof -
  from assms have "∃zs. xs = zs @ ys ∧ (∀z ∈ set zs. P z) ∧ no_leading P ys"
  proof (induct xs arbitrary: ys)
    case Nil then show ?case by simp
  next
    case (Cons x xs ys)
    show ?case proof (cases "P x")
      case True with Cons.hyps [of ys] Cons.prems
      have "∃zs. xs = zs @ ys ∧ (∀a∈set zs. P a) ∧ no_leading P ys"
        by simp
      then obtain zs where "xs = zs @ ys" and "⋀z. z ∈ set zs ⟹ P z"
        and *: "no_leading P ys"
        by blast
      with True have "x # xs = (x # zs) @ ys" and "⋀z. z ∈ set (x # zs) ⟹ P z"
        by auto
      with * show ?thesis
        by blast    next
      case False
      with Cons show ?thesis by (cases ys) simp_all
    qed
  qed
  with that show thesis
    by blast
qed

lemma dropWhile_idem_iff:
  "dropWhile P xs = xs ⟷ no_leading P xs"
  by (cases xs) (auto elim: dropWhile_eq_obtain_leading)


abbreviation no_trailing :: "('a ⇒ bool) ⇒ 'a list ⇒ bool"
where
  "no_trailing P xs ≡ no_leading P (rev xs)"

lemma no_trailing_unfold:
  "no_trailing P xs ⟷ (xs ≠ [] ⟶ ¬ P (last xs))"
  by (induct xs) simp_all

lemma no_trailing_Nil [iff]:
  "no_trailing P []"
  by simp

lemma no_trailing_Cons [simp]:
  "no_trailing P (x # xs) ⟷ no_trailing P xs ∧ (xs = [] ⟶ ¬ P x)"
  by simp

lemma no_trailing_append:
  "no_trailing P (xs @ ys) ⟷ no_trailing P ys ∧ (ys = [] ⟶ no_trailing P xs)"
  by (induct xs) simp_all

lemma no_trailing_append_Cons [simp]:
  "no_trailing P (xs @ y # ys) ⟷ no_trailing P (y # ys)"
  by simp

lemma no_trailing_strip_while [simp]:
  "no_trailing P (strip_while P xs)"
  by (induct xs rule: rev_induct) simp_all

lemma strip_while_idem [simp]:
  "no_trailing P xs ⟹ strip_while P xs = xs"
  by (cases xs rule: rev_cases) simp_all

lemma strip_while_eq_obtain_trailing:
  assumes "strip_while P xs = ys"
  obtains zs where "xs = ys @ zs" and "⋀z. z ∈ set zs ⟹ P z" and "no_trailing P ys"
proof -
  from assms have "rev (rev (dropWhile P (rev xs))) = rev ys"
    by (simp add: strip_while_def)
  then have "dropWhile P (rev xs) = rev ys"
    by simp
  then obtain zs where A: "rev xs = zs @ rev ys" and B: "⋀z. z ∈ set zs ⟹ P z"
    and C: "no_trailing P ys"
    using dropWhile_eq_obtain_leading by blast
  from A have "rev (rev xs) = rev (zs @ rev ys)"
    by simp
  then have "xs = ys @ rev zs"
    by simp
  moreover from B have "⋀z. z ∈ set (rev zs) ⟹ P z"
    by simp
  ultimately show thesis using that C by blast
qed

lemma strip_while_idem_iff:
  "strip_while P xs = xs ⟷ no_trailing P xs"
proof -
  define ys where "ys = rev xs"
  moreover have "strip_while P (rev ys) = rev ys ⟷ no_trailing P (rev ys)"
    by (simp add: dropWhile_idem_iff)
  ultimately show ?thesis by simp
qed

lemma no_trailing_map:
  "no_trailing P (map f xs) ⟷ no_trailing (P ∘ f) xs"
  by (simp add: last_map no_trailing_unfold)

lemma no_trailing_drop [simp]:
  "no_trailing P (drop n xs)" if "no_trailing P xs"
proof -
  from that have "no_trailing P (take n xs @ drop n xs)"
    by simp
  then show ?thesis
    by (simp only: no_trailing_append)
qed

lemma no_trailing_upt [simp]:
  "no_trailing P [n..<m] ⟷ (n < m ⟶ ¬ P (m - 1))"
  by (auto simp add: no_trailing_unfold)


definition nth_default :: "'a ⇒ 'a list ⇒ nat ⇒ 'a"
where
  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"

lemma nth_default_nth:
  "n < length xs ⟹ nth_default dflt xs n = xs ! n"
  by (simp add: nth_default_def)

lemma nth_default_beyond:
  "length xs ≤ n ⟹ nth_default dflt xs n = dflt"
  by (simp add: nth_default_def)

lemma nth_default_Nil [simp]:
  "nth_default dflt [] n = dflt"
  by (simp add: nth_default_def)

lemma nth_default_Cons:
  "nth_default dflt (x # xs) n = (case n of 0 ⇒ x | Suc n' ⇒ nth_default dflt xs n')"
  by (simp add: nth_default_def split: nat.split)

lemma nth_default_Cons_0 [simp]:
  "nth_default dflt (x # xs) 0 = x"
  by (simp add: nth_default_Cons)

lemma nth_default_Cons_Suc [simp]:
  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
  by (simp add: nth_default_Cons)

lemma nth_default_replicate_dflt [simp]:
  "nth_default dflt (replicate n dflt) m = dflt"
  by (simp add: nth_default_def)

lemma nth_default_append:
  "nth_default dflt (xs @ ys) n =
    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
  by (auto simp add: nth_default_def nth_append)

lemma nth_default_append_trailing [simp]:
  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)

lemma nth_default_snoc_default [simp]:
  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
  by (auto simp add: nth_default_def fun_eq_iff nth_append)

lemma nth_default_eq_dflt_iff:
  "nth_default dflt xs k = dflt ⟷ (k < length xs ⟶ xs ! k = dflt)"
  by (simp add: nth_default_def)

lemma nth_default_take_eq:
  "nth_default dflt (take m xs) n =
    (if n < m then nth_default dflt xs n else dflt)"
  by (simp add: nth_default_def)

lemma in_enumerate_iff_nth_default_eq:
  "x ≠ dflt ⟹ (n, x) ∈ set (enumerate 0 xs) ⟷ nth_default dflt xs n = x"
  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)

lemma last_conv_nth_default:
  assumes "xs ≠ []"
  shows "last xs = nth_default dflt xs (length xs - 1)"
  using assms by (simp add: nth_default_def last_conv_nth)
  
lemma nth_default_map_eq:
  "f dflt' = dflt ⟹ nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
  by (simp add: nth_default_def)

lemma finite_nth_default_neq_default [simp]:
  "finite {k. nth_default dflt xs k ≠ dflt}"
  by (simp add: nth_default_def)

lemma sorted_list_of_set_nth_default:
  "sorted_list_of_set {k. nth_default dflt xs k ≠ dflt} = map fst (filter (λ(_, x). x ≠ dflt) (enumerate 0 xs))"
  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)

lemma map_nth_default:
  "map (nth_default x xs) [0..<length xs] = xs"
proof -
  have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
    by (rule map_cong) (simp_all add: nth_default_nth)
  show ?thesis by (simp add: * map_nth)
qed

lemma range_nth_default [simp]:
  "range (nth_default dflt xs) = insert dflt (set xs)"
  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)

lemma nth_strip_while:
  assumes "n < length (strip_while P xs)"
  shows "strip_while P xs ! n = xs ! n"
proof -
  have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs"
    by (subst add.commute)
      (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append])
  then show ?thesis using assms
    by (simp add: strip_while_def rev_nth dropWhile_nth)
qed

lemma length_strip_while_le:
  "length (strip_while P xs) ≤ length xs"
  unfolding strip_while_def o_def length_rev
  by (subst (2) length_rev[symmetric])
    (simp add: strip_while_def length_dropWhile_le del: length_rev)

lemma nth_default_strip_while_dflt [simp]:
  "nth_default dflt (strip_while ((=) dflt) xs) = nth_default dflt xs"
  by (induct xs rule: rev_induct) auto

lemma nth_default_eq_iff:
  "nth_default dflt xs = nth_default dflt ys
     ⟷ strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P ⟷ ?Q")
proof
  let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
  assume ?P
  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
    by simp
  have len: "length ?xs = length ?ys"
  proof (rule ccontr)
    assume len: "length ?xs ≠ length ?ys"
    { fix xs ys :: "'a list"
      let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
      assume len: "length ?xs < length ?ys"
      then have "length ?ys > 0" by arith
      then have "?ys ≠ []" by simp
      with last_conv_nth_default [of ?ys dflt]
      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
        by auto
      moreover from ‹?ys ≠ []› no_trailing_strip_while [of "HOL.eq dflt" ys]
        have "last ?ys ≠ dflt" by (simp add: no_trailing_unfold)
      ultimately have "nth_default dflt ?xs (length ?ys - 1) ≠ dflt"
        using eq by simp
      moreover from len have "length ?ys - 1 ≥ length ?xs" by simp
      ultimately have False by (simp only: nth_default_beyond) simp
    } 
    from this [of xs ys] this [of ys xs] len eq show False
      by (auto simp only: linorder_class.neq_iff)
  qed
  then show ?Q
  proof (rule nth_equalityI [rule_format])
    fix n
    assume n: "n < length ?xs"
    with len have "n < length ?ys"
      by simp
    with n have xs: "nth_default dflt ?xs n = ?xs ! n"
      and ys: "nth_default dflt ?ys n = ?ys ! n"
      by (simp_all only: nth_default_nth)
    with eq show "?xs ! n = ?ys ! n"
      by simp
  qed
next
  assume ?Q
  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
    by simp
  then show ?P
    by simp
qed

lemma nth_default_map2:
  ‹nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)›
    if ‹length xs = length ys› and ‹f d1 d2 = d› for bs cs
using that proof (induction xs ys arbitrary: n rule: list_induct2)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs y ys)
  then show ?case
    by (cases n) simp_all
qed

end