src/HOL/Parity.thy
changeset 58769 70fff47875cd
parent 58740 cb9d84d3e7f2
child 58770 ae5e9b4f8daf
     1.1 --- a/src/HOL/Parity.thy	Wed Oct 22 23:15:40 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
     1.3 @@ -353,6 +353,32 @@
     1.4  lemma odd_two_times_div_two_Suc:
     1.5    "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
     1.6    using odd_two_times_div_two_succ [of n] by simp
     1.7 +
     1.8 +lemma parity_induct [case_names zero even odd]:
     1.9 +  assumes zero: "P 0"
    1.10 +  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
    1.11 +  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
    1.12 +  shows "P n"
    1.13 +proof (induct n rule: less_induct)
    1.14 +  case (less n)
    1.15 +  show "P n"
    1.16 +  proof (cases "n = 0")
    1.17 +    case True with zero show ?thesis by simp
    1.18 +  next
    1.19 +    case False
    1.20 +    with less have hyp: "P (n div 2)" by simp
    1.21 +    show ?thesis
    1.22 +    proof (cases "even n")
    1.23 +      case True
    1.24 +      with hyp even [of "n div 2"] show ?thesis
    1.25 +        by (simp add: dvd_mult_div_cancel)
    1.26 +    next
    1.27 +      case False
    1.28 +      with hyp odd [of "n div 2"] show ?thesis 
    1.29 +        by (simp add: odd_two_times_div_two_Suc)
    1.30 +    qed
    1.31 +  qed
    1.32 +qed
    1.33    
    1.34  text {* Nice facts about division by @{term 4} *}  
    1.35