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