author  haftmann 
Fri, 07 Dec 2007 15:07:59 +0100  
changeset 25571  c9e39eafc7a0 
parent 25502  9200b36280c0 
child 25594  43c718438f9f 
permissions  rwrr 
21263  1 
(* Title: HOL/Library/Parity.thy 
21256  2 
ID: $Id$ 
3 
Author: Jeremy Avigad 

4 
*) 

5 

6 
header {* Even and Odd for int and nat *} 

7 

8 
theory Parity 

9 
imports Main 

10 
begin 

11 

22473  12 
class even_odd = type + 
22390  13 
fixes even :: "'a \<Rightarrow> bool" 
21256  14 

15 
abbreviation 

22390  16 
odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where 
17 
"odd x \<equiv> \<not> even x" 

18 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

19 
instantiation int and nat :: even_odd 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

20 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

21 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

22 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

23 
even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0" 
22390  24 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

25 
definition 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

26 
even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

27 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

28 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

29 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25502
diff
changeset

30 
end 
21256  31 

32 

33 
subsection {* Even and odd are mutually exclusive *} 

34 

21263  35 
lemma int_pos_lt_two_imp_zero_or_one: 
21256  36 
"0 <= x ==> (x::int) < 2 ==> x = 0  x = 1" 
23522  37 
by presburger 
21256  38 

23522  39 
lemma neq_one_mod_two [simp, presburger]: 
40 
"((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger 

21256  41 

42 
subsection {* Behavior under integer arithmetic operations *} 

43 

44 
lemma even_times_anything: "even (x::int) ==> even (x * y)" 

45 
by (simp add: even_def zmod_zmult1_eq') 

46 

47 
lemma anything_times_even: "even (y::int) ==> even (x * y)" 

48 
by (simp add: even_def zmod_zmult1_eq) 

49 

50 
lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)" 

51 
by (simp add: even_def zmod_zmult1_eq) 

52 

23522  53 
lemma even_product[presburger]: "even((x::int) * y) = (even x  even y)" 
21263  54 
apply (auto simp add: even_times_anything anything_times_even) 
21256  55 
apply (rule ccontr) 
56 
apply (auto simp add: odd_times_odd) 

57 
done 

58 

59 
lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)" 

23522  60 
by presburger 
21256  61 

62 
lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)" 

23522  63 
by presburger 
21256  64 

65 
lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)" 

23522  66 
by presburger 
21256  67 

23522  68 
lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)" by presburger 
21256  69 

23522  70 
lemma even_sum[presburger]: "even ((x::int) + y) = ((even x & even y)  (odd x & odd y))" 
71 
by presburger 

21256  72 

23522  73 
lemma even_neg[presburger]: "even ((x::int)) = even x" by presburger 
21256  74 

21263  75 
lemma even_difference: 
23522  76 
"even ((x::int)  y) = ((even x & even y)  (odd x & odd y))" by presburger 
21256  77 

21263  78 
lemma even_pow_gt_zero: 
79 
"even (x::int) ==> 0 < n ==> even (x^n)" 

80 
by (induct n) (auto simp add: even_product) 

21256  81 

23522  82 
lemma odd_pow_iff[presburger]: "odd ((x::int) ^ n) \<longleftrightarrow> (n = 0 \<or> odd x)" 
83 
apply (induct n, simp_all) 

84 
apply presburger 

85 
apply (case_tac n, auto) 

86 
apply (simp_all add: even_product) 

21256  87 
done 
88 

23522  89 
lemma odd_pow: "odd x ==> odd((x::int)^n)" by (simp add: odd_pow_iff) 
90 

91 
lemma even_power[presburger]: "even ((x::int)^n) = (even x & 0 < n)" 

21263  92 
apply (auto simp add: even_pow_gt_zero) 
21256  93 
apply (erule contrapos_pp, erule odd_pow) 
94 
apply (erule contrapos_pp, simp add: even_def) 

95 
done 

96 

23522  97 
lemma even_zero[presburger]: "even (0::int)" by presburger 
21256  98 

23522  99 
lemma odd_one[presburger]: "odd (1::int)" by presburger 
21256  100 

21263  101 
lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero 
21256  102 
odd_one even_product even_sum even_neg even_difference even_power 
103 

104 

105 
subsection {* Equivalent definitions *} 

106 

23522  107 
lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x" 
108 
by presburger 

21256  109 

21263  110 
lemma two_times_odd_div_two_plus_one: "odd (x::int) ==> 
23522  111 
2 * (x div 2) + 1 = x" by presburger 
21256  112 

23522  113 
lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" by presburger 
21256  114 

23522  115 
lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" by presburger 
21256  116 

117 
subsection {* even and odd for nats *} 

118 

119 
lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)" 

120 
by (simp add: even_nat_def) 

121 

23522  122 
lemma even_nat_product[presburger]: "even((x::nat) * y) = (even x  even y)" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23309
diff
changeset

123 
by (simp add: even_nat_def int_mult) 
21256  124 

23522  125 
lemma even_nat_sum[presburger]: "even ((x::nat) + y) = 
126 
((even x & even y)  (odd x & odd y))" by presburger 

21256  127 

23522  128 
lemma even_nat_difference[presburger]: 
21256  129 
"even ((x::nat)  y) = (x < y  (even x & even y)  (odd x & odd y))" 
23522  130 
by presburger 
21256  131 

23522  132 
lemma even_nat_Suc[presburger]: "even (Suc x) = odd x" by presburger 
21256  133 

23522  134 
lemma even_nat_power[presburger]: "even ((x::nat)^y) = (even x & 0 < y)" 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23309
diff
changeset

135 
by (simp add: even_nat_def int_power) 
21256  136 

23522  137 
lemma even_nat_zero[presburger]: "even (0::nat)" by presburger 
21256  138 

21263  139 
lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard] 
21256  140 
even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power 
141 

142 

143 
subsection {* Equivalent definitions *} 

144 

21263  145 
lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==> 
23522  146 
x = 0  x = Suc 0" by presburger 
21256  147 

148 
lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" 

23522  149 
by presburger 
21256  150 

151 
lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0" 

23522  152 
by presburger 
21256  153 

21263  154 
lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)" 
23522  155 
by presburger 
21256  156 

157 
lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)" 

23522  158 
by presburger 
21256  159 

21263  160 
lemma even_nat_div_two_times_two: "even (x::nat) ==> 
23522  161 
Suc (Suc 0) * (x div Suc (Suc 0)) = x" by presburger 
21256  162 

21263  163 
lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==> 
23522  164 
Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x" by presburger 
21256  165 

166 
lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)" 

23522  167 
by presburger 
21256  168 

169 
lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))" 

23522  170 
by presburger 
21256  171 

172 
subsection {* Parity and powers *} 

173 

21263  174 
lemma minus_one_even_odd_power: 
175 
"(even x > ( 1::'a::{comm_ring_1,recpower})^x = 1) & 

21256  176 
(odd x > ( 1::'a)^x =  1)" 
177 
apply (induct x) 

178 
apply (rule conjI) 

179 
apply simp 

180 
apply (insert even_nat_zero, blast) 

181 
apply (simp add: power_Suc) 

21263  182 
done 
21256  183 

184 
lemma minus_one_even_power [simp]: 

21263  185 
"even x ==> ( 1::'a::{comm_ring_1,recpower})^x = 1" 
186 
using minus_one_even_odd_power by blast 

21256  187 

188 
lemma minus_one_odd_power [simp]: 

21263  189 
"odd x ==> ( 1::'a::{comm_ring_1,recpower})^x =  1" 
190 
using minus_one_even_odd_power by blast 

21256  191 

192 
lemma neg_one_even_odd_power: 

21263  193 
"(even x > (1::'a::{number_ring,recpower})^x = 1) & 
21256  194 
(odd x > (1::'a)^x = 1)" 
195 
apply (induct x) 

196 
apply (simp, simp add: power_Suc) 

197 
done 

198 

199 
lemma neg_one_even_power [simp]: 

21263  200 
"even x ==> (1::'a::{number_ring,recpower})^x = 1" 
201 
using neg_one_even_odd_power by blast 

21256  202 

203 
lemma neg_one_odd_power [simp]: 

21263  204 
"odd x ==> (1::'a::{number_ring,recpower})^x = 1" 
205 
using neg_one_even_odd_power by blast 

21256  206 

207 
lemma neg_power_if: 

21263  208 
"(x::'a::{comm_ring_1,recpower}) ^ n = 
21256  209 
(if even n then (x ^ n) else (x ^ n))" 
21263  210 
apply (induct n) 
211 
apply (simp_all split: split_if_asm add: power_Suc) 

212 
done 

21256  213 

21263  214 
lemma zero_le_even_power: "even n ==> 
21256  215 
0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" 
216 
apply (simp add: even_nat_equiv_def2) 

217 
apply (erule exE) 

218 
apply (erule ssubst) 

219 
apply (subst power_add) 

220 
apply (rule zero_le_square) 

221 
done 

222 

21263  223 
lemma zero_le_odd_power: "odd n ==> 
21256  224 
(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" 
225 
apply (simp add: odd_nat_equiv_def2) 

226 
apply (erule exE) 

227 
apply (erule ssubst) 

228 
apply (subst power_Suc) 

229 
apply (subst power_add) 

230 
apply (subst zero_le_mult_iff) 

231 
apply auto 

25162  232 
apply (subgoal_tac "x = 0 & y > 0") 
21256  233 
apply (erule conjE, assumption) 
21263  234 
apply (subst power_eq_0_iff [symmetric]) 
21256  235 
apply (subgoal_tac "0 <= x^y * x^y") 
236 
apply simp 

237 
apply (rule zero_le_square)+ 

21263  238 
done 
21256  239 

23522  240 
lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = 
21256  241 
(even n  (odd n & 0 <= x))" 
242 
apply auto 

21263  243 
apply (subst zero_le_odd_power [symmetric]) 
21256  244 
apply assumption+ 
245 
apply (erule zero_le_even_power) 

21263  246 
apply (subst zero_le_odd_power) 
21256  247 
apply assumption+ 
21263  248 
done 
21256  249 

23522  250 
lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = 
21256  251 
(n = 0  (even n & x ~= 0)  (odd n & 0 < x))" 
252 
apply (rule iffI) 

253 
apply clarsimp 

254 
apply (rule conjI) 

255 
apply clarsimp 

256 
apply (rule ccontr) 

257 
apply (subgoal_tac "~ (0 <= x^n)") 

258 
apply simp 

259 
apply (subst zero_le_odd_power) 

21263  260 
apply assumption 
21256  261 
apply simp 
262 
apply (rule notI) 

263 
apply (simp add: power_0_left) 

264 
apply (rule notI) 

265 
apply (simp add: power_0_left) 

266 
apply auto 

267 
apply (subgoal_tac "0 <= x^n") 

268 
apply (frule order_le_imp_less_or_eq) 

269 
apply simp 

270 
apply (erule zero_le_even_power) 

271 
apply (subgoal_tac "0 <= x^n") 

272 
apply (frule order_le_imp_less_or_eq) 

273 
apply auto 

274 
apply (subst zero_le_odd_power) 

275 
apply assumption 

276 
apply (erule order_less_imp_le) 

21263  277 
done 
21256  278 

23522  279 
lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = 
280 
(odd n & x < 0)" 

21263  281 
apply (subst linorder_not_le [symmetric])+ 
21256  282 
apply (subst zero_le_power_eq) 
283 
apply auto 

21263  284 
done 
21256  285 

23522  286 
lemma power_le_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = 
21256  287 
(n ~= 0 & ((odd n & x <= 0)  (even n & x = 0)))" 
21263  288 
apply (subst linorder_not_less [symmetric])+ 
21256  289 
apply (subst zero_less_power_eq) 
290 
apply auto 

21263  291 
done 
21256  292 

21263  293 
lemma power_even_abs: "even n ==> 
21256  294 
(abs (x::'a::{recpower,ordered_idom}))^n = x^n" 
21263  295 
apply (subst power_abs [symmetric]) 
21256  296 
apply (simp add: zero_le_even_power) 
21263  297 
done 
21256  298 

23522  299 
lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0  0 < x)" 
21263  300 
by (induct n) auto 
21256  301 

21263  302 
lemma power_minus_even [simp]: "even n ==> 
21256  303 
( x)^n = (x^n::'a::{recpower,comm_ring_1})" 
304 
apply (subst power_minus) 

305 
apply simp 

21263  306 
done 
21256  307 

21263  308 
lemma power_minus_odd [simp]: "odd n ==> 
21256  309 
( x)^n =  (x^n::'a::{recpower,comm_ring_1})" 
310 
apply (subst power_minus) 

311 
apply simp 

21263  312 
done 
21256  313 

21263  314 

315 
text {* Simplify, when the exponent is a numeral *} 

21256  316 

317 
lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] 

318 
declare power_0_left_number_of [simp] 

319 

21263  320 
lemmas zero_le_power_eq_number_of [simp] = 
21256  321 
zero_le_power_eq [of _ "number_of w", standard] 
322 

21263  323 
lemmas zero_less_power_eq_number_of [simp] = 
21256  324 
zero_less_power_eq [of _ "number_of w", standard] 
325 

21263  326 
lemmas power_le_zero_eq_number_of [simp] = 
21256  327 
power_le_zero_eq [of _ "number_of w", standard] 
328 

21263  329 
lemmas power_less_zero_eq_number_of [simp] = 
21256  330 
power_less_zero_eq [of _ "number_of w", standard] 
331 

21263  332 
lemmas zero_less_power_nat_eq_number_of [simp] = 
21256  333 
zero_less_power_nat_eq [of _ "number_of w", standard] 
334 

21263  335 
lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard] 
21256  336 

21263  337 
lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard] 
21256  338 

339 

340 
subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} 

341 

342 
lemma even_power_le_0_imp_0: 

21263  343 
"a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0" 
344 
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) 

21256  345 

23522  346 
lemma zero_le_power_iff[presburger]: 
21263  347 
"(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower})  even n)" 
21256  348 
proof cases 
349 
assume even: "even n" 

350 
then obtain k where "n = 2*k" 

351 
by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) 

21263  352 
thus ?thesis by (simp add: zero_le_even_power even) 
21256  353 
next 
354 
assume odd: "odd n" 

355 
then obtain k where "n = Suc(2*k)" 

356 
by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) 

357 
thus ?thesis 

21263  358 
by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power 
359 
dest!: even_power_le_0_imp_0) 

360 
qed 

361 

21256  362 

363 
subsection {* Miscellaneous *} 

364 

23522  365 
lemma [presburger]:"(x + 1) div 2 = x div 2 \<longleftrightarrow> even (x::int)" by presburger 
366 
lemma [presburger]: "(x + 1) div 2 = x div 2 + 1 \<longleftrightarrow> odd (x::int)" by presburger 

367 
lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2" by presburger 

368 
lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger 

21256  369 

21263  370 
lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + 
23522  371 
(a mod c + Suc 0 mod c) div c" 
21256  372 
apply (subgoal_tac "Suc a = a + Suc 0") 
373 
apply (erule ssubst) 

374 
apply (rule div_add1_eq, simp) 

375 
done 

376 

23522  377 
lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger 
378 
lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger 

21263  379 
lemma even_nat_plus_one_div_two: "even (x::nat) ==> 
23522  380 
(Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger 
21256  381 

21263  382 
lemma odd_nat_plus_one_div_two: "odd (x::nat) ==> 
23522  383 
(Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger 
21256  384 

385 
end 