wneuper/isa: src/HOL/Integ/Bin.ML@08b34c902618

     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

    10 Arithmetic on binary integers.

    11 *)

    13 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)

    15 Goal "NCons bin.Pls False = bin.Pls";

    16 by (Simp_tac 1);

    17 qed "NCons_Pls_0";

    19 Goal "NCons bin.Pls True = bin.Pls BIT True";

    20 by (Simp_tac 1);

    21 qed "NCons_Pls_1";

    23 Goal "NCons bin.Min False = bin.Min BIT False";

    24 by (Simp_tac 1);

    25 qed "NCons_Min_0";

    27 Goal "NCons bin.Min True = bin.Min";

    28 by (Simp_tac 1);

    29 qed "NCons_Min_1";

    31 Goal "bin_succ(w BIT True) = (bin_succ w) BIT False";

    32 by (Simp_tac 1);

    33 qed "bin_succ_1";

    35 Goal "bin_succ(w BIT False) =  NCons w True";

    36 by (Simp_tac 1);

    37 qed "bin_succ_0";

    39 Goal "bin_pred(w BIT True) = NCons w False";

    40 by (Simp_tac 1);

    41 qed "bin_pred_1";

    43 Goal "bin_pred(w BIT False) = (bin_pred w) BIT True";

    44 by (Simp_tac 1);

    45 qed "bin_pred_0";

    47 Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)";

    48 by (Simp_tac 1);

    49 qed "bin_minus_1";

    51 Goal "bin_minus(w BIT False) = (bin_minus w) BIT False";

    52 by (Simp_tac 1);

    53 qed "bin_minus_0";

    56 (*** bin_add: binary addition ***)

    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";

    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";

    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";

    71 Goal "bin_add w bin.Pls = w";

    72 by (induct_tac "w" 1);

    73 by Auto_tac;

    74 qed "bin_add_Pls_right";

    76 Goal "bin_add w bin.Min = bin_pred w";

    77 by (induct_tac "w" 1);

    78 by Auto_tac;

    79 qed "bin_add_Min_right";

    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";

    87 (*** bin_mult: binary multiplication ***)

    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";

    93 Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False";

    94 by (Simp_tac 1);

    95 qed "bin_mult_0";

    98 (**** The carry/borrow functions, bin_succ and bin_pred ****)

   101 (** number_of **)

   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";

   108 Addsimps [number_of_NCons];

   110 Goal "number_of(bin_succ w) = (1 + number_of w :: int)";

   111 by (induct_tac "w" 1);

   112 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));

   113 qed "number_of_succ";

   115 Goal "number_of(bin_pred w) = (- 1 + number_of w :: int)";

   116 by (induct_tac "w" 1);

   117 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));

   118 qed "number_of_pred";

   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";

   130 (*This proof is complicated by the mutual recursion*)

   131 Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";

   132 by (induct_tac "v" 1);

   133 by (Simp_tac 1);

   134 by (simp_tac (simpset() addsimps [number_of_pred]) 1);

   135 by (rtac allI 1);

   136 by (induct_tac "w" 1);

   137 by (ALLGOALS (asm_simp_tac (simpset() addsimps

   138                [bin_add_BIT_BIT, number_of_succ, number_of_pred] @ zadd_ac)));

   139 qed_spec_mp "number_of_add";

   142 (*Subtraction*)

   143 Goalw [zdiff_def]

   144      "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)";

   145 by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);

   146 qed "diff_number_of_eq";

   148 bind_thms ("bin_mult_simps",

   149            [int_Suc0_eq_1, zmult_zminus, number_of_minus, number_of_add]);

   151 Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";

   152 by (induct_tac "v" 1);

   153 by (simp_tac (simpset() addsimps bin_mult_simps) 1);

   154 by (simp_tac (simpset() addsimps bin_mult_simps) 1);

   155 by (asm_simp_tac

   156     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);

   157 qed "number_of_mult";

   160 (*The correctness of shifting.  But it doesn't seem to give a measurable

   161   speed-up.*)

   162 Goal "(2::int) * number_of w = number_of (w BIT False)";

   163 by (induct_tac "w" 1);

   164 by (ALLGOALS (asm_simp_tac

   165     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));

   166 qed "double_number_of_BIT";

   169 (** Converting numerals 0 and 1 to their abstract versions **)

   171 Goal "Numeral0 = (0::int)";

   172 by (Simp_tac 1);

   173 qed "int_numeral_0_eq_0";

   175 Goal "Numeral1 = (1::int)";

   176 by (simp_tac (simpset() addsimps [int_1, int_Suc0_eq_1]) 1);

   177 qed "int_numeral_1_eq_1";

   180 (** Special simplification, for constants only **)

   182 (*Distributive laws for literals*)

   183 Addsimps (map (inst "w" "number_of ?v")

   184 	  [zadd_zmult_distrib, zadd_zmult_distrib2,

   185 	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);

   187 Addsimps (map (inst "x" "number_of ?v")

   188 	  [zless_zminus, zle_zminus, equation_zminus]);

   189 Addsimps (map (inst "y" "number_of ?v")

   190 	  [zminus_zless, zminus_zle, zminus_equation]);

   192 (*Equations and inequations involving 1*)

   193 Addsimps (map (simplify (simpset()) o inst "x" "1")

   194 	  [zless_zminus, zle_zminus, equation_zminus]);

   195 Addsimps (map (simplify (simpset()) o inst "y" "1")

   196 	  [zminus_zless, zminus_zle, zminus_equation]);

   198 (*Moving negation out of products*)

   199 Addsimps [zmult_zminus, zmult_zminus_right];

   201 (*Cancellation of constant factors in comparisons (< and <=) *)

   202 Addsimps (map (inst "k" "number_of ?v")

   203 	  [zmult_zless_cancel1, zmult_zless_cancel2,

   204 	   zmult_zle_cancel1, zmult_zle_cancel2]);

   207 (** Special-case simplification for small constants **)

   209 Goal "-1 * z = -(z::int)";

   210 by (simp_tac (simpset() addsimps zcompare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);

   211 qed "zmult_minus1";

   213 Goal "z * -1 = -(z::int)";

   214 by (stac zmult_commute 1 THEN rtac zmult_minus1 1);

   215 qed "zmult_minus1_right";

   217 Addsimps [zmult_minus1, zmult_minus1_right];

   219 (*Negation of a coefficient*)

   220 Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";

   221 by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1);

   222 qed "zminus_number_of_zmult";

   223 Addsimps [zminus_number_of_zmult];

   225 (*Integer unary minus for the abstract constant 1. Cannot be inserted

   226   as a simprule until later: it is number_of_Min re-oriented!*)

   227 Goal "- 1 = (-1::int)";

   228 by (Simp_tac 1);

   229 qed "zminus_1_eq_m1";

   231 Goal "(0 < nat z) = (0 < z)";

   232 by (cut_inst_tac [("w","0")] zless_nat_conj 1);

   233 by Auto_tac;

   234 qed "zero_less_nat_eq";

   235 Addsimps [zero_less_nat_eq];

   238 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)

   240 (** Equals (=) **)

   242 Goalw [iszero_def]

   243   "((number_of x::int) = number_of y) = \

   244 \  iszero (number_of (bin_add x (bin_minus y)))";

   245 by (simp_tac (simpset()

   246                  addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1);

   247 qed "eq_number_of_eq";

   249 Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)";

   250 by (Simp_tac 1);

   251 qed "iszero_number_of_Pls";

   253 Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";

   254 by (simp_tac (simpset() addsimps [eq_commute]) 1);

   255 qed "nonzero_number_of_Min";

   257 fun int_case_tac x = res_inst_tac [("z",x)] int_cases;

   259 Goalw [iszero_def]

   260      "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))";

   261 by (int_case_tac "number_of w" 1);

   262 by (ALLGOALS

   263     (asm_simp_tac

   264      (simpset() addsimps zcompare_rls @

   265   	                 [zero_reorient, zminus_zadd_distrib RS sym,

   266                           int_Suc0_eq_1 RS sym, zadd_int])));

   267 qed "iszero_number_of_BIT";

   269 Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)";

   270 by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1);

   271 qed "iszero_number_of_0";

   273 Goal "~ iszero (number_of (w BIT True)::int)";

   274 by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1);

   275 qed "iszero_number_of_1";

   279 (** Less-than (<) **)

   281 Goalw [zless_def,zdiff_def]

   282     "((number_of x::int) < number_of y) \

   283 \    = neg (number_of (bin_add x (bin_minus y)))";

   284 by (simp_tac (simpset() addsimps bin_mult_simps) 1);

   285 qed "less_number_of_eq_neg";

   287 (*But if Numeral0 is rewritten to 0 then this rule can't be applied:

   288   Numeral0 IS (number_of Pls) *)

   289 Goal "~ neg (number_of bin.Pls)";

   290 by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1);

   291 qed "not_neg_number_of_Pls";

   293 Goal "neg (number_of bin.Min)";

   294 by (simp_tac (simpset() addsimps [neg_eq_less_0, int_0_less_1]) 1);

   295 qed "neg_number_of_Min";

   297 Goal "neg (number_of (w BIT x)) = neg (number_of w)";

   298 by (Asm_simp_tac 1);

   299 by (int_case_tac "number_of w" 1);

   300 by (ALLGOALS (asm_simp_tac

   301 	      (simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int,

   302                          neg_eq_less_0, symmetric zdiff_def] @ zcompare_rls)));

   303 qed "neg_number_of_BIT";

   306 (** Less-than-or-equals (<=) **)

   308 Goal "(number_of x <= (number_of y::int)) = \

   309 \     (~ number_of y < (number_of x::int))";

   310 by (rtac (linorder_not_less RS sym) 1);

   311 qed "le_number_of_eq_not_less";

   313 (** Absolute value (abs) **)

   315 Goalw [zabs_def]

   316  "abs(number_of x::int) = \

   317 \ (if number_of x < (0::int) then -number_of x else number_of x)";

   318 by (rtac refl 1);

   319 qed "zabs_number_of";

   321 (*0 and 1 require special rewrites because they aren't numerals*)

   322 Goal "abs (0::int) = 0";

   323 by (simp_tac (simpset() addsimps [zabs_def]) 1);

   324 qed "zabs_0";

   326 Goal "abs (1::int) = 1";

   327 by (simp_tac (simpset() delsimps [int_0, int_1]

   328                        addsimps [int_0 RS sym, int_1 RS sym, zabs_def]) 1);

   329 qed "zabs_1";

   331 (*Re-orientation of the equation nnn=x*)

   332 Goal "(number_of w = x) = (x = number_of w)";

   333 by Auto_tac;

   334 qed "number_of_reorient";

   337 structure Bin_Simprocs =

   338   struct

   339   fun prove_conv tacs sg (hyps: thm list) xs (t, u) =

   340     if t aconv u then None

   341     else

   342       let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))

   343       in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end

   345   fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];

   346   fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];

   348   fun prep_simproc (name, pats, proc) =

   349     Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;

   351   fun is_numeral (Const("Numeral.number_of", _) $ w) = true

   352     | is_numeral _ = false

   354   fun simplify_meta_eq f_number_of_eq f_eq =

   355       mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)

   357   structure IntAbstractNumeralsData =

   358     struct

   359     val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of

   360     val is_numeral	= is_numeral

   361     val numeral_0_eq_0    = int_numeral_0_eq_0

   362     val numeral_1_eq_1    = int_numeral_1_eq_1

   363     val prove_conv	= prove_conv_nohyps_novars

   364     fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))

   365     val simplify_meta_eq  = simplify_meta_eq

   366     end

   368   structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData)

   371   (*For addition, we already have rules for the operand 0.

   372     Multiplication is omitted because there are already special rules for

   373     both 0 and 1 as operands.  Unary minus is trivial, just have - 1 = -1.

   374     For the others, having three patterns is a compromise between just having

   375     one (many spurious calls) and having nine (just too many!) *)

   376   val eval_numerals =

   377     map prep_simproc

   378      [("int_add_eval_numerals",

   379        ["(m::int) + 1", "(m::int) + number_of v"],

   380        IntAbstractNumerals.proc (number_of_add RS sym)),

   381       ("int_diff_eval_numerals",

   382        ["(m::int) - 1", "(m::int) - number_of v"],

   383        IntAbstractNumerals.proc diff_number_of_eq),

   384       ("int_eq_eval_numerals",

   385        ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"],

   386        IntAbstractNumerals.proc eq_number_of_eq),

   387       ("int_less_eval_numerals",

   388        ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"],

   389        IntAbstractNumerals.proc less_number_of_eq_neg),

   390       ("int_le_eval_numerals",

   391        ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],

   392        IntAbstractNumerals.proc le_number_of_eq_not_less)]

   394   (*reorientation simprules using ==, for the following simproc*)

   395   val meta_zero_reorient = zero_reorient RS eq_reflection

   396   val meta_one_reorient = one_reorient RS eq_reflection

   397   val meta_number_of_reorient = number_of_reorient RS eq_reflection

   399   (*reorientation simplification procedure: reorients (polymorphic)

   400     0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)

   401   fun reorient_proc sg _ (_ $ t $ u) =

   402     case u of

   403 	Const("0", _) => None

   404       | Const("1", _) => None

   405       | Const("Numeral.number_of", _) $ _ => None

   406       | _ => Some (case t of

   407 		  Const("0", _) => meta_zero_reorient

   408 		| Const("1", _) => meta_one_reorient

   409 		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)

   411   val reorient_simproc =

   412       prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)

   414   end;

   417 Addsimprocs Bin_Simprocs.eval_numerals;

   418 Addsimprocs [Bin_Simprocs.reorient_simproc];

   421 (*Delete the original rewrites, with their clumsy conditional expressions*)

   422 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,

   423           NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];

   425 (*Hide the binary representation of integer constants*)

   426 Delsimps [number_of_Pls, number_of_Min, number_of_BIT];

   430 (*Simplification of arithmetic operations on integer constants.

   431   Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)

   433 bind_thms ("NCons_simps",

   434            [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);

   436 bind_thms ("bin_arith_extra_simps",

   437     [number_of_add RS sym,

   438      number_of_minus RS sym, zminus_1_eq_m1,

   439      number_of_mult RS sym,

   440      bin_succ_1, bin_succ_0,

   441      bin_pred_1, bin_pred_0,

   442      bin_minus_1, bin_minus_0,

   443      bin_add_Pls_right, bin_add_Min_right,

   444      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,

   445      diff_number_of_eq, zabs_number_of, zabs_0, zabs_1,

   446      bin_mult_1, bin_mult_0] @ NCons_simps);

   448 (*For making a minimal simpset, one must include these default simprules

   449   of thy.  Also include simp_thms, or at least (~False)=True*)

   450 bind_thms ("bin_arith_simps",

   451     [bin_pred_Pls, bin_pred_Min,

   452      bin_succ_Pls, bin_succ_Min,

   453      bin_add_Pls, bin_add_Min,

   454      bin_minus_Pls, bin_minus_Min,

   455      bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);

   457 (*Simplification of relational operations*)

   458 bind_thms ("bin_rel_simps",

   459     [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,

   460      iszero_number_of_0, iszero_number_of_1,

   461      less_number_of_eq_neg,

   462      not_neg_number_of_Pls, not_neg_0, not_neg_1, not_iszero_1,

   463      neg_number_of_Min, neg_number_of_BIT,

   464      le_number_of_eq_not_less]);

   466 Addsimps bin_arith_extra_simps;

   467 Addsimps bin_rel_simps;

   470 (** Simplification of arithmetic when nested to the right **)

   472 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";

   473 by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);

   474 qed "add_number_of_left";

   476 Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";

   477 by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);

   478 qed "mult_number_of_left";

   480 Goalw [zdiff_def]

   481     "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)";

   482 by (rtac add_number_of_left 1);

   483 qed "add_number_of_diff1";

   485 Goal "number_of v + (c - number_of w) = \

   486 \    number_of (bin_add v (bin_minus w)) + (c::int)";

   487 by (stac (diff_number_of_eq RS sym) 1);

   488 by Auto_tac;

   489 qed "add_number_of_diff2";

   491 Addsimps [add_number_of_left, mult_number_of_left,

   492 	  add_number_of_diff1, add_number_of_diff2];

   495 (** Inserting these natural simprules earlier would break many proofs! **)

   497 (* int (Suc n) = 1 + int n *)

   498 Addsimps [int_Suc];

   500 (* Numeral0 -> 0 and Numeral1 -> 1 *)

   501 Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];

author	paulson
	Mon, 24 Nov 2003 15:33:07 +0100
changeset 14266	08b34c902618
parent 14264	3d0c6238162a
child 14271	8ed6989228bb
permissions	-rw-r--r--