Theory List_Misc

section‹Miscellaneous List Lemmas›
theory List_Misc
imports Main
begin

lemma list_app_singletonE:
  assumes "rs⇩1 @ rs⇩2 = [x]"
  obtains (first) "rs⇩1 = [x]" "rs⇩2 = []"
        | (second) "rs⇩1 = []" "rs⇩2 = [x]"
using assms
by (cases "rs⇩1") auto

lemma list_app_eq_cases:
  assumes "xs⇩1 @ xs⇩2 = ys⇩1 @ ys⇩2"
  obtains (longer)  "xs⇩1 = take (length xs⇩1) ys⇩1" "xs⇩2 = drop (length xs⇩1) ys⇩1 @ ys⇩2"
        | (shorter) "ys⇩1 = take (length ys⇩1) xs⇩1" "ys⇩2 = drop (length ys⇩1) xs⇩1 @ xs⇩2"
using assms by (cases "length xs⇩1 ≤ length ys⇩1") (metis append_eq_append_conv_if)+

lemma empty_concat: "concat (map (λx. []) ms) = []" by simp
end