src/HOL/Parity.thy
 changeset 58678 398e05aa84d4 parent 58645 94bef115c08f child 58679 33c90658448a
```     1.1 --- a/src/HOL/Parity.thy	Tue Oct 14 16:19:42 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
1.3 @@ -9,50 +9,211 @@
1.4  imports Main
1.5  begin
1.6
1.7 -class even_odd = semiring_div_parity
1.8 +subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
1.9 +
1.10 +lemma two_dvd_Suc_Suc_iff [simp]:
1.11 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
1.12 +  using dvd_add_triv_right_iff [of 2 n] by simp
1.13 +
1.14 +lemma two_dvd_Suc_iff:
1.15 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
1.16 +  by (induct n) auto
1.17 +
1.18 +lemma two_dvd_diff_iff:
1.19 +  fixes k l :: int
1.20 +  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
1.21 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
1.22 +
1.24 +  fixes k l :: int
1.25 +  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
1.26 +  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
1.27 +
1.29 +  fixes k l :: int
1.30 +  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
1.32 +
1.33 +
1.34 +subsection {* Ring structures with parity *}
1.35 +
1.36 +class semiring_parity = semiring_dvd + semiring_numeral +
1.37 +  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
1.38 +  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
1.39 +  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
1.40 +begin
1.41 +
1.42 +lemma two_dvd_plus_one_iff [simp]:
1.43 +  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
1.45 +
1.46 +end
1.47 +
1.48 +instance nat :: semiring_parity
1.49 +proof
1.50 +  show "\<not> (2 :: nat) dvd 1"
1.51 +    by (rule notI, erule dvdE) simp
1.52 +next
1.53 +  fix m n :: nat
1.54 +  assume "\<not> 2 dvd m"
1.55 +  moreover assume "\<not> 2 dvd n"
1.56 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
1.57 +    by (simp add: two_dvd_Suc_iff)
1.58 +  then have "2 dvd Suc m + Suc n"
1.59 +    by (blast intro: dvd_add)
1.60 +  also have "Suc m + Suc n = m + n + 2"
1.61 +    by simp
1.62 +  finally show "2 dvd m + n"
1.63 +    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
1.64 +next
1.65 +  fix m n :: nat
1.66 +  assume *: "2 dvd m * n"
1.67 +  show "2 dvd m \<or> 2 dvd n"
1.68 +  proof (rule disjCI)
1.69 +    assume "\<not> 2 dvd n"
1.70 +    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
1.71 +    then obtain r where "Suc n = 2 * r" ..
1.72 +    moreover from * obtain s where "m * n = 2 * s" ..
1.73 +    then have "2 * s + m = m * Suc n" by simp
1.74 +    ultimately have " 2 * s + m = 2 * (m * r)" by simp
1.75 +    then have "m = 2 * (m * r - s)" by simp
1.76 +    then show "2 dvd m" ..
1.77 +  qed
1.78 +qed
1.79 +
1.80 +class ring_parity = comm_ring_1 + semiring_parity
1.81 +
1.82 +instance int :: ring_parity
1.83 +proof
1.84 +  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
1.85 +  fix k l :: int
1.86 +  assume "\<not> 2 dvd k"
1.87 +  moreover assume "\<not> 2 dvd l"
1.88 +  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>"
1.90 +  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
1.92 +  then show "2 dvd k + l"
1.94 +qed (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
1.95 +
1.96 +context semiring_div_parity
1.97 +begin
1.98 +
1.99 +subclass semiring_parity
1.100 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
1.101 +  fix a b c
1.102 +  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
1.103 +    by simp
1.104 +next
1.105 +  fix a b c
1.106 +  assume "(b + c) mod a = 0"
1.107 +  with mod_add_eq [of b c a]
1.108 +  have "(b mod a + c mod a) mod a = 0"
1.109 +    by simp
1.110 +  moreover assume "b mod a = 0"
1.111 +  ultimately show "c mod a = 0"
1.112 +    by simp
1.113 +next
1.114 +  show "1 mod 2 = 1"
1.115 +    by (fact one_mod_two_eq_one)
1.116 +next
1.117 +  fix a b
1.118 +  assume "a mod 2 = 1"
1.119 +  moreover assume "b mod 2 = 1"
1.120 +  ultimately show "(a + b) mod 2 = 0"
1.121 +    using mod_add_eq [of a b 2] by simp
1.122 +next
1.123 +  fix a b
1.124 +  assume "(a * b) mod 2 = 0"
1.125 +  then have "(a mod 2) * (b mod 2) = 0"
1.126 +    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
1.127 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
1.128 +    by (rule divisors_zero)
1.129 +qed
1.130 +
1.131 +end
1.132 +
1.133 +
1.134 +subsection {* Dedicated @{text even}/@{text odd} predicate *}
1.135 +
1.136 +context semiring_parity
1.137  begin
1.138
1.139  definition even :: "'a \<Rightarrow> bool"
1.140  where
1.141    [algebra]: "even a \<longleftrightarrow> 2 dvd a"
1.142
1.143 -lemmas even_iff_2_dvd = even_def
1.144 +abbreviation odd :: "'a \<Rightarrow> bool"
1.145 +where
1.146 +  "odd a \<equiv> \<not> even a"
1.147 +
1.148 +lemma even_times_iff [simp, presburger, algebra]:
1.149 +  "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.150 +  by (auto simp add: even_def dest: two_is_prime)
1.151 +
1.152 +lemma even_zero [simp]:
1.153 +  "even 0"
1.154 +  by (simp add: even_def)
1.155 +
1.156 +lemma odd_one [simp]:
1.157 +  "odd 1"
1.158 +  by (simp add: even_def)
1.159 +
1.160 +lemma even_numeral [simp]:
1.161 +  "even (numeral (Num.Bit0 n))"
1.162 +proof -
1.163 +  have "even (2 * numeral n)"
1.164 +    unfolding even_times_iff by (simp add: even_def)
1.165 +  then have "even (numeral n + numeral n)"
1.166 +    unfolding mult_2 .
1.167 +  then show ?thesis
1.168 +    unfolding numeral.simps .
1.169 +qed
1.170 +
1.171 +lemma odd_numeral [simp]:
1.172 +  "odd (numeral (Num.Bit1 n))"
1.173 +proof
1.174 +  assume "even (numeral (num.Bit1 n))"
1.175 +  then have "even (numeral n + numeral n + 1)"
1.176 +    unfolding numeral.simps .
1.177 +  then have "even (2 * numeral n + 1)"
1.178 +    unfolding mult_2 .
1.179 +  then have "2 dvd numeral n * 2 + 1"
1.180 +    unfolding even_def by (simp add: ac_simps)
1.181 +  with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
1.182 +    have "2 dvd 1"
1.183 +    by simp
1.184 +  then show False by simp
1.185 +qed
1.186 +
1.187 +end
1.188 +
1.189 +context semiring_div_parity
1.190 +begin
1.191
1.192  lemma even_iff_mod_2_eq_zero [presburger]:
1.193    "even a \<longleftrightarrow> a mod 2 = 0"
1.194    by (simp add: even_def dvd_eq_mod_eq_0)
1.195
1.196 -lemma even_zero [simp]:
1.197 -  "even 0"
1.198 -  by (simp add: even_iff_mod_2_eq_zero)
1.199 -
1.200  lemma even_times_anything:
1.201    "even a \<Longrightarrow> even (a * b)"
1.202 -  by (simp add: even_iff_2_dvd)
1.203 +  by (simp add: even_def)
1.204
1.205  lemma anything_times_even:
1.206    "even a \<Longrightarrow> even (b * a)"
1.207 -  by (simp add: even_iff_2_dvd)
1.208 -
1.209 -abbreviation odd :: "'a \<Rightarrow> bool"
1.210 -where
1.211 -  "odd a \<equiv> \<not> even a"
1.212 +  by (simp add: even_def)
1.213
1.214  lemma odd_times_odd:
1.215    "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
1.216    by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
1.217
1.218 -lemma even_product [simp, presburger]:
1.219 +lemma even_product:
1.220    "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.221 -  apply (auto simp add: even_times_anything anything_times_even)
1.222 -  apply (rule ccontr)
1.223 -  apply (auto simp add: odd_times_odd)
1.224 -  done
1.225 +  by (fact even_times_iff)
1.226
1.227  end
1.228
1.229 -instance nat and int  :: even_odd ..
1.230 -
1.231  lemma even_nat_def [presburger]:
1.232    "even x \<longleftrightarrow> even (int x)"
1.233    by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
1.234 @@ -65,31 +226,8 @@
1.235    transfer_int_nat_relations
1.236  ]
1.237
1.238 -lemma odd_one_int [simp]:
1.239 -  "odd (1::int)"
1.240 -  by presburger
1.241 -
1.242 -lemma odd_1_nat [simp]:
1.243 -  "odd (1::nat)"
1.244 -  by presburger
1.245 -
1.246 -lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
1.247 -  unfolding even_iff_mod_2_eq_zero by simp
1.248 -
1.249 -lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
1.250 -  unfolding even_iff_mod_2_eq_zero by simp
1.251 -
1.252 -(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
1.253  declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
1.254
1.255 -lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
1.256 -  unfolding even_nat_def by simp
1.257 -
1.258 -lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
1.259 -  unfolding even_nat_def by simp
1.260 -
1.261 -subsection {* Even and odd are mutually exclusive *}
1.262 -
1.263
1.264  subsection {* Behavior under integer arithmetic operations *}
1.265
1.266 @@ -128,7 +266,7 @@
1.267  lemma two_times_odd_div_two_plus_one:
1.268    "odd (x::int) ==> 2 * (x div 2) + 1 = x"
1.269  by presburger
1.270 -
1.271 +
1.272  lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" by presburger
1.273
1.274  lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" by presburger
1.275 @@ -138,9 +276,9 @@
1.276  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"