src/HOL/Parity.thy
 changeset 60343 063698416239 parent 59816 034b13f4efae child 60562 24af00b010cf
```     1.1 --- a/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
1.2 +++ b/src/HOL/Parity.thy	Mon Jun 01 18:59:20 2015 +0200
1.3 @@ -118,75 +118,60 @@
1.4  subsection {* Instances for @{typ nat} and @{typ int} *}
1.5
1.6  lemma even_Suc_Suc_iff [simp]:
1.7 -  "even (Suc (Suc n)) \<longleftrightarrow> even n"
1.8 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
1.9    using dvd_add_triv_right_iff [of 2 n] by simp
1.10
1.11  lemma even_Suc [simp]:
1.12 -  "even (Suc n) \<longleftrightarrow> odd n"
1.13 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
1.14    by (induct n) auto
1.15
1.16  lemma even_diff_nat [simp]:
1.17    fixes m n :: nat
1.18 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
1.19 +  shows "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
1.20  proof (cases "n \<le> m")
1.21    case True
1.22    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
1.23 -  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
1.24 -  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
1.25 +  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
1.26 +  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
1.27    then show ?thesis by auto
1.28  next
1.29    case False
1.30    then show ?thesis by simp
1.31  qed
1.32
1.33 -lemma even_diff_iff [simp]:
1.34 -  fixes k l :: int
1.35 -  shows "even (k - l) \<longleftrightarrow> even (k + l)"
1.36 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.37 -
1.39 -  fixes k l :: int
1.40 -  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
1.41 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
1.42 -
1.44 -  fixes k l :: int
1.45 -  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
1.47 -
1.48  instance nat :: semiring_parity
1.49  proof
1.50 -  show "odd (1 :: nat)"
1.51 +  show "\<not> 2 dvd (1 :: nat)"
1.52      by (rule notI, erule dvdE) simp
1.53  next
1.54    fix m n :: nat
1.55 -  assume "odd m"
1.56 -  moreover assume "odd n"
1.57 -  ultimately have *: "even (Suc m) \<and> even (Suc n)"
1.58 +  assume "\<not> 2 dvd m"
1.59 +  moreover assume "\<not> 2 dvd n"
1.60 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
1.61      by simp
1.62 -  then have "even (Suc m + Suc n)"
1.63 +  then have "2 dvd (Suc m + Suc n)"
1.65    also have "Suc m + Suc n = m + n + 2"
1.66      by simp
1.67 -  finally show "even (m + n)"
1.68 +  finally show "2 dvd (m + n)"
1.69      using dvd_add_triv_right_iff [of 2 "m + n"] by simp
1.70  next
1.71    fix m n :: nat
1.72 -  assume *: "even (m * n)"
1.73 -  show "even m \<or> even n"
1.74 +  assume *: "2 dvd (m * n)"
1.75 +  show "2 dvd m \<or> 2 dvd n"
1.76    proof (rule disjCI)
1.77 -    assume "odd n"
1.78 -    then have "even (Suc n)" by simp
1.79 +    assume "\<not> 2 dvd n"
1.80 +    then have "2 dvd (Suc n)" by simp
1.81      then obtain r where "Suc n = 2 * r" ..
1.82      moreover from * obtain s where "m * n = 2 * s" ..
1.83      then have "2 * s + m = m * Suc n" by simp
1.84      ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
1.85      then have "m = 2 * (m * r - s)" by simp
1.86 -    then show "even m" ..
1.87 +    then show "2 dvd m" ..
1.88    qed
1.89  next
1.90    fix n :: nat
1.91 -  assume "odd n"
1.92 +  assume "\<not> 2 dvd n"
1.93    then show "\<exists>m. n = m + 1"
1.94      by (cases n) simp_all
1.95  qed
1.96 @@ -194,23 +179,38 @@
1.97  lemma odd_pos:
1.98    "odd (n :: nat) \<Longrightarrow> 0 < n"
1.99    by (auto elim: oddE)
1.100 -
1.101 +
1.102 +lemma even_diff_iff [simp]:
1.103 +  fixes k l :: int
1.104 +  shows "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
1.105 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.106 +
1.108 +  fixes k l :: int
1.109 +  shows "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
1.110 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
1.111 +
1.113 +  fixes k l :: int
1.114 +  shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
1.116 +
1.117  instance int :: ring_parity
1.118  proof
1.119 -  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
1.120 +  show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
1.121    fix k l :: int
1.122 -  assume "odd k"
1.123 -  moreover assume "odd l"
1.124 -  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
1.125 +  assume "\<not> 2 dvd k"
1.126 +  moreover assume "\<not> 2 dvd l"
1.127 +  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
1.129 -  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
1.130 +  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
1.132 -  then show "even (k + l)"
1.133 +  then show "2 dvd (k + l)"
1.134      by simp
1.135  next
1.136    fix k l :: int
1.137 -  assume "even (k * l)"
1.138 -  then show "even k \<or> even l"
1.139 +  assume "2 dvd (k * l)"
1.140 +  then show "2 dvd k \<or> 2 dvd l"
1.141      by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
1.142  next
1.143    fix k :: int
1.144 @@ -352,4 +352,3 @@
1.145  ]
1.146
1.147  end
1.148 -
```