src/HOL/Hyperreal/HyperBin.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 12018 ec054019c910
child 13485 acf39e924091
permissions -rw-r--r--
sane interface for simprocs;
     1 (*  Title:      HOL/Hyperreal/HyperBin.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     5 
     6 Binary arithmetic for the hypreals (integer literals only).
     7 *)
     8 
     9 (** hypreal_of_real (coercion from int to real) **)
    10 
    11 Goal "hypreal_of_real (number_of w) = number_of w";
    12 by (simp_tac (simpset() addsimps [hypreal_number_of_def]) 1);
    13 qed "hypreal_number_of";
    14 Addsimps [hypreal_number_of];
    15 
    16 Goalw [hypreal_number_of_def] "Numeral0 = (0::hypreal)";
    17 by (Simp_tac 1);
    18 qed "hypreal_numeral_0_eq_0";
    19 
    20 Goalw [hypreal_number_of_def] "Numeral1 = (1::hypreal)";
    21 by (Simp_tac 1);
    22 qed "hypreal_numeral_1_eq_1";
    23 
    24 (** Addition **)
    25 
    26 Goal "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')";
    27 by (simp_tac
    28     (HOL_ss addsimps [hypreal_number_of_def,
    29                       hypreal_of_real_add RS sym, add_real_number_of]) 1);
    30 qed "add_hypreal_number_of";
    31 Addsimps [add_hypreal_number_of];
    32 
    33 
    34 (** Subtraction **)
    35 
    36 Goalw [hypreal_number_of_def]
    37      "- (number_of w :: hypreal) = number_of (bin_minus w)";
    38 by (simp_tac
    39     (HOL_ss addsimps [minus_real_number_of, hypreal_of_real_minus RS sym]) 1);
    40 qed "minus_hypreal_number_of";
    41 Addsimps [minus_hypreal_number_of];
    42 
    43 Goalw [hypreal_number_of_def, hypreal_diff_def]
    44      "(number_of v :: hypreal) - number_of w = \
    45 \     number_of (bin_add v (bin_minus w))";
    46 by (Simp_tac 1);
    47 qed "diff_hypreal_number_of";
    48 Addsimps [diff_hypreal_number_of];
    49 
    50 
    51 (** Multiplication **)
    52 
    53 Goal "(number_of v :: hypreal) * number_of v' = number_of (bin_mult v v')";
    54 by (simp_tac
    55     (HOL_ss addsimps [hypreal_number_of_def,
    56                       hypreal_of_real_mult RS sym, mult_real_number_of]) 1);
    57 qed "mult_hypreal_number_of";
    58 Addsimps [mult_hypreal_number_of];
    59 
    60 Goal "(2::hypreal) = 1 + 1";
    61 by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1);
    62 val lemma = result();
    63 
    64 (*For specialist use: NOT as default simprules*)
    65 Goal "2 * z = (z+z::hypreal)";
    66 by (simp_tac (simpset ()
    67               addsimps [lemma, hypreal_add_mult_distrib,
    68                         hypreal_numeral_1_eq_1]) 1);
    69 qed "hypreal_mult_2";
    70 
    71 Goal "z * 2 = (z+z::hypreal)";
    72 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_2 1);
    73 qed "hypreal_mult_2_right";
    74 
    75 
    76 (*** Comparisons ***)
    77 
    78 (** Equals (=) **)
    79 
    80 Goal "((number_of v :: hypreal) = number_of v') = \
    81 \     iszero (number_of (bin_add v (bin_minus v')))";
    82 by (simp_tac
    83     (HOL_ss addsimps [hypreal_number_of_def,
    84                       hypreal_of_real_eq_iff, eq_real_number_of]) 1);
    85 qed "eq_hypreal_number_of";
    86 Addsimps [eq_hypreal_number_of];
    87 
    88 (** Less-than (<) **)
    89 
    90 (*"neg" is used in rewrite rules for binary comparisons*)
    91 Goal "((number_of v :: hypreal) < number_of v') = \
    92 \     neg (number_of (bin_add v (bin_minus v')))";
    93 by (simp_tac
    94     (HOL_ss addsimps [hypreal_number_of_def, hypreal_of_real_less_iff,
    95                       less_real_number_of]) 1);
    96 qed "less_hypreal_number_of";
    97 Addsimps [less_hypreal_number_of];
    98 
    99 
   100 (** Less-than-or-equals (<=) **)
   101 
   102 Goal "(number_of x <= (number_of y::hypreal)) = \
   103 \     (~ number_of y < (number_of x::hypreal))";
   104 by (rtac (linorder_not_less RS sym) 1);
   105 qed "le_hypreal_number_of_eq_not_less";
   106 Addsimps [le_hypreal_number_of_eq_not_less];
   107 
   108 (*** New versions of existing theorems involving 0, 1 ***)
   109 
   110 Goal "- 1 = (-1::hypreal)";
   111 by (simp_tac (simpset() addsimps [hypreal_numeral_1_eq_1 RS sym]) 1);
   112 qed "hypreal_minus_1_eq_m1";
   113 
   114 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
   115 val hypreal_numeral_ss =
   116     real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym,
   117                               hypreal_numeral_1_eq_1 RS sym,
   118                               hypreal_minus_1_eq_m1];
   119 
   120 fun rename_numerals th =
   121     asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th);
   122 
   123 
   124 (** Simplification of arithmetic when nested to the right **)
   125 
   126 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)";
   127 by Auto_tac;
   128 qed "hypreal_add_number_of_left";
   129 
   130 Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)";
   131 by (simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   132 qed "hypreal_mult_number_of_left";
   133 
   134 Goalw [hypreal_diff_def]
   135     "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::hypreal)";
   136 by (rtac hypreal_add_number_of_left 1);
   137 qed "hypreal_add_number_of_diff1";
   138 
   139 Goal "number_of v + (c - number_of w) = \
   140 \     number_of (bin_add v (bin_minus w)) + (c::hypreal)";
   141 by (stac (diff_hypreal_number_of RS sym) 1);
   142 by Auto_tac;
   143 qed "hypreal_add_number_of_diff2";
   144 
   145 Addsimps [hypreal_add_number_of_left, hypreal_mult_number_of_left,
   146           hypreal_add_number_of_diff1, hypreal_add_number_of_diff2];
   147 
   148 
   149 (**** Simprocs for numeric literals ****)
   150 
   151 (** Combining of literal coefficients in sums of products **)
   152 
   153 Goal "(x < y) = (x-y < (0::hypreal))";
   154 by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
   155 qed "hypreal_less_iff_diff_less_0";
   156 
   157 Goal "(x = y) = (x-y = (0::hypreal))";
   158 by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1);
   159 qed "hypreal_eq_iff_diff_eq_0";
   160 
   161 Goal "(x <= y) = (x-y <= (0::hypreal))";
   162 by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1);
   163 qed "hypreal_le_iff_diff_le_0";
   164 
   165 
   166 (** For combine_numerals **)
   167 
   168 Goal "i*u + (j*u + k) = (i+j)*u + (k::hypreal)";
   169 by (asm_simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
   170 qed "left_hypreal_add_mult_distrib";
   171 
   172 
   173 (** For cancel_numerals **)
   174 
   175 val rel_iff_rel_0_rls =
   176     map (inst "y" "?u+?v")
   177       [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
   178        hypreal_le_iff_diff_le_0] @
   179     map (inst "y" "n")
   180       [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
   181        hypreal_le_iff_diff_le_0];
   182 
   183 Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
   184 by (asm_simp_tac
   185     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   186                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
   187 qed "hypreal_eq_add_iff1";
   188 
   189 Goal "!!i::hypreal. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
   190 by (asm_simp_tac
   191     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   192                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
   193 qed "hypreal_eq_add_iff2";
   194 
   195 Goal "!!i::hypreal. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
   196 by (asm_simp_tac
   197     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   198                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
   199 qed "hypreal_less_add_iff1";
   200 
   201 Goal "!!i::hypreal. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
   202 by (asm_simp_tac
   203     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   204                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
   205 qed "hypreal_less_add_iff2";
   206 
   207 Goal "!!i::hypreal. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
   208 by (asm_simp_tac
   209     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   210                          hypreal_add_ac@rel_iff_rel_0_rls) 1);
   211 qed "hypreal_le_add_iff1";
   212 
   213 Goal "!!i::hypreal. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
   214 by (asm_simp_tac
   215     (simpset() addsimps [hypreal_diff_def, hypreal_add_mult_distrib]@
   216                         hypreal_add_ac@rel_iff_rel_0_rls) 1);
   217 qed "hypreal_le_add_iff2";
   218 
   219 Goal "-1 * (z::hypreal) = -z";
   220 by (simp_tac (simpset() addsimps [hypreal_minus_1_eq_m1 RS sym,
   221                                   hypreal_mult_minus_1]) 1);
   222 qed "hypreal_mult_minus1";
   223 Addsimps [hypreal_mult_minus1];
   224 
   225 Goal "(z::hypreal) * -1 = -z";
   226 by (stac hypreal_mult_commute 1 THEN rtac hypreal_mult_minus1 1);
   227 qed "hypreal_mult_minus1_right";
   228 Addsimps [hypreal_mult_minus1_right];
   229 
   230 
   231 Addsimps [hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1];
   232 
   233 
   234 structure Hyperreal_Numeral_Simprocs =
   235 struct
   236 
   237 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
   238   isn't complicated by the abstract 0 and 1.*)
   239 val numeral_syms = [hypreal_numeral_0_eq_0 RS sym,
   240                     hypreal_numeral_1_eq_1 RS sym];
   241 
   242 (*Utilities*)
   243 
   244 val hyprealT = Type("HyperDef.hypreal",[]);
   245 
   246 fun mk_numeral n = HOLogic.number_of_const hyprealT $ HOLogic.mk_bin n;
   247 
   248 val dest_numeral = Real_Numeral_Simprocs.dest_numeral;
   249 
   250 val find_first_numeral = Real_Numeral_Simprocs.find_first_numeral;
   251 
   252 val zero = mk_numeral 0;
   253 val mk_plus = Real_Numeral_Simprocs.mk_plus;
   254 
   255 val uminus_const = Const ("uminus", hyprealT --> hyprealT);
   256 
   257 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   258 fun mk_sum []        = zero
   259   | mk_sum [t,u]     = mk_plus (t, u)
   260   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   261 
   262 (*this version ALWAYS includes a trailing zero*)
   263 fun long_mk_sum []        = zero
   264   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   265 
   266 val dest_plus = HOLogic.dest_bin "op +" hyprealT;
   267 
   268 (*decompose additions AND subtractions as a sum*)
   269 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   270         dest_summing (pos, t, dest_summing (pos, u, ts))
   271   | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   272         dest_summing (pos, t, dest_summing (not pos, u, ts))
   273   | dest_summing (pos, t, ts) =
   274         if pos then t::ts else uminus_const$t :: ts;
   275 
   276 fun dest_sum t = dest_summing (true, t, []);
   277 
   278 val mk_diff = HOLogic.mk_binop "op -";
   279 val dest_diff = HOLogic.dest_bin "op -" hyprealT;
   280 
   281 val one = mk_numeral 1;
   282 val mk_times = HOLogic.mk_binop "op *";
   283 
   284 fun mk_prod [] = one
   285   | mk_prod [t] = t
   286   | mk_prod (t :: ts) = if t = one then mk_prod ts
   287                         else mk_times (t, mk_prod ts);
   288 
   289 val dest_times = HOLogic.dest_bin "op *" hyprealT;
   290 
   291 fun dest_prod t =
   292       let val (t,u) = dest_times t
   293       in  dest_prod t @ dest_prod u  end
   294       handle TERM _ => [t];
   295 
   296 (*DON'T do the obvious simplifications; that would create special cases*)
   297 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   298 
   299 (*Express t as a product of (possibly) a numeral with other sorted terms*)
   300 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   301   | dest_coeff sign t =
   302     let val ts = sort Term.term_ord (dest_prod t)
   303         val (n, ts') = find_first_numeral [] ts
   304                           handle TERM _ => (1, ts)
   305     in (sign*n, mk_prod ts') end;
   306 
   307 (*Find first coefficient-term THAT MATCHES u*)
   308 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   309   | find_first_coeff past u (t::terms) =
   310         let val (n,u') = dest_coeff 1 t
   311         in  if u aconv u' then (n, rev past @ terms)
   312                           else find_first_coeff (t::past) u terms
   313         end
   314         handle TERM _ => find_first_coeff (t::past) u terms;
   315 
   316 
   317 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
   318 val add_0s = map rename_numerals
   319                  [hypreal_add_zero_left, hypreal_add_zero_right];
   320 val mult_1s = map rename_numerals [hypreal_mult_1, hypreal_mult_1_right] @
   321               [hypreal_mult_minus1, hypreal_mult_minus1_right];
   322 
   323 (*To perform binary arithmetic*)
   324 val bin_simps =
   325     [hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym,
   326      add_hypreal_number_of, hypreal_add_number_of_left,
   327      minus_hypreal_number_of,
   328      diff_hypreal_number_of, mult_hypreal_number_of,
   329      hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
   330 
   331 (*To evaluate binary negations of coefficients*)
   332 val hypreal_minus_simps = NCons_simps @
   333                    [hypreal_minus_1_eq_m1, minus_hypreal_number_of,
   334                     bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   335                     bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   336 
   337 (*To let us treat subtraction as addition*)
   338 val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib,
   339                   hypreal_minus_minus];
   340 
   341 (*push the unary minus down: - x * y = x * - y *)
   342 val hypreal_minus_mult_eq_1_to_2 =
   343     [hypreal_minus_mult_eq1 RS sym, hypreal_minus_mult_eq2] MRS trans
   344     |> standard;
   345 
   346 (*to extract again any uncancelled minuses*)
   347 val hypreal_minus_from_mult_simps =
   348     [hypreal_minus_minus, hypreal_minus_mult_eq1 RS sym,
   349      hypreal_minus_mult_eq2 RS sym];
   350 
   351 (*combine unary minus with numeric literals, however nested within a product*)
   352 val hypreal_mult_minus_simps =
   353     [hypreal_mult_assoc, hypreal_minus_mult_eq1, hypreal_minus_mult_eq_1_to_2];
   354 
   355 (*Final simplification: cancel + and *  *)
   356 val simplify_meta_eq =
   357     Int_Numeral_Simprocs.simplify_meta_eq
   358          [hypreal_add_zero_left, hypreal_add_zero_right,
   359           hypreal_mult_0, hypreal_mult_0_right, hypreal_mult_1,
   360           hypreal_mult_1_right];
   361 
   362 val prep_simproc = Real_Numeral_Simprocs.prep_simproc;
   363 
   364 structure CancelNumeralsCommon =
   365   struct
   366   val mk_sum            = mk_sum
   367   val dest_sum          = dest_sum
   368   val mk_coeff          = mk_coeff
   369   val dest_coeff        = dest_coeff 1
   370   val find_first_coeff  = find_first_coeff []
   371   val trans_tac         = Real_Numeral_Simprocs.trans_tac
   372   val norm_tac =
   373      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   374                                          hypreal_minus_simps@hypreal_add_ac))
   375      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
   376      THEN ALLGOALS
   377               (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
   378                                          hypreal_add_ac@hypreal_mult_ac))
   379   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   380   val simplify_meta_eq  = simplify_meta_eq
   381   end;
   382 
   383 
   384 structure EqCancelNumerals = CancelNumeralsFun
   385  (open CancelNumeralsCommon
   386   val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealeq_cancel_numerals"
   387   val mk_bal   = HOLogic.mk_eq
   388   val dest_bal = HOLogic.dest_bin "op =" hyprealT
   389   val bal_add1 = hypreal_eq_add_iff1 RS trans
   390   val bal_add2 = hypreal_eq_add_iff2 RS trans
   391 );
   392 
   393 structure LessCancelNumerals = CancelNumeralsFun
   394  (open CancelNumeralsCommon
   395   val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealless_cancel_numerals"
   396   val mk_bal   = HOLogic.mk_binrel "op <"
   397   val dest_bal = HOLogic.dest_bin "op <" hyprealT
   398   val bal_add1 = hypreal_less_add_iff1 RS trans
   399   val bal_add2 = hypreal_less_add_iff2 RS trans
   400 );
   401 
   402 structure LeCancelNumerals = CancelNumeralsFun
   403  (open CancelNumeralsCommon
   404   val prove_conv = Real_Numeral_Simprocs.prove_conv "hyprealle_cancel_numerals"
   405   val mk_bal   = HOLogic.mk_binrel "op <="
   406   val dest_bal = HOLogic.dest_bin "op <=" hyprealT
   407   val bal_add1 = hypreal_le_add_iff1 RS trans
   408   val bal_add2 = hypreal_le_add_iff2 RS trans
   409 );
   410 
   411 val cancel_numerals =
   412   map prep_simproc
   413    [("hyprealeq_cancel_numerals",
   414      ["(l::hypreal) + m = n", "(l::hypreal) = m + n",
   415       "(l::hypreal) - m = n", "(l::hypreal) = m - n",
   416       "(l::hypreal) * m = n", "(l::hypreal) = m * n"],
   417      EqCancelNumerals.proc),
   418     ("hyprealless_cancel_numerals",
   419      ["(l::hypreal) + m < n", "(l::hypreal) < m + n",
   420       "(l::hypreal) - m < n", "(l::hypreal) < m - n",
   421       "(l::hypreal) * m < n", "(l::hypreal) < m * n"],
   422      LessCancelNumerals.proc),
   423     ("hyprealle_cancel_numerals",
   424      ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n",
   425       "(l::hypreal) - m <= n", "(l::hypreal) <= m - n",
   426       "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
   427      LeCancelNumerals.proc)];
   428 
   429 
   430 structure CombineNumeralsData =
   431   struct
   432   val add               = op + : int*int -> int
   433   val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   434   val dest_sum          = dest_sum
   435   val mk_coeff          = mk_coeff
   436   val dest_coeff        = dest_coeff 1
   437   val left_distrib      = left_hypreal_add_mult_distrib RS trans
   438   val prove_conv        = Real_Numeral_Simprocs.prove_conv_nohyps
   439                                                 "hypreal_combine_numerals"
   440   val trans_tac         = Real_Numeral_Simprocs.trans_tac
   441   val norm_tac =
   442      ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   443                                          hypreal_minus_simps@hypreal_add_ac))
   444      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
   445      THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
   446                                               hypreal_add_ac@hypreal_mult_ac))
   447   val numeral_simp_tac  = ALLGOALS
   448                     (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   449   val simplify_meta_eq  = simplify_meta_eq
   450   end;
   451 
   452 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   453 
   454 val combine_numerals =
   455   prep_simproc
   456     ("hypreal_combine_numerals", ["(i::hypreal) + j", "(i::hypreal) - j"], CombineNumerals.proc);
   457 
   458 
   459 (** Declarations for ExtractCommonTerm **)
   460 
   461 (*this version ALWAYS includes a trailing one*)
   462 fun long_mk_prod []        = one
   463   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   464 
   465 (*Find first term that matches u*)
   466 fun find_first past u []         = raise TERM("find_first", [])
   467   | find_first past u (t::terms) =
   468         if u aconv t then (rev past @ terms)
   469         else find_first (t::past) u terms
   470         handle TERM _ => find_first (t::past) u terms;
   471 
   472 (*Final simplification: cancel + and *  *)
   473 fun cancel_simplify_meta_eq cancel_th th =
   474     Int_Numeral_Simprocs.simplify_meta_eq
   475         [hypreal_mult_1, hypreal_mult_1_right]
   476         (([th, cancel_th]) MRS trans);
   477 
   478 (*** Making constant folding work for 0 and 1 too ***)
   479 
   480 structure HyperrealAbstractNumeralsData =
   481   struct
   482   val dest_eq         = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   483   val is_numeral      = Bin_Simprocs.is_numeral
   484   val numeral_0_eq_0  = hypreal_numeral_0_eq_0
   485   val numeral_1_eq_1  = hypreal_numeral_1_eq_1
   486   val prove_conv      = Real_Numeral_Simprocs.prove_conv_nohyps
   487                           "hypreal_abstract_numerals"
   488   fun norm_tac simps  = ALLGOALS (simp_tac (HOL_ss addsimps simps))
   489   val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
   490   end
   491 
   492 structure HyperrealAbstractNumerals =
   493   AbstractNumeralsFun (HyperrealAbstractNumeralsData)
   494 
   495 (*For addition, we already have rules for the operand 0.
   496   Multiplication is omitted because there are already special rules for
   497   both 0 and 1 as operands.  Unary minus is trivial, just have - 1 = -1.
   498   For the others, having three patterns is a compromise between just having
   499   one (many spurious calls) and having nine (just too many!) *)
   500 val eval_numerals =
   501   map prep_simproc
   502    [("hypreal_add_eval_numerals",
   503      ["(m::hypreal) + 1", "(m::hypreal) + number_of v"],
   504      HyperrealAbstractNumerals.proc add_hypreal_number_of),
   505     ("hypreal_diff_eval_numerals",
   506      ["(m::hypreal) - 1", "(m::hypreal) - number_of v"],
   507      HyperrealAbstractNumerals.proc diff_hypreal_number_of),
   508     ("hypreal_eq_eval_numerals",
   509      ["(m::hypreal) = 0", "(m::hypreal) = 1", "(m::hypreal) = number_of v"],
   510      HyperrealAbstractNumerals.proc eq_hypreal_number_of),
   511     ("hypreal_less_eval_numerals",
   512      ["(m::hypreal) < 0", "(m::hypreal) < 1", "(m::hypreal) < number_of v"],
   513      HyperrealAbstractNumerals.proc less_hypreal_number_of),
   514     ("hypreal_le_eval_numerals",
   515      ["(m::hypreal) <= 0", "(m::hypreal) <= 1", "(m::hypreal) <= number_of v"],
   516      HyperrealAbstractNumerals.proc le_hypreal_number_of_eq_not_less)]
   517 
   518 end;
   519 
   520 Addsimprocs Hyperreal_Numeral_Simprocs.eval_numerals;
   521 Addsimprocs Hyperreal_Numeral_Simprocs.cancel_numerals;
   522 Addsimprocs [Hyperreal_Numeral_Simprocs.combine_numerals];
   523 
   524 (*The Abel_Cancel simprocs are now obsolete*)
   525 Delsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
   526 
   527 (*examples:
   528 print_depth 22;
   529 set timing;
   530 set trace_simp;
   531 fun test s = (Goal s, by (Simp_tac 1));
   532 
   533 test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
   534 test "2*u = (u::hypreal)";
   535 test "(i + j + 12 + (k::hypreal)) - 15 = y";
   536 test "(i + j + 12 + (k::hypreal)) - 5 = y";
   537 
   538 test "y - b < (b::hypreal)";
   539 test "y - (3*b + c) < (b::hypreal) - 2*c";
   540 
   541 test "(2*x - (u*v) + y) - v*3*u = (w::hypreal)";
   542 test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::hypreal)";
   543 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::hypreal)";
   544 test "u*v - (x*u*v + (u*v)*4 + y) = (w::hypreal)";
   545 
   546 test "(i + j + 12 + (k::hypreal)) = u + 15 + y";
   547 test "(i + j*2 + 12 + (k::hypreal)) = j + 5 + y";
   548 
   549 test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::hypreal)";
   550 
   551 test "a + -(b+c) + b = (d::hypreal)";
   552 test "a + -(b+c) - b = (d::hypreal)";
   553 
   554 (*negative numerals*)
   555 test "(i + j + -2 + (k::hypreal)) - (u + 5 + y) = zz";
   556 test "(i + j + -3 + (k::hypreal)) < u + 5 + y";
   557 test "(i + j + 3 + (k::hypreal)) < u + -6 + y";
   558 test "(i + j + -12 + (k::hypreal)) - 15 = y";
   559 test "(i + j + 12 + (k::hypreal)) - -15 = y";
   560 test "(i + j + -12 + (k::hypreal)) - -15 = y";
   561 *)
   562 
   563 
   564 (** Constant folding for hypreal plus and times **)
   565 
   566 (*We do not need
   567     structure Hyperreal_Plus_Assoc = Assoc_Fold (Hyperreal_Plus_Assoc_Data);
   568   because combine_numerals does the same thing*)
   569 
   570 structure Hyperreal_Times_Assoc_Data : ASSOC_FOLD_DATA =
   571 struct
   572   val ss                = HOL_ss
   573   val eq_reflection     = eq_reflection
   574   val sg_ref    = Sign.self_ref (Theory.sign_of (the_context ()))
   575   val T      = Hyperreal_Numeral_Simprocs.hyprealT
   576   val plus   = Const ("op *", [T,T] ---> T)
   577   val add_ac = hypreal_mult_ac
   578 end;
   579 
   580 structure Hyperreal_Times_Assoc = Assoc_Fold (Hyperreal_Times_Assoc_Data);
   581 
   582 Addsimprocs [Hyperreal_Times_Assoc.conv];
   583 
   584 (*Simplification of  x-y < 0, etc.*)
   585 AddIffs [hypreal_less_iff_diff_less_0 RS sym];
   586 AddIffs [hypreal_eq_iff_diff_eq_0 RS sym];
   587 AddIffs [hypreal_le_iff_diff_le_0 RS sym];
   588 
   589 
   590 (** number_of related to hypreal_of_real **)
   591 
   592 Goal "(number_of w < hypreal_of_real z) = (number_of w < z)";
   593 by (stac (hypreal_of_real_less_iff RS sym) 1);
   594 by (Simp_tac 1);
   595 qed "number_of_less_hypreal_of_real_iff";
   596 Addsimps [number_of_less_hypreal_of_real_iff];
   597 
   598 Goal "(number_of w <= hypreal_of_real z) = (number_of w <= z)";
   599 by (stac (hypreal_of_real_le_iff RS sym) 1);
   600 by (Simp_tac 1);
   601 qed "number_of_le_hypreal_of_real_iff";
   602 Addsimps [number_of_le_hypreal_of_real_iff];
   603 
   604 Goal "(hypreal_of_real z = number_of w) = (z = number_of w)";
   605 by (stac (hypreal_of_real_eq_iff RS sym) 1);
   606 by (Simp_tac 1);
   607 qed "hypreal_of_real_eq_number_of_iff";
   608 Addsimps [hypreal_of_real_eq_number_of_iff];
   609 
   610 Goal "(hypreal_of_real z < number_of w) = (z < number_of w)";
   611 by (stac (hypreal_of_real_less_iff RS sym) 1);
   612 by (Simp_tac 1);
   613 qed "hypreal_of_real_less_number_of_iff";
   614 Addsimps [hypreal_of_real_less_number_of_iff];
   615 
   616 Goal "(hypreal_of_real z <= number_of w) = (z <= number_of w)";
   617 by (stac (hypreal_of_real_le_iff RS sym) 1);
   618 by (Simp_tac 1);
   619 qed "hypreal_of_real_le_number_of_iff";
   620 Addsimps [hypreal_of_real_le_number_of_iff];
   621 
   622 (*As above, for the special case of zero*)
   623 Addsimps
   624   (map (simplify (simpset()) o inst "w" "Pls")
   625    [hypreal_of_real_eq_number_of_iff,
   626     hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
   627     number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
   628 
   629 (*As above, for the special case of one*)
   630 Addsimps
   631   (map (simplify (simpset()) o inst "w" "Pls BIT True")
   632    [hypreal_of_real_eq_number_of_iff,
   633     hypreal_of_real_le_number_of_iff, hypreal_of_real_less_number_of_iff,
   634     number_of_le_hypreal_of_real_iff, number_of_less_hypreal_of_real_iff]);
   635 
   636 (** <= monotonicity results: needed for arithmetic **)
   637 
   638 Goal "[| i <= j;  (0::hypreal) <= k |] ==> i*k <= j*k";
   639 by (auto_tac (claset(),
   640               simpset() addsimps [order_le_less, hypreal_mult_less_mono1]));
   641 qed "hypreal_mult_le_mono1";
   642 
   643 Goal "[| i <= j;  (0::hypreal) <= k |] ==> k*i <= k*j";
   644 by (dtac hypreal_mult_le_mono1 1);
   645 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));
   646 qed "hypreal_mult_le_mono2";
   647 
   648 Goal "[| u <= v;  x <= y;  0 <= v;  (0::hypreal) <= x |] ==> u * x <= v * y";
   649 by (etac (hypreal_mult_le_mono1 RS order_trans) 1);
   650 by (assume_tac 1);
   651 by (etac hypreal_mult_le_mono2 1);
   652 by (assume_tac 1);
   653 qed "hypreal_mult_le_mono";
   654 
   655 Addsimps [hypreal_minus_1_eq_m1];