# HG changeset patch
# User haftmann
# Date 1275485714 -7200
# Node ID 881fa5012451a26d187b9066c046924b8f9bd934
# Parent  2b1c6dd4899593bd99e6e1807ea2ddbc4bca6938
induction over non-empty lists

diff -r 2b1c6dd48995 -r 881fa5012451 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 02 15:35:14 2010 +0200
+++ b/src/HOL/List.thy	Wed Jun 02 15:35:14 2010 +0200
@@ -451,6 +451,23 @@
   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
 by (rule measure_induct [of length]) iprover
 
+lemma list_nonempty_induct [consumes 1, case_names single cons]:
+  assumes "xs \<noteq> []"
+  assumes single: "\<And>x. P [x]"
+  assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
+  shows "P xs"
+using `xs \<noteq> []` proof (induct xs)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) show ?case proof (cases xs)
+    case Nil with single show ?thesis by simp
+  next
+    case Cons then have "xs \<noteq> []" by simp
+    moreover with Cons.hyps have "P xs" .
+    ultimately show ?thesis by (rule cons)
+  qed
+qed
+
 
 subsubsection {* @{const length} *}