Theory List_Extensions

section ‹Lists›

theory List_Extensions
imports "HOL-Library.Sublist"
begin

  declare remove1_idem[simp]

  lemma nth_append_simps[simp]:
    "i < length xs ⟹ (xs @ ys) ! i = xs ! i"
    "i ≥ length xs ⟹ (xs @ ys) ! i = ys ! (i - length xs)"
    unfolding nth_append by simp+

  notation zip (infixr ‹||› 51)

  abbreviation "project A ≡ filter (λ a. a ∈ A)"
  abbreviation "select s w ≡ nths w s"

  lemma map_plus[simp]: "map (plus n) [i ..< j] = [i + n ..< j + n]"
  proof (induct n)
    case 0
    show ?case by simp
  next
    case (Suc n)
    have "map (plus (Suc n)) [i ..< j] = map (Suc ∘ plus n) [i ..< j]" by simp
    also have "… = (map Suc ∘ map (plus n)) [i ..< j]" by simp
    also have "… = map Suc (map (plus n) [i ..< j])" by simp
    also have "… = map Suc [i + n ..< j + n]" unfolding Suc by simp
    also have "… = [Suc (i + n) ..< Suc (j + n)]" unfolding map_Suc_upt by simp
    also have "… = [i + Suc n ..< j + Suc n]" by simp
    finally show ?case by this
  qed

  lemma singleton_list_lengthE[elim]:
    assumes "length xs = 1"
    obtains x
    where "xs = [x]"
  proof -
    have 0: "length xs = Suc 0" using assms by simp
    obtain y ys where 1: "xs = y # ys" "length ys = 0" using 0 Suc_length_conv by metis
    show ?thesis using that 1 by blast
  qed

  lemma singleton_hd_last: "length xs = 1 ⟹ hd xs = last xs" by fastforce

  lemma set_subsetI[intro]:
    assumes "⋀ i. i < length xs ⟹ xs ! i ∈ S"
    shows "set xs ⊆ S"
  proof
    fix x
    assume 0: "x ∈ set xs"
    obtain i where 1: "i < length xs" "x = xs ! i" using 0 unfolding in_set_conv_nth by blast
    show "x ∈ S" using assms(1) 1 by auto
  qed

  lemma hd_take[simp]:
    assumes "n ≠ 0" "xs ≠ []"
    shows "hd (take n xs) = hd xs"
  proof -
    have 1: "take n xs ≠ []" using assms by simp
    have 2: "0 < n" using assms by simp
    have "hd (take n xs) = take n xs ! 0" using hd_conv_nth[OF 1] by this
    also have "… = xs ! 0" using nth_take[OF 2] by this
    also have "… = hd xs" using hd_conv_nth[OF assms(2)] by simp
    finally show ?thesis by this
  qed
  lemma hd_drop[simp]:
    assumes "n < length xs"
    shows "hd (drop n xs) = xs ! n"
    using hd_drop_conv_nth assms by this
  lemma last_take[simp]:
    assumes "n < length xs"
    shows "last (take (Suc n) xs) = xs ! n"
  using assms
  proof (induct xs arbitrary: n)
    case (Nil)
    show ?case using Nil by simp
  next
    case (Cons x xs)
    show ?case using Cons by (auto) (metis Suc_less_eq Suc_pred)
  qed

  lemma split_list_first_unique:
    assumes "u⇩1 @ [a] @ u⇩2 = v⇩1 @ [a] @ v⇩2" "a ∉ set u⇩1" "a ∉ set v⇩1"
    shows "u⇩1 = v⇩1"
  proof -
    obtain w where "u⇩1 = v⇩1 @ w ∧ w @ [a] @ u⇩2 = [a] @ v⇩2 ∨
      u⇩1 @ w = v⇩1 ∧ [a] @ u⇩2 = w @ [a] @ v⇩2" using assms(1) append_eq_append_conv2 by blast
    thus ?thesis using assms(2, 3) by (auto) (metis hd_append2 list.sel(1) list.set_sel(1))+
  qed

end