Theory List_Misc

section‹Miscellaneous List Lemmas›
theory List_Misc
imports Main
begin

lemma list_app_singletonE:
  assumes "rs1 @ rs2 = [x]"
  obtains (first) "rs1 = [x]" "rs2 = []"
        | (second) "rs1 = []" "rs2 = [x]"
using assms
by (cases "rs1") auto

lemma list_app_eq_cases:
  assumes "xs1 @ xs2 = ys1 @ ys2"
  obtains (longer)  "xs1 = take (length xs1) ys1" "xs2 = drop (length xs1) ys1 @ ys2"
        | (shorter) "ys1 = take (length ys1) xs1" "ys2 = drop (length ys1) xs1 @ xs2"
using assms by (cases "length xs1  length ys1") (metis append_eq_append_conv_if)+

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