src/HOL/Integ/Bin.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 9062 7b34ffecaaa8
child 9214 9454f30eacc7
permissions -rw-r--r--
bind_thm(s);
     1 (*  Title:      HOL/Integ/Bin.ML
     2     ID:         $Id$
     3     Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 David Spelt, University of Twente 
     5                 Tobias Nipkow, Technical University Munich
     6     Copyright   1994  University of Cambridge
     7     Copyright   1996  University of Twente
     8     Copyright   1999  TU Munich
     9 
    10 Arithmetic on binary integers.
    11 *)
    12 
    13 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
    14 
    15 Goal "NCons Pls False = Pls";
    16 by (Simp_tac 1);
    17 qed "NCons_Pls_0";
    18 
    19 Goal "NCons Pls True = Pls BIT True";
    20 by (Simp_tac 1);
    21 qed "NCons_Pls_1";
    22 
    23 Goal "NCons Min False = Min BIT False";
    24 by (Simp_tac 1);
    25 qed "NCons_Min_0";
    26 
    27 Goal "NCons Min True = Min";
    28 by (Simp_tac 1);
    29 qed "NCons_Min_1";
    30 
    31 Goal "bin_succ(w BIT True) = (bin_succ w) BIT False";
    32 by (Simp_tac 1);
    33 qed "bin_succ_1";
    34 
    35 Goal "bin_succ(w BIT False) =  NCons w True";
    36 by (Simp_tac 1);
    37 qed "bin_succ_0";
    38 
    39 Goal "bin_pred(w BIT True) = NCons w False";
    40 by (Simp_tac 1);
    41 qed "bin_pred_1";
    42 
    43 Goal "bin_pred(w BIT False) = (bin_pred w) BIT True";
    44 by (Simp_tac 1);
    45 qed "bin_pred_0";
    46 
    47 Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)";
    48 by (Simp_tac 1);
    49 qed "bin_minus_1";
    50 
    51 Goal "bin_minus(w BIT False) = (bin_minus w) BIT False";
    52 by (Simp_tac 1);
    53 qed "bin_minus_0";
    54 
    55 
    56 (*** bin_add: binary addition ***)
    57 
    58 Goal "bin_add (v BIT True) (w BIT True) = \
    59 \    NCons (bin_add v (bin_succ w)) False";
    60 by (Simp_tac 1);
    61 qed "bin_add_BIT_11";
    62 
    63 Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True";
    64 by (Simp_tac 1);
    65 qed "bin_add_BIT_10";
    66 
    67 Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y";
    68 by Auto_tac;
    69 qed "bin_add_BIT_0";
    70 
    71 Goal "bin_add w Pls = w";
    72 by (induct_tac "w" 1);
    73 by Auto_tac;
    74 qed "bin_add_Pls_right";
    75 
    76 Goal "bin_add w Min = bin_pred w";
    77 by (induct_tac "w" 1);
    78 by Auto_tac;
    79 qed "bin_add_Min_right";
    80 
    81 Goal "bin_add (v BIT x) (w BIT y) = \
    82 \    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)";
    83 by (Simp_tac 1);
    84 qed "bin_add_BIT_BIT";
    85 
    86 
    87 (*** bin_mult: binary multiplication ***)
    88 
    89 Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w";
    90 by (Simp_tac 1);
    91 qed "bin_mult_1";
    92 
    93 Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False";
    94 by (Simp_tac 1);
    95 qed "bin_mult_0";
    96 
    97 
    98 (**** The carry/borrow functions, bin_succ and bin_pred ****)
    99 
   100 
   101 (**** number_of ****)
   102 
   103 Goal "number_of(NCons w b) = (number_of(w BIT b)::int)";
   104 by (induct_tac "w" 1);
   105 by (ALLGOALS Asm_simp_tac);
   106 qed "number_of_NCons";
   107 
   108 Addsimps [number_of_NCons];
   109 
   110 Goal "number_of(bin_succ w) = int 1 + number_of w";
   111 by (induct_tac "w" 1);
   112 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   113 qed "number_of_succ";
   114 
   115 Goal "number_of(bin_pred w) = - (int 1) + number_of w";
   116 by (induct_tac "w" 1);
   117 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   118 qed "number_of_pred";
   119 
   120 Goal "number_of(bin_minus w) = (- (number_of w)::int)";
   121 by (induct_tac "w" 1);
   122 by (Simp_tac 1);
   123 by (Simp_tac 1);
   124 by (asm_simp_tac (simpset()
   125 		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
   126 		  addsimps [number_of_succ,number_of_pred,
   127 			    zadd_assoc]) 1);
   128 qed "number_of_minus";
   129 
   130  
   131 bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]);
   132 
   133 (*This proof is complicated by the mutual recursion*)
   134 Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
   135 by (induct_tac "v" 1);
   136 by (simp_tac (simpset() addsimps bin_add_simps) 1);
   137 by (simp_tac (simpset() addsimps bin_add_simps) 1);
   138 by (rtac allI 1);
   139 by (induct_tac "w" 1);
   140 by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
   141 qed_spec_mp "number_of_add";
   142 
   143 
   144 (*Subtraction*)
   145 Goalw [zdiff_def]
   146      "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)";
   147 by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
   148 qed "diff_number_of_eq";
   149 
   150 bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]);
   151 
   152 Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
   153 by (induct_tac "v" 1);
   154 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   155 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   156 by (asm_simp_tac
   157     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
   158 qed "number_of_mult";
   159 
   160 
   161 (*The correctness of shifting.  But it doesn't seem to give a measurable
   162   speed-up.*)
   163 Goal "(#2::int) * number_of w = number_of (w BIT False)";
   164 by (induct_tac "w" 1);
   165 by (ALLGOALS (asm_simp_tac
   166     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
   167 qed "double_number_of_BIT";
   168 
   169 
   170 (** Simplification rules with integer constants **)
   171 
   172 Goal "#0 + z = (z::int)";
   173 by (Simp_tac 1);
   174 qed "zadd_0";
   175 
   176 Goal "z + #0 = (z::int)";
   177 by (Simp_tac 1);
   178 qed "zadd_0_right";
   179 
   180 Addsimps [zadd_0, zadd_0_right];
   181 
   182 
   183 (** Converting simple cases of (int n) to numerals **)
   184 
   185 (*int 0 = #0 *)
   186 bind_thm ("int_0", number_of_Pls RS sym);
   187 
   188 Goal "int (Suc n) = #1 + int n";
   189 by (simp_tac (simpset() addsimps [zadd_int]) 1);
   190 qed "int_Suc";
   191 
   192 Goal "- (#0) = (#0::int)";
   193 by (Simp_tac 1);
   194 qed "zminus_0";
   195 
   196 Addsimps [zminus_0];
   197 
   198 
   199 Goal "(#0::int) - x = -x";
   200 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   201 qed "zdiff0";
   202 
   203 Goal "x - (#0::int) = x";
   204 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   205 qed "zdiff0_right";
   206 
   207 Goal "x - x = (#0::int)";
   208 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   209 qed "zdiff_self";
   210 
   211 Addsimps [zdiff0, zdiff0_right, zdiff_self];
   212 
   213 
   214 (** Special simplification, for constants only **)
   215 
   216 (*Distributive laws for literals*)
   217 Addsimps (map (inst "w" "number_of ?v")
   218 	  [zadd_zmult_distrib, zadd_zmult_distrib2,
   219 	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);
   220 
   221 Addsimps (map (inst "x" "number_of ?v") 
   222 	  [zless_zminus, zle_zminus, equation_zminus]);
   223 Addsimps (map (inst "y" "number_of ?v") 
   224 	  [zminus_zless, zminus_zle, zminus_equation]);
   225 
   226 (*Moving negation out of products*)
   227 Addsimps [zmult_zminus, zmult_zminus_right];
   228 
   229 (** Special-case simplification for small constants **)
   230 
   231 Goal "#0 * z = (#0::int)";
   232 by (Simp_tac 1);
   233 qed "zmult_0";
   234 
   235 Goal "z * #0 = (#0::int)";
   236 by (Simp_tac 1);
   237 qed "zmult_0_right";
   238 
   239 Goal "#1 * z = (z::int)";
   240 by (Simp_tac 1);
   241 qed "zmult_1";
   242 
   243 Goal "z * #1 = (z::int)";
   244 by (Simp_tac 1);
   245 qed "zmult_1_right";
   246 
   247 Goal "#-1 * z = -(z::int)";
   248 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
   249 qed "zmult_minus1";
   250 
   251 Goal "z * #-1 = -(z::int)";
   252 by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
   253 qed "zmult_minus1_right";
   254 
   255 Addsimps [zmult_0, zmult_0_right, 
   256 	  zmult_1, zmult_1_right,
   257 	  zmult_minus1, zmult_minus1_right];
   258 
   259 (*Negation of a coefficient*)
   260 Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
   261 by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
   262 qed "zminus_number_of_zmult";
   263 
   264 Addsimps [zminus_number_of_zmult];
   265 
   266 
   267 (** Inequality reasoning **)
   268 
   269 Goal "(m*n = (#0::int)) = (m = #0 | n = #0)";
   270 by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1);
   271 qed "zmult_eq_0_iff";
   272 
   273 Goal "((#0::int) = m*n) = (#0 = m | #0 = n)";
   274 by (stac eq_commute 1 THEN stac zmult_eq_0_iff 1);
   275 by Auto_tac;
   276 qed "zmult_0_eq_iff";
   277 
   278 Addsimps [zmult_eq_0_iff, zmult_0_eq_iff];
   279 
   280 Goal "(w < z + (#1::int)) = (w<z | w=z)";
   281 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
   282 qed "zless_add1_eq";
   283 
   284 Goal "(w + (#1::int) <= z) = (w<z)";
   285 by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
   286 qed "add1_zle_eq";
   287 
   288 Goal "((#1::int) + w <= z) = (w<z)";
   289 by (stac zadd_commute 1);
   290 by (rtac add1_zle_eq 1);
   291 qed "add1_left_zle_eq";
   292 
   293 Goal "neg x = (x < #0)";
   294 by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
   295 qed "neg_eq_less_0"; 
   296 
   297 Goal "(~neg x) = (#0 <= x)";
   298 by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
   299 qed "not_neg_eq_ge_0"; 
   300 
   301 Goal "#0 <= int m";
   302 by (Simp_tac 1);
   303 qed "zero_zle_int";
   304 AddIffs [zero_zle_int];
   305 
   306 
   307 (** Needed because (int 0) rewrites to #0.
   308     Can these be generalized without evaluating large numbers?**)
   309 
   310 Goal "~ (int k < #0)";
   311 by (Simp_tac 1);
   312 qed "int_less_0_conv";
   313 
   314 Goal "(int k <= #0) = (k=0)";
   315 by (Simp_tac 1);
   316 qed "int_le_0_conv";
   317 
   318 Goal "(int k = #0) = (k=0)";
   319 by (Simp_tac 1);
   320 qed "int_eq_0_conv";
   321 
   322 Goal "(#0 = int k) = (k=0)";
   323 by Auto_tac;
   324 qed "int_eq_0_conv'";
   325 
   326 Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
   327 
   328 
   329 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
   330 
   331 (** Equals (=) **)
   332 
   333 Goalw [iszero_def]
   334   "((number_of x::int) = number_of y) = \
   335 \  iszero (number_of (bin_add x (bin_minus y)))"; 
   336 by (simp_tac (simpset() addsimps
   337               (zcompare_rls @ [number_of_add, number_of_minus])) 1); 
   338 qed "eq_number_of_eq"; 
   339 
   340 Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
   341 by (Simp_tac 1); 
   342 qed "iszero_number_of_Pls"; 
   343 
   344 Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
   345 by (Simp_tac 1);
   346 qed "nonzero_number_of_Min"; 
   347 
   348 Goalw [iszero_def]
   349      "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
   350 by (Simp_tac 1);
   351 by (int_case_tac "number_of w" 1); 
   352 by (ALLGOALS (asm_simp_tac 
   353 	      (simpset() addsimps zcompare_rls @ 
   354 				  [zminus_zadd_distrib RS sym, 
   355 				   zadd_int]))); 
   356 qed "iszero_number_of_BIT"; 
   357 
   358 Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
   359 by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
   360 qed "iszero_number_of_0"; 
   361 
   362 Goal "~ iszero (number_of (w BIT True)::int)"; 
   363 by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
   364 qed "iszero_number_of_1"; 
   365 
   366 
   367 
   368 (** Less-than (<) **)
   369 
   370 Goalw [zless_def,zdiff_def] 
   371     "(number_of x::int) < number_of y \
   372 \    = neg (number_of (bin_add x (bin_minus y)))";
   373 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   374 qed "less_number_of_eq_neg"; 
   375 
   376 Goal "~ neg (number_of Pls)"; 
   377 by (Simp_tac 1); 
   378 qed "not_neg_number_of_Pls"; 
   379 
   380 Goal "neg (number_of Min)"; 
   381 by (Simp_tac 1);
   382 qed "neg_number_of_Min"; 
   383 
   384 Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
   385 by (Asm_simp_tac 1); 
   386 by (int_case_tac "number_of w" 1); 
   387 by (ALLGOALS (asm_simp_tac 
   388 	      (simpset() addsimps [zadd_int, neg_eq_less_int0, 
   389 				   symmetric zdiff_def] @ zcompare_rls))); 
   390 qed "neg_number_of_BIT"; 
   391 
   392 
   393 (** Less-than-or-equals (<=) **)
   394 
   395 Goal "(number_of x <= (number_of y::int)) = \
   396 \     (~ number_of y < (number_of x::int))";
   397 by (rtac (linorder_not_less RS sym) 1);
   398 qed "le_number_of_eq_not_less"; 
   399 
   400 (*Delete the original rewrites, with their clumsy conditional expressions*)
   401 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   402           NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
   403 
   404 (*Hide the binary representation of integer constants*)
   405 Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
   406 
   407 (*Simplification of arithmetic operations on integer constants.
   408   Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
   409 
   410 bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
   411 
   412 bind_thms ("bin_arith_extra_simps",
   413     [number_of_add RS sym,
   414      number_of_minus RS sym,
   415      number_of_mult RS sym,
   416      bin_succ_1, bin_succ_0, 
   417      bin_pred_1, bin_pred_0, 
   418      bin_minus_1, bin_minus_0,  
   419      bin_add_Pls_right, bin_add_Min_right,
   420      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   421      diff_number_of_eq, 
   422      bin_mult_1, bin_mult_0] @ NCons_simps);
   423 
   424 (*For making a minimal simpset, one must include these default simprules
   425   of thy.  Also include simp_thms, or at least (~False)=True*)
   426 bind_thms ("bin_arith_simps",
   427     [bin_pred_Pls, bin_pred_Min,
   428      bin_succ_Pls, bin_succ_Min,
   429      bin_add_Pls, bin_add_Min,
   430      bin_minus_Pls, bin_minus_Min,
   431      bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
   432 
   433 (*Simplification of relational operations*)
   434 bind_thms ("bin_rel_simps",
   435     [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
   436      iszero_number_of_0, iszero_number_of_1,
   437      less_number_of_eq_neg,
   438      not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
   439      le_number_of_eq_not_less]);
   440 
   441 Addsimps bin_arith_extra_simps;
   442 Addsimps bin_rel_simps;
   443 
   444 
   445 (** Simplification of arithmetic when nested to the right **)
   446 
   447 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";
   448 by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   449 qed "add_number_of_left";
   450 
   451 Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";
   452 by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   453 qed "mult_number_of_left";
   454 
   455 Goalw [zdiff_def]
   456     "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)";
   457 by (rtac add_number_of_left 1);
   458 qed "add_number_of_diff1";
   459 
   460 Goal "number_of v + (c - number_of w) = \
   461 \    number_of (bin_add v (bin_minus w)) + (c::int)";
   462 by (stac (diff_number_of_eq RS sym) 1);
   463 by Auto_tac;
   464 qed "add_number_of_diff2";
   465 
   466 Addsimps [add_number_of_left, mult_number_of_left,
   467 	  add_number_of_diff1, add_number_of_diff2];