src/HOL/Numeral.thy
 author haftmann Tue Jul 10 17:30:49 2007 +0200 (2007-07-10) changeset 23708 b5eb0b4dd17d parent 23574 42765aff66d6 child 23855 b1a754e544b6 permissions -rw-r--r--
clarified import
1 (*  Title:      HOL/Numeral.thy
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1994  University of Cambridge
5 *)
7 header {* Arithmetic on Binary Integers *}
9 theory Numeral
10 imports Datatype IntDef
11 uses
12   ("Tools/numeral.ML")
13   ("Tools/numeral_syntax.ML")
14 begin
16 subsection {* Binary representation *}
18 text {*
19   This formalization defines binary arithmetic in terms of the integers
20   rather than using a datatype. This avoids multiple representations (leading
21   zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
22   int_of_binary}, for the numerical interpretation.
24   The representation expects that @{text "(m mod 2)"} is 0 or 1,
25   even if m is negative;
26   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
27   @{text "-5 = (-3)*2 + 1"}.
28 *}
30 datatype bit = B0 | B1
32 text{*
33   Type @{typ bit} avoids the use of type @{typ bool}, which would make
34   all of the rewrite rules higher-order.
35 *}
37 definition
38   Pls :: int where
39   [code func del]:"Pls = 0"
41 definition
42   Min :: int where
43   [code func del]:"Min = - 1"
45 definition
46   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
47   [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
49 class number = type + -- {* for numeric types: nat, int, real, \dots *}
50   fixes number_of :: "int \<Rightarrow> 'a"
52 use "Tools/numeral.ML"
54 syntax
55   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
57 use "Tools/numeral_syntax.ML"
58 setup NumeralSyntax.setup
60 abbreviation
61   "Numeral0 \<equiv> number_of Pls"
63 abbreviation
64   "Numeral1 \<equiv> number_of (Pls BIT B1)"
66 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
67   -- {* Unfold all @{text let}s involving constants *}
68   unfolding Let_def ..
70 lemma Let_0 [simp]: "Let 0 f = f 0"
71   unfolding Let_def ..
73 lemma Let_1 [simp]: "Let 1 f = f 1"
74   unfolding Let_def ..
76 definition
77   succ :: "int \<Rightarrow> int" where
78   [code func del]: "succ k = k + 1"
80 definition
81   pred :: "int \<Rightarrow> int" where
82   [code func del]: "pred k = k - 1"
84 lemmas
85   max_number_of [simp] = max_def
86     [of "number_of u" "number_of v", standard, simp]
87 and
88   min_number_of [simp] = min_def
89     [of "number_of u" "number_of v", standard, simp]
90   -- {* unfolding @{text minx} and @{text max} on numerals *}
92 lemmas numeral_simps =
93   succ_def pred_def Pls_def Min_def Bit_def
95 text {* Removal of leading zeroes *}
97 lemma Pls_0_eq [simp, normal post]:
98   "Pls BIT B0 = Pls"
99   unfolding numeral_simps by simp
101 lemma Min_1_eq [simp, normal post]:
102   "Min BIT B1 = Min"
103   unfolding numeral_simps by simp
106 subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
108 lemma succ_Pls [simp]:
109   "succ Pls = Pls BIT B1"
110   unfolding numeral_simps by simp
112 lemma succ_Min [simp]:
113   "succ Min = Pls"
114   unfolding numeral_simps by simp
116 lemma succ_1 [simp]:
117   "succ (k BIT B1) = succ k BIT B0"
118   unfolding numeral_simps by simp
120 lemma succ_0 [simp]:
121   "succ (k BIT B0) = k BIT B1"
122   unfolding numeral_simps by simp
124 lemma pred_Pls [simp]:
125   "pred Pls = Min"
126   unfolding numeral_simps by simp
128 lemma pred_Min [simp]:
129   "pred Min = Min BIT B0"
130   unfolding numeral_simps by simp
132 lemma pred_1 [simp]:
133   "pred (k BIT B1) = k BIT B0"
134   unfolding numeral_simps by simp
136 lemma pred_0 [simp]:
137   "pred (k BIT B0) = pred k BIT B1"
138   unfolding numeral_simps by simp
140 lemma minus_Pls [simp]:
141   "- Pls = Pls"
142   unfolding numeral_simps by simp
144 lemma minus_Min [simp]:
145   "- Min = Pls BIT B1"
146   unfolding numeral_simps by simp
148 lemma minus_1 [simp]:
149   "- (k BIT B1) = pred (- k) BIT B1"
150   unfolding numeral_simps by simp
152 lemma minus_0 [simp]:
153   "- (k BIT B0) = (- k) BIT B0"
154   unfolding numeral_simps by simp
157 subsection {*
158   Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
159     and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
160 *}
163   "Pls + k = k"
164   unfolding numeral_simps by simp
167   "Min + k = pred k"
168   unfolding numeral_simps by simp
171   "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
172   unfolding numeral_simps by simp
175   "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
176   unfolding numeral_simps by simp
179   "(k BIT B0) + (l BIT b) = (k + l) BIT b"
180   unfolding numeral_simps by simp
183   "k + Pls = k"
184   unfolding numeral_simps by simp
187   "k + Min = pred k"
188   unfolding numeral_simps by simp
190 lemma mult_Pls [simp]:
191   "Pls * w = Pls"
192   unfolding numeral_simps by simp
194 lemma mult_Min [simp]:
195   "Min * k = - k"
196   unfolding numeral_simps by simp
198 lemma mult_num1 [simp]:
199   "(k BIT B1) * l = ((k * l) BIT B0) + l"
200   unfolding numeral_simps int_distrib by simp
202 lemma mult_num0 [simp]:
203   "(k BIT B0) * l = (k * l) BIT B0"
204   unfolding numeral_simps int_distrib by simp
208 subsection {* Converting Numerals to Rings: @{term number_of} *}
210 axclass number_ring \<subseteq> number, comm_ring_1
211   number_of_eq: "number_of k = of_int k"
213 text {* self-embedding of the intergers *}
215 instance int :: number_ring
216   int_number_of_def: "number_of w \<equiv> of_int w"
217   by intro_classes (simp only: int_number_of_def)
219 lemmas [code func del] = int_number_of_def
221 lemma number_of_is_id:
222   "number_of (k::int) = k"
223   unfolding int_number_of_def by simp
225 lemma number_of_succ:
226   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
227   unfolding number_of_eq numeral_simps by simp
229 lemma number_of_pred:
230   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
231   unfolding number_of_eq numeral_simps by simp
233 lemma number_of_minus:
234   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
235   unfolding number_of_eq numeral_simps by simp
238   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
239   unfolding number_of_eq numeral_simps by simp
241 lemma number_of_mult:
242   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
243   unfolding number_of_eq numeral_simps by simp
245 text {*
246   The correctness of shifting.
247   But it doesn't seem to give a measurable speed-up.
248 *}
250 lemma double_number_of_BIT:
251   "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
252   unfolding number_of_eq numeral_simps left_distrib by simp
254 text {*
255   Converting numerals 0 and 1 to their abstract versions.
256 *}
258 lemma numeral_0_eq_0 [simp]:
259   "Numeral0 = (0::'a::number_ring)"
260   unfolding number_of_eq numeral_simps by simp
262 lemma numeral_1_eq_1 [simp]:
263   "Numeral1 = (1::'a::number_ring)"
264   unfolding number_of_eq numeral_simps by simp
266 text {*
267   Special-case simplification for small constants.
268 *}
270 text{*
271   Unary minus for the abstract constant 1. Cannot be inserted
272   as a simprule until later: it is @{text number_of_Min} re-oriented!
273 *}
275 lemma numeral_m1_eq_minus_1:
276   "(-1::'a::number_ring) = - 1"
277   unfolding number_of_eq numeral_simps by simp
279 lemma mult_minus1 [simp]:
280   "-1 * z = -(z::'a::number_ring)"
281   unfolding number_of_eq numeral_simps by simp
283 lemma mult_minus1_right [simp]:
284   "z * -1 = -(z::'a::number_ring)"
285   unfolding number_of_eq numeral_simps by simp
287 (*Negation of a coefficient*)
288 lemma minus_number_of_mult [simp]:
289    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
290    unfolding number_of_eq by simp
292 text {* Subtraction *}
294 lemma diff_number_of_eq:
295   "number_of v - number_of w =
296     (number_of (v + uminus w)::'a::number_ring)"
297   unfolding number_of_eq by simp
299 lemma number_of_Pls:
300   "number_of Pls = (0::'a::number_ring)"
301   unfolding number_of_eq numeral_simps by simp
303 lemma number_of_Min:
304   "number_of Min = (- 1::'a::number_ring)"
305   unfolding number_of_eq numeral_simps by simp
307 lemma number_of_BIT:
308   "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
309     + (number_of w) + (number_of w)"
310   unfolding number_of_eq numeral_simps by (simp split: bit.split)
313 subsection {* Equality of Binary Numbers *}
315 text {* First version by Norbert Voelker *}
317 lemma eq_number_of_eq:
318   "((number_of x::'a::number_ring) = number_of y) =
319    iszero (number_of (x + uminus y) :: 'a)"
323 lemma iszero_number_of_Pls:
324   "iszero ((number_of Pls)::'a::number_ring)"
325   unfolding iszero_def numeral_0_eq_0 ..
327 lemma nonzero_number_of_Min:
328   "~ iszero ((number_of Min)::'a::number_ring)"
329   unfolding iszero_def numeral_m1_eq_minus_1 by simp
332 subsection {* Comparisons, for Ordered Rings *}
334 lemma double_eq_0_iff:
335   "(a + a = 0) = (a = (0::'a::ordered_idom))"
336 proof -
337   have "a + a = (1 + 1) * a" unfolding left_distrib by simp
338   with zero_less_two [where 'a = 'a]
339   show ?thesis by force
340 qed
342 lemma le_imp_0_less:
343   assumes le: "0 \<le> z"
344   shows "(0::int) < 1 + z"
345 proof -
346   have "0 \<le> z" by fact
347   also have "... < z + 1" by (rule less_add_one)
348   also have "... = 1 + z" by (simp add: add_ac)
349   finally show "0 < 1 + z" .
350 qed
352 lemma odd_nonzero:
353   "1 + z + z \<noteq> (0::int)";
354 proof (cases z rule: int_cases)
355   case (nonneg n)
357   thus ?thesis using  le_imp_0_less [OF le]
359 next
360   case (neg n)
361   show ?thesis
362   proof
363     assume eq: "1 + z + z = 0"
364     have "0 < 1 + (int n + int n)"
366     also have "... = - (1 + z + z)"
368     also have "... = 0" by (simp add: eq)
369     finally have "0<0" ..
370     thus False by blast
371   qed
372 qed
374 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
376 lemma Ints_double_eq_0_iff:
377   assumes in_Ints: "a \<in> Ints"
378   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
379 proof -
380   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
381   then obtain z where a: "a = of_int z" ..
382   show ?thesis
383   proof
384     assume "a = 0"
385     thus "a + a = 0" by simp
386   next
387     assume eq: "a + a = 0"
388     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
389     hence "z + z = 0" by (simp only: of_int_eq_iff)
390     hence "z = 0" by (simp only: double_eq_0_iff)
391     thus "a = 0" by (simp add: a)
392   qed
393 qed
395 lemma Ints_odd_nonzero:
396   assumes in_Ints: "a \<in> Ints"
397   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
398 proof -
399   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
400   then obtain z where a: "a = of_int z" ..
401   show ?thesis
402   proof
403     assume eq: "1 + a + a = 0"
404     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
405     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
406     with odd_nonzero show False by blast
407   qed
408 qed
410 lemma Ints_number_of:
411   "(number_of w :: 'a::number_ring) \<in> Ints"
412   unfolding number_of_eq Ints_def by simp
414 lemma iszero_number_of_BIT:
415   "iszero (number_of (w BIT x)::'a) =
416    (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
417   by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff
418     Ints_odd_nonzero Ints_def split: bit.split)
420 lemma iszero_number_of_0:
421   "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) =
422   iszero (number_of w :: 'a)"
423   by (simp only: iszero_number_of_BIT simp_thms)
425 lemma iszero_number_of_1:
426   "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
430 subsection {* The Less-Than Relation *}
432 lemma less_number_of_eq_neg:
433   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
434   = neg (number_of (x + uminus y) :: 'a)"
435 apply (subst less_iff_diff_less_0)
437 done
439 text {*
440   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
441   @{term Numeral0} IS @{term "number_of Pls"}
442 *}
444 lemma not_neg_number_of_Pls:
445   "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
446   by (simp add: neg_def numeral_0_eq_0)
448 lemma neg_number_of_Min:
449   "neg (number_of Min ::'a::{ordered_idom,number_ring})"
450   by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
452 lemma double_less_0_iff:
453   "(a + a < 0) = (a < (0::'a::ordered_idom))"
454 proof -
455   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
456   also have "... = (a < 0)"
457     by (simp add: mult_less_0_iff zero_less_two
458                   order_less_not_sym [OF zero_less_two])
459   finally show ?thesis .
460 qed
462 lemma odd_less_0:
463   "(1 + z + z < 0) = (z < (0::int))";
464 proof (cases z rule: int_cases)
465   case (nonneg n)
467                              le_imp_0_less [THEN order_less_imp_le])
468 next
469   case (neg n)
470   thus ?thesis by (simp del: of_nat_Suc of_nat_add
472 qed
474 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
476 lemma Ints_odd_less_0:
477   assumes in_Ints: "a \<in> Ints"
478   shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
479 proof -
480   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
481   then obtain z where a: "a = of_int z" ..
482   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
484   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
485   also have "... = (a < 0)" by (simp add: a)
486   finally show ?thesis .
487 qed
489 lemma neg_number_of_BIT:
490   "neg (number_of (w BIT x)::'a) =
491   neg (number_of w :: 'a::{ordered_idom,number_ring})"
492   by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
493     Ints_odd_less_0 Ints_def split: bit.split)
496 text {* Less-Than or Equals *}
498 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
500 lemmas le_number_of_eq_not_less =
501   linorder_not_less [of "number_of w" "number_of v", symmetric,
502   standard]
504 lemma le_number_of_eq:
505     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
506      = (~ (neg (number_of (y + uminus x) :: 'a)))"
507 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
510 text {* Absolute value (@{term abs}) *}
512 lemma abs_number_of:
513   "abs(number_of x::'a::{ordered_idom,number_ring}) =
514    (if number_of x < (0::'a) then -number_of x else number_of x)"
518 text {* Re-orientation of the equation nnn=x *}
520 lemma number_of_reorient:
521   "(number_of w = x) = (x = number_of w)"
522   by auto
525 subsection {* Simplification of arithmetic operations on integer constants. *}
527 lemmas arith_extra_simps [standard, simp] =
529   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
530   number_of_mult [symmetric]
531   diff_number_of_eq abs_number_of
533 text {*
534   For making a minimal simpset, one must include these default simprules.
535   Also include @{text simp_thms}.
536 *}
538 lemmas arith_simps =
539   bit.distinct
540   Pls_0_eq Min_1_eq
541   pred_Pls pred_Min pred_1 pred_0
542   succ_Pls succ_Min succ_1 succ_0
544   minus_Pls minus_Min minus_1 minus_0
545   mult_Pls mult_Min mult_num1 mult_num0
547   abs_zero abs_one arith_extra_simps
549 text {* Simplification of relational operations *}
551 lemmas rel_simps [simp] =
552   eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
553   iszero_number_of_0 iszero_number_of_1
554   less_number_of_eq_neg
555   not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
556   neg_number_of_Min neg_number_of_BIT
557   le_number_of_eq
560 subsection {* Simplification of arithmetic when nested to the right. *}
563   "number_of v + (number_of w + z) =
564    (number_of(v + w) + z::'a::number_ring)"
567 lemma mult_number_of_left [simp]:
568   "number_of v * (number_of w * z) =
569    (number_of(v * w) * z::'a::number_ring)"
570   by (simp add: mult_assoc [symmetric])
573   "number_of v + (number_of w - c) =
574   number_of(v + w) - (c::'a::number_ring)"
578   "number_of v + (c - number_of w) =
579    number_of (v + uminus w) + (c::'a::number_ring)"
580 apply (subst diff_number_of_eq [symmetric])
581 apply (simp only: compare_rls)
582 done
585 subsection {* Configuration of the code generator *}
587 instance int :: eq ..
589 code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
591 definition
592   int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
593   "int_aux i n = (i + int n)"
595 lemma [code]:
596   "int_aux i 0 = i"
597   "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
600 lemma [code unfold]:
601   "int n = int_aux 0 n"
604 definition
605   nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
606   "nat_aux n i = (n + nat i)"
608 lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
609   -- {* tail recursive *}
610   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
613 lemma [code]: "nat i = nat_aux 0 i"
616 lemma zero_is_num_zero [code func, code inline, symmetric, normal post]:
617   "(0\<Colon>int) = number_of Numeral.Pls"
618   by simp
620 lemma one_is_num_one [code func, code inline, symmetric, normal post]:
621   "(1\<Colon>int) = number_of (Numeral.Pls BIT bit.B1)"
622   by simp
624 code_modulename SML
625   IntDef Integer
627 code_modulename OCaml
628   IntDef Integer
631   IntDef Integer
633 code_modulename SML
634   Numeral Integer
636 code_modulename OCaml
637   Numeral Integer
640   Numeral Integer
642 (*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
644 types_code
645   "int" ("int")
646 attach (term_of) {*
647 val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
648 *}
649 attach (test) {*
650 fun gen_int i = one_of [~1, 1] * random_range 0 i;
651 *}
653 setup {*
654 let
656 fun number_of_codegen thy defs gr dep module b (Const (@{const_name Numeral.number_of}, Type ("fun", [_, T])) \$ t) =
657       if T = HOLogic.intT then
658         (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
659           (Pretty.str o IntInf.toString o HOLogic.dest_numeral) t) handle TERM _ => NONE)
660       else if T = HOLogic.natT then
661         SOME (Codegen.invoke_codegen thy defs dep module b (gr,
662           Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) \$
663             (Const (@{const_name Numeral.number_of}, HOLogic.intT --> HOLogic.intT) \$ t)))
664       else NONE
665   | number_of_codegen _ _ _ _ _ _ _ = NONE;
667 in
671 end
672 *}
674 consts_code
675   "0 :: int"                   ("0")
676   "1 :: int"                   ("1")
677   "uminus :: int => int"       ("~")
678   "op + :: int => int => int"  ("(_ +/ _)")
679   "op * :: int => int => int"  ("(_ */ _)")
680   "op \<le> :: int => int => bool" ("(_ <=/ _)")
681   "op < :: int => int => bool" ("(_ </ _)")
683 quickcheck_params [default_type = int]
685 (*setup continues in theory Presburger*)
687 hide (open) const Pls Min B0 B1 succ pred
689 end