src/HOL/Integ/Numeral.thy
author haftmann
Tue Sep 19 15:22:03 2006 +0200 (2006-09-19)
changeset 20596 3950e65f48f8
parent 20500 11da1ce8dbd8
child 20699 0cc77abb185a
permissions -rw-r--r--
(void)
     1 (*  Title:      HOL/Integ/Numeral.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header {* Arithmetic on Binary Integers *}
     8 
     9 theory Numeral
    10 imports IntDef Datatype
    11 uses "../Tools/numeral_syntax.ML"
    12 begin
    13 
    14 text {*
    15   This formalization defines binary arithmetic in terms of the integers
    16   rather than using a datatype. This avoids multiple representations (leading
    17   zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
    18   int_of_binary}, for the numerical interpretation.
    19 
    20   The representation expects that @{text "(m mod 2)"} is 0 or 1,
    21   even if m is negative;
    22   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
    23   @{text "-5 = (-3)*2 + 1"}.
    24 *}
    25 
    26 text{*
    27   This datatype avoids the use of type @{typ bool}, which would make
    28   all of the rewrite rules higher-order.
    29 *}
    30 
    31 datatype bit = B0 | B1
    32 
    33 constdefs
    34   Pls :: int
    35   "Pls == 0"
    36   Min :: int
    37   "Min == - 1"
    38   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90)
    39   "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
    40 
    41 axclass
    42   number < type  -- {* for numeric types: nat, int, real, \dots *}
    43 
    44 consts
    45   number_of :: "int \<Rightarrow> 'a::number"
    46 
    47 syntax
    48   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
    49 
    50 setup NumeralSyntax.setup
    51 
    52 abbreviation
    53   "Numeral0 \<equiv> number_of Pls"
    54   "Numeral1 \<equiv> number_of (Pls BIT B1)"
    55 
    56 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
    57   -- {* Unfold all @{text let}s involving constants *}
    58   unfolding Let_def ..
    59 
    60 lemma Let_0 [simp]: "Let 0 f = f 0"
    61   unfolding Let_def ..
    62 
    63 lemma Let_1 [simp]: "Let 1 f = f 1"
    64   unfolding Let_def ..
    65 
    66 definition
    67   succ :: "int \<Rightarrow> int"
    68   "succ k = k + 1"
    69   pred :: "int \<Rightarrow> int"
    70   "pred k = k - 1"
    71 
    72 lemmas numeral_simps = 
    73   succ_def pred_def Pls_def Min_def Bit_def
    74 
    75 text {* Removal of leading zeroes *}
    76 
    77 lemma Pls_0_eq [simp]:
    78   "Pls BIT B0 = Pls"
    79   unfolding numeral_simps by simp
    80 
    81 lemma Min_1_eq [simp]:
    82   "Min BIT B1 = Min"
    83   unfolding numeral_simps by simp
    84 
    85 
    86 subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
    87 
    88 lemma succ_Pls [simp]:
    89   "succ Pls = Pls BIT B1"
    90   unfolding numeral_simps by simp
    91 
    92 lemma succ_Min [simp]:
    93   "succ Min = Pls"
    94   unfolding numeral_simps by simp
    95 
    96 lemma succ_1 [simp]:
    97   "succ (k BIT B1) = succ k BIT B0"
    98   unfolding numeral_simps by simp
    99 
   100 lemma succ_0 [simp]:
   101   "succ (k BIT B0) = k BIT B1"
   102   unfolding numeral_simps by simp
   103 
   104 lemma pred_Pls [simp]:
   105   "pred Pls = Min"
   106   unfolding numeral_simps by simp
   107 
   108 lemma pred_Min [simp]:
   109   "pred Min = Min BIT B0"
   110   unfolding numeral_simps by simp
   111 
   112 lemma pred_1 [simp]:
   113   "pred (k BIT B1) = k BIT B0"
   114   unfolding numeral_simps by simp
   115 
   116 lemma pred_0 [simp]:
   117   "pred (k BIT B0) = pred k BIT B1"
   118   unfolding numeral_simps by simp 
   119 
   120 lemma minus_Pls [simp]:
   121   "- Pls = Pls"
   122   unfolding numeral_simps by simp 
   123 
   124 lemma minus_Min [simp]:
   125   "- Min = Pls BIT B1"
   126   unfolding numeral_simps by simp 
   127 
   128 lemma minus_1 [simp]:
   129   "- (k BIT B1) = pred (- k) BIT B1"
   130   unfolding numeral_simps by simp 
   131 
   132 lemma minus_0 [simp]:
   133   "- (k BIT B0) = (- k) BIT B0"
   134   unfolding numeral_simps by simp 
   135 
   136 
   137 subsection {*
   138   Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   139     and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
   140 *}
   141 
   142 lemma add_Pls [simp]:
   143   "Pls + k = k"
   144   unfolding numeral_simps by simp 
   145 
   146 lemma add_Min [simp]:
   147   "Min + k = pred k"
   148   unfolding numeral_simps by simp
   149 
   150 lemma add_BIT_11 [simp]:
   151   "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
   152   unfolding numeral_simps by simp
   153 
   154 lemma add_BIT_10 [simp]:
   155   "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
   156   unfolding numeral_simps by simp
   157 
   158 lemma add_BIT_0 [simp]:
   159   "(k BIT B0) + (l BIT b) = (k + l) BIT b"
   160   unfolding numeral_simps by simp 
   161 
   162 lemma add_Pls_right [simp]:
   163   "k + Pls = k"
   164   unfolding numeral_simps by simp 
   165 
   166 lemma add_Min_right [simp]:
   167   "k + Min = pred k"
   168   unfolding numeral_simps by simp 
   169 
   170 lemma mult_Pls [simp]:
   171   "Pls * w = Pls"
   172   unfolding numeral_simps by simp 
   173 
   174 lemma mult_Min [simp]:
   175   "Min * k = - k"
   176   unfolding numeral_simps by simp 
   177 
   178 lemma mult_num1 [simp]:
   179   "(k BIT B1) * l = ((k * l) BIT B0) + l"
   180   unfolding numeral_simps int_distrib by simp 
   181 
   182 lemma mult_num0 [simp]:
   183   "(k BIT B0) * l = (k * l) BIT B0"
   184   unfolding numeral_simps int_distrib by simp 
   185 
   186 
   187 
   188 subsection {* Converting Numerals to Rings: @{term number_of} *}
   189 
   190 axclass number_ring \<subseteq> number, comm_ring_1
   191   number_of_eq: "number_of k = of_int k"
   192 
   193 lemma number_of_succ:
   194   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   195   unfolding number_of_eq numeral_simps by simp
   196 
   197 lemma number_of_pred:
   198   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
   199   unfolding number_of_eq numeral_simps by simp
   200 
   201 lemma number_of_minus:
   202   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
   203   unfolding number_of_eq numeral_simps by simp
   204 
   205 lemma number_of_add:
   206   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
   207   unfolding number_of_eq numeral_simps by simp
   208 
   209 lemma number_of_mult:
   210   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
   211   unfolding number_of_eq numeral_simps by simp
   212 
   213 text {*
   214   The correctness of shifting.
   215   But it doesn't seem to give a measurable speed-up.
   216 *}
   217 
   218 lemma double_number_of_BIT:
   219   "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
   220   unfolding number_of_eq numeral_simps left_distrib by simp
   221 
   222 text {*
   223   Converting numerals 0 and 1 to their abstract versions.
   224 *}
   225 
   226 lemma numeral_0_eq_0 [simp]:
   227   "Numeral0 = (0::'a::number_ring)"
   228   unfolding number_of_eq numeral_simps by simp
   229 
   230 lemma numeral_1_eq_1 [simp]:
   231   "Numeral1 = (1::'a::number_ring)"
   232   unfolding number_of_eq numeral_simps by simp
   233 
   234 text {*
   235   Special-case simplification for small constants.
   236 *}
   237 
   238 text{*
   239   Unary minus for the abstract constant 1. Cannot be inserted
   240   as a simprule until later: it is @{text number_of_Min} re-oriented!
   241 *}
   242 
   243 lemma numeral_m1_eq_minus_1:
   244   "(-1::'a::number_ring) = - 1"
   245   unfolding number_of_eq numeral_simps by simp
   246 
   247 lemma mult_minus1 [simp]:
   248   "-1 * z = -(z::'a::number_ring)"
   249   unfolding number_of_eq numeral_simps by simp
   250 
   251 lemma mult_minus1_right [simp]:
   252   "z * -1 = -(z::'a::number_ring)"
   253   unfolding number_of_eq numeral_simps by simp
   254 
   255 (*Negation of a coefficient*)
   256 lemma minus_number_of_mult [simp]:
   257    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
   258    unfolding number_of_eq by simp
   259 
   260 text {* Subtraction *}
   261 
   262 lemma diff_number_of_eq:
   263   "number_of v - number_of w =
   264     (number_of (v + uminus w)::'a::number_ring)"
   265   unfolding number_of_eq by simp
   266 
   267 lemma number_of_Pls:
   268   "number_of Pls = (0::'a::number_ring)"
   269   unfolding number_of_eq numeral_simps by simp
   270 
   271 lemma number_of_Min:
   272   "number_of Min = (- 1::'a::number_ring)"
   273   unfolding number_of_eq numeral_simps by simp
   274 
   275 lemma number_of_BIT:
   276   "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
   277     + (number_of w) + (number_of w)"
   278   unfolding number_of_eq numeral_simps by (simp split: bit.split)
   279 
   280 
   281 subsection {* Equality of Binary Numbers *}
   282 
   283 text {* First version by Norbert Voelker *}
   284 
   285 lemma eq_number_of_eq:
   286   "((number_of x::'a::number_ring) = number_of y) =
   287    iszero (number_of (x + uminus y) :: 'a)"
   288   unfolding iszero_def number_of_add number_of_minus
   289   by (simp add: compare_rls)
   290 
   291 lemma iszero_number_of_Pls:
   292   "iszero ((number_of Pls)::'a::number_ring)"
   293   unfolding iszero_def numeral_0_eq_0 ..
   294 
   295 lemma nonzero_number_of_Min:
   296   "~ iszero ((number_of Min)::'a::number_ring)"
   297   unfolding iszero_def numeral_m1_eq_minus_1 by simp
   298 
   299 
   300 subsection {* Comparisons, for Ordered Rings *}
   301 
   302 lemma double_eq_0_iff:
   303   "(a + a = 0) = (a = (0::'a::ordered_idom))"
   304 proof -
   305   have "a + a = (1 + 1) * a" unfolding left_distrib by simp
   306   with zero_less_two [where 'a = 'a]
   307   show ?thesis by force
   308 qed
   309 
   310 lemma le_imp_0_less: 
   311   assumes le: "0 \<le> z"
   312   shows "(0::int) < 1 + z"
   313 proof -
   314   have "0 \<le> z" .
   315   also have "... < z + 1" by (rule less_add_one) 
   316   also have "... = 1 + z" by (simp add: add_ac)
   317   finally show "0 < 1 + z" .
   318 qed
   319 
   320 lemma odd_nonzero:
   321   "1 + z + z \<noteq> (0::int)";
   322 proof (cases z rule: int_cases)
   323   case (nonneg n)
   324   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   325   thus ?thesis using  le_imp_0_less [OF le]
   326     by (auto simp add: add_assoc) 
   327 next
   328   case (neg n)
   329   show ?thesis
   330   proof
   331     assume eq: "1 + z + z = 0"
   332     have "0 < 1 + (int n + int n)"
   333       by (simp add: le_imp_0_less add_increasing) 
   334     also have "... = - (1 + z + z)" 
   335       by (simp add: neg add_assoc [symmetric]) 
   336     also have "... = 0" by (simp add: eq) 
   337     finally have "0<0" ..
   338     thus False by blast
   339   qed
   340 qed
   341 
   342 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   343 
   344 lemma Ints_odd_nonzero:
   345   assumes in_Ints: "a \<in> Ints"
   346   shows "1 + a + a \<noteq> (0::'a::ordered_idom)"
   347 proof -
   348   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   349   then obtain z where a: "a = of_int z" ..
   350   show ?thesis
   351   proof
   352     assume eq: "1 + a + a = 0"
   353     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
   354     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
   355     with odd_nonzero show False by blast
   356   qed
   357 qed 
   358 
   359 lemma Ints_number_of:
   360   "(number_of w :: 'a::number_ring) \<in> Ints"
   361   unfolding number_of_eq Ints_def by simp
   362 
   363 lemma iszero_number_of_BIT:
   364   "iszero (number_of (w BIT x)::'a) = 
   365    (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
   366   by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff 
   367     Ints_odd_nonzero Ints_def split: bit.split)
   368 
   369 lemma iszero_number_of_0:
   370   "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
   371   iszero (number_of w :: 'a)"
   372   by (simp only: iszero_number_of_BIT simp_thms)
   373 
   374 lemma iszero_number_of_1:
   375   "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
   376   by (simp add: iszero_number_of_BIT) 
   377 
   378 
   379 subsection {* The Less-Than Relation *}
   380 
   381 lemma less_number_of_eq_neg:
   382   "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
   383   = neg (number_of (x + uminus y) :: 'a)"
   384 apply (subst less_iff_diff_less_0) 
   385 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
   386 done
   387 
   388 text {*
   389   If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   390   @{term Numeral0} IS @{term "number_of Pls"}
   391 *}
   392 
   393 lemma not_neg_number_of_Pls:
   394   "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
   395   by (simp add: neg_def numeral_0_eq_0)
   396 
   397 lemma neg_number_of_Min:
   398   "neg (number_of Min ::'a::{ordered_idom,number_ring})"
   399   by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
   400 
   401 lemma double_less_0_iff:
   402   "(a + a < 0) = (a < (0::'a::ordered_idom))"
   403 proof -
   404   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
   405   also have "... = (a < 0)"
   406     by (simp add: mult_less_0_iff zero_less_two 
   407                   order_less_not_sym [OF zero_less_two]) 
   408   finally show ?thesis .
   409 qed
   410 
   411 lemma odd_less_0:
   412   "(1 + z + z < 0) = (z < (0::int))";
   413 proof (cases z rule: int_cases)
   414   case (nonneg n)
   415   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   416                              le_imp_0_less [THEN order_less_imp_le])  
   417 next
   418   case (neg n)
   419   thus ?thesis by (simp del: int_Suc
   420     add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
   421 qed
   422 
   423 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   424 
   425 lemma Ints_odd_less_0: 
   426   assumes in_Ints: "a \<in> Ints"
   427   shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
   428 proof -
   429   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   430   then obtain z where a: "a = of_int z" ..
   431   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
   432     by (simp add: a)
   433   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
   434   also have "... = (a < 0)" by (simp add: a)
   435   finally show ?thesis .
   436 qed
   437 
   438 lemma neg_number_of_BIT:
   439   "neg (number_of (w BIT x)::'a) = 
   440   neg (number_of w :: 'a::{ordered_idom,number_ring})"
   441   by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
   442     Ints_odd_less_0 Ints_def split: bit.split)
   443 
   444 
   445 text {* Less-Than or Equals *}
   446 
   447 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
   448 
   449 lemmas le_number_of_eq_not_less =
   450   linorder_not_less [of "number_of w" "number_of v", symmetric, 
   451   standard]
   452 
   453 lemma le_number_of_eq:
   454     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
   455      = (~ (neg (number_of (y + uminus x) :: 'a)))"
   456 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
   457 
   458 
   459 text {* Absolute value (@{term abs}) *}
   460 
   461 lemma abs_number_of:
   462   "abs(number_of x::'a::{ordered_idom,number_ring}) =
   463    (if number_of x < (0::'a) then -number_of x else number_of x)"
   464   by (simp add: abs_if)
   465 
   466 
   467 text {* Re-orientation of the equation nnn=x *}
   468 
   469 lemma number_of_reorient:
   470   "(number_of w = x) = (x = number_of w)"
   471   by auto
   472 
   473 
   474 subsection {* Simplification of arithmetic operations on integer constants. *}
   475 
   476 lemmas arith_extra_simps = 
   477   number_of_add [symmetric]
   478   number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
   479   number_of_mult [symmetric]
   480   diff_number_of_eq abs_number_of 
   481 
   482 text {*
   483   For making a minimal simpset, one must include these default simprules.
   484   Also include @{text simp_thms}.
   485 *}
   486 
   487 lemmas arith_simps = 
   488   bit.distinct
   489   Pls_0_eq Min_1_eq
   490   pred_Pls pred_Min pred_1 pred_0
   491   succ_Pls succ_Min succ_1 succ_0
   492   add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
   493   minus_Pls minus_Min minus_1 minus_0
   494   mult_Pls mult_Min mult_num1 mult_num0 
   495   add_Pls_right add_Min_right
   496   abs_zero abs_one arith_extra_simps
   497 
   498 text {* Simplification of relational operations *}
   499 
   500 lemmas rel_simps = 
   501   eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
   502   iszero_number_of_0 iszero_number_of_1
   503   less_number_of_eq_neg
   504   not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
   505   neg_number_of_Min neg_number_of_BIT
   506   le_number_of_eq
   507 
   508 declare arith_extra_simps [simp]
   509 declare rel_simps [simp]
   510 
   511 
   512 subsection {* Simplification of arithmetic when nested to the right. *}
   513 
   514 lemma add_number_of_left [simp]:
   515   "number_of v + (number_of w + z) =
   516    (number_of(v + w) + z::'a::number_ring)"
   517   by (simp add: add_assoc [symmetric])
   518 
   519 lemma mult_number_of_left [simp]:
   520   "number_of v * (number_of w * z) =
   521    (number_of(v * w) * z::'a::number_ring)"
   522   by (simp add: mult_assoc [symmetric])
   523 
   524 lemma add_number_of_diff1:
   525   "number_of v + (number_of w - c) = 
   526   number_of(v + w) - (c::'a::number_ring)"
   527   by (simp add: diff_minus add_number_of_left)
   528 
   529 lemma add_number_of_diff2 [simp]:
   530   "number_of v + (c - number_of w) =
   531    number_of (v + uminus w) + (c::'a::number_ring)"
   532 apply (subst diff_number_of_eq [symmetric])
   533 apply (simp only: compare_rls)
   534 done
   535 
   536 
   537 hide (open) const Pls Min B0 B1 succ pred
   538 
   539 end