--- a/src/HOL/List.thy Sat Jul 19 18:30:42 2014 +0200
+++ b/src/HOL/List.thy Sat Jul 19 18:30:43 2014 +0200
@@ -1235,6 +1235,20 @@
lemmas rev_cases = rev_exhaust
+lemma rev_nonempty_induct [consumes 1, case_names single snoc]:
+ assumes "xs \<noteq> []"
+ and single: "\<And>x. P [x]"
+ and snoc': "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (xs@[x])"
+ shows "P xs"
+using `xs \<noteq> []` proof (induct xs rule: rev_induct)
+ case (snoc x xs) then show ?case
+ proof (cases xs)
+ case Nil thus ?thesis by (simp add: single)
+ next
+ case Cons with snoc show ?thesis by (fastforce intro!: snoc')
+ qed
+qed simp
+
lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
by(rule rev_cases[of xs]) auto