equal
deleted
inserted
replaced
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 