src/HOL/Integ/Numeral.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15013 34264f5e4691
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
     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 import IntDef
    11 files "Tools/numeral_syntax.ML"
    12 begin
    13 
    14 text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
    15    Only qualified access Numeral.Pls and Numeral.Min is allowed.
    16    We do not hide Bit because we need the BIT infix syntax.*}
    17 
    18 text{*This formalization defines binary arithmetic in terms of the integers
    19 rather than using a datatype. This avoids multiple representations (leading
    20 zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
    21 int_of_binary}, for the numerical interpretation.
    22 
    23 The representation expects that @{text "(m mod 2)"} is 0 or 1,
    24 even if m is negative;
    25 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
    26 @{text "-5 = (-3)*2 + 1"}.
    27 *}
    28 
    29 
    30 typedef (Bin)
    31   bin = "UNIV::int set"
    32     by (auto)
    33 
    34 constdefs
    35   Pls :: "bin"
    36    "Pls == Abs_Bin 0"
    37 
    38   Min :: "bin"
    39    "Min == Abs_Bin (- 1)"
    40 
    41   Bit :: "[bin,bool] => bin"    (infixl "BIT" 90)
    42    --{*That is, 2w+b*}
    43    "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
    44 
    45 
    46 axclass
    47   number < type  -- {* for numeric types: nat, int, real, \dots *}
    48 
    49 consts
    50   number_of :: "bin => 'a::number"
    51 
    52 syntax
    53   "_Numeral" :: "num_const => 'a"    ("_")
    54   Numeral0 :: 'a
    55   Numeral1 :: 'a
    56 
    57 translations
    58   "Numeral0" == "number_of Numeral.Pls"
    59   "Numeral1" == "number_of (Numeral.Pls BIT True)"
    60 
    61 
    62 setup NumeralSyntax.setup
    63 
    64 syntax (xsymbols)
    65   "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
    66 syntax (HTML output)
    67   "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
    68 syntax (output)
    69   "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
    70 translations
    71   "x\<twosuperior>" == "x^2"
    72   "x\<twosuperior>" <= "x^(2::nat)"
    73 
    74 
    75 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
    76   -- {* Unfold all @{text let}s involving constants *}
    77   by (simp add: Let_def)
    78 
    79 lemma Let_0 [simp]: "Let 0 f == f 0"
    80   by (simp add: Let_def)
    81 
    82 lemma Let_1 [simp]: "Let 1 f == f 1"
    83   by (simp add: Let_def)
    84 
    85 
    86 constdefs
    87   bin_succ  :: "bin=>bin"
    88    "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
    89 
    90   bin_pred  :: "bin=>bin"
    91    "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
    92 
    93   bin_minus  :: "bin=>bin"
    94    "bin_minus w == Abs_Bin(- (Rep_Bin w))"
    95 
    96   bin_add  :: "[bin,bin]=>bin"
    97    "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
    98 
    99   bin_mult  :: "[bin,bin]=>bin"
   100    "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
   101 
   102 
   103 lemmas Bin_simps = 
   104        bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
   105        Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
   106 
   107 text{*Removal of leading zeroes*}
   108 lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
   109 by (simp add: Bin_simps)
   110 
   111 lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
   112 by (simp add: Bin_simps)
   113 
   114 subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
   115 
   116 lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
   117 by (simp add: Bin_simps) 
   118 
   119 lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
   120 by (simp add: Bin_simps) 
   121 
   122 lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
   123 by (simp add: Bin_simps add_ac) 
   124 
   125 lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
   126 by (simp add: Bin_simps add_ac) 
   127 
   128 lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
   129 by (simp add: Bin_simps) 
   130 
   131 lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
   132 by (simp add: Bin_simps diff_minus) 
   133 
   134 lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
   135 by (simp add: Bin_simps) 
   136 
   137 lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
   138 by (simp add: Bin_simps diff_minus add_ac) 
   139 
   140 lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
   141 by (simp add: Bin_simps) 
   142 
   143 lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
   144 by (simp add: Bin_simps) 
   145 
   146 lemma bin_minus_1 [simp]:
   147      "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
   148 by (simp add: Bin_simps add_ac diff_minus) 
   149 
   150  lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
   151 by (simp add: Bin_simps) 
   152 
   153 
   154 subsection{*Binary Addition and Multiplication:
   155          @{term bin_add} and @{term bin_mult}*}
   156 
   157 lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
   158 by (simp add: Bin_simps) 
   159 
   160 lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
   161 by (simp add: Bin_simps diff_minus add_ac) 
   162 
   163 lemma bin_add_BIT_11 [simp]:
   164      "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
   165 by (simp add: Bin_simps add_ac)
   166 
   167 lemma bin_add_BIT_10 [simp]:
   168      "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
   169 by (simp add: Bin_simps add_ac)
   170 
   171 lemma bin_add_BIT_0 [simp]:
   172      "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
   173 by (simp add: Bin_simps add_ac)
   174 
   175 lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
   176 by (simp add: Bin_simps) 
   177 
   178 lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
   179 by (simp add: Bin_simps diff_minus) 
   180 
   181 lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
   182 by (simp add: Bin_simps) 
   183 
   184 lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
   185 by (simp add: Bin_simps) 
   186 
   187 lemma bin_mult_1 [simp]:
   188      "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
   189 by (simp add: Bin_simps add_ac left_distrib)
   190 
   191 lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
   192 by (simp add: Bin_simps left_distrib)
   193 
   194 
   195 
   196 subsection{*Converting Numerals to Rings: @{term number_of}*}
   197 
   198 axclass number_ring \<subseteq> number, comm_ring_1
   199   number_of_eq: "number_of w = of_int (Rep_Bin w)"
   200 
   201 lemma number_of_succ:
   202      "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
   203 by (simp add: number_of_eq Bin_simps)
   204 
   205 lemma number_of_pred:
   206      "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
   207 by (simp add: number_of_eq Bin_simps)
   208 
   209 lemma number_of_minus:
   210      "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
   211 by (simp add: number_of_eq Bin_simps) 
   212 
   213 lemma number_of_add:
   214      "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
   215 by (simp add: number_of_eq Bin_simps) 
   216 
   217 lemma number_of_mult:
   218      "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
   219 by (simp add: number_of_eq Bin_simps) 
   220 
   221 text{*The correctness of shifting.  But it doesn't seem to give a measurable
   222   speed-up.*}
   223 lemma double_number_of_BIT:
   224      "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
   225 by (simp add: number_of_eq Bin_simps left_distrib) 
   226 
   227 text{*Converting numerals 0 and 1 to their abstract versions*}
   228 lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
   229 by (simp add: number_of_eq Bin_simps) 
   230 
   231 lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
   232 by (simp add: number_of_eq Bin_simps) 
   233 
   234 text{*Special-case simplification for small constants*}
   235 
   236 text{*Unary minus for the abstract constant 1. Cannot be inserted
   237   as a simprule until later: it is @{text number_of_Min} re-oriented!*}
   238 lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
   239 by (simp add: number_of_eq Bin_simps) 
   240 
   241 
   242 lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
   243 by (simp add: numeral_m1_eq_minus_1)
   244 
   245 lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
   246 by (simp add: numeral_m1_eq_minus_1)
   247 
   248 (*Negation of a coefficient*)
   249 lemma minus_number_of_mult [simp]:
   250      "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
   251 by (simp add: number_of_minus)
   252 
   253 text{*Subtraction*}
   254 lemma diff_number_of_eq:
   255      "number_of v - number_of w =
   256       (number_of(bin_add v (bin_minus w))::'a::number_ring)"
   257 by (simp add: diff_minus number_of_add number_of_minus)
   258 
   259 
   260 lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
   261 by (simp add: number_of_eq Bin_simps) 
   262 
   263 lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
   264 by (simp add: number_of_eq Bin_simps) 
   265 
   266 lemma number_of_BIT:
   267      "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
   268 	                   (number_of w) + (number_of w)"
   269 by (simp add: number_of_eq Bin_simps) 
   270 
   271 
   272 
   273 subsection{*Equality of Binary Numbers*}
   274 
   275 text{*First version by Norbert Voelker*}
   276 
   277 lemma eq_number_of_eq:
   278   "((number_of x::'a::number_ring) = number_of y) =
   279    iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
   280 by (simp add: iszero_def compare_rls number_of_add number_of_minus)
   281 
   282 lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
   283 by (simp add: iszero_def numeral_0_eq_0)
   284 
   285 lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
   286 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
   287 
   288 
   289 subsection{*Comparisons, for Ordered Rings*}
   290 
   291 lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
   292 proof -
   293   have "a + a = (1+1)*a" by (simp add: left_distrib)
   294   with zero_less_two [where 'a = 'a]
   295   show ?thesis by force
   296 qed
   297 
   298 lemma le_imp_0_less: 
   299   assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
   300 proof -
   301   have "0 \<le> z" .
   302   also have "... < z + 1" by (rule less_add_one) 
   303   also have "... = 1 + z" by (simp add: add_ac)
   304   finally show "0 < 1 + z" .
   305 qed
   306 
   307 lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
   308 proof (cases z rule: int_cases)
   309   case (nonneg n)
   310   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   311   thus ?thesis using  le_imp_0_less [OF le]
   312     by (auto simp add: add_assoc) 
   313 next
   314   case (neg n)
   315   show ?thesis
   316   proof
   317     assume eq: "1 + z + z = 0"
   318     have "0 < 1 + (int n + int n)"
   319       by (simp add: le_imp_0_less add_increasing) 
   320     also have "... = - (1 + z + z)" 
   321       by (simp add: neg add_assoc [symmetric]) 
   322     also have "... = 0" by (simp add: eq) 
   323     finally have "0<0" ..
   324     thus False by blast
   325   qed
   326 qed
   327 
   328 
   329 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
   330 lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
   331 proof (unfold Ints_def) 
   332   assume "a \<in> range of_int"
   333   then obtain z where a: "a = of_int z" ..
   334   show ?thesis
   335   proof
   336     assume eq: "1 + a + a = 0"
   337     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
   338     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
   339     with odd_nonzero show False by blast
   340   qed
   341 qed 
   342 
   343 lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
   344 by (simp add: number_of_eq Ints_def) 
   345 
   346 
   347 lemma iszero_number_of_BIT:
   348      "iszero (number_of (w BIT x)::'a) = 
   349       (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
   350 by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
   351               Ints_odd_nonzero Ints_def)
   352 
   353 lemma iszero_number_of_0:
   354      "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = 
   355       iszero (number_of w :: 'a)"
   356 by (simp only: iszero_number_of_BIT simp_thms)
   357 
   358 lemma iszero_number_of_1:
   359      "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
   360 by (simp only: iszero_number_of_BIT simp_thms)
   361 
   362 
   363 
   364 subsection{*The Less-Than Relation*}
   365 
   366 lemma less_number_of_eq_neg:
   367     "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
   368      = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
   369 apply (subst less_iff_diff_less_0) 
   370 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
   371 done
   372 
   373 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
   374   @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
   375 lemma not_neg_number_of_Pls:
   376      "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
   377 by (simp add: neg_def numeral_0_eq_0)
   378 
   379 lemma neg_number_of_Min:
   380      "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
   381 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
   382 
   383 lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
   384 proof -
   385   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
   386   also have "... = (a < 0)"
   387     by (simp add: mult_less_0_iff zero_less_two 
   388                   order_less_not_sym [OF zero_less_two]) 
   389   finally show ?thesis .
   390 qed
   391 
   392 lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
   393 proof (cases z rule: int_cases)
   394   case (nonneg n)
   395   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   396                              le_imp_0_less [THEN order_less_imp_le])  
   397 next
   398   case (neg n)
   399   thus ?thesis by (simp del: int_Suc
   400 			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
   401 qed
   402 
   403 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
   404 lemma Ints_odd_less_0: 
   405      "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
   406 proof (unfold Ints_def) 
   407   assume "a \<in> range of_int"
   408   then obtain z where a: "a = of_int z" ..
   409   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
   410     by (simp add: a)
   411   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
   412   also have "... = (a < 0)" by (simp add: a)
   413   finally show ?thesis .
   414 qed
   415 
   416 lemma neg_number_of_BIT:
   417      "neg (number_of (w BIT x)::'a) = 
   418       neg (number_of w :: 'a::{ordered_idom,number_ring})"
   419 by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
   420               Ints_odd_less_0 Ints_def)
   421 
   422 
   423 text{*Less-Than or Equals*}
   424 
   425 text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
   426 lemmas le_number_of_eq_not_less =
   427        linorder_not_less [of "number_of w" "number_of v", symmetric, 
   428                           standard]
   429 
   430 lemma le_number_of_eq:
   431     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
   432      = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
   433 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
   434 
   435 
   436 text{*Absolute value (@{term abs})*}
   437 
   438 lemma abs_number_of:
   439      "abs(number_of x::'a::{ordered_idom,number_ring}) =
   440       (if number_of x < (0::'a) then -number_of x else number_of x)"
   441 by (simp add: abs_if)
   442 
   443 
   444 text{*Re-orientation of the equation nnn=x*}
   445 lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
   446 by auto
   447 
   448 
   449 
   450 
   451 subsection{*Simplification of arithmetic operations on integer constants.*}
   452 
   453 lemmas bin_arith_extra_simps = 
   454        number_of_add [symmetric]
   455        number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
   456        number_of_mult [symmetric]
   457        diff_number_of_eq abs_number_of 
   458 
   459 text{*For making a minimal simpset, one must include these default simprules.
   460   Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
   461 lemmas bin_arith_simps = 
   462        Pls_0_eq Min_1_eq
   463        bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
   464        bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
   465        bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
   466        bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
   467        bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
   468        bin_add_Pls_right bin_add_Min_right
   469        abs_zero abs_one bin_arith_extra_simps
   470 
   471 text{*Simplification of relational operations*}
   472 lemmas bin_rel_simps = 
   473        eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
   474        iszero_number_of_0 iszero_number_of_1
   475        less_number_of_eq_neg
   476        not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
   477        neg_number_of_Min neg_number_of_BIT
   478        le_number_of_eq
   479 
   480 declare bin_arith_extra_simps [simp]
   481 declare bin_rel_simps [simp]
   482 
   483 
   484 subsection{*Simplification of arithmetic when nested to the right*}
   485 
   486 lemma add_number_of_left [simp]:
   487      "number_of v + (number_of w + z) =
   488       (number_of(bin_add v w) + z::'a::number_ring)"
   489 by (simp add: add_assoc [symmetric])
   490 
   491 lemma mult_number_of_left [simp]:
   492     "number_of v * (number_of w * z) =
   493      (number_of(bin_mult v w) * z::'a::number_ring)"
   494 by (simp add: mult_assoc [symmetric])
   495 
   496 lemma add_number_of_diff1:
   497     "number_of v + (number_of w - c) = 
   498      number_of(bin_add v w) - (c::'a::number_ring)"
   499 by (simp add: diff_minus add_number_of_left)
   500 
   501 lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
   502      number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
   503 apply (subst diff_number_of_eq [symmetric])
   504 apply (simp only: compare_rls)
   505 done
   506 
   507 end