equal
deleted
inserted
replaced
572 |
572 |
573 lemma odd_card_imp_not_empty: |
573 lemma odd_card_imp_not_empty: |
574 \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close> |
574 \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close> |
575 using that by auto |
575 using that by auto |
576 |
576 |
|
577 lemma nat_induct2 [case_names 0 1 step]: |
|
578 assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)" |
|
579 shows "P n" |
|
580 proof (induct n rule: less_induct) |
|
581 case (less n) |
|
582 show ?case |
|
583 proof (cases "n < Suc (Suc 0)") |
|
584 case True |
|
585 then show ?thesis |
|
586 using assms by (auto simp: less_Suc_eq) |
|
587 next |
|
588 case False |
|
589 then obtain k where k: "n = Suc (Suc k)" |
|
590 by (force simp: not_less nat_le_iff_add) |
|
591 then have "k<n" |
|
592 by simp |
|
593 with less assms have "P (k+2)" |
|
594 by blast |
|
595 then show ?thesis |
|
596 by (simp add: k) |
|
597 qed |
|
598 qed |
577 |
599 |
578 subsection \<open>Parity and powers\<close> |
600 subsection \<open>Parity and powers\<close> |
579 |
601 |
580 context ring_1 |
602 context ring_1 |
581 begin |
603 begin |