src/HOL/Tools/int_arith.ML
changeset 28952 15a4b2cf8c34
parent 28262 aa7ca36d67fd
child 29269 5c25a2012975
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,588 @@
     1.4 +(*  Title:      HOL/int_arith1.ML
     1.5 +    ID:         $Id$
     1.6 +    Authors:    Larry Paulson and Tobias Nipkow
     1.7 +
     1.8 +Simprocs and decision procedure for linear arithmetic.
     1.9 +*)
    1.10 +
    1.11 +structure Int_Numeral_Base_Simprocs =
    1.12 +  struct
    1.13 +  fun prove_conv tacs ctxt (_: thm list) (t, u) =
    1.14 +    if t aconv u then NONE
    1.15 +    else
    1.16 +      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    1.17 +      in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end
    1.18 +
    1.19 +  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    1.20 +
    1.21 +  fun prep_simproc (name, pats, proc) =
    1.22 +    Simplifier.simproc (the_context()) name pats proc;
    1.23 +
    1.24 +  fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
    1.25 +    | is_numeral _ = false
    1.26 +
    1.27 +  fun simplify_meta_eq f_number_of_eq f_eq =
    1.28 +      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
    1.29 +
    1.30 +  (*reorientation simprules using ==, for the following simproc*)
    1.31 +  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
    1.32 +  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
    1.33 +  val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
    1.34 +
    1.35 +  (*reorientation simplification procedure: reorients (polymorphic) 
    1.36 +    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
    1.37 +  fun reorient_proc sg _ (_ $ t $ u) =
    1.38 +    case u of
    1.39 +        Const(@{const_name HOL.zero}, _) => NONE
    1.40 +      | Const(@{const_name HOL.one}, _) => NONE
    1.41 +      | Const(@{const_name Int.number_of}, _) $ _ => NONE
    1.42 +      | _ => SOME (case t of
    1.43 +          Const(@{const_name HOL.zero}, _) => meta_zero_reorient
    1.44 +        | Const(@{const_name HOL.one}, _) => meta_one_reorient
    1.45 +        | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
    1.46 +
    1.47 +  val reorient_simproc = 
    1.48 +      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
    1.49 +
    1.50 +  end;
    1.51 +
    1.52 +
    1.53 +Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
    1.54 +
    1.55 +
    1.56 +structure Int_Numeral_Simprocs =
    1.57 +struct
    1.58 +
    1.59 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
    1.60 +  isn't complicated by the abstract 0 and 1.*)
    1.61 +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
    1.62 +
    1.63 +(** New term ordering so that AC-rewriting brings numerals to the front **)
    1.64 +
    1.65 +(*Order integers by absolute value and then by sign. The standard integer
    1.66 +  ordering is not well-founded.*)
    1.67 +fun num_ord (i,j) =
    1.68 +  (case int_ord (abs i, abs j) of
    1.69 +    EQUAL => int_ord (Int.sign i, Int.sign j) 
    1.70 +  | ord => ord);
    1.71 +
    1.72 +(*This resembles Term.term_ord, but it puts binary numerals before other
    1.73 +  non-atomic terms.*)
    1.74 +local open Term 
    1.75 +in 
    1.76 +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.77 +      (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.78 +  | numterm_ord
    1.79 +     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
    1.80 +     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
    1.81 +  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
    1.82 +  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
    1.83 +  | numterm_ord (t, u) =
    1.84 +      (case int_ord (size_of_term t, size_of_term u) of
    1.85 +        EQUAL =>
    1.86 +          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.87 +            (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
    1.88 +          end
    1.89 +      | ord => ord)
    1.90 +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    1.91 +end;
    1.92 +
    1.93 +fun numtermless tu = (numterm_ord tu = LESS);
    1.94 +
    1.95 +(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
    1.96 +val num_ss = HOL_ss settermless numtermless;
    1.97 +
    1.98 +
    1.99 +(** Utilities **)
   1.100 +
   1.101 +fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
   1.102 +
   1.103 +fun find_first_numeral past (t::terms) =
   1.104 +        ((snd (HOLogic.dest_number t), rev past @ terms)
   1.105 +         handle TERM _ => find_first_numeral (t::past) terms)
   1.106 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
   1.107 +
   1.108 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
   1.109 +
   1.110 +fun mk_minus t = 
   1.111 +  let val T = Term.fastype_of t
   1.112 +  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
   1.113 +
   1.114 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   1.115 +fun mk_sum T []        = mk_number T 0
   1.116 +  | mk_sum T [t,u]     = mk_plus (t, u)
   1.117 +  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
   1.118 +
   1.119 +(*this version ALWAYS includes a trailing zero*)
   1.120 +fun long_mk_sum T []        = mk_number T 0
   1.121 +  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
   1.122 +
   1.123 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
   1.124 +
   1.125 +(*decompose additions AND subtractions as a sum*)
   1.126 +fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
   1.127 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   1.128 +  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
   1.129 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   1.130 +  | dest_summing (pos, t, ts) =
   1.131 +        if pos then t::ts else mk_minus t :: ts;
   1.132 +
   1.133 +fun dest_sum t = dest_summing (true, t, []);
   1.134 +
   1.135 +val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
   1.136 +val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
   1.137 +
   1.138 +val mk_times = HOLogic.mk_binop @{const_name HOL.times};
   1.139 +
   1.140 +fun one_of T = Const(@{const_name HOL.one},T);
   1.141 +
   1.142 +(* build product with trailing 1 rather than Numeral 1 in order to avoid the
   1.143 +   unnecessary restriction to type class number_ring
   1.144 +   which is not required for cancellation of common factors in divisions.
   1.145 +*)
   1.146 +fun mk_prod T = 
   1.147 +  let val one = one_of T
   1.148 +  fun mk [] = one
   1.149 +    | mk [t] = t
   1.150 +    | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
   1.151 +  in mk end;
   1.152 +
   1.153 +(*This version ALWAYS includes a trailing one*)
   1.154 +fun long_mk_prod T []        = one_of T
   1.155 +  | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
   1.156 +
   1.157 +val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
   1.158 +
   1.159 +fun dest_prod t =
   1.160 +      let val (t,u) = dest_times t
   1.161 +      in dest_prod t @ dest_prod u end
   1.162 +      handle TERM _ => [t];
   1.163 +
   1.164 +(*DON'T do the obvious simplifications; that would create special cases*)
   1.165 +fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   1.166 +
   1.167 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   1.168 +fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   1.169 +  | dest_coeff sign t =
   1.170 +    let val ts = sort Term.term_ord (dest_prod t)
   1.171 +        val (n, ts') = find_first_numeral [] ts
   1.172 +                          handle TERM _ => (1, ts)
   1.173 +    in (sign*n, mk_prod (Term.fastype_of t) ts') end;
   1.174 +
   1.175 +(*Find first coefficient-term THAT MATCHES u*)
   1.176 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   1.177 +  | find_first_coeff past u (t::terms) =
   1.178 +        let val (n,u') = dest_coeff 1 t
   1.179 +        in if u aconv u' then (n, rev past @ terms)
   1.180 +                         else find_first_coeff (t::past) u terms
   1.181 +        end
   1.182 +        handle TERM _ => find_first_coeff (t::past) u terms;
   1.183 +
   1.184 +(*Fractions as pairs of ints. Can't use Rat.rat because the representation
   1.185 +  needs to preserve negative values in the denominator.*)
   1.186 +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
   1.187 +
   1.188 +(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   1.189 +  Fractions are reduced later by the cancel_numeral_factor simproc.*)
   1.190 +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   1.191 +
   1.192 +val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
   1.193 +
   1.194 +(*Build term (p / q) * t*)
   1.195 +fun mk_fcoeff ((p, q), t) =
   1.196 +  let val T = Term.fastype_of t
   1.197 +  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   1.198 +
   1.199 +(*Express t as a product of a fraction with other sorted terms*)
   1.200 +fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
   1.201 +  | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
   1.202 +    let val (p, t') = dest_coeff sign t
   1.203 +        val (q, u') = dest_coeff 1 u
   1.204 +    in (mk_frac (p, q), mk_divide (t', u')) end
   1.205 +  | dest_fcoeff sign t =
   1.206 +    let val (p, t') = dest_coeff sign t
   1.207 +        val T = Term.fastype_of t
   1.208 +    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
   1.209 +
   1.210 +
   1.211 +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
   1.212 +val add_0s =  thms "add_0s";
   1.213 +val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
   1.214 +
   1.215 +(*Simplify inverse Numeral1, a/Numeral1*)
   1.216 +val inverse_1s = [@{thm inverse_numeral_1}];
   1.217 +val divide_1s = [@{thm divide_numeral_1}];
   1.218 +
   1.219 +(*To perform binary arithmetic.  The "left" rewriting handles patterns
   1.220 +  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
   1.221 +val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
   1.222 +                 @{thm add_number_of_left}, @{thm mult_number_of_left}] @
   1.223 +                @{thms arith_simps} @ @{thms rel_simps};
   1.224 +
   1.225 +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   1.226 +  during re-arrangement*)
   1.227 +val non_add_simps =
   1.228 +  subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
   1.229 +
   1.230 +(*To evaluate binary negations of coefficients*)
   1.231 +val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
   1.232 +                   @{thms minus_bin_simps} @ @{thms pred_bin_simps};
   1.233 +
   1.234 +(*To let us treat subtraction as addition*)
   1.235 +val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
   1.236 +
   1.237 +(*To let us treat division as multiplication*)
   1.238 +val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   1.239 +
   1.240 +(*push the unary minus down: - x * y = x * - y *)
   1.241 +val minus_mult_eq_1_to_2 =
   1.242 +    [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
   1.243 +
   1.244 +(*to extract again any uncancelled minuses*)
   1.245 +val minus_from_mult_simps =
   1.246 +    [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
   1.247 +
   1.248 +(*combine unary minus with numeric literals, however nested within a product*)
   1.249 +val mult_minus_simps =
   1.250 +    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
   1.251 +
   1.252 +(*Apply the given rewrite (if present) just once*)
   1.253 +fun trans_tac NONE      = all_tac
   1.254 +  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
   1.255 +
   1.256 +fun simplify_meta_eq rules =
   1.257 +  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
   1.258 +  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
   1.259 +
   1.260 +structure CancelNumeralsCommon =
   1.261 +  struct
   1.262 +  val mk_sum            = mk_sum
   1.263 +  val dest_sum          = dest_sum
   1.264 +  val mk_coeff          = mk_coeff
   1.265 +  val dest_coeff        = dest_coeff 1
   1.266 +  val find_first_coeff  = find_first_coeff []
   1.267 +  val trans_tac         = fn _ => trans_tac
   1.268 +
   1.269 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.270 +    diff_simps @ minus_simps @ @{thms add_ac}
   1.271 +  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   1.272 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.273 +  fun norm_tac ss =
   1.274 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.275 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.276 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   1.277 +
   1.278 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   1.279 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.280 +  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   1.281 +  end;
   1.282 +
   1.283 +
   1.284 +structure EqCancelNumerals = CancelNumeralsFun
   1.285 + (open CancelNumeralsCommon
   1.286 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.287 +  val mk_bal   = HOLogic.mk_eq
   1.288 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   1.289 +  val bal_add1 = @{thm eq_add_iff1} RS trans
   1.290 +  val bal_add2 = @{thm eq_add_iff2} RS trans
   1.291 +);
   1.292 +
   1.293 +structure LessCancelNumerals = CancelNumeralsFun
   1.294 + (open CancelNumeralsCommon
   1.295 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.296 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.297 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   1.298 +  val bal_add1 = @{thm less_add_iff1} RS trans
   1.299 +  val bal_add2 = @{thm less_add_iff2} RS trans
   1.300 +);
   1.301 +
   1.302 +structure LeCancelNumerals = CancelNumeralsFun
   1.303 + (open CancelNumeralsCommon
   1.304 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   1.305 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.306 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   1.307 +  val bal_add1 = @{thm le_add_iff1} RS trans
   1.308 +  val bal_add2 = @{thm le_add_iff2} RS trans
   1.309 +);
   1.310 +
   1.311 +val cancel_numerals =
   1.312 +  map Int_Numeral_Base_Simprocs.prep_simproc
   1.313 +   [("inteq_cancel_numerals",
   1.314 +     ["(l::'a::number_ring) + m = n",
   1.315 +      "(l::'a::number_ring) = m + n",
   1.316 +      "(l::'a::number_ring) - m = n",
   1.317 +      "(l::'a::number_ring) = m - n",
   1.318 +      "(l::'a::number_ring) * m = n",
   1.319 +      "(l::'a::number_ring) = m * n"],
   1.320 +     K EqCancelNumerals.proc),
   1.321 +    ("intless_cancel_numerals",
   1.322 +     ["(l::'a::{ordered_idom,number_ring}) + m < n",
   1.323 +      "(l::'a::{ordered_idom,number_ring}) < m + n",
   1.324 +      "(l::'a::{ordered_idom,number_ring}) - m < n",
   1.325 +      "(l::'a::{ordered_idom,number_ring}) < m - n",
   1.326 +      "(l::'a::{ordered_idom,number_ring}) * m < n",
   1.327 +      "(l::'a::{ordered_idom,number_ring}) < m * n"],
   1.328 +     K LessCancelNumerals.proc),
   1.329 +    ("intle_cancel_numerals",
   1.330 +     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
   1.331 +      "(l::'a::{ordered_idom,number_ring}) <= m + n",
   1.332 +      "(l::'a::{ordered_idom,number_ring}) - m <= n",
   1.333 +      "(l::'a::{ordered_idom,number_ring}) <= m - n",
   1.334 +      "(l::'a::{ordered_idom,number_ring}) * m <= n",
   1.335 +      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   1.336 +     K LeCancelNumerals.proc)];
   1.337 +
   1.338 +
   1.339 +structure CombineNumeralsData =
   1.340 +  struct
   1.341 +  type coeff            = int
   1.342 +  val iszero            = (fn x => x = 0)
   1.343 +  val add               = op +
   1.344 +  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   1.345 +  val dest_sum          = dest_sum
   1.346 +  val mk_coeff          = mk_coeff
   1.347 +  val dest_coeff        = dest_coeff 1
   1.348 +  val left_distrib      = @{thm combine_common_factor} RS trans
   1.349 +  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   1.350 +  val trans_tac         = fn _ => trans_tac
   1.351 +
   1.352 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.353 +    diff_simps @ minus_simps @ @{thms add_ac}
   1.354 +  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   1.355 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.356 +  fun norm_tac ss =
   1.357 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.358 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.359 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   1.360 +
   1.361 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   1.362 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.363 +  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
   1.364 +  end;
   1.365 +
   1.366 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.367 +
   1.368 +(*Version for fields, where coefficients can be fractions*)
   1.369 +structure FieldCombineNumeralsData =
   1.370 +  struct
   1.371 +  type coeff            = int * int
   1.372 +  val iszero            = (fn (p, q) => p = 0)
   1.373 +  val add               = add_frac
   1.374 +  val mk_sum            = long_mk_sum
   1.375 +  val dest_sum          = dest_sum
   1.376 +  val mk_coeff          = mk_fcoeff
   1.377 +  val dest_coeff        = dest_fcoeff 1
   1.378 +  val left_distrib      = @{thm combine_common_factor} RS trans
   1.379 +  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   1.380 +  val trans_tac         = fn _ => trans_tac
   1.381 +
   1.382 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.383 +    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
   1.384 +  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   1.385 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.386 +  fun norm_tac ss =
   1.387 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.388 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.389 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   1.390 +
   1.391 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   1.392 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.393 +  val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   1.394 +  end;
   1.395 +
   1.396 +structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   1.397 +
   1.398 +val combine_numerals =
   1.399 +  Int_Numeral_Base_Simprocs.prep_simproc
   1.400 +    ("int_combine_numerals", 
   1.401 +     ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   1.402 +     K CombineNumerals.proc);
   1.403 +
   1.404 +val field_combine_numerals =
   1.405 +  Int_Numeral_Base_Simprocs.prep_simproc
   1.406 +    ("field_combine_numerals", 
   1.407 +     ["(i::'a::{number_ring,field,division_by_zero}) + j",
   1.408 +      "(i::'a::{number_ring,field,division_by_zero}) - j"], 
   1.409 +     K FieldCombineNumerals.proc);
   1.410 +
   1.411 +end;
   1.412 +
   1.413 +Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   1.414 +Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   1.415 +Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
   1.416 +
   1.417 +(*examples:
   1.418 +print_depth 22;
   1.419 +set timing;
   1.420 +set trace_simp;
   1.421 +fun test s = (Goal s, by (Simp_tac 1));
   1.422 +
   1.423 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   1.424 +
   1.425 +test "2*u = (u::int)";
   1.426 +test "(i + j + 12 + (k::int)) - 15 = y";
   1.427 +test "(i + j + 12 + (k::int)) - 5 = y";
   1.428 +
   1.429 +test "y - b < (b::int)";
   1.430 +test "y - (3*b + c) < (b::int) - 2*c";
   1.431 +
   1.432 +test "(2*x - (u*v) + y) - v*3*u = (w::int)";
   1.433 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
   1.434 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
   1.435 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
   1.436 +
   1.437 +test "(i + j + 12 + (k::int)) = u + 15 + y";
   1.438 +test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
   1.439 +
   1.440 +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::int)";
   1.441 +
   1.442 +test "a + -(b+c) + b = (d::int)";
   1.443 +test "a + -(b+c) - b = (d::int)";
   1.444 +
   1.445 +(*negative numerals*)
   1.446 +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
   1.447 +test "(i + j + -3 + (k::int)) < u + 5 + y";
   1.448 +test "(i + j + 3 + (k::int)) < u + -6 + y";
   1.449 +test "(i + j + -12 + (k::int)) - 15 = y";
   1.450 +test "(i + j + 12 + (k::int)) - -15 = y";
   1.451 +test "(i + j + -12 + (k::int)) - -15 = y";
   1.452 +*)
   1.453 +
   1.454 +
   1.455 +(** Constant folding for multiplication in semirings **)
   1.456 +
   1.457 +(*We do not need folding for addition: combine_numerals does the same thing*)
   1.458 +
   1.459 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.460 +struct
   1.461 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   1.462 +  val eq_reflection = eq_reflection
   1.463 +end;
   1.464 +
   1.465 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   1.466 +
   1.467 +val assoc_fold_simproc =
   1.468 +  Int_Numeral_Base_Simprocs.prep_simproc
   1.469 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   1.470 +    K Semiring_Times_Assoc.proc);
   1.471 +
   1.472 +Addsimprocs [assoc_fold_simproc];
   1.473 +
   1.474 +
   1.475 +
   1.476 +
   1.477 +(*** decision procedure for linear arithmetic ***)
   1.478 +
   1.479 +(*---------------------------------------------------------------------------*)
   1.480 +(* Linear arithmetic                                                         *)
   1.481 +(*---------------------------------------------------------------------------*)
   1.482 +
   1.483 +(*
   1.484 +Instantiation of the generic linear arithmetic package for int.
   1.485 +*)
   1.486 +
   1.487 +(* Update parameters of arithmetic prover *)
   1.488 +local
   1.489 +
   1.490 +(* reduce contradictory =/</<= to False *)
   1.491 +
   1.492 +(* Evaluation of terms of the form "m R n" where R is one of "=", "<=" or "<",
   1.493 +   and m and n are ground terms over rings (roughly speaking).
   1.494 +   That is, m and n consist only of 1s combined with "+", "-" and "*".
   1.495 +*)
   1.496 +local
   1.497 +val zeroth = (symmetric o mk_meta_eq) @{thm of_int_0};
   1.498 +val lhss0 = [@{cpat "0::?'a::ring"}];
   1.499 +fun proc0 phi ss ct =
   1.500 +  let val T = ctyp_of_term ct
   1.501 +  in if typ_of T = @{typ int} then NONE else
   1.502 +     SOME (instantiate' [SOME T] [] zeroth)
   1.503 +  end;
   1.504 +val zero_to_of_int_zero_simproc =
   1.505 +  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   1.506 +  proc = proc0, identifier = []};
   1.507 +
   1.508 +val oneth = (symmetric o mk_meta_eq) @{thm of_int_1};
   1.509 +val lhss1 = [@{cpat "1::?'a::ring_1"}];
   1.510 +fun proc1 phi ss ct =
   1.511 +  let val T = ctyp_of_term ct
   1.512 +  in if typ_of T = @{typ int} then NONE else
   1.513 +     SOME (instantiate' [SOME T] [] oneth)
   1.514 +  end;
   1.515 +val one_to_of_int_one_simproc =
   1.516 +  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   1.517 +  proc = proc1, identifier = []};
   1.518 +
   1.519 +val allowed_consts =
   1.520 +  [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
   1.521 +   @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
   1.522 +   @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
   1.523 +   @{const_name "HOL.less_eq"}];
   1.524 +
   1.525 +fun check t = case t of
   1.526 +   Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
   1.527 +                else s mem_string allowed_consts
   1.528 + | a$b => check a andalso check b
   1.529 + | _ => false;
   1.530 +
   1.531 +val conv =
   1.532 +  Simplifier.rewrite
   1.533 +   (HOL_basic_ss addsimps
   1.534 +     ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult},
   1.535 +             @{thm of_int_diff},  @{thm of_int_minus}])@
   1.536 +      [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
   1.537 +     addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
   1.538 +
   1.539 +fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE
   1.540 +val lhss' =
   1.541 +  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
   1.542 +   @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"},
   1.543 +   @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}]
   1.544 +in
   1.545 +val zero_one_idom_simproc =
   1.546 +  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   1.547 +  proc = sproc, identifier = []}
   1.548 +end;
   1.549 +
   1.550 +val add_rules =
   1.551 +    simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
   1.552 +    [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
   1.553 +     @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
   1.554 +     @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
   1.555 +     @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
   1.556 +     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
   1.557 +     @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
   1.558 +     @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
   1.559 +     @{thm of_int_mult}]
   1.560 +
   1.561 +val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   1.562 +
   1.563 +val Int_Numeral_Base_Simprocs = assoc_fold_simproc :: zero_one_idom_simproc
   1.564 +  :: Int_Numeral_Simprocs.combine_numerals
   1.565 +  :: Int_Numeral_Simprocs.cancel_numerals;
   1.566 +
   1.567 +in
   1.568 +
   1.569 +val int_arith_setup =
   1.570 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   1.571 +   {add_mono_thms = add_mono_thms,
   1.572 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
   1.573 +    inj_thms = nat_inj_thms @ inj_thms,
   1.574 +    lessD = lessD @ [@{thm zless_imp_add1_zle}],
   1.575 +    neqE = neqE,
   1.576 +    simpset = simpset addsimps add_rules
   1.577 +                      addsimprocs Int_Numeral_Base_Simprocs
   1.578 +                      addcongs [if_weak_cong]}) #>
   1.579 +  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   1.580 +  arith_discrete @{type_name Int.int}
   1.581 +
   1.582 +end;
   1.583 +
   1.584 +val fast_int_arith_simproc =
   1.585 +  Simplifier.simproc (the_context ())
   1.586 +  "fast_int_arith" 
   1.587 +     ["(m::'a::{ordered_idom,number_ring}) < n",
   1.588 +      "(m::'a::{ordered_idom,number_ring}) <= n",
   1.589 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
   1.590 +
   1.591 +Addsimprocs [fast_int_arith_simproc];