# HG changeset patch
# User haftmann
# Date 1405787443 -7200
# Node ID e848a17d9deeca00a1f4428cd15aa3ca932770fc
# Parent  083dfad2727ce1e655846dd614aa42a3efde372b
reverse induction over nonempty lists

diff -r 083dfad2727c -r e848a17d9dee src/HOL/List.thy
--- 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