theory Foo imports Main begin

lemma list_prefix_decomp:
  shows "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys' \<and> (xs' = Nil \<or> ys' = Nil \<or> hd xs' \<noteq> hd ys')"
proof-
  {
    text {* Exclude some trivial cases. *}
    assume "\<not>(\<exists>ys'. ys = xs @ ys')" "\<not>(\<exists>xs'. xs = ys @ xs')" "xs \<noteq> ys"
    text {* Determine an index where the lists diverge. *}
    hence "\<exists>n. n < length xs \<and> n < length ys \<and> xs ! n \<noteq> ys ! n"
    proof(induct xs arbitrary: ys, simp)
      case (Cons x xs ys)
      show ?case proof(cases)
        assume "ys = Nil" thus ?thesis sledgehammer
    (* ... *)