7 |
7 |
8 theory Parity |
8 theory Parity |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 class even_odd = semiring_div_parity |
12 subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *} |
|
13 |
|
14 lemma two_dvd_Suc_Suc_iff [simp]: |
|
15 "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n" |
|
16 using dvd_add_triv_right_iff [of 2 n] by simp |
|
17 |
|
18 lemma two_dvd_Suc_iff: |
|
19 "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n" |
|
20 by (induct n) auto |
|
21 |
|
22 lemma two_dvd_diff_iff: |
|
23 fixes k l :: int |
|
24 shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l" |
|
25 using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps) |
|
26 |
|
27 lemma two_dvd_abs_add_iff: |
|
28 fixes k l :: int |
|
29 shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l" |
|
30 by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps) |
|
31 |
|
32 lemma two_dvd_add_abs_iff: |
|
33 fixes k l :: int |
|
34 shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l" |
|
35 using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps) |
|
36 |
|
37 |
|
38 subsection {* Ring structures with parity *} |
|
39 |
|
40 class semiring_parity = semiring_dvd + semiring_numeral + |
|
41 assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1" |
|
42 assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b" |
|
43 assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b" |
|
44 begin |
|
45 |
|
46 lemma two_dvd_plus_one_iff [simp]: |
|
47 "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a" |
|
48 by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add) |
|
49 |
|
50 end |
|
51 |
|
52 instance nat :: semiring_parity |
|
53 proof |
|
54 show "\<not> (2 :: nat) dvd 1" |
|
55 by (rule notI, erule dvdE) simp |
|
56 next |
|
57 fix m n :: nat |
|
58 assume "\<not> 2 dvd m" |
|
59 moreover assume "\<not> 2 dvd n" |
|
60 ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n" |
|
61 by (simp add: two_dvd_Suc_iff) |
|
62 then have "2 dvd Suc m + Suc n" |
|
63 by (blast intro: dvd_add) |
|
64 also have "Suc m + Suc n = m + n + 2" |
|
65 by simp |
|
66 finally show "2 dvd m + n" |
|
67 using dvd_add_triv_right_iff [of 2 "m + n"] by simp |
|
68 next |
|
69 fix m n :: nat |
|
70 assume *: "2 dvd m * n" |
|
71 show "2 dvd m \<or> 2 dvd n" |
|
72 proof (rule disjCI) |
|
73 assume "\<not> 2 dvd n" |
|
74 then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff) |
|
75 then obtain r where "Suc n = 2 * r" .. |
|
76 moreover from * obtain s where "m * n = 2 * s" .. |
|
77 then have "2 * s + m = m * Suc n" by simp |
|
78 ultimately have " 2 * s + m = 2 * (m * r)" by simp |
|
79 then have "m = 2 * (m * r - s)" by simp |
|
80 then show "2 dvd m" .. |
|
81 qed |
|
82 qed |
|
83 |
|
84 class ring_parity = comm_ring_1 + semiring_parity |
|
85 |
|
86 instance int :: ring_parity |
|
87 proof |
|
88 show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat) |
|
89 fix k l :: int |
|
90 assume "\<not> 2 dvd k" |
|
91 moreover assume "\<not> 2 dvd l" |
|
92 ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" |
|
93 by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add) |
|
94 then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>" |
|
95 by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib) |
|
96 then show "2 dvd k + l" |
|
97 by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff) |
|
98 qed (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib) |
|
99 |
|
100 context semiring_div_parity |
|
101 begin |
|
102 |
|
103 subclass semiring_parity |
|
104 proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1) |
|
105 fix a b c |
|
106 show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0" |
|
107 by simp |
|
108 next |
|
109 fix a b c |
|
110 assume "(b + c) mod a = 0" |
|
111 with mod_add_eq [of b c a] |
|
112 have "(b mod a + c mod a) mod a = 0" |
|
113 by simp |
|
114 moreover assume "b mod a = 0" |
|
115 ultimately show "c mod a = 0" |
|
116 by simp |
|
117 next |
|
118 show "1 mod 2 = 1" |
|
119 by (fact one_mod_two_eq_one) |
|
120 next |
|
121 fix a b |
|
122 assume "a mod 2 = 1" |
|
123 moreover assume "b mod 2 = 1" |
|
124 ultimately show "(a + b) mod 2 = 0" |
|
125 using mod_add_eq [of a b 2] by simp |
|
126 next |
|
127 fix a b |
|
128 assume "(a * b) mod 2 = 0" |
|
129 then have "(a mod 2) * (b mod 2) = 0" |
|
130 by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2]) |
|
131 then show "a mod 2 = 0 \<or> b mod 2 = 0" |
|
132 by (rule divisors_zero) |
|
133 qed |
|
134 |
|
135 end |
|
136 |
|
137 |
|
138 subsection {* Dedicated @{text even}/@{text odd} predicate *} |
|
139 |
|
140 context semiring_parity |
13 begin |
141 begin |
14 |
142 |
15 definition even :: "'a \<Rightarrow> bool" |
143 definition even :: "'a \<Rightarrow> bool" |
16 where |
144 where |
17 [algebra]: "even a \<longleftrightarrow> 2 dvd a" |
145 [algebra]: "even a \<longleftrightarrow> 2 dvd a" |
18 |
146 |
19 lemmas even_iff_2_dvd = even_def |
147 abbreviation odd :: "'a \<Rightarrow> bool" |
|
148 where |
|
149 "odd a \<equiv> \<not> even a" |
|
150 |
|
151 lemma even_times_iff [simp, presburger, algebra]: |
|
152 "even (a * b) \<longleftrightarrow> even a \<or> even b" |
|
153 by (auto simp add: even_def dest: two_is_prime) |
|
154 |
|
155 lemma even_zero [simp]: |
|
156 "even 0" |
|
157 by (simp add: even_def) |
|
158 |
|
159 lemma odd_one [simp]: |
|
160 "odd 1" |
|
161 by (simp add: even_def) |
|
162 |
|
163 lemma even_numeral [simp]: |
|
164 "even (numeral (Num.Bit0 n))" |
|
165 proof - |
|
166 have "even (2 * numeral n)" |
|
167 unfolding even_times_iff by (simp add: even_def) |
|
168 then have "even (numeral n + numeral n)" |
|
169 unfolding mult_2 . |
|
170 then show ?thesis |
|
171 unfolding numeral.simps . |
|
172 qed |
|
173 |
|
174 lemma odd_numeral [simp]: |
|
175 "odd (numeral (Num.Bit1 n))" |
|
176 proof |
|
177 assume "even (numeral (num.Bit1 n))" |
|
178 then have "even (numeral n + numeral n + 1)" |
|
179 unfolding numeral.simps . |
|
180 then have "even (2 * numeral n + 1)" |
|
181 unfolding mult_2 . |
|
182 then have "2 dvd numeral n * 2 + 1" |
|
183 unfolding even_def by (simp add: ac_simps) |
|
184 with dvd_add_times_triv_left_iff [of 2 "numeral n" 1] |
|
185 have "2 dvd 1" |
|
186 by simp |
|
187 then show False by simp |
|
188 qed |
|
189 |
|
190 end |
|
191 |
|
192 context semiring_div_parity |
|
193 begin |
20 |
194 |
21 lemma even_iff_mod_2_eq_zero [presburger]: |
195 lemma even_iff_mod_2_eq_zero [presburger]: |
22 "even a \<longleftrightarrow> a mod 2 = 0" |
196 "even a \<longleftrightarrow> a mod 2 = 0" |
23 by (simp add: even_def dvd_eq_mod_eq_0) |
197 by (simp add: even_def dvd_eq_mod_eq_0) |
24 |
198 |
25 lemma even_zero [simp]: |
|
26 "even 0" |
|
27 by (simp add: even_iff_mod_2_eq_zero) |
|
28 |
|
29 lemma even_times_anything: |
199 lemma even_times_anything: |
30 "even a \<Longrightarrow> even (a * b)" |
200 "even a \<Longrightarrow> even (a * b)" |
31 by (simp add: even_iff_2_dvd) |
201 by (simp add: even_def) |
32 |
202 |
33 lemma anything_times_even: |
203 lemma anything_times_even: |
34 "even a \<Longrightarrow> even (b * a)" |
204 "even a \<Longrightarrow> even (b * a)" |
35 by (simp add: even_iff_2_dvd) |
205 by (simp add: even_def) |
36 |
|
37 abbreviation odd :: "'a \<Rightarrow> bool" |
|
38 where |
|
39 "odd a \<equiv> \<not> even a" |
|
40 |
206 |
41 lemma odd_times_odd: |
207 lemma odd_times_odd: |
42 "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" |
208 "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" |
43 by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq) |
209 by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq) |
44 |
210 |
45 lemma even_product [simp, presburger]: |
211 lemma even_product: |
46 "even (a * b) \<longleftrightarrow> even a \<or> even b" |
212 "even (a * b) \<longleftrightarrow> even a \<or> even b" |
47 apply (auto simp add: even_times_anything anything_times_even) |
213 by (fact even_times_iff) |
48 apply (rule ccontr) |
|
49 apply (auto simp add: odd_times_odd) |
|
50 done |
|
51 |
214 |
52 end |
215 end |
53 |
|
54 instance nat and int :: even_odd .. |
|
55 |
216 |
56 lemma even_nat_def [presburger]: |
217 lemma even_nat_def [presburger]: |
57 "even x \<longleftrightarrow> even (int x)" |
218 "even x \<longleftrightarrow> even (int x)" |
58 by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib) |
219 by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib) |
59 |
220 |