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.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
```