4 *) |
4 *) |
5 |
5 |
6 section \<open>Binary Numerals\<close> |
6 section \<open>Binary Numerals\<close> |
7 |
7 |
8 theory Num |
8 theory Num |
9 imports BNF_Least_Fixpoint |
9 imports BNF_Least_Fixpoint |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>The \<open>num\<close> type\<close> |
12 subsection \<open>The \<open>num\<close> type\<close> |
13 |
13 |
14 datatype num = One | Bit0 num | Bit1 num |
14 datatype num = One | Bit0 num | Bit1 num |
15 |
15 |
16 text \<open>Increment function for type @{typ num}\<close> |
16 text \<open>Increment function for type @{typ num}\<close> |
17 |
17 |
18 primrec inc :: "num \<Rightarrow> num" where |
18 primrec inc :: "num \<Rightarrow> num" |
19 "inc One = Bit0 One" | |
19 where |
20 "inc (Bit0 x) = Bit1 x" | |
20 "inc One = Bit0 One" |
21 "inc (Bit1 x) = Bit0 (inc x)" |
21 | "inc (Bit0 x) = Bit1 x" |
|
22 | "inc (Bit1 x) = Bit0 (inc x)" |
22 |
23 |
23 text \<open>Converting between type @{typ num} and type @{typ nat}\<close> |
24 text \<open>Converting between type @{typ num} and type @{typ nat}\<close> |
24 |
25 |
25 primrec nat_of_num :: "num \<Rightarrow> nat" where |
26 primrec nat_of_num :: "num \<Rightarrow> nat" |
26 "nat_of_num One = Suc 0" | |
27 where |
27 "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x" | |
28 "nat_of_num One = Suc 0" |
28 "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)" |
29 | "nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x" |
29 |
30 | "nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)" |
30 primrec num_of_nat :: "nat \<Rightarrow> num" where |
31 |
31 "num_of_nat 0 = One" | |
32 primrec num_of_nat :: "nat \<Rightarrow> num" |
32 "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" |
33 where |
|
34 "num_of_nat 0 = One" |
|
35 | "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)" |
33 |
36 |
34 lemma nat_of_num_pos: "0 < nat_of_num x" |
37 lemma nat_of_num_pos: "0 < nat_of_num x" |
35 by (induct x) simp_all |
38 by (induct x) simp_all |
36 |
39 |
37 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0" |
40 lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0" |
38 by (induct x) simp_all |
41 by (induct x) simp_all |
39 |
42 |
40 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" |
43 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)" |
41 by (induct x) simp_all |
44 by (induct x) simp_all |
42 |
45 |
43 lemma num_of_nat_double: |
46 lemma num_of_nat_double: "0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)" |
44 "0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)" |
|
45 by (induct n) simp_all |
47 by (induct n) simp_all |
46 |
48 |
47 text \<open> |
49 text \<open>Type @{typ num} is isomorphic to the strictly positive natural numbers.\<close> |
48 Type @{typ num} is isomorphic to the strictly positive |
|
49 natural numbers. |
|
50 \<close> |
|
51 |
50 |
52 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" |
51 lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x" |
53 by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) |
52 by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) |
54 |
53 |
55 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
54 lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n" |
66 assumes One: "P One" |
65 assumes One: "P One" |
67 and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
66 and inc: "\<And>x. P x \<Longrightarrow> P (inc x)" |
68 shows "P x" |
67 shows "P x" |
69 proof - |
68 proof - |
70 obtain n where n: "Suc n = nat_of_num x" |
69 obtain n where n: "Suc n = nat_of_num x" |
71 by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0) |
70 by (cases "nat_of_num x") (simp_all add: nat_of_num_neq_0) |
72 have "P (num_of_nat (Suc n))" |
71 have "P (num_of_nat (Suc n))" |
73 proof (induct n) |
72 proof (induct n) |
74 case 0 show ?case using One by simp |
73 case 0 |
|
74 from One show ?case by simp |
75 next |
75 next |
76 case (Suc n) |
76 case (Suc n) |
77 then have "P (inc (num_of_nat (Suc n)))" by (rule inc) |
77 then have "P (inc (num_of_nat (Suc n)))" by (rule inc) |
78 then show "P (num_of_nat (Suc (Suc n)))" by simp |
78 then show "P (num_of_nat (Suc (Suc n)))" by simp |
79 qed |
79 qed |
80 with n show "P x" |
80 with n show "P x" |
81 by (simp add: nat_of_num_inverse) |
81 by (simp add: nat_of_num_inverse) |
82 qed |
82 qed |
83 |
83 |
84 text \<open> |
84 text \<open> |
85 From now on, there are two possible models for @{typ num}: |
85 From now on, there are two possible models for @{typ num}: as positive |
86 as positive naturals (rule \<open>num_induct\<close>) |
86 naturals (rule \<open>num_induct\<close>) and as digit representation (rules |
87 and as digit representation (rules \<open>num.induct\<close>, \<open>num.cases\<close>). |
87 \<open>num.induct\<close>, \<open>num.cases\<close>). |
88 \<close> |
88 \<close> |
89 |
89 |
90 |
90 |
91 subsection \<open>Numeral operations\<close> |
91 subsection \<open>Numeral operations\<close> |
92 |
92 |
93 instantiation num :: "{plus,times,linorder}" |
93 instantiation num :: "{plus,times,linorder}" |
94 begin |
94 begin |
95 |
95 |
96 definition [code del]: |
96 definition [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
97 "m + n = num_of_nat (nat_of_num m + nat_of_num n)" |
97 |
98 |
98 definition [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
99 definition [code del]: |
99 |
100 "m * n = num_of_nat (nat_of_num m * nat_of_num n)" |
100 definition [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" |
101 |
101 |
102 definition [code del]: |
102 definition [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
103 "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n" |
|
104 |
|
105 definition [code del]: |
|
106 "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n" |
|
107 |
103 |
108 instance |
104 instance |
109 by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff) |
105 by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff) |
110 |
106 |
111 end |
107 end |
173 "Bit1 m < Bit0 n \<longleftrightarrow> m < n" |
168 "Bit1 m < Bit0 n \<longleftrightarrow> m < n" |
174 using nat_of_num_pos [of n] nat_of_num_pos [of m] |
169 using nat_of_num_pos [of n] nat_of_num_pos [of m] |
175 by (auto simp add: less_eq_num_def less_num_def) |
170 by (auto simp add: less_eq_num_def less_num_def) |
176 |
171 |
177 lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One" |
172 lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One" |
178 by (simp add: antisym_conv) |
173 by (simp add: antisym_conv) |
179 |
174 |
180 text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors\<close> |
175 text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors.\<close> |
181 |
176 |
182 lemma add_One: "x + One = inc x" |
177 lemma add_One: "x + One = inc x" |
183 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
178 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
184 |
179 |
185 lemma add_One_commute: "One + n = n + One" |
180 lemma add_One_commute: "One + n = n + One" |
189 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
184 by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
190 |
185 |
191 lemma mult_inc: "x * inc y = x * y + x" |
186 lemma mult_inc: "x * inc y = x * y + x" |
192 by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
187 by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
193 |
188 |
194 text \<open>The @{const num_of_nat} conversion\<close> |
189 text \<open>The @{const num_of_nat} conversion.\<close> |
195 |
190 |
196 lemma num_of_nat_One: |
191 lemma num_of_nat_One: "n \<le> 1 \<Longrightarrow> num_of_nat n = One" |
197 "n \<le> 1 \<Longrightarrow> num_of_nat n = One" |
|
198 by (cases n) simp_all |
192 by (cases n) simp_all |
199 |
193 |
200 lemma num_of_nat_plus_distrib: |
194 lemma num_of_nat_plus_distrib: |
201 "0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n" |
195 "0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n" |
202 by (induct n) (auto simp add: add_One add_One_commute add_inc) |
196 by (induct n) (auto simp add: add_One add_One_commute add_inc) |
203 |
197 |
204 text \<open>A double-and-decrement function\<close> |
198 text \<open>A double-and-decrement function.\<close> |
205 |
199 |
206 primrec BitM :: "num \<Rightarrow> num" where |
200 primrec BitM :: "num \<Rightarrow> num" |
207 "BitM One = One" | |
201 where |
208 "BitM (Bit0 n) = Bit1 (BitM n)" | |
202 "BitM One = One" |
209 "BitM (Bit1 n) = Bit1 (Bit0 n)" |
203 | "BitM (Bit0 n) = Bit1 (BitM n)" |
|
204 | "BitM (Bit1 n) = Bit1 (Bit0 n)" |
210 |
205 |
211 lemma BitM_plus_one: "BitM n + One = Bit0 n" |
206 lemma BitM_plus_one: "BitM n + One = Bit0 n" |
212 by (induct n) simp_all |
207 by (induct n) simp_all |
213 |
208 |
214 lemma one_plus_BitM: "One + BitM n = Bit0 n" |
209 lemma one_plus_BitM: "One + BitM n = Bit0 n" |
215 unfolding add_One_commute BitM_plus_one .. |
210 unfolding add_One_commute BitM_plus_one .. |
216 |
211 |
217 text \<open>Squaring and exponentiation\<close> |
212 text \<open>Squaring and exponentiation.\<close> |
218 |
213 |
219 primrec sqr :: "num \<Rightarrow> num" where |
214 primrec sqr :: "num \<Rightarrow> num" |
220 "sqr One = One" | |
215 where |
221 "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))" | |
216 "sqr One = One" |
222 "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))" |
217 | "sqr (Bit0 n) = Bit0 (Bit0 (sqr n))" |
223 |
218 | "sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))" |
224 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" where |
219 |
225 "pow x One = x" | |
220 primrec pow :: "num \<Rightarrow> num \<Rightarrow> num" |
226 "pow x (Bit0 y) = sqr (pow x y)" | |
221 where |
227 "pow x (Bit1 y) = sqr (pow x y) * x" |
222 "pow x One = x" |
|
223 | "pow x (Bit0 y) = sqr (pow x y)" |
|
224 | "pow x (Bit1 y) = sqr (pow x y) * x" |
228 |
225 |
229 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x" |
226 lemma nat_of_num_sqr: "nat_of_num (sqr x) = nat_of_num x * nat_of_num x" |
230 by (induct x, simp_all add: algebra_simps nat_of_num_add) |
227 by (induct x) (simp_all add: algebra_simps nat_of_num_add) |
231 |
228 |
232 lemma sqr_conv_mult: "sqr x = x * x" |
229 lemma sqr_conv_mult: "sqr x = x * x" |
233 by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) |
230 by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) |
234 |
231 |
235 |
232 |
241 \<close> |
238 \<close> |
242 |
239 |
243 class numeral = one + semigroup_add |
240 class numeral = one + semigroup_add |
244 begin |
241 begin |
245 |
242 |
246 primrec numeral :: "num \<Rightarrow> 'a" where |
243 primrec numeral :: "num \<Rightarrow> 'a" |
247 numeral_One: "numeral One = 1" | |
244 where |
248 numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" | |
245 numeral_One: "numeral One = 1" |
249 numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1" |
246 | numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
|
247 | numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1" |
250 |
248 |
251 lemma numeral_code [code]: |
249 lemma numeral_code [code]: |
252 "numeral One = 1" |
250 "numeral One = 1" |
253 "numeral (Bit0 n) = (let m = numeral n in m + m)" |
251 "numeral (Bit0 n) = (let m = numeral n in m + m)" |
254 "numeral (Bit1 n) = (let m = numeral n in m + m + 1)" |
252 "numeral (Bit1 n) = (let m = numeral n in m + m + 1)" |
255 by (simp_all add: Let_def) |
253 by (simp_all add: Let_def) |
256 |
254 |
257 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1" |
255 lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1" |
258 apply (induct x) |
256 proof (induct x) |
259 apply simp |
257 case One |
260 apply (simp add: add.assoc [symmetric], simp add: add.assoc) |
258 then show ?case by simp |
261 apply (simp add: add.assoc [symmetric], simp add: add.assoc) |
259 next |
262 done |
260 case Bit0 |
|
261 then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc) |
|
262 next |
|
263 case Bit1 |
|
264 then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc) |
|
265 qed |
263 |
266 |
264 lemma numeral_inc: "numeral (inc x) = numeral x + 1" |
267 lemma numeral_inc: "numeral (inc x) = numeral x + 1" |
265 proof (induct x) |
268 proof (induct x) |
|
269 case One |
|
270 then show ?case by simp |
|
271 next |
|
272 case Bit0 |
|
273 then show ?case by simp |
|
274 next |
266 case (Bit1 x) |
275 case (Bit1 x) |
267 have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1" |
276 have "numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1" |
268 by (simp only: one_plus_numeral_commute) |
277 by (simp only: one_plus_numeral_commute) |
269 with Bit1 show ?case |
278 with Bit1 show ?case |
270 by (simp add: add.assoc) |
279 by (simp add: add.assoc) |
271 qed simp_all |
280 qed |
272 |
281 |
273 declare numeral.simps [simp del] |
282 declare numeral.simps [simp del] |
274 |
283 |
275 abbreviation "Numeral1 \<equiv> numeral One" |
284 abbreviation "Numeral1 \<equiv> numeral One" |
276 |
285 |
318 \<close> |
327 \<close> |
319 |
328 |
320 |
329 |
321 subsection \<open>Class-specific numeral rules\<close> |
330 subsection \<open>Class-specific numeral rules\<close> |
322 |
331 |
323 text \<open> |
332 text \<open>@{const numeral} is a morphism.\<close> |
324 @{const numeral} is a morphism. |
333 |
325 \<close> |
|
326 |
334 |
327 subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close> |
335 subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close> |
328 |
336 |
329 context numeral |
337 context numeral |
330 begin |
338 begin |
331 |
339 |
332 lemma numeral_add: "numeral (m + n) = numeral m + numeral n" |
340 lemma numeral_add: "numeral (m + n) = numeral m + numeral n" |
333 by (induct n rule: num_induct) |
341 by (induct n rule: num_induct) |
334 (simp_all only: numeral_One add_One add_inc numeral_inc add.assoc) |
342 (simp_all only: numeral_One add_One add_inc numeral_inc add.assoc) |
335 |
343 |
336 lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)" |
344 lemma numeral_plus_numeral: "numeral m + numeral n = numeral (m + n)" |
337 by (rule numeral_add [symmetric]) |
345 by (rule numeral_add [symmetric]) |
338 |
346 |
339 lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)" |
347 lemma numeral_plus_one: "numeral n + 1 = numeral (n + One)" |
348 lemmas add_numeral_special = |
356 lemmas add_numeral_special = |
349 numeral_plus_one one_plus_numeral one_add_one |
357 numeral_plus_one one_plus_numeral one_add_one |
350 |
358 |
351 end |
359 end |
352 |
360 |
353 subsubsection \<open> |
361 |
354 Structures with negation: class \<open>neg_numeral\<close> |
362 subsubsection \<open>Structures with negation: class \<open>neg_numeral\<close>\<close> |
355 \<close> |
|
356 |
363 |
357 class neg_numeral = numeral + group_add |
364 class neg_numeral = numeral + group_add |
358 begin |
365 begin |
359 |
366 |
360 lemma uminus_numeral_One: |
367 lemma uminus_numeral_One: "- Numeral1 = - 1" |
361 "- Numeral1 = - 1" |
|
362 by (simp add: numeral_One) |
368 by (simp add: numeral_One) |
363 |
369 |
364 text \<open>Numerals form an abelian subgroup.\<close> |
370 text \<open>Numerals form an abelian subgroup.\<close> |
365 |
371 |
366 inductive is_num :: "'a \<Rightarrow> bool" where |
372 inductive is_num :: "'a \<Rightarrow> bool" |
367 "is_num 1" | |
373 where |
368 "is_num x \<Longrightarrow> is_num (- x)" | |
374 "is_num 1" |
369 "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> is_num (x + y)" |
375 | "is_num x \<Longrightarrow> is_num (- x)" |
|
376 | "is_num x \<Longrightarrow> is_num y \<Longrightarrow> is_num (x + y)" |
370 |
377 |
371 lemma is_num_numeral: "is_num (numeral k)" |
378 lemma is_num_numeral: "is_num (numeral k)" |
372 by (induct k, simp_all add: numeral.simps is_num.intros) |
379 by (induct k) (simp_all add: numeral.simps is_num.intros) |
373 |
380 |
374 lemma is_num_add_commute: |
381 lemma is_num_add_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + y = y + x" |
375 "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + y = y + x" |
|
376 apply (induct x rule: is_num.induct) |
382 apply (induct x rule: is_num.induct) |
377 apply (induct y rule: is_num.induct) |
383 apply (induct y rule: is_num.induct) |
378 apply simp |
384 apply simp |
379 apply (rule_tac a=x in add_left_imp_eq) |
385 apply (rule_tac a=x in add_left_imp_eq) |
380 apply (rule_tac a=x in add_right_imp_eq) |
386 apply (rule_tac a=x in add_right_imp_eq) |
|
387 apply (simp add: add.assoc) |
|
388 apply (simp add: add.assoc [symmetric]) |
|
389 apply (simp add: add.assoc) |
|
390 apply (rule_tac a=x in add_left_imp_eq) |
|
391 apply (rule_tac a=x in add_right_imp_eq) |
|
392 apply (simp add: add.assoc) |
381 apply (simp add: add.assoc) |
393 apply (simp add: add.assoc) |
382 apply (simp add: add.assoc [symmetric], simp add: add.assoc) |
394 apply (simp add: add.assoc [symmetric]) |
383 apply (rule_tac a=x in add_left_imp_eq) |
|
384 apply (rule_tac a=x in add_right_imp_eq) |
|
385 apply (simp add: add.assoc) |
|
386 apply (simp add: add.assoc, simp add: add.assoc [symmetric]) |
|
387 done |
395 done |
388 |
396 |
389 lemma is_num_add_left_commute: |
397 lemma is_num_add_left_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + (y + z) = y + (x + z)" |
390 "\<lbrakk>is_num x; is_num y\<rbrakk> \<Longrightarrow> x + (y + z) = y + (x + z)" |
|
391 by (simp only: add.assoc [symmetric] is_num_add_commute) |
398 by (simp only: add.assoc [symmetric] is_num_add_commute) |
392 |
399 |
393 lemmas is_num_normalize = |
400 lemmas is_num_normalize = |
394 add.assoc is_num_add_commute is_num_add_left_commute |
401 add.assoc is_num_add_commute is_num_add_left_commute |
395 is_num.intros is_num_numeral |
402 is_num.intros is_num_numeral |
396 minus_add |
403 minus_add |
397 |
404 |
398 definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x" |
405 definition dbl :: "'a \<Rightarrow> 'a" |
399 definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1" |
406 where "dbl x = x + x" |
400 definition dbl_dec :: "'a \<Rightarrow> 'a" where "dbl_dec x = x + x - 1" |
407 |
401 |
408 definition dbl_inc :: "'a \<Rightarrow> 'a" |
402 definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a" where |
409 where "dbl_inc x = x + x + 1" |
403 "sub k l = numeral k - numeral l" |
410 |
|
411 definition dbl_dec :: "'a \<Rightarrow> 'a" |
|
412 where "dbl_dec x = x + x - 1" |
|
413 |
|
414 definition sub :: "num \<Rightarrow> num \<Rightarrow> 'a" |
|
415 where "sub k l = numeral k - numeral l" |
404 |
416 |
405 lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1" |
417 lemma numeral_BitM: "numeral (BitM n) = numeral (Bit0 n) - 1" |
406 by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq) |
418 by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq) |
407 |
419 |
408 lemma dbl_simps [simp]: |
420 lemma dbl_simps [simp]: |
445 lemma add_neg_numeral_simps: |
458 lemma add_neg_numeral_simps: |
446 "numeral m + - numeral n = sub m n" |
459 "numeral m + - numeral n = sub m n" |
447 "- numeral m + numeral n = sub n m" |
460 "- numeral m + numeral n = sub n m" |
448 "- numeral m + - numeral n = - (numeral m + numeral n)" |
461 "- numeral m + - numeral n = - (numeral m + numeral n)" |
449 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
462 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
450 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
463 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
451 |
464 |
452 lemma add_neg_numeral_special: |
465 lemma add_neg_numeral_special: |
453 "1 + - numeral m = sub One m" |
466 "1 + - numeral m = sub One m" |
454 "- numeral m + 1 = sub One m" |
467 "- numeral m + 1 = sub One m" |
455 "numeral m + - 1 = sub m One" |
468 "numeral m + - 1 = sub m One" |
458 "- numeral m + - 1 = - numeral (inc m)" |
471 "- numeral m + - 1 = - numeral (inc m)" |
459 "1 + - 1 = 0" |
472 "1 + - 1 = 0" |
460 "- 1 + 1 = 0" |
473 "- 1 + 1 = 0" |
461 "- 1 + - 1 = - 2" |
474 "- 1 + - 1 = - 2" |
462 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc |
475 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc |
463 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
476 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
464 |
477 |
465 lemma diff_numeral_simps: |
478 lemma diff_numeral_simps: |
466 "numeral m - numeral n = sub m n" |
479 "numeral m - numeral n = sub m n" |
467 "numeral m - - numeral n = numeral (m + n)" |
480 "numeral m - - numeral n = numeral (m + n)" |
468 "- numeral m - numeral n = - numeral (m + n)" |
481 "- numeral m - numeral n = - numeral (m + n)" |
469 "- numeral m - - numeral n = sub n m" |
482 "- numeral m - - numeral n = sub n m" |
470 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
483 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
471 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
484 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
472 |
485 |
473 lemma diff_numeral_special: |
486 lemma diff_numeral_special: |
474 "1 - numeral n = sub One n" |
487 "1 - numeral n = sub One n" |
475 "numeral m - 1 = sub m One" |
488 "numeral m - 1 = sub m One" |
476 "1 - - numeral n = numeral (One + n)" |
489 "1 - - numeral n = numeral (One + n)" |
482 "1 - 1 = 0" |
495 "1 - 1 = 0" |
483 "- 1 - 1 = - 2" |
496 "- 1 - 1 = - 2" |
484 "1 - - 1 = 2" |
497 "1 - - 1 = 2" |
485 "- 1 - - 1 = 0" |
498 "- 1 - - 1 = 0" |
486 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc |
499 by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc |
487 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
500 del: add_uminus_conv_diff add: diff_conv_add_uminus) |
488 |
501 |
489 end |
502 end |
490 |
503 |
491 subsubsection \<open> |
504 |
492 Structures with multiplication: class \<open>semiring_numeral\<close> |
505 subsubsection \<open>Structures with multiplication: class \<open>semiring_numeral\<close>\<close> |
493 \<close> |
|
494 |
506 |
495 class semiring_numeral = semiring + monoid_mult |
507 class semiring_numeral = semiring + monoid_mult |
496 begin |
508 begin |
497 |
509 |
498 subclass numeral .. |
510 subclass numeral .. |
499 |
511 |
500 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n" |
512 lemma numeral_mult: "numeral (m * n) = numeral m * numeral n" |
501 apply (induct n rule: num_induct) |
513 by (induct n rule: num_induct) |
502 apply (simp add: numeral_One) |
514 (simp_all add: numeral_One mult_inc numeral_inc numeral_add distrib_left) |
503 apply (simp add: mult_inc numeral_inc numeral_add distrib_left) |
|
504 done |
|
505 |
515 |
506 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)" |
516 lemma numeral_times_numeral: "numeral m * numeral n = numeral (m * n)" |
507 by (rule numeral_mult [symmetric]) |
517 by (rule numeral_mult [symmetric]) |
508 |
518 |
509 lemma mult_2: "2 * z = z + z" |
519 lemma mult_2: "2 * z = z + z" |
510 unfolding one_add_one [symmetric] distrib_right by simp |
520 by (simp add: one_add_one [symmetric] distrib_right) |
511 |
521 |
512 lemma mult_2_right: "z * 2 = z + z" |
522 lemma mult_2_right: "z * 2 = z + z" |
513 unfolding one_add_one [symmetric] distrib_left by simp |
523 by (simp add: one_add_one [symmetric] distrib_left) |
514 |
524 |
515 end |
525 end |
516 |
526 |
517 subsubsection \<open> |
527 |
518 Structures with a zero: class \<open>semiring_1\<close> |
528 subsubsection \<open>Structures with a zero: class \<open>semiring_1\<close>\<close> |
519 \<close> |
|
520 |
529 |
521 context semiring_1 |
530 context semiring_1 |
522 begin |
531 begin |
523 |
532 |
524 subclass semiring_numeral .. |
533 subclass semiring_numeral .. |
525 |
534 |
526 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
535 lemma of_nat_numeral [simp]: "of_nat (numeral n) = numeral n" |
527 by (induct n, |
536 by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
528 simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
537 |
529 |
538 end |
530 end |
539 |
531 |
540 lemma nat_of_num_numeral [code_abbrev]: "nat_of_num = numeral" |
532 lemma nat_of_num_numeral [code_abbrev]: |
|
533 "nat_of_num = numeral" |
|
534 proof |
541 proof |
535 fix n |
542 fix n |
536 have "numeral n = nat_of_num n" |
543 have "numeral n = nat_of_num n" |
537 by (induct n) (simp_all add: numeral.simps) |
544 by (induct n) (simp_all add: numeral.simps) |
538 then show "nat_of_num n = numeral n" by simp |
545 then show "nat_of_num n = numeral n" |
|
546 by simp |
539 qed |
547 qed |
540 |
548 |
541 lemma nat_of_num_code [code]: |
549 lemma nat_of_num_code [code]: |
542 "nat_of_num One = 1" |
550 "nat_of_num One = 1" |
543 "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)" |
551 "nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)" |
544 "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))" |
552 "nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))" |
545 by (simp_all add: Let_def) |
553 by (simp_all add: Let_def) |
546 |
554 |
547 subsubsection \<open> |
555 |
548 Equality: class \<open>semiring_char_0\<close> |
556 subsubsection \<open>Equality: class \<open>semiring_char_0\<close>\<close> |
549 \<close> |
|
550 |
557 |
551 context semiring_char_0 |
558 context semiring_char_0 |
552 begin |
559 begin |
553 |
560 |
554 lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n" |
561 lemma numeral_eq_iff: "numeral m = numeral n \<longleftrightarrow> m = n" |
555 unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] |
562 by (simp only: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] |
556 of_nat_eq_iff num_eq_iff .. |
563 of_nat_eq_iff num_eq_iff) |
557 |
564 |
558 lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One" |
565 lemma numeral_eq_one_iff: "numeral n = 1 \<longleftrightarrow> n = One" |
559 by (rule numeral_eq_iff [of n One, unfolded numeral_One]) |
566 by (rule numeral_eq_iff [of n One, unfolded numeral_One]) |
560 |
567 |
561 lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n" |
568 lemma one_eq_numeral_iff: "1 = numeral n \<longleftrightarrow> One = n" |
562 by (rule numeral_eq_iff [of One n, unfolded numeral_One]) |
569 by (rule numeral_eq_iff [of One n, unfolded numeral_One]) |
563 |
570 |
564 lemma numeral_neq_zero: "numeral n \<noteq> 0" |
571 lemma numeral_neq_zero: "numeral n \<noteq> 0" |
565 unfolding of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] |
572 by (simp add: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] nat_of_num_pos) |
566 by (simp add: nat_of_num_pos) |
|
567 |
573 |
568 lemma zero_neq_numeral: "0 \<noteq> numeral n" |
574 lemma zero_neq_numeral: "0 \<noteq> numeral n" |
569 unfolding eq_commute [of 0] by (rule numeral_neq_zero) |
575 unfolding eq_commute [of 0] by (rule numeral_neq_zero) |
570 |
576 |
571 lemmas eq_numeral_simps [simp] = |
577 lemmas eq_numeral_simps [simp] = |
575 numeral_neq_zero |
581 numeral_neq_zero |
576 zero_neq_numeral |
582 zero_neq_numeral |
577 |
583 |
578 end |
584 end |
579 |
585 |
580 subsubsection \<open> |
586 |
581 Comparisons: class \<open>linordered_semidom\<close> |
587 subsubsection \<open>Comparisons: class \<open>linordered_semidom\<close>\<close> |
582 \<close> |
|
583 |
588 |
584 text \<open>Could be perhaps more general than here.\<close> |
589 text \<open>Could be perhaps more general than here.\<close> |
585 |
590 |
586 context linordered_semidom |
591 context linordered_semidom |
587 begin |
592 begin |
588 |
593 |
589 lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n" |
594 lemma numeral_le_iff: "numeral m \<le> numeral n \<longleftrightarrow> m \<le> n" |
590 proof - |
595 proof - |
591 have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n" |
596 have "of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n" |
592 unfolding less_eq_num_def nat_of_num_numeral of_nat_le_iff .. |
597 by (simp only: less_eq_num_def nat_of_num_numeral of_nat_le_iff) |
593 then show ?thesis by simp |
598 then show ?thesis by simp |
594 qed |
599 qed |
595 |
600 |
596 lemma one_le_numeral: "1 \<le> numeral n" |
601 lemma one_le_numeral: "1 \<le> numeral n" |
597 using numeral_le_iff [of One n] by (simp add: numeral_One) |
602 using numeral_le_iff [of One n] by (simp add: numeral_One) |
598 |
603 |
599 lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One" |
604 lemma numeral_le_one_iff: "numeral n \<le> 1 \<longleftrightarrow> n \<le> One" |
600 using numeral_le_iff [of n One] by (simp add: numeral_One) |
605 using numeral_le_iff [of n One] by (simp add: numeral_One) |
601 |
606 |
602 lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n" |
607 lemma numeral_less_iff: "numeral m < numeral n \<longleftrightarrow> m < n" |
603 proof - |
608 proof - |
604 have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n" |
609 have "of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n" |
605 unfolding less_num_def nat_of_num_numeral of_nat_less_iff .. |
610 unfolding less_num_def nat_of_num_numeral of_nat_less_iff .. |
645 not_numeral_less_one |
650 not_numeral_less_one |
646 zero_less_numeral |
651 zero_less_numeral |
647 not_numeral_less_zero |
652 not_numeral_less_zero |
648 |
653 |
649 lemma min_0_1 [simp]: |
654 lemma min_0_1 [simp]: |
650 fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "min' \<equiv> min" shows |
655 fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
651 "min' 0 1 = 0" |
656 defines "min' \<equiv> min" |
652 "min' 1 0 = 0" |
657 shows |
653 "min' 0 (numeral x) = 0" |
658 "min' 0 1 = 0" |
654 "min' (numeral x) 0 = 0" |
659 "min' 1 0 = 0" |
655 "min' 1 (numeral x) = 1" |
660 "min' 0 (numeral x) = 0" |
656 "min' (numeral x) 1 = 1" |
661 "min' (numeral x) 0 = 0" |
657 by(simp_all add: min'_def min_def le_num_One_iff) |
662 "min' 1 (numeral x) = 1" |
658 |
663 "min' (numeral x) 1 = 1" |
659 lemma max_0_1 [simp]: |
664 by (simp_all add: min'_def min_def le_num_One_iff) |
660 fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "max' \<equiv> max" shows |
665 |
661 "max' 0 1 = 1" |
666 lemma max_0_1 [simp]: |
662 "max' 1 0 = 1" |
667 fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
663 "max' 0 (numeral x) = numeral x" |
668 defines "max' \<equiv> max" |
664 "max' (numeral x) 0 = numeral x" |
669 shows |
665 "max' 1 (numeral x) = numeral x" |
670 "max' 0 1 = 1" |
666 "max' (numeral x) 1 = numeral x" |
671 "max' 1 0 = 1" |
667 by(simp_all add: max'_def max_def le_num_One_iff) |
672 "max' 0 (numeral x) = numeral x" |
668 |
673 "max' (numeral x) 0 = numeral x" |
669 end |
674 "max' 1 (numeral x) = numeral x" |
670 |
675 "max' (numeral x) 1 = numeral x" |
671 subsubsection \<open> |
676 by (simp_all add: max'_def max_def le_num_One_iff) |
672 Multiplication and negation: class \<open>ring_1\<close> |
677 |
673 \<close> |
678 end |
|
679 |
|
680 |
|
681 subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close> |
674 |
682 |
675 context ring_1 |
683 context ring_1 |
676 begin |
684 begin |
677 |
685 |
678 subclass neg_numeral .. |
686 subclass neg_numeral .. |
679 |
687 |
680 lemma mult_neg_numeral_simps: |
688 lemma mult_neg_numeral_simps: |
681 "- numeral m * - numeral n = numeral (m * n)" |
689 "- numeral m * - numeral n = numeral (m * n)" |
682 "- numeral m * numeral n = - numeral (m * n)" |
690 "- numeral m * numeral n = - numeral (m * n)" |
683 "numeral m * - numeral n = - numeral (m * n)" |
691 "numeral m * - numeral n = - numeral (m * n)" |
684 unfolding mult_minus_left mult_minus_right |
692 by (simp_all only: mult_minus_left mult_minus_right minus_minus numeral_mult) |
685 by (simp_all only: minus_minus numeral_mult) |
|
686 |
693 |
687 lemma mult_minus1 [simp]: "- 1 * z = - z" |
694 lemma mult_minus1 [simp]: "- 1 * z = - z" |
688 unfolding numeral.simps mult_minus_left by simp |
695 by (simp add: numeral.simps) |
689 |
696 |
690 lemma mult_minus1_right [simp]: "z * - 1 = - z" |
697 lemma mult_minus1_right [simp]: "z * - 1 = - z" |
691 unfolding numeral.simps mult_minus_right by simp |
698 by (simp add: numeral.simps) |
692 |
699 |
693 end |
700 end |
694 |
701 |
695 subsubsection \<open> |
702 |
696 Equality using \<open>iszero\<close> for rings with non-zero characteristic |
703 subsubsection \<open>Equality using \<open>iszero\<close> for rings with non-zero characteristic\<close> |
697 \<close> |
|
698 |
704 |
699 context ring_1 |
705 context ring_1 |
700 begin |
706 begin |
701 |
707 |
702 definition iszero :: "'a \<Rightarrow> bool" |
708 definition iszero :: "'a \<Rightarrow> bool" |
715 by (simp add: iszero_def) |
721 by (simp add: iszero_def) |
716 |
722 |
717 lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)" |
723 lemma not_iszero_neg_Numeral1: "\<not> iszero (- Numeral1)" |
718 by (simp add: numeral_One) |
724 by (simp add: numeral_One) |
719 |
725 |
720 lemma iszero_neg_numeral [simp]: |
726 lemma iszero_neg_numeral [simp]: "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)" |
721 "iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)" |
727 unfolding iszero_def by (rule neg_equal_0_iff_equal) |
722 unfolding iszero_def |
|
723 by (rule neg_equal_0_iff_equal) |
|
724 |
728 |
725 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)" |
729 lemma eq_iff_iszero_diff: "x = y \<longleftrightarrow> iszero (x - y)" |
726 unfolding iszero_def by (rule eq_iff_diff_eq_0) |
730 unfolding iszero_def by (rule eq_iff_diff_eq_0) |
727 |
731 |
728 text \<open>The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared |
732 text \<open> |
729 \<open>[simp]\<close> by default, because for rings of characteristic zero, |
733 The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared \<open>[simp]\<close> by default, |
730 better simp rules are possible. For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules should be added to the |
734 because for rings of characteristic zero, better simp rules are possible. |
731 simplifier, along with a type-specific rule for deciding propositions |
735 For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules |
732 of the form \<open>iszero (numeral w)\<close>. |
736 should be added to the simplifier, along with a type-specific rule for |
733 |
737 deciding propositions of the form \<open>iszero (numeral w)\<close>. |
734 bh: Maybe it would not be so bad to just declare these as simp |
738 |
735 rules anyway? I should test whether these rules take precedence over |
739 bh: Maybe it would not be so bad to just declare these as simp rules anyway? |
736 the \<open>ring_char_0\<close> rules in the simplifier. |
740 I should test whether these rules take precedence over the \<open>ring_char_0\<close> |
|
741 rules in the simplifier. |
737 \<close> |
742 \<close> |
738 |
743 |
739 lemma eq_numeral_iff_iszero: |
744 lemma eq_numeral_iff_iszero: |
740 "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)" |
745 "numeral x = numeral y \<longleftrightarrow> iszero (sub x y)" |
741 "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))" |
746 "numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))" |
766 |
770 |
767 lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n" |
771 lemma neg_numeral_eq_iff: "- numeral m = - numeral n \<longleftrightarrow> m = n" |
768 by simp |
772 by simp |
769 |
773 |
770 lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n" |
774 lemma numeral_neq_neg_numeral: "numeral m \<noteq> - numeral n" |
771 unfolding eq_neg_iff_add_eq_0 |
775 by (simp add: eq_neg_iff_add_eq_0 numeral_plus_numeral) |
772 by (simp add: numeral_plus_numeral) |
|
773 |
776 |
774 lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n" |
777 lemma neg_numeral_neq_numeral: "- numeral m \<noteq> numeral n" |
775 by (rule numeral_neq_neg_numeral [symmetric]) |
778 by (rule numeral_neq_neg_numeral [symmetric]) |
776 |
779 |
777 lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n" |
780 lemma zero_neq_neg_numeral: "0 \<noteq> - numeral n" |
778 unfolding neg_0_equal_iff_equal by simp |
781 by simp |
779 |
782 |
780 lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0" |
783 lemma neg_numeral_neq_zero: "- numeral n \<noteq> 0" |
781 unfolding neg_equal_0_iff_equal by simp |
784 by simp |
782 |
785 |
783 lemma one_neq_neg_numeral: "1 \<noteq> - numeral n" |
786 lemma one_neq_neg_numeral: "1 \<noteq> - numeral n" |
784 using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One) |
787 using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One) |
785 |
788 |
786 lemma neg_numeral_neq_one: "- numeral n \<noteq> 1" |
789 lemma neg_numeral_neq_one: "- numeral n \<noteq> 1" |
787 using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One) |
790 using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One) |
788 |
791 |
789 lemma neg_one_neq_numeral: |
792 lemma neg_one_neq_numeral: "- 1 \<noteq> numeral n" |
790 "- 1 \<noteq> numeral n" |
|
791 using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One) |
793 using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One) |
792 |
794 |
793 lemma numeral_neq_neg_one: |
795 lemma numeral_neq_neg_one: "numeral n \<noteq> - 1" |
794 "numeral n \<noteq> - 1" |
|
795 using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One) |
796 using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One) |
796 |
797 |
797 lemma neg_one_eq_numeral_iff: |
798 lemma neg_one_eq_numeral_iff: "- 1 = - numeral n \<longleftrightarrow> n = One" |
798 "- 1 = - numeral n \<longleftrightarrow> n = One" |
|
799 using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One) |
799 using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One) |
800 |
800 |
801 lemma numeral_eq_neg_one_iff: |
801 lemma numeral_eq_neg_one_iff: "- numeral n = - 1 \<longleftrightarrow> n = One" |
802 "- numeral n = - 1 \<longleftrightarrow> n = One" |
|
803 using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One) |
802 using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One) |
804 |
803 |
805 lemma neg_one_neq_zero: |
804 lemma neg_one_neq_zero: "- 1 \<noteq> 0" |
806 "- 1 \<noteq> 0" |
805 by simp |
807 by simp |
806 |
808 |
807 lemma zero_neq_neg_one: "0 \<noteq> - 1" |
809 lemma zero_neq_neg_one: |
808 by simp |
810 "0 \<noteq> - 1" |
809 |
811 by simp |
810 lemma neg_one_neq_one: "- 1 \<noteq> 1" |
812 |
|
813 lemma neg_one_neq_one: |
|
814 "- 1 \<noteq> 1" |
|
815 using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
811 using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
816 |
812 |
817 lemma one_neq_neg_one: |
813 lemma one_neq_neg_one: "1 \<noteq> - 1" |
818 "1 \<noteq> - 1" |
|
819 using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
814 using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
820 |
815 |
821 lemmas eq_neg_numeral_simps [simp] = |
816 lemmas eq_neg_numeral_simps [simp] = |
822 neg_numeral_eq_iff |
817 neg_numeral_eq_iff |
823 numeral_neq_neg_numeral neg_numeral_neq_numeral |
818 numeral_neq_neg_numeral neg_numeral_neq_numeral |
867 lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n" |
860 lemma not_numeral_less_neg_numeral: "\<not> numeral m < - numeral n" |
868 by (simp only: not_less neg_numeral_le_numeral) |
861 by (simp only: not_less neg_numeral_le_numeral) |
869 |
862 |
870 lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n" |
863 lemma not_numeral_le_neg_numeral: "\<not> numeral m \<le> - numeral n" |
871 by (simp only: not_le neg_numeral_less_numeral) |
864 by (simp only: not_le neg_numeral_less_numeral) |
872 |
865 |
873 lemma neg_numeral_less_one: "- numeral m < 1" |
866 lemma neg_numeral_less_one: "- numeral m < 1" |
874 by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One]) |
867 by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One]) |
875 |
868 |
876 lemma neg_numeral_le_one: "- numeral m \<le> 1" |
869 lemma neg_numeral_le_one: "- numeral m \<le> 1" |
877 by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One]) |
870 by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One]) |
904 by simp |
897 by simp |
905 |
898 |
906 lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One" |
899 lemma not_neg_one_le_neg_numeral_iff: "\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One" |
907 by (cases m) simp_all |
900 by (cases m) simp_all |
908 |
901 |
909 lemma sub_non_negative: |
902 lemma sub_non_negative: "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m" |
910 "sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m" |
|
911 by (simp only: sub_def le_diff_eq) simp |
903 by (simp only: sub_def le_diff_eq) simp |
912 |
904 |
913 lemma sub_positive: |
905 lemma sub_positive: "sub n m > 0 \<longleftrightarrow> n > m" |
914 "sub n m > 0 \<longleftrightarrow> n > m" |
|
915 by (simp only: sub_def less_diff_eq) simp |
906 by (simp only: sub_def less_diff_eq) simp |
916 |
907 |
917 lemma sub_non_positive: |
908 lemma sub_non_positive: "sub n m \<le> 0 \<longleftrightarrow> n \<le> m" |
918 "sub n m \<le> 0 \<longleftrightarrow> n \<le> m" |
|
919 by (simp only: sub_def diff_le_eq) simp |
909 by (simp only: sub_def diff_le_eq) simp |
920 |
910 |
921 lemma sub_negative: |
911 lemma sub_negative: "sub n m < 0 \<longleftrightarrow> n < m" |
922 "sub n m < 0 \<longleftrightarrow> n < m" |
|
923 by (simp only: sub_def diff_less_eq) simp |
912 by (simp only: sub_def diff_less_eq) simp |
924 |
913 |
925 lemmas le_neg_numeral_simps [simp] = |
914 lemmas le_neg_numeral_simps [simp] = |
926 neg_numeral_le_iff |
915 neg_numeral_le_iff |
927 neg_numeral_le_numeral not_numeral_le_neg_numeral |
916 neg_numeral_le_numeral not_numeral_le_neg_numeral |
987 |
975 |
988 lemma pred_numeral_simps [simp]: |
976 lemma pred_numeral_simps [simp]: |
989 "pred_numeral One = 0" |
977 "pred_numeral One = 0" |
990 "pred_numeral (Bit0 k) = numeral (BitM k)" |
978 "pred_numeral (Bit0 k) = numeral (BitM k)" |
991 "pred_numeral (Bit1 k) = numeral (Bit0 k)" |
979 "pred_numeral (Bit1 k) = numeral (Bit0 k)" |
992 unfolding pred_numeral_def eval_nat_numeral |
980 by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0) |
993 by (simp_all only: diff_Suc_Suc diff_0) |
|
994 |
981 |
995 lemma numeral_2_eq_2: "2 = Suc (Suc 0)" |
982 lemma numeral_2_eq_2: "2 = Suc (Suc 0)" |
996 by (simp add: eval_nat_numeral) |
983 by (simp add: eval_nat_numeral) |
997 |
984 |
998 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))" |
985 lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))" |
999 by (simp add: eval_nat_numeral) |
986 by (simp add: eval_nat_numeral) |
1000 |
987 |
1001 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" |
988 lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" |
1002 by (simp only: numeral_One One_nat_def) |
989 by (simp only: numeral_One One_nat_def) |
1003 |
990 |
1004 lemma Suc_nat_number_of_add: |
991 lemma Suc_nat_number_of_add: "Suc (numeral v + n) = numeral (v + One) + n" |
1005 "Suc (numeral v + n) = numeral (v + One) + n" |
992 by simp |
1006 by simp |
993 |
1007 |
994 lemma numerals: "Numeral1 = (1::nat)" "2 = Suc (Suc 0)" |
1008 (*Maps #n to n for n = 1, 2*) |
995 by (rule numeral_One) (rule numeral_2_eq_2) |
1009 lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2 |
|
1010 |
996 |
1011 text \<open>Comparisons involving @{term Suc}.\<close> |
997 text \<open>Comparisons involving @{term Suc}.\<close> |
1012 |
998 |
1013 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n" |
999 lemma eq_numeral_Suc [simp]: "numeral k = Suc n \<longleftrightarrow> pred_numeral k = n" |
1014 by (simp add: numeral_eq_Suc) |
1000 by (simp add: numeral_eq_Suc) |
1032 by (simp add: numeral_eq_Suc) |
1018 by (simp add: numeral_eq_Suc) |
1033 |
1019 |
1034 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n" |
1020 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n" |
1035 by (simp add: numeral_eq_Suc) |
1021 by (simp add: numeral_eq_Suc) |
1036 |
1022 |
1037 lemma max_Suc_numeral [simp]: |
1023 lemma max_Suc_numeral [simp]: "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))" |
1038 "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))" |
1024 by (simp add: numeral_eq_Suc) |
1039 by (simp add: numeral_eq_Suc) |
1025 |
1040 |
1026 lemma max_numeral_Suc [simp]: "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)" |
1041 lemma max_numeral_Suc [simp]: |
1027 by (simp add: numeral_eq_Suc) |
1042 "max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)" |
1028 |
1043 by (simp add: numeral_eq_Suc) |
1029 lemma min_Suc_numeral [simp]: "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))" |
1044 |
1030 by (simp add: numeral_eq_Suc) |
1045 lemma min_Suc_numeral [simp]: |
1031 |
1046 "min (Suc n) (numeral k) = Suc (min n (pred_numeral k))" |
1032 lemma min_numeral_Suc [simp]: "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)" |
1047 by (simp add: numeral_eq_Suc) |
|
1048 |
|
1049 lemma min_numeral_Suc [simp]: |
|
1050 "min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)" |
|
1051 by (simp add: numeral_eq_Suc) |
1033 by (simp add: numeral_eq_Suc) |
1052 |
1034 |
1053 text \<open>For @{term case_nat} and @{term rec_nat}.\<close> |
1035 text \<open>For @{term case_nat} and @{term rec_nat}.\<close> |
1054 |
1036 |
1055 lemma case_nat_numeral [simp]: |
1037 lemma case_nat_numeral [simp]: "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)" |
1056 "case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)" |
|
1057 by (simp add: numeral_eq_Suc) |
1038 by (simp add: numeral_eq_Suc) |
1058 |
1039 |
1059 lemma case_nat_add_eq_if [simp]: |
1040 lemma case_nat_add_eq_if [simp]: |
1060 "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))" |
1041 "case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))" |
1061 by (simp add: numeral_eq_Suc) |
1042 by (simp add: numeral_eq_Suc) |
1062 |
1043 |
1063 lemma rec_nat_numeral [simp]: |
1044 lemma rec_nat_numeral [simp]: |
1064 "rec_nat a f (numeral v) = |
1045 "rec_nat a f (numeral v) = (let pv = pred_numeral v in f pv (rec_nat a f pv))" |
1065 (let pv = pred_numeral v in f pv (rec_nat a f pv))" |
|
1066 by (simp add: numeral_eq_Suc Let_def) |
1046 by (simp add: numeral_eq_Suc Let_def) |
1067 |
1047 |
1068 lemma rec_nat_add_eq_if [simp]: |
1048 lemma rec_nat_add_eq_if [simp]: |
1069 "rec_nat a f (numeral v + n) = |
1049 "rec_nat a f (numeral v + n) = (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))" |
1070 (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))" |
|
1071 by (simp add: numeral_eq_Suc Let_def) |
1050 by (simp add: numeral_eq_Suc Let_def) |
1072 |
1051 |
1073 text \<open>Case analysis on @{term "n < 2"}\<close> |
1052 text \<open>Case analysis on @{term "n < 2"}.\<close> |
1074 |
|
1075 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
1053 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
1076 by (auto simp add: numeral_2_eq_2) |
1054 by (auto simp add: numeral_2_eq_2) |
1077 |
1055 |
1078 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2\<close> |
1056 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close> |
1079 text \<open>bh: Are these rules really a good idea?\<close> |
1057 text \<open>bh: Are these rules really a good idea?\<close> |
1080 |
1058 |
1081 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
1059 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
1082 by simp |
1060 by simp |
1083 |
1061 |
1084 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
1062 lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
1085 by simp |
1063 by simp |
1086 |
1064 |
1087 text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close> |
1065 text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close> |
1088 |
|
1089 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
1066 lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
1090 by simp |
1067 by simp |
1091 |
1068 |
1092 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) |
1069 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) |
1093 |
1070 |
1122 declare (in semiring_numeral) numeral_times_numeral [simp] |
1097 declare (in semiring_numeral) numeral_times_numeral [simp] |
1123 declare (in ring_1) mult_neg_numeral_simps [simp] |
1098 declare (in ring_1) mult_neg_numeral_simps [simp] |
1124 |
1099 |
1125 subsection \<open>Setting up simprocs\<close> |
1100 subsection \<open>Setting up simprocs\<close> |
1126 |
1101 |
1127 lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)" |
1102 lemma mult_numeral_1: "Numeral1 * a = a" |
1128 by simp |
1103 for a :: "'a::semiring_numeral" |
1129 |
1104 by simp |
1130 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::semiring_numeral)" |
1105 |
1131 by simp |
1106 lemma mult_numeral_1_right: "a * Numeral1 = a" |
1132 |
1107 for a :: "'a::semiring_numeral" |
1133 lemma divide_numeral_1: "a / Numeral1 = (a::'a::field)" |
1108 by simp |
1134 by simp |
1109 |
1135 |
1110 lemma divide_numeral_1: "a / Numeral1 = a" |
1136 lemma inverse_numeral_1: |
1111 for a :: "'a::field" |
1137 "inverse Numeral1 = (Numeral1::'a::division_ring)" |
1112 by simp |
1138 by simp |
1113 |
1139 |
1114 lemma inverse_numeral_1: "inverse Numeral1 = (Numeral1::'a::division_ring)" |
1140 text\<open>Theorem lists for the cancellation simprocs. The use of a binary |
1115 by simp |
1141 numeral for 1 reduces the number of special cases.\<close> |
1116 |
|
1117 text \<open> |
|
1118 Theorem lists for the cancellation simprocs. The use of a binary |
|
1119 numeral for 1 reduces the number of special cases. |
|
1120 \<close> |
1142 |
1121 |
1143 lemma mult_1s: |
1122 lemma mult_1s: |
1144 fixes a :: "'a::semiring_numeral" |
1123 "Numeral1 * a = a" |
1145 and b :: "'b::ring_1" |
1124 "a * Numeral1 = a" |
1146 shows "Numeral1 * a = a" |
1125 "- Numeral1 * b = - b" |
1147 "a * Numeral1 = a" |
1126 "b * - Numeral1 = - b" |
1148 "- Numeral1 * b = - b" |
1127 for a :: "'a::semiring_numeral" and b :: "'b::ring_1" |
1149 "b * - Numeral1 = - b" |
|
1150 by simp_all |
1128 by simp_all |
1151 |
1129 |
1152 setup \<open> |
1130 setup \<open> |
1153 Reorient_Proc.add |
1131 Reorient_Proc.add |
1154 (fn Const (@{const_name numeral}, _) $ _ => true |
1132 (fn Const (@{const_name numeral}, _) $ _ => true |
1155 | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true |
1133 | Const (@{const_name uminus}, _) $ (Const (@{const_name numeral}, _) $ _) => true |
1156 | _ => false) |
1134 | _ => false) |
1157 \<close> |
1135 \<close> |
1158 |
1136 |
1159 simproc_setup reorient_numeral |
1137 simproc_setup reorient_numeral ("numeral w = x" | "- numeral w = y") = |
1160 ("numeral w = x" | "- numeral w = y") = Reorient_Proc.proc |
1138 Reorient_Proc.proc |
1161 |
1139 |
1162 |
1140 |
1163 subsubsection \<open>Simplification of arithmetic operations on integer constants.\<close> |
1141 subsubsection \<open>Simplification of arithmetic operations on integer constants\<close> |
1164 |
1142 |
1165 lemmas arith_special = (* already declared simp above *) |
1143 lemmas arith_special = (* already declared simp above *) |
1166 add_numeral_special add_neg_numeral_special |
1144 add_numeral_special add_neg_numeral_special |
1167 diff_numeral_special |
1145 diff_numeral_special |
1168 |
1146 |
1169 (* rules already in simpset *) |
1147 lemmas arith_extra_simps = (* rules already in simpset *) |
1170 lemmas arith_extra_simps = |
|
1171 numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right |
1148 numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right |
1172 minus_zero |
1149 minus_zero |
1173 diff_numeral_simps diff_0 diff_0_right |
1150 diff_numeral_simps diff_0 diff_0_right |
1174 numeral_times_numeral mult_neg_numeral_simps |
1151 numeral_times_numeral mult_neg_numeral_simps |
1175 mult_zero_left mult_zero_right |
1152 mult_zero_left mult_zero_right |
1213 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)" |
1190 lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)" |
1214 \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> |
1191 \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> |
1215 unfolding Let_def .. |
1192 unfolding Let_def .. |
1216 |
1193 |
1217 declaration \<open> |
1194 declaration \<open> |
1218 let |
1195 let |
1219 fun number_of ctxt T n = |
1196 fun number_of ctxt T n = |
1220 if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral})) |
1197 if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral})) |
1221 then raise CTERM ("number_of", []) |
1198 then raise CTERM ("number_of", []) |
1222 else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; |
1199 else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; |
1223 in |
1200 in |
1224 K ( |
1201 K ( |
1225 Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps} |
1202 Lin_Arith.add_simps |
1226 @ @{thms rel_simps} |
1203 @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps |
1227 @ @{thms pred_numeral_simps} |
1204 arith_special numeral_One of_nat_simps} |
1228 @ @{thms arith_special numeral_One} |
1205 #> Lin_Arith.add_simps |
1229 @ @{thms of_nat_simps}) |
1206 @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1 |
1230 #> Lin_Arith.add_simps [@{thm Suc_numeral}, |
1207 le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc |
1231 @{thm Let_numeral}, @{thm Let_neg_numeral}, @{thm Let_0}, @{thm Let_1}, |
1208 Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral} |
1232 @{thm le_Suc_numeral}, @{thm le_numeral_Suc}, |
|
1233 @{thm less_Suc_numeral}, @{thm less_numeral_Suc}, |
|
1234 @{thm Suc_eq_numeral}, @{thm eq_numeral_Suc}, |
|
1235 @{thm mult_Suc}, @{thm mult_Suc_right}, |
|
1236 @{thm of_nat_numeral}] |
|
1237 #> Lin_Arith.set_number_of number_of) |
1209 #> Lin_Arith.set_number_of number_of) |
1238 end |
1210 end |
1239 \<close> |
1211 \<close> |
1240 |
1212 |
1241 |
1213 |
1242 subsubsection \<open>Simplification of arithmetic when nested to the right.\<close> |
1214 subsubsection \<open>Simplification of arithmetic when nested to the right\<close> |
1243 |
1215 |
1244 lemma add_numeral_left [simp]: |
1216 lemma add_numeral_left [simp]: "numeral v + (numeral w + z) = (numeral(v + w) + z)" |
1245 "numeral v + (numeral w + z) = (numeral(v + w) + z)" |
|
1246 by (simp_all add: add.assoc [symmetric]) |
1217 by (simp_all add: add.assoc [symmetric]) |
1247 |
1218 |
1248 lemma add_neg_numeral_left [simp]: |
1219 lemma add_neg_numeral_left [simp]: |
1249 "numeral v + (- numeral w + y) = (sub v w + y)" |
1220 "numeral v + (- numeral w + y) = (sub v w + y)" |
1250 "- numeral v + (numeral w + y) = (sub w v + y)" |
1221 "- numeral v + (numeral w + y) = (sub w v + y)" |