summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 37289 | 881fa5012451 |

parent 37123 | 9cce71cd4bf0 |

child 37408 | f51ff37811bf |

--- 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} *}