3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
4 *) |
4 *) |
5 |
5 |
6 header {*Parity: Even and Odd Integers*} |
6 header {*Parity: Even and Odd Integers*} |
7 |
7 |
8 theory EvenOdd imports Int2 begin; |
8 theory EvenOdd imports Int2 begin |
9 |
9 |
10 text{*Note. This theory is being revised. See the web page |
10 text{*Note. This theory is being revised. See the web page |
11 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
11 \url{http://www.andrew.cmu.edu/~avigad/isabelle}.*} |
12 |
12 |
13 constdefs |
13 constdefs |
14 zOdd :: "int set" |
14 zOdd :: "int set" |
15 "zOdd == {x. \<exists>k. x = 2*k + 1}" |
15 "zOdd == {x. \<exists>k. x = 2 * k + 1}" |
16 zEven :: "int set" |
16 zEven :: "int set" |
17 "zEven == {x. \<exists>k. x = 2 * k}" |
17 "zEven == {x. \<exists>k. x = 2 * k}" |
18 |
18 |
19 (***********************************************************) |
19 (***********************************************************) |
20 (* *) |
20 (* *) |
21 (* Some useful properties about even and odd *) |
21 (* Some useful properties about even and odd *) |
22 (* *) |
22 (* *) |
23 (***********************************************************) |
23 (***********************************************************) |
24 |
24 |
25 lemma one_not_even: "~(1 \<in> zEven)"; |
25 lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd" |
26 apply (simp add: zEven_def) |
26 and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C" |
27 apply (rule allI, case_tac "k \<le> 0", auto) |
27 by (auto simp add: zOdd_def) |
28 done |
28 |
29 |
29 lemma zEvenI [intro?]: "x = 2 * k \<Longrightarrow> x \<in> zEven" |
30 lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)"; |
30 and zEvenE [elim?]: "x \<in> zEven \<Longrightarrow> (!!k. x = 2 * k \<Longrightarrow> C) \<Longrightarrow> C" |
31 apply (auto simp add: zOdd_def zEven_def) |
31 by (auto simp add: zEven_def) |
32 proof -; |
32 |
33 fix a b; |
33 lemma one_not_even: "~(1 \<in> zEven)" |
34 assume "2 * (a::int) = 2 * (b::int) + 1"; |
34 proof |
35 then have "2 * (a::int) - 2 * (b :: int) = 1"; |
35 assume "1 \<in> zEven" |
36 by arith |
36 then obtain k :: int where "1 = 2 * k" .. |
37 then have "2 * (a - b) = 1"; |
37 then show False by arith |
38 by (auto simp add: zdiff_zmult_distrib) |
38 qed |
39 moreover have "(2 * (a - b)):zEven"; |
39 |
40 by (auto simp only: zEven_def) |
40 lemma even_odd_conj: "~(x \<in> zOdd & x \<in> zEven)" |
41 ultimately show "False"; |
41 proof - |
42 by (auto simp add: one_not_even) |
42 { |
43 qed; |
43 fix a b |
44 |
44 assume "2 * (a::int) = 2 * (b::int) + 1" |
45 lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)"; |
45 then have "2 * (a::int) - 2 * (b :: int) = 1" |
46 by (simp add: zOdd_def zEven_def, presburger) |
|
47 |
|
48 lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven"; |
|
49 by (insert even_odd_disj, auto) |
|
50 |
|
51 lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd"; |
|
52 apply (case_tac "x \<in> zOdd", auto) |
|
53 apply (drule not_odd_impl_even) |
|
54 apply (auto simp add: zEven_def zOdd_def) |
|
55 proof -; |
|
56 fix a b; |
|
57 assume "2 * a * y = 2 * b + 1"; |
|
58 then have "2 * a * y - 2 * b = 1"; |
|
59 by arith |
46 by arith |
60 then have "2 * (a * y - b) = 1"; |
47 then have "2 * (a - b) = 1" |
61 by (auto simp add: zdiff_zmult_distrib) |
48 by (auto simp add: zdiff_zmult_distrib) |
62 moreover have "(2 * (a * y - b)):zEven"; |
49 moreover have "(2 * (a - b)):zEven" |
63 by (auto simp only: zEven_def) |
50 by (auto simp only: zEven_def) |
64 ultimately show "False"; |
51 ultimately have False |
65 by (auto simp add: one_not_even) |
52 by (auto simp add: one_not_even) |
66 qed; |
53 } |
67 |
54 then show ?thesis |
68 lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven"; |
55 by (auto simp add: zOdd_def zEven_def) |
|
56 qed |
|
57 |
|
58 lemma even_odd_disj: "(x \<in> zOdd | x \<in> zEven)" |
|
59 by (simp add: zOdd_def zEven_def) arith |
|
60 |
|
61 lemma not_odd_impl_even: "~(x \<in> zOdd) ==> x \<in> zEven" |
|
62 using even_odd_disj by auto |
|
63 |
|
64 lemma odd_mult_odd_prop: "(x*y):zOdd ==> x \<in> zOdd" |
|
65 proof (rule classical) |
|
66 assume "\<not> ?thesis" |
|
67 then have "x \<in> zEven" by (rule not_odd_impl_even) |
|
68 then obtain a where a: "x = 2 * a" .. |
|
69 assume "x * y : zOdd" |
|
70 then obtain b where "x * y = 2 * b + 1" .. |
|
71 with a have "2 * a * y = 2 * b + 1" by simp |
|
72 then have "2 * a * y - 2 * b = 1" |
|
73 by arith |
|
74 then have "2 * (a * y - b) = 1" |
|
75 by (auto simp add: zdiff_zmult_distrib) |
|
76 moreover have "(2 * (a * y - b)):zEven" |
|
77 by (auto simp only: zEven_def) |
|
78 ultimately have False |
|
79 by (auto simp add: one_not_even) |
|
80 then show ?thesis .. |
|
81 qed |
|
82 |
|
83 lemma odd_minus_one_even: "x \<in> zOdd ==> (x - 1):zEven" |
69 by (auto simp add: zOdd_def zEven_def) |
84 by (auto simp add: zOdd_def zEven_def) |
70 |
85 |
71 lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0"; |
86 lemma even_div_2_prop1: "x \<in> zEven ==> (x mod 2) = 0" |
72 by (auto simp add: zEven_def) |
87 by (auto simp add: zEven_def) |
73 |
88 |
74 lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x"; |
89 lemma even_div_2_prop2: "x \<in> zEven ==> (2 * (x div 2)) = x" |
75 by (auto simp add: zEven_def) |
90 by (auto simp add: zEven_def) |
76 |
91 |
77 lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"; |
92 lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven" |
78 apply (auto simp add: zEven_def) |
93 apply (auto simp add: zEven_def) |
79 by (auto simp only: zadd_zmult_distrib2 [THEN sym]) |
94 apply (auto simp only: zadd_zmult_distrib2 [symmetric]) |
80 |
95 done |
81 lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"; |
96 |
82 by (auto simp add: zEven_def) |
97 lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven" |
83 |
98 by (auto simp add: zEven_def) |
84 lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"; |
99 |
|
100 lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven" |
85 apply (auto simp add: zEven_def) |
101 apply (auto simp add: zEven_def) |
86 by (auto simp only: zdiff_zmult_distrib2 [THEN sym]) |
102 apply (auto simp only: zdiff_zmult_distrib2 [symmetric]) |
87 |
103 done |
88 lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"; |
104 |
89 apply (auto simp add: zOdd_def zEven_def) |
105 lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven" |
90 by (auto simp only: zdiff_zmult_distrib2 [THEN sym]) |
106 apply (auto simp add: zOdd_def zEven_def) |
91 |
107 apply (auto simp only: zdiff_zmult_distrib2 [symmetric]) |
92 lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"; |
108 done |
|
109 |
|
110 lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd" |
93 apply (auto simp add: zOdd_def zEven_def) |
111 apply (auto simp add: zOdd_def zEven_def) |
94 apply (rule_tac x = "k - ka - 1" in exI) |
112 apply (rule_tac x = "k - ka - 1" in exI) |
95 by auto |
113 apply auto |
96 |
114 done |
97 lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"; |
115 |
98 apply (auto simp add: zOdd_def zEven_def) |
116 lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd" |
99 by (auto simp only: zdiff_zmult_distrib2 [THEN sym]) |
117 apply (auto simp add: zOdd_def zEven_def) |
100 |
118 apply (auto simp only: zdiff_zmult_distrib2 [symmetric]) |
101 lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd"; |
119 done |
|
120 |
|
121 lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd" |
102 apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2) |
122 apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2) |
103 apply (rule_tac x = "2 * ka * k + ka + k" in exI) |
123 apply (rule_tac x = "2 * ka * k + ka + k" in exI) |
104 by (auto simp add: zadd_zmult_distrib) |
124 apply (auto simp add: zadd_zmult_distrib) |
105 |
125 done |
106 lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"; |
126 |
107 by (insert even_odd_conj even_odd_disj, auto) |
127 lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))" |
108 |
128 using even_odd_conj even_odd_disj by auto |
109 lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven"; |
129 |
110 by (insert odd_iff_not_even odd_times_odd, auto) |
130 lemma even_product: "x * y \<in> zEven ==> x \<in> zEven | y \<in> zEven" |
111 |
131 using odd_iff_not_even odd_times_odd by auto |
112 lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))"; |
132 |
113 apply (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd |
133 lemma even_diff: "x - y \<in> zEven = ((x \<in> zEven) = (y \<in> zEven))" |
114 even_minus_odd odd_minus_even) |
134 proof |
115 proof -; |
135 assume xy: "x - y \<in> zEven" |
116 assume "x - y \<in> zEven" and "x \<in> zEven"; |
136 { |
117 show "y \<in> zEven"; |
137 assume x: "x \<in> zEven" |
118 proof (rule classical); |
138 have "y \<in> zEven" |
119 assume "~(y \<in> zEven)"; |
139 proof (rule classical) |
120 then have "y \<in> zOdd" |
140 assume "\<not> ?thesis" |
|
141 then have "y \<in> zOdd" |
|
142 by (simp add: odd_iff_not_even) |
|
143 with x have "x - y \<in> zOdd" |
|
144 by (simp add: even_minus_odd) |
|
145 with xy have False |
121 by (auto simp add: odd_iff_not_even) |
146 by (auto simp add: odd_iff_not_even) |
122 with prems have "x - y \<in> zOdd"; |
147 then show ?thesis .. |
123 by (simp add: even_minus_odd) |
148 qed |
124 with prems have "False"; |
149 } moreover { |
|
150 assume y: "y \<in> zEven" |
|
151 have "x \<in> zEven" |
|
152 proof (rule classical) |
|
153 assume "\<not> ?thesis" |
|
154 then have "x \<in> zOdd" |
125 by (auto simp add: odd_iff_not_even) |
155 by (auto simp add: odd_iff_not_even) |
126 thus ?thesis; |
156 with y have "x - y \<in> zOdd" |
127 by auto |
157 by (simp add: odd_minus_even) |
128 qed; |
158 with xy have False |
129 next assume "x - y \<in> zEven" and "y \<in> zEven"; |
|
130 show "x \<in> zEven"; |
|
131 proof (rule classical); |
|
132 assume "~(x \<in> zEven)"; |
|
133 then have "x \<in> zOdd" |
|
134 by (auto simp add: odd_iff_not_even) |
159 by (auto simp add: odd_iff_not_even) |
135 with prems have "x - y \<in> zOdd"; |
160 then show ?thesis .. |
136 by (simp add: odd_minus_even) |
161 qed |
137 with prems have "False"; |
162 } |
138 by (auto simp add: odd_iff_not_even) |
163 ultimately show "(x \<in> zEven) = (y \<in> zEven)" |
139 thus ?thesis; |
164 by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd |
140 by auto |
165 even_minus_odd odd_minus_even) |
141 qed; |
166 next |
142 qed; |
167 assume "(x \<in> zEven) = (y \<in> zEven)" |
143 |
168 then show "x - y \<in> zEven" |
144 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1"; |
169 by (auto simp add: odd_iff_not_even even_minus_even odd_minus_odd |
145 proof -; |
170 even_minus_odd odd_minus_even) |
146 assume "x \<in> zEven" and "0 \<le> x"; |
171 qed |
147 then have "\<exists>k. x = 2 * k"; |
172 |
148 by (auto simp only: zEven_def) |
173 lemma neg_one_even_power: "[| x \<in> zEven; 0 \<le> x |] ==> (-1::int)^(nat x) = 1" |
149 then show ?thesis; |
174 proof - |
150 proof; |
175 assume 1: "x \<in> zEven" and 2: "0 \<le> x" |
151 fix a; |
176 from 1 obtain a where 3: "x = 2 * a" .. |
152 assume "x = 2 * a"; |
177 with 2 have "0 \<le> a" by simp |
153 from prems have a: "0 \<le> a"; |
178 from 2 3 have "nat x = nat (2 * a)" |
154 by arith |
179 by simp |
155 from prems have "nat x = nat(2 * a)"; |
180 also from 3 have "nat (2 * a) = 2 * nat a" |
156 by auto |
181 by (simp add: nat_mult_distrib) |
157 also from a have "nat (2 * a) = 2 * nat a"; |
182 finally have "(-1::int)^nat x = (-1)^(2 * nat a)" |
158 by (auto simp add: nat_mult_distrib) |
183 by simp |
159 finally have "(-1::int)^nat x = (-1)^(2 * nat a)"; |
184 also have "... = ((-1::int)^2)^ (nat a)" |
160 by auto |
185 by (simp add: zpower_zpower [symmetric]) |
161 also have "... = ((-1::int)^2)^ (nat a)"; |
186 also have "(-1::int)^2 = 1" |
162 by (auto simp add: zpower_zpower [THEN sym]) |
187 by simp |
163 also have "(-1::int)^2 = 1"; |
188 finally show ?thesis |
164 by auto |
189 by simp |
165 finally; show ?thesis; |
190 qed |
166 by auto |
191 |
167 qed; |
192 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1" |
168 qed; |
193 proof - |
169 |
194 assume 1: "x \<in> zOdd" and 2: "0 \<le> x" |
170 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1"; |
195 from 1 obtain a where 3: "x = 2 * a + 1" .. |
171 proof -; |
196 with 2 have a: "0 \<le> a" by simp |
172 assume "x \<in> zOdd" and "0 \<le> x"; |
197 with 2 3 have "nat x = nat (2 * a + 1)" |
173 then have "\<exists>k. x = 2 * k + 1"; |
198 by simp |
174 by (auto simp only: zOdd_def) |
199 also from a have "nat (2 * a + 1) = 2 * nat a + 1" |
175 then show ?thesis; |
200 by (auto simp add: nat_mult_distrib nat_add_distrib) |
176 proof; |
201 finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)" |
177 fix a; |
202 by simp |
178 assume "x = 2 * a + 1"; |
203 also have "... = ((-1::int)^2)^ (nat a) * (-1)^1" |
179 from prems have a: "0 \<le> a"; |
204 by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib) |
180 by arith |
205 also have "(-1::int)^2 = 1" |
181 from prems have "nat x = nat(2 * a + 1)"; |
206 by simp |
182 by auto |
207 finally show ?thesis |
183 also from a have "nat (2 * a + 1) = 2 * nat a + 1"; |
208 by simp |
184 by (auto simp add: nat_mult_distrib nat_add_distrib) |
209 qed |
185 finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"; |
210 |
186 by auto |
211 lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> |
187 also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"; |
212 (-1::int)^(nat x) = (-1::int)^(nat y)" |
188 by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib) |
213 using even_odd_disj [of x] even_odd_disj [of y] |
189 also have "(-1::int)^2 = 1"; |
|
190 by auto |
|
191 finally; show ?thesis; |
|
192 by auto |
|
193 qed; |
|
194 qed; |
|
195 |
|
196 lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> |
|
197 (-1::int)^(nat x) = (-1::int)^(nat y)"; |
|
198 apply (insert even_odd_disj [of x]) |
|
199 apply (insert even_odd_disj [of y]) |
|
200 by (auto simp add: neg_one_even_power neg_one_odd_power) |
214 by (auto simp add: neg_one_even_power neg_one_odd_power) |
201 |
215 |
202 lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))"; |
216 |
|
217 lemma one_not_neg_one_mod_m: "2 < m ==> ~([1 = -1] (mod m))" |
203 by (auto simp add: zcong_def zdvd_not_zless) |
218 by (auto simp add: zcong_def zdvd_not_zless) |
204 |
219 |
205 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2"; |
220 lemma even_div_2_l: "[| y \<in> zEven; x < y |] ==> x div 2 < y div 2" |
206 apply (auto simp only: zEven_def) |
221 proof - |
207 proof -; |
222 assume 1: "y \<in> zEven" and 2: "x < y" |
208 fix k assume "x < 2 * k"; |
223 from 1 obtain k where k: "y = 2 * k" .. |
209 then have "x div 2 < k" by (auto simp add: div_prop1) |
224 with 2 have "x < 2 * k" by simp |
210 also have "k = (2 * k) div 2"; by auto |
225 then have "x div 2 < k" by (auto simp add: div_prop1) |
211 finally show "x div 2 < 2 * k div 2" by auto |
226 also have "k = (2 * k) div 2" by simp |
212 qed; |
227 finally have "x div 2 < 2 * k div 2" by simp |
213 |
228 with k show ?thesis by simp |
214 lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2"; |
229 qed |
|
230 |
|
231 lemma even_sum_div_2: "[| x \<in> zEven; y \<in> zEven |] ==> (x + y) div 2 = x div 2 + y div 2" |
215 by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq) |
232 by (auto simp add: zEven_def, auto simp add: zdiv_zadd1_eq) |
216 |
233 |
217 lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y"; |
234 lemma even_prod_div_2: "[| x \<in> zEven |] ==> (x * y) div 2 = (x div 2) * y" |
218 by (auto simp add: zEven_def) |
235 by (auto simp add: zEven_def) |
219 |
236 |
220 (* An odd prime is greater than 2 *) |
237 (* An odd prime is greater than 2 *) |
221 |
238 |
222 lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)"; |
239 lemma zprime_zOdd_eq_grt_2: "zprime p ==> (p \<in> zOdd) = (2 < p)" |
223 apply (auto simp add: zOdd_def zprime_def) |
240 apply (auto simp add: zOdd_def zprime_def) |
224 apply (drule_tac x = 2 in allE) |
241 apply (drule_tac x = 2 in allE) |
225 apply (insert odd_iff_not_even [of p]) |
242 using odd_iff_not_even [of p] |
226 by (auto simp add: zOdd_def zEven_def) |
243 apply (auto simp add: zOdd_def zEven_def) |
|
244 done |
227 |
245 |
228 (* Powers of -1 and parity *) |
246 (* Powers of -1 and parity *) |
229 |
247 |
230 lemma neg_one_special: "finite A ==> |
248 lemma neg_one_special: "finite A ==> |
231 ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"; |
249 ((-1 :: int) ^ card A) * (-1 ^ card A) = 1" |
232 by (induct set: Finites, auto) |
250 by (induct set: Finites) auto |
233 |
251 |
234 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"; |
252 lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1" |
235 apply (induct_tac n) |
253 by (induct n) auto |
236 by auto |
|
237 |
254 |
238 lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |] |
255 lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |] |
239 ==> ((-1::int)^j = (-1::int)^k)"; |
256 ==> ((-1::int)^j = (-1::int)^k)" |
240 apply (insert neg_one_power [of j]) |
257 using neg_one_power [of j] and insert neg_one_power [of k] |
241 apply (insert neg_one_power [of k]) |
|
242 by (auto simp add: one_not_neg_one_mod_m zcong_sym) |
258 by (auto simp add: one_not_neg_one_mod_m zcong_sym) |
243 |
259 |
244 end; |
260 end |