1.1 --- a/src/HOL/List.thy	Sat Jul 19 18:30:42 2014 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Jul 19 18:30:43 2014 +0200
     1.3 @@ -1235,6 +1235,20 @@
     1.4  
     1.5  lemmas rev_cases = rev_exhaust
     1.6  
     1.7 +lemma rev_nonempty_induct [consumes 1, case_names single snoc]:
     1.8 +  assumes "xs \<noteq> []"
     1.9 +  and single: "\<And>x. P [x]"
    1.10 +  and snoc': "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (xs@[x])"
    1.11 +  shows "P xs"
    1.12 +using `xs \<noteq> []` proof (induct xs rule: rev_induct)
    1.13 +  case (snoc x xs) then show ?case
    1.14 +  proof (cases xs)
    1.15 +    case Nil thus ?thesis by (simp add: single)
    1.16 +  next
    1.17 +    case Cons with snoc show ?thesis by (fastforce intro!: snoc')
    1.18 +  qed
    1.19 +qed simp
    1.20 +
    1.21  lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
    1.22  by(rule rev_cases[of xs]) auto
    1.23