# Theory Partial_Order_Reduction.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```