[STATEMENT]
lemma list_cases_Cons_snoc [case_names Nil Single Cons_snoc]:
  assumes       Nil: "xs = [] \<Longrightarrow> P"
  and        Single: "\<And>x. xs = [x] \<Longrightarrow> P"
  and     Cons_snoc: "\<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof (cases xs, rule Nil)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> xs = []
 2. \<And>a list. xs = a # list \<Longrightarrow> P
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
xs = x # xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> xs = []
 2. \<And>a list. xs = a # list \<Longrightarrow> P
[PROOF STEP]
with Single Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
xs = [?x] \<Longrightarrow> P
xs = ?x # ?ys @ [?y] \<Longrightarrow> P
xs = x # xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = [?x] \<Longrightarrow> P
xs = ?x # ?ys @ [?y] \<Longrightarrow> P
xs = x # xs

goal (1 subgoal):
 1. P
[PROOF STEP]
by (cases xs rule: rev_cases) auto
[PROOF STATE]
proof (state)
this:
P

goal (1 subgoal):
 1. xs = [] \<Longrightarrow> xs = []
[PROOF STEP]
qed