summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 02 Jun 2010 15:35:14 +0200 | |

changeset 37289 | 881fa5012451 |

parent 37288 | 2b1c6dd48995 |

child 37290 | 3464d7232670 |

induction over non-empty lists

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

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