src/HOL/List.thy
 changeset 37289 881fa5012451 parent 37123 9cce71cd4bf0 child 37408 f51ff37811bf
equal inserted replaced
37288:2b1c6dd48995 37289:881fa5012451
`   449 `
`   449 `
`   450 lemma length_induct:`
`   450 lemma length_induct:`
`   451   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"`
`   451   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"`
`   452 by (rule measure_induct [of length]) iprover`
`   452 by (rule measure_induct [of length]) iprover`
`   453 `
`   453 `
`       `
`   454 lemma list_nonempty_induct [consumes 1, case_names single cons]:`
`       `
`   455   assumes "xs \<noteq> []"`
`       `
`   456   assumes single: "\<And>x. P [x]"`
`       `
`   457   assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"`
`       `
`   458   shows "P xs"`
`       `
`   459 using `xs \<noteq> []` proof (induct xs)`
`       `
`   460   case Nil then show ?case by simp`
`       `
`   461 next`
`       `
`   462   case (Cons x xs) show ?case proof (cases xs)`
`       `
`   463     case Nil with single show ?thesis by simp`
`       `
`   464   next`
`       `
`   465     case Cons then have "xs \<noteq> []" by simp`
`       `
`   466     moreover with Cons.hyps have "P xs" .`
`       `
`   467     ultimately show ?thesis by (rule cons)`
`       `
`   468   qed`
`       `
`   469 qed`
`       `
`   470 `
`   454 `
`   471 `
`   455 subsubsection {* @{const length} *}`
`   472 subsubsection {* @{const length} *}`
`   456 `
`   473 `
`   457 text {*`
`   474 text {*`
`   458   Needs to come before @{text "@"} because of theorem @{text`
`   475   Needs to come before @{text "@"} because of theorem @{text`