src/HOL/List.thy
changeset 37289 881fa5012451
parent 37123 9cce71cd4bf0
child 37408 f51ff37811bf
equal deleted 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