src/HOL/Divides.thy
changeset 58778 e29cae8eab1f
parent 58710 7216a10d69ba
child 58786 fa5b67fb70ad
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 23 19:40:39 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 23 19:40:41 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* The division operators div and mod *}
     1.5  
     1.6  theory Divides
     1.7 -imports Nat_Transfer
     1.8 +imports Parity
     1.9  begin
    1.10  
    1.11  subsection {* Syntactic division operations *}
    1.12 @@ -504,6 +504,9 @@
    1.13  
    1.14  end
    1.15  
    1.16 +
    1.17 +subsubsection {* Parity and division *}
    1.18 +
    1.19  class semiring_div_parity = semiring_div + semiring_numeral +
    1.20    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
    1.21    assumes one_mod_two_eq_one: "1 mod 2 = 1"
    1.22 @@ -524,6 +527,76 @@
    1.23    "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
    1.24    by (cases a rule: parity_cases) simp_all
    1.25  
    1.26 +lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
    1.27 +  "1 div 2 = 0"
    1.28 +proof (cases "2 = 0")
    1.29 +  case True then show ?thesis by simp
    1.30 +next
    1.31 +  case False
    1.32 +  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
    1.33 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    1.34 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
    1.35 +  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
    1.36 +  with False show ?thesis by auto
    1.37 +qed
    1.38 +
    1.39 +subclass semiring_parity
    1.40 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
    1.41 +  fix a b c
    1.42 +  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
    1.43 +    by simp
    1.44 +next
    1.45 +  fix a b c
    1.46 +  assume "(b + c) mod a = 0"
    1.47 +  with mod_add_eq [of b c a]
    1.48 +  have "(b mod a + c mod a) mod a = 0"
    1.49 +    by simp
    1.50 +  moreover assume "b mod a = 0"
    1.51 +  ultimately show "c mod a = 0"
    1.52 +    by simp
    1.53 +next
    1.54 +  show "1 mod 2 = 1"
    1.55 +    by (fact one_mod_two_eq_one)
    1.56 +next
    1.57 +  fix a b
    1.58 +  assume "a mod 2 = 1"
    1.59 +  moreover assume "b mod 2 = 1"
    1.60 +  ultimately show "(a + b) mod 2 = 0"
    1.61 +    using mod_add_eq [of a b 2] by simp
    1.62 +next
    1.63 +  fix a b
    1.64 +  assume "(a * b) mod 2 = 0"
    1.65 +  then have "(a mod 2) * (b mod 2) = 0"
    1.66 +    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
    1.67 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
    1.68 +    by (rule divisors_zero)
    1.69 +next
    1.70 +  fix a
    1.71 +  assume "a mod 2 = 1"
    1.72 +  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
    1.73 +  then show "\<exists>b. a = b + 1" ..
    1.74 +qed
    1.75 +
    1.76 +lemma even_iff_mod_2_eq_zero:
    1.77 +  "even a \<longleftrightarrow> a mod 2 = 0"
    1.78 +  by (fact dvd_eq_mod_eq_0)
    1.79 +
    1.80 +lemma even_succ_div_two [simp]:
    1.81 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.82 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    1.83 +
    1.84 +lemma odd_succ_div_two [simp]:
    1.85 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    1.86 +  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    1.87 +
    1.88 +lemma even_two_times_div_two:
    1.89 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
    1.90 +  by (fact dvd_mult_div_cancel)
    1.91 +
    1.92 +lemma odd_two_times_div_two_succ:
    1.93 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    1.94 +  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    1.95 +
    1.96  end
    1.97  
    1.98  
    1.99 @@ -1451,6 +1524,44 @@
   1.100  instance nat :: semiring_numeral_div
   1.101    by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
   1.102  
   1.103 +lemma even_Suc_div_two [simp]:
   1.104 +  "even n \<Longrightarrow> Suc n div 2 = n div 2"
   1.105 +  using even_succ_div_two [of n] by simp
   1.106 +  
   1.107 +lemma odd_Suc_div_two [simp]:
   1.108 +  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
   1.109 +  using odd_succ_div_two [of n] by simp
   1.110 +
   1.111 +lemma odd_two_times_div_two_Suc:
   1.112 +  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
   1.113 +  using odd_two_times_div_two_succ [of n] by simp
   1.114 +
   1.115 +lemma parity_induct [case_names zero even odd]:
   1.116 +  assumes zero: "P 0"
   1.117 +  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
   1.118 +  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
   1.119 +  shows "P n"
   1.120 +proof (induct n rule: less_induct)
   1.121 +  case (less n)
   1.122 +  show "P n"
   1.123 +  proof (cases "n = 0")
   1.124 +    case True with zero show ?thesis by simp
   1.125 +  next
   1.126 +    case False
   1.127 +    with less have hyp: "P (n div 2)" by simp
   1.128 +    show ?thesis
   1.129 +    proof (cases "even n")
   1.130 +      case True
   1.131 +      with hyp even [of "n div 2"] show ?thesis
   1.132 +        by (simp add: dvd_mult_div_cancel)
   1.133 +    next
   1.134 +      case False
   1.135 +      with hyp odd [of "n div 2"] show ?thesis 
   1.136 +        by (simp add: odd_two_times_div_two_Suc)
   1.137 +    qed
   1.138 +  qed
   1.139 +qed
   1.140 +
   1.141  
   1.142  subsection {* Division on @{typ int} *}
   1.143