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 

22390

12 
class even_odd =


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 


19 
instance int :: even_odd


20 
even_def: "even x \<equiv> x mod 2 = 0" ..


21 


22 
instance nat :: even_odd


23 
even_nat_def: "even x \<equiv> even (int x)" ..

21256

24 


25 


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


27 

21263

28 
lemma int_pos_lt_two_imp_zero_or_one:

21256

29 
"0 <= x ==> (x::int) < 2 ==> x = 0  x = 1"


30 
by auto


31 


32 
lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"

21263

33 
proof 


34 
have "x mod 2 = 0  x mod 2 = 1"


35 
by (rule int_pos_lt_two_imp_zero_or_one) auto


36 
then show ?thesis by force


37 
qed


38 

21256

39 


40 
subsection {* Behavior under integer arithmetic operations *}


41 


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


43 
by (simp add: even_def zmod_zmult1_eq')


44 


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


46 
by (simp add: even_def zmod_zmult1_eq)


47 


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


49 
by (simp add: even_def zmod_zmult1_eq)


50 


51 
lemma even_product: "even((x::int) * y) = (even x  even y)"

21263

52 
apply (auto simp add: even_times_anything anything_times_even)

21256

53 
apply (rule ccontr)


54 
apply (auto simp add: odd_times_odd)


55 
done


56 


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


58 
by (simp add: even_def zmod_zadd1_eq)


59 


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


61 
by (simp add: even_def zmod_zadd1_eq)


62 


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


64 
by (simp add: even_def zmod_zadd1_eq)


65 


66 
lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"


67 
by (simp add: even_def zmod_zadd1_eq)


68 


69 
lemma even_sum: "even ((x::int) + y) = ((even x & even y)  (odd x & odd y))"


70 
apply (auto intro: even_plus_even odd_plus_odd)


71 
apply (rule ccontr, simp add: even_plus_odd)


72 
apply (rule ccontr, simp add: odd_plus_even)


73 
done


74 


75 
lemma even_neg: "even ((x::int)) = even x"


76 
by (auto simp add: even_def zmod_zminus1_eq_if)


77 

21263

78 
lemma even_difference:


79 
"even ((x::int)  y) = ((even x & even y)  (odd x & odd y))"

21256

80 
by (simp only: diff_minus even_sum even_neg)


81 

21263

82 
lemma even_pow_gt_zero:


83 
"even (x::int) ==> 0 < n ==> even (x^n)"


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

21256

85 


86 
lemma odd_pow: "odd x ==> odd((x::int)^n)"


87 
apply (induct n)

21263

88 
apply (simp add: even_def)

21256

89 
apply (simp add: even_product)


90 
done


91 


92 
lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"

21263

93 
apply (auto simp add: even_pow_gt_zero)

21256

94 
apply (erule contrapos_pp, erule odd_pow)


95 
apply (erule contrapos_pp, simp add: even_def)


96 
done


97 


98 
lemma even_zero: "even (0::int)"


99 
by (simp add: even_def)


100 


101 
lemma odd_one: "odd (1::int)"


102 
by (simp add: even_def)


103 

21263

104 
lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero

21256

105 
odd_one even_product even_sum even_neg even_difference even_power


106 


107 


108 
subsection {* Equivalent definitions *}


109 

21263

110 
lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x"

21256

111 
by (auto simp add: even_def)


112 

21263

113 
lemma two_times_odd_div_two_plus_one: "odd (x::int) ==>

21256

114 
2 * (x div 2) + 1 = x"

21263

115 
apply (insert zmod_zdiv_equality [of x 2, symmetric])


116 
apply (simp add: even_def)


117 
done

21256

118 


119 
lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"


120 
apply auto


121 
apply (rule exI)

21263

122 
apply (erule two_times_even_div_two [symmetric])


123 
done

21256

124 


125 
lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"


126 
apply auto


127 
apply (rule exI)

21263

128 
apply (erule two_times_odd_div_two_plus_one [symmetric])


129 
done

21256

130 


131 


132 
subsection {* even and odd for nats *}


133 


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


135 
by (simp add: even_nat_def)


136 


137 
lemma even_nat_product: "even((x::nat) * y) = (even x  even y)"


138 
by (simp add: even_nat_def int_mult)


139 

21263

140 
lemma even_nat_sum: "even ((x::nat) + y) =

21256

141 
((even x & even y)  (odd x & odd y))"


142 
by (unfold even_nat_def, simp)


143 

21263

144 
lemma even_nat_difference:

21256

145 
"even ((x::nat)  y) = (x < y  (even x & even y)  (odd x & odd y))"

21263

146 
apply (auto simp add: even_nat_def zdiff_int [symmetric])


147 
apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])


148 
apply (case_tac "x < y", auto simp add: zdiff_int [symmetric])

21256

149 
done


150 


151 
lemma even_nat_Suc: "even (Suc x) = odd x"


152 
by (simp add: even_nat_def)


153 


154 
lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"


155 
by (simp add: even_nat_def int_power)


156 


157 
lemma even_nat_zero: "even (0::nat)"


158 
by (simp add: even_nat_def)


159 

21263

160 
lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard]

21256

161 
even_nat_zero even_nat_Suc even_nat_product even_nat_sum even_nat_power


162 


163 


164 
subsection {* Equivalent definitions *}


165 

21263

166 
lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==>

21256

167 
x = 0  x = Suc 0"


168 
by auto


169 


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

21263

171 
apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric])

21256

172 
apply (drule subst, assumption)


173 
apply (subgoal_tac "x mod Suc (Suc 0) = 0  x mod Suc (Suc 0) = Suc 0")


174 
apply force


175 
apply (subgoal_tac "0 < Suc (Suc 0)")


176 
apply (frule mod_less_divisor [of "Suc (Suc 0)" x])


177 
apply (erule nat_lt_two_imp_zero_or_one, auto)


178 
done


179 


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

21263

181 
apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric])

21256

182 
apply (drule subst, assumption)


183 
apply (subgoal_tac "x mod Suc (Suc 0) = 0  x mod Suc (Suc 0) = Suc 0")

21263

184 
apply force

21256

185 
apply (subgoal_tac "0 < Suc (Suc 0)")


186 
apply (frule mod_less_divisor [of "Suc (Suc 0)" x])


187 
apply (erule nat_lt_two_imp_zero_or_one, auto)


188 
done


189 

21263

190 
lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)"

21256

191 
apply (rule iffI)


192 
apply (erule even_nat_mod_two_eq_zero)


193 
apply (insert odd_nat_mod_two_eq_one [of x], auto)


194 
done


195 


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


197 
apply (auto simp add: even_nat_equiv_def)


198 
apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")


199 
apply (frule nat_lt_two_imp_zero_or_one, auto)


200 
done


201 

21263

202 
lemma even_nat_div_two_times_two: "even (x::nat) ==>

21256

203 
Suc (Suc 0) * (x div Suc (Suc 0)) = x"

21263

204 
apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric])

21256

205 
apply (drule even_nat_mod_two_eq_zero, simp)


206 
done


207 

21263

208 
lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>


209 
Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"


210 
apply (insert mod_div_equality [of x "Suc (Suc 0)", symmetric])

21256

211 
apply (drule odd_nat_mod_two_eq_one, simp)


212 
done


213 


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


215 
apply (rule iffI, rule exI)

21263

216 
apply (erule even_nat_div_two_times_two [symmetric], auto)

21256

217 
done


218 


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


220 
apply (rule iffI, rule exI)

21263

221 
apply (erule odd_nat_div_two_times_two_plus_one [symmetric], auto)

21256

222 
done


223 


224 
subsection {* Parity and powers *}


225 

21263

226 
lemma minus_one_even_odd_power:


227 
"(even x > ( 1::'a::{comm_ring_1,recpower})^x = 1) &

21256

228 
(odd x > ( 1::'a)^x =  1)"


229 
apply (induct x)


230 
apply (rule conjI)


231 
apply simp


232 
apply (insert even_nat_zero, blast)


233 
apply (simp add: power_Suc)

21263

234 
done

21256

235 


236 
lemma minus_one_even_power [simp]:

21263

237 
"even x ==> ( 1::'a::{comm_ring_1,recpower})^x = 1"


238 
using minus_one_even_odd_power by blast

21256

239 


240 
lemma minus_one_odd_power [simp]:

21263

241 
"odd x ==> ( 1::'a::{comm_ring_1,recpower})^x =  1"


242 
using minus_one_even_odd_power by blast

21256

243 


244 
lemma neg_one_even_odd_power:

21263

245 
"(even x > (1::'a::{number_ring,recpower})^x = 1) &

21256

246 
(odd x > (1::'a)^x = 1)"


247 
apply (induct x)


248 
apply (simp, simp add: power_Suc)


249 
done


250 


251 
lemma neg_one_even_power [simp]:

21263

252 
"even x ==> (1::'a::{number_ring,recpower})^x = 1"


253 
using neg_one_even_odd_power by blast

21256

254 


255 
lemma neg_one_odd_power [simp]:

21263

256 
"odd x ==> (1::'a::{number_ring,recpower})^x = 1"


257 
using neg_one_even_odd_power by blast

21256

258 


259 
lemma neg_power_if:

21263

260 
"(x::'a::{comm_ring_1,recpower}) ^ n =

21256

261 
(if even n then (x ^ n) else (x ^ n))"

21263

262 
apply (induct n)


263 
apply (simp_all split: split_if_asm add: power_Suc)


264 
done

21256

265 

21263

266 
lemma zero_le_even_power: "even n ==>

21256

267 
0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"


268 
apply (simp add: even_nat_equiv_def2)


269 
apply (erule exE)


270 
apply (erule ssubst)


271 
apply (subst power_add)


272 
apply (rule zero_le_square)


273 
done


274 

21263

275 
lemma zero_le_odd_power: "odd n ==>

21256

276 
(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"


277 
apply (simp add: odd_nat_equiv_def2)


278 
apply (erule exE)


279 
apply (erule ssubst)


280 
apply (subst power_Suc)


281 
apply (subst power_add)


282 
apply (subst zero_le_mult_iff)


283 
apply auto


284 
apply (subgoal_tac "x = 0 & 0 < y")


285 
apply (erule conjE, assumption)

21263

286 
apply (subst power_eq_0_iff [symmetric])

21256

287 
apply (subgoal_tac "0 <= x^y * x^y")


288 
apply simp


289 
apply (rule zero_le_square)+

21263

290 
done

21256

291 

21263

292 
lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =

21256

293 
(even n  (odd n & 0 <= x))"


294 
apply auto

21263

295 
apply (subst zero_le_odd_power [symmetric])

21256

296 
apply assumption+


297 
apply (erule zero_le_even_power)

21263

298 
apply (subst zero_le_odd_power)

21256

299 
apply assumption+

21263

300 
done

21256

301 

21263

302 
lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =

21256

303 
(n = 0  (even n & x ~= 0)  (odd n & 0 < x))"


304 
apply (rule iffI)


305 
apply clarsimp


306 
apply (rule conjI)


307 
apply clarsimp


308 
apply (rule ccontr)


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


310 
apply simp


311 
apply (subst zero_le_odd_power)

21263

312 
apply assumption

21256

313 
apply simp


314 
apply (rule notI)


315 
apply (simp add: power_0_left)


316 
apply (rule notI)


317 
apply (simp add: power_0_left)


318 
apply auto


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


320 
apply (frule order_le_imp_less_or_eq)


321 
apply simp


322 
apply (erule zero_le_even_power)


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


324 
apply (frule order_le_imp_less_or_eq)


325 
apply auto


326 
apply (subst zero_le_odd_power)


327 
apply assumption


328 
apply (erule order_less_imp_le)

21263

329 
done

21256

330 


331 
lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =

21263

332 
(odd n & x < 0)"


333 
apply (subst linorder_not_le [symmetric])+

21256

334 
apply (subst zero_le_power_eq)


335 
apply auto

21263

336 
done

21256

337 


338 
lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =


339 
(n ~= 0 & ((odd n & x <= 0)  (even n & x = 0)))"

21263

340 
apply (subst linorder_not_less [symmetric])+

21256

341 
apply (subst zero_less_power_eq)


342 
apply auto

21263

343 
done

21256

344 

21263

345 
lemma power_even_abs: "even n ==>

21256

346 
(abs (x::'a::{recpower,ordered_idom}))^n = x^n"

21263

347 
apply (subst power_abs [symmetric])

21256

348 
apply (simp add: zero_le_even_power)

21263

349 
done

21256

350 


351 
lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0  0 < x)"

21263

352 
by (induct n) auto

21256

353 

21263

354 
lemma power_minus_even [simp]: "even n ==>

21256

355 
( x)^n = (x^n::'a::{recpower,comm_ring_1})"


356 
apply (subst power_minus)


357 
apply simp

21263

358 
done

21256

359 

21263

360 
lemma power_minus_odd [simp]: "odd n ==>

21256

361 
( x)^n =  (x^n::'a::{recpower,comm_ring_1})"


362 
apply (subst power_minus)


363 
apply simp

21263

364 
done

21256

365 

21263

366 


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

21256

368 


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


370 
declare power_0_left_number_of [simp]


371 

21263

372 
lemmas zero_le_power_eq_number_of [simp] =

21256

373 
zero_le_power_eq [of _ "number_of w", standard]


374 

21263

375 
lemmas zero_less_power_eq_number_of [simp] =

21256

376 
zero_less_power_eq [of _ "number_of w", standard]


377 

21263

378 
lemmas power_le_zero_eq_number_of [simp] =

21256

379 
power_le_zero_eq [of _ "number_of w", standard]


380 

21263

381 
lemmas power_less_zero_eq_number_of [simp] =

21256

382 
power_less_zero_eq [of _ "number_of w", standard]


383 

21263

384 
lemmas zero_less_power_nat_eq_number_of [simp] =

21256

385 
zero_less_power_nat_eq [of _ "number_of w", standard]


386 

21263

387 
lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard]

21256

388 

21263

389 
lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard]

21256

390 


391 


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


393 


394 
lemma even_power_le_0_imp_0:

21263

395 
"a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"


396 
by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)

21256

397 


398 
lemma zero_le_power_iff:

21263

399 
"(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower})  even n)"

21256

400 
proof cases


401 
assume even: "even n"


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


403 
by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2)

21263

404 
thus ?thesis by (simp add: zero_le_even_power even)

21256

405 
next


406 
assume odd: "odd n"


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


408 
by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)


409 
thus ?thesis

21263

410 
by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power


411 
dest!: even_power_le_0_imp_0)


412 
qed


413 

21256

414 


415 
subsection {* Miscellaneous *}


416 


417 
lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"


418 
apply (subst zdiv_zadd1_eq)


419 
apply (simp add: even_def)


420 
done


421 


422 
lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"


423 
apply (subst zdiv_zadd1_eq)


424 
apply (simp add: even_def)


425 
done


426 

21263

427 
lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +

21256

428 
(a mod c + Suc 0 mod c) div c"


429 
apply (subgoal_tac "Suc a = a + Suc 0")


430 
apply (erule ssubst)


431 
apply (rule div_add1_eq, simp)


432 
done


433 

21263

434 
lemma even_nat_plus_one_div_two: "even (x::nat) ==>


435 
(Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"

21256

436 
apply (subst div_Suc)


437 
apply (simp add: even_nat_equiv_def)


438 
done


439 

21263

440 
lemma odd_nat_plus_one_div_two: "odd (x::nat) ==>

21256

441 
(Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"


442 
apply (subst div_Suc)


443 
apply (simp add: odd_nat_equiv_def)


444 
done


445 


446 
end
