more algebraic deductions for facts on even/odd
authorhaftmann
Tue Oct 14 08:23:23 2014 +0200 (2014-10-14)
changeset 586806b2fa479945f
parent 58679 33c90658448a
child 58681 a478a0742a8e
more algebraic deductions for facts on even/odd
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -41,12 +41,26 @@
     1.4    assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
     1.5    assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
     1.6    assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
     1.7 +  assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
     1.8  begin
     1.9  
    1.10  lemma two_dvd_plus_one_iff [simp]:
    1.11    "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
    1.12    by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
    1.13  
    1.14 +lemma not_two_dvdE [elim?]:
    1.15 +  assumes "\<not> 2 dvd a"
    1.16 +  obtains b where "a = 2 * b + 1"
    1.17 +proof -
    1.18 +  from assms obtain b where *: "a = b + 1"
    1.19 +    by (blast dest: not_dvd_ex_decrement)
    1.20 +  with assms have "2 dvd b + 2" by simp
    1.21 +  then have "2 dvd b" by simp
    1.22 +  then obtain c where "b = 2 * c" ..
    1.23 +  with * have "a = 2 * c + 1" by simp
    1.24 +  with that show thesis .
    1.25 +qed
    1.26 +
    1.27  end
    1.28  
    1.29  instance nat :: semiring_parity
    1.30 @@ -79,6 +93,11 @@
    1.31      then have "m = 2 * (m * r - s)" by simp
    1.32      then show "2 dvd m" ..
    1.33    qed
    1.34 +next
    1.35 +  fix n :: nat
    1.36 +  assume "\<not> 2 dvd n"
    1.37 +  then show "\<exists>m. n = m + 1"
    1.38 +    by (cases n) simp_all
    1.39  qed
    1.40  
    1.41  class ring_parity = comm_ring_1 + semiring_parity
    1.42 @@ -95,7 +114,16 @@
    1.43      by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
    1.44    then show "2 dvd k + l"
    1.45      by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
    1.46 -qed (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
    1.47 +next
    1.48 +  fix k l :: int
    1.49 +  assume "2 dvd k * l"
    1.50 +  then show "2 dvd k \<or> 2 dvd l"
    1.51 +    by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
    1.52 +next
    1.53 +  fix k :: int
    1.54 +  have "k = (k - 1) + 1" by simp
    1.55 +  then show "\<exists>l. k = l + 1" ..
    1.56 +qed
    1.57  
    1.58  context semiring_div_parity
    1.59  begin
    1.60 @@ -130,6 +158,11 @@
    1.61      by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
    1.62    then show "a mod 2 = 0 \<or> b mod 2 = 0"
    1.63      by (rule divisors_zero)
    1.64 +next
    1.65 +  fix a
    1.66 +  assume "a mod 2 = 1"
    1.67 +  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
    1.68 +  then show "\<exists>b. a = b + 1" ..
    1.69  qed
    1.70  
    1.71  end
    1.72 @@ -137,6 +170,8 @@
    1.73  
    1.74  subsection {* Dedicated @{text even}/@{text odd} predicate *}
    1.75  
    1.76 +subsubsection {* Properties *}
    1.77 +
    1.78  context semiring_parity
    1.79  begin
    1.80  
    1.81 @@ -148,6 +183,14 @@
    1.82  where
    1.83    "odd a \<equiv> \<not> even a"
    1.84  
    1.85 +lemma odd_dvdE [elim?]:
    1.86 +  assumes "odd a"
    1.87 +  obtains b where "a = 2 * b + 1"
    1.88 +proof -
    1.89 +  from assms have "\<not> 2 dvd a" by (simp add: even_def)
    1.90 +  then show thesis using that by (rule not_two_dvdE)
    1.91 +qed
    1.92 +  
    1.93  lemma even_times_iff [simp, presburger, algebra]:
    1.94    "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.95    by (auto simp add: even_def dest: two_is_prime)
    1.96 @@ -187,6 +230,18 @@
    1.97    then show False by simp
    1.98  qed
    1.99  
   1.100 +lemma even_add [simp]:
   1.101 +  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
   1.102 +  by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
   1.103 +
   1.104 +lemma odd_add [simp]:
   1.105 +  "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
   1.106 +  by simp
   1.107 +
   1.108 +lemma even_power [simp, presburger]:
   1.109 +  "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
   1.110 +  by (induct n) auto
   1.111 +
   1.112  end
   1.113  
   1.114  context ring_parity
   1.115 @@ -196,6 +251,10 @@
   1.116    "even (- a) \<longleftrightarrow> even a"
   1.117    by (simp add: even_def)
   1.118  
   1.119 +lemma even_diff [simp]:
   1.120 +  "even (a - b) \<longleftrightarrow> even (a + b)"
   1.121 +  using even_add [of a "- b"] by simp
   1.122 +
   1.123  end
   1.124  
   1.125  context semiring_div_parity
   1.126 @@ -207,6 +266,9 @@
   1.127  
   1.128  end
   1.129  
   1.130 +
   1.131 +subsubsection {* Particularities for @{typ nat}/@{typ int} *}
   1.132 +
   1.133  lemma even_int_iff:
   1.134    "even (int n) \<longleftrightarrow> even n"
   1.135    by (simp add: even_def dvd_int_iff)
   1.136 @@ -215,72 +277,71 @@
   1.137    even_int_iff
   1.138  ]
   1.139  
   1.140 +
   1.141 +subsubsection {* Tools setup *}
   1.142 +
   1.143  lemma [presburger]:
   1.144    "even n \<longleftrightarrow> even (int n)"
   1.145    using even_int_iff [of n] by simp
   1.146 -  
   1.147  
   1.148 -subsection {* Behavior under integer arithmetic operations *}
   1.149 -
   1.150 -lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
   1.151 -by presburger
   1.152 -
   1.153 -lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
   1.154 -by presburger
   1.155 -
   1.156 -lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
   1.157 -by presburger
   1.158 -
   1.159 -lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" by presburger
   1.160 -
   1.161 -lemma even_sum[simp,presburger]:
   1.162 -  "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
   1.163 -by presburger
   1.164 -
   1.165 -lemma even_difference[simp]:
   1.166 -    "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger
   1.167 -
   1.168 -lemma even_power[simp,presburger]: "even ((x::int)^n) = (even x & n \<noteq> 0)"
   1.169 -by (induct n) auto
   1.170 -
   1.171 -lemma odd_pow: "odd x ==> odd((x::int)^n)" by simp
   1.172 +lemma [presburger]:
   1.173 +  "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
   1.174 +  by auto
   1.175  
   1.176  
   1.177 -subsection {* Equivalent definitions *}
   1.178 +subsubsection {* Legacy cruft *}
   1.179 +
   1.180 +lemma even_plus_even:
   1.181 +  "even (x::int) ==> even y ==> even (x + y)"
   1.182 +  by simp
   1.183 +
   1.184 +lemma odd_plus_odd:
   1.185 +  "odd (x::int) ==> odd y ==> even (x + y)"
   1.186 +  by simp
   1.187 +
   1.188 +lemma even_sum_nat:
   1.189 +  "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
   1.190 +  by auto
   1.191  
   1.192 -lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
   1.193 -by presburger
   1.194 +lemma odd_pow:
   1.195 +  "odd x ==> odd((x::int)^n)"
   1.196 +  by simp
   1.197 +
   1.198 +lemma even_equiv_def:
   1.199 +  "even (x::int) = (EX y. x = 2 * y)"
   1.200 +  by presburger
   1.201 +
   1.202 +
   1.203 +subsubsection {* Equivalent definitions *}
   1.204 +
   1.205 +lemma two_times_even_div_two:
   1.206 +  "even (x::int) ==> 2 * (x div 2) = x" 
   1.207 +  by presburger
   1.208  
   1.209  lemma two_times_odd_div_two_plus_one:
   1.210    "odd (x::int) ==> 2 * (x div 2) + 1 = x"
   1.211 -by presburger
   1.212 +  by presburger
   1.213    
   1.214 -lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" by presburger
   1.215  
   1.216 -lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" by presburger
   1.217 -
   1.218 -subsection {* even and odd for nats *}
   1.219 +subsubsection {* even and odd for nats *}
   1.220  
   1.221  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
   1.222  by (simp add: even_int_iff [symmetric])
   1.223  
   1.224 -lemma even_sum_nat[simp,presburger,algebra]:
   1.225 -  "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
   1.226 -by presburger
   1.227 +lemma even_difference_nat [simp,presburger,algebra]:
   1.228 +  "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
   1.229 +  by presburger
   1.230  
   1.231 -lemma even_difference_nat[simp,presburger,algebra]:
   1.232 -  "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
   1.233 -by presburger
   1.234 -
   1.235 -lemma even_Suc[simp,presburger,algebra]: "even (Suc x) = odd x"
   1.236 -by presburger
   1.237 +lemma even_Suc [simp ,presburger, algebra]:
   1.238 +  "even (Suc x) = odd x"
   1.239 +  by presburger
   1.240  
   1.241  lemma even_power_nat[simp,presburger,algebra]:
   1.242    "even ((x::nat)^y) = (even x & 0 < y)"
   1.243 -by (simp add: even_int_iff [symmetric] int_power)
   1.244 +  by simp
   1.245  
   1.246  
   1.247 -subsection {* Equivalent definitions *}
   1.248 +subsubsection {* Equivalent definitions *}
   1.249  
   1.250  lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
   1.251  by presburger
   1.252 @@ -300,14 +361,11 @@
   1.253  lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>
   1.254      Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger
   1.255  
   1.256 -lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
   1.257 -by presburger
   1.258 -
   1.259  lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
   1.260 -by presburger
   1.261 +  by presburger
   1.262  
   1.263  
   1.264 -subsection {* Parity and powers *}
   1.265 +subsubsection {* Parity and powers *}
   1.266  
   1.267  lemma (in comm_ring_1) neg_power_if:
   1.268    "(- a) ^ n = (if even n then (a ^ n) else - (a ^ n))"
   1.269 @@ -320,10 +378,11 @@
   1.270  
   1.271  lemma zero_le_even_power: "even n ==>
   1.272      0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
   1.273 -  apply (simp add: even_nat_equiv_def2)
   1.274 -  apply (erule exE)
   1.275 +  apply (simp add: even_def)
   1.276 +  apply (erule dvdE)
   1.277    apply (erule ssubst)
   1.278 -  apply (subst power_add)
   1.279 +  unfolding mult.commute [of 2]
   1.280 +  unfolding power_mult power2_eq_square
   1.281    apply (rule zero_le_square)
   1.282    done
   1.283  
   1.284 @@ -343,7 +402,6 @@
   1.285  
   1.286  lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) =
   1.287      (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
   1.288 -
   1.289    unfolding order_less_le zero_le_power_eq by auto
   1.290  
   1.291  lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) =
   1.292 @@ -414,13 +472,10 @@
   1.293  qed
   1.294  
   1.295  
   1.296 -subsection {* More Even/Odd Results *}
   1.297 +subsubsection {* More Even/Odd Results *}
   1.298   
   1.299  lemma even_mult_two_ex: "even(n) = (\<exists>m::nat. n = 2*m)" by presburger
   1.300  lemma odd_Suc_mult_two_ex: "odd(n) = (\<exists>m. n = Suc (2*m))" by presburger
   1.301 -lemma even_add [simp]: "even(m + n::nat) = (even m = even n)"  by presburger
   1.302 -
   1.303 -lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
   1.304  
   1.305  lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
   1.306  
   1.307 @@ -459,14 +514,14 @@
   1.308    power_even_abs [of "numeral w" _] for w
   1.309  
   1.310  
   1.311 -subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
   1.312 +subsubsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
   1.313  
   1.314  lemma zero_le_power_iff[presburger]:
   1.315    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
   1.316  proof cases
   1.317    assume even: "even n"
   1.318 -  then obtain k where "n = 2*k"
   1.319 -    by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2)
   1.320 +  then have "2 dvd n" by (simp add: even_def)
   1.321 +  then obtain k where "n = 2 * k" ..
   1.322    thus ?thesis by (simp add: zero_le_even_power even)
   1.323  next
   1.324    assume odd: "odd n"
   1.325 @@ -479,7 +534,7 @@
   1.326  qed
   1.327  
   1.328  
   1.329 -subsection {* Miscellaneous *}
   1.330 +subsubsection {* Miscellaneous *}
   1.331  
   1.332  lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger
   1.333  lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger