modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
authorhaftmann
Fri May 08 09:48:07 2009 +0200 (2009-05-08)
changeset 31068f591144b0f17
parent 31067 fd7ec31f850c
child 31069 d47fa1db1820
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
src/HOL/Groebner_Basis.thy
src/HOL/Int.thy
src/HOL/IntDiv.thy
src/HOL/IsaMakefile
src/HOL/Nat_Numeral.thy
src/HOL/Tools/int_arith.ML
src/HOL/Tools/int_factor_simprocs.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/rat_arith.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri May 08 08:01:09 2009 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri May 08 09:48:07 2009 +0200
     1.3 @@ -635,7 +635,7 @@
     1.4  val comp_conv = (Simplifier.rewrite
     1.5  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
     1.6                addsimps ths addsimps simp_thms
     1.7 -              addsimprocs field_cancel_numeral_factors
     1.8 +              addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
     1.9                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
    1.10                              ord_frac_simproc]
    1.11                  addcongs [@{thm "if_weak_cong"}]))
     2.1 --- a/src/HOL/Int.thy	Fri May 08 08:01:09 2009 +0200
     2.2 +++ b/src/HOL/Int.thy	Fri May 08 09:48:07 2009 +0200
     2.3 @@ -12,13 +12,13 @@
     2.4  uses
     2.5    ("Tools/numeral.ML")
     2.6    ("Tools/numeral_syntax.ML")
     2.7 +  ("Tools/int_arith.ML")
     2.8    "~~/src/Provers/Arith/assoc_fold.ML"
     2.9    "~~/src/Provers/Arith/cancel_numerals.ML"
    2.10    "~~/src/Provers/Arith/combine_numerals.ML"
    2.11    "~~/src/Provers/Arith/cancel_numeral_factor.ML"
    2.12    "~~/src/Provers/Arith/extract_common_term.ML"
    2.13 -  ("Tools/int_factor_simprocs.ML")
    2.14 -  ("Tools/int_arith.ML")
    2.15 +  ("Tools/numeral_simprocs.ML")
    2.16  begin
    2.17  
    2.18  subsection {* The equivalence relation underlying the integers *}
    2.19 @@ -1518,9 +1518,10 @@
    2.20    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
    2.21    of_int_0 of_int_1 of_int_add of_int_mult
    2.22  
    2.23 +use "Tools/numeral_simprocs.ML"
    2.24 +
    2.25  use "Tools/int_arith.ML"
    2.26  declaration {* K Int_Arith.setup *}
    2.27 -use "Tools/int_factor_simprocs.ML"
    2.28  
    2.29  setup {*
    2.30    ReorientProc.add
     3.1 --- a/src/HOL/IntDiv.thy	Fri May 08 08:01:09 2009 +0200
     3.2 +++ b/src/HOL/IntDiv.thy	Fri May 08 09:48:07 2009 +0200
     3.3 @@ -252,8 +252,8 @@
     3.4    val div_name = @{const_name div};
     3.5    val mod_name = @{const_name mod};
     3.6    val mk_binop = HOLogic.mk_binop;
     3.7 -  val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
     3.8 -  val dest_sum = Int_Numeral_Simprocs.dest_sum;
     3.9 +  val mk_sum = Numeral_Simprocs.mk_sum HOLogic.intT;
    3.10 +  val dest_sum = Numeral_Simprocs.dest_sum;
    3.11  
    3.12    val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
    3.13  
     4.1 --- a/src/HOL/IsaMakefile	Fri May 08 08:01:09 2009 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Fri May 08 09:48:07 2009 +0200
     4.3 @@ -226,19 +226,19 @@
     4.4    $(SRC)/Provers/Arith/combine_numerals.ML \
     4.5    $(SRC)/Provers/Arith/extract_common_term.ML \
     4.6    $(SRC)/Tools/Metis/metis.ML \
     4.7 -  Tools/int_arith.ML \
     4.8 -  Tools/int_factor_simprocs.ML \
     4.9 -  Tools/nat_simprocs.ML \
    4.10    Tools/Groebner_Basis/groebner.ML \
    4.11    Tools/Groebner_Basis/misc.ML \
    4.12    Tools/Groebner_Basis/normalizer_data.ML \
    4.13    Tools/Groebner_Basis/normalizer.ML \
    4.14    Tools/atp_manager.ML \
    4.15    Tools/atp_wrapper.ML \
    4.16 +  Tools/int_arith.ML \
    4.17    Tools/list_code.ML \
    4.18    Tools/meson.ML \
    4.19    Tools/metis_tools.ML \
    4.20 +  Tools/nat_numeral_simprocs.ML \
    4.21    Tools/numeral.ML \
    4.22 +  Tools/numeral_simprocs.ML \
    4.23    Tools/numeral_syntax.ML \
    4.24    Tools/polyhash.ML \
    4.25    Tools/Qelim/cooper_data.ML \
     5.1 --- a/src/HOL/Nat_Numeral.thy	Fri May 08 08:01:09 2009 +0200
     5.2 +++ b/src/HOL/Nat_Numeral.thy	Fri May 08 09:48:07 2009 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  theory Nat_Numeral
     5.6  imports IntDiv
     5.7 -uses ("Tools/nat_simprocs.ML")
     5.8 +uses ("Tools/nat_numeral_simprocs.ML")
     5.9  begin
    5.10  
    5.11  subsection {* Numerals for natural numbers *}
    5.12 @@ -455,29 +455,6 @@
    5.13  
    5.14  declare dvd_eq_mod_eq_0_number_of [simp]
    5.15  
    5.16 -ML
    5.17 -{*
    5.18 -val nat_number_of_def = thm"nat_number_of_def";
    5.19 -
    5.20 -val nat_number_of = thm"nat_number_of";
    5.21 -val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0";
    5.22 -val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1";
    5.23 -val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
    5.24 -val numeral_2_eq_2 = thm"numeral_2_eq_2";
    5.25 -val nat_div_distrib = thm"nat_div_distrib";
    5.26 -val nat_mod_distrib = thm"nat_mod_distrib";
    5.27 -val int_nat_number_of = thm"int_nat_number_of";
    5.28 -val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
    5.29 -val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
    5.30 -val Suc_nat_number_of = thm"Suc_nat_number_of";
    5.31 -val add_nat_number_of = thm"add_nat_number_of";
    5.32 -val diff_nat_eq_if = thm"diff_nat_eq_if";
    5.33 -val diff_nat_number_of = thm"diff_nat_number_of";
    5.34 -val mult_nat_number_of = thm"mult_nat_number_of";
    5.35 -val div_nat_number_of = thm"div_nat_number_of";
    5.36 -val mod_nat_number_of = thm"mod_nat_number_of";
    5.37 -*}
    5.38 -
    5.39  
    5.40  subsection{*Comparisons*}
    5.41  
    5.42 @@ -737,23 +714,6 @@
    5.43      power_number_of_odd [of "number_of v", standard]
    5.44  
    5.45  
    5.46 -
    5.47 -ML
    5.48 -{*
    5.49 -val numeral_ss = @{simpset} addsimps @{thms numerals};
    5.50 -
    5.51 -val nat_bin_arith_setup =
    5.52 - Lin_Arith.map_data
    5.53 -   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    5.54 -     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    5.55 -      inj_thms = inj_thms,
    5.56 -      lessD = lessD, neqE = neqE,
    5.57 -      simpset = simpset addsimps @{thms neg_simps} @
    5.58 -        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
    5.59 -*}
    5.60 -
    5.61 -declaration {* K nat_bin_arith_setup *}
    5.62 -
    5.63  (* Enable arith to deal with div/mod k where k is a numeral: *)
    5.64  declare split_div[of _ _ "number_of k", standard, arith_split]
    5.65  declare split_mod[of _ _ "number_of k", standard, arith_split]
    5.66 @@ -912,8 +872,37 @@
    5.67  
    5.68  subsection {* Simprocs for the Naturals *}
    5.69  
    5.70 -use "Tools/nat_simprocs.ML"
    5.71 -declaration {* K nat_simprocs_setup *}
    5.72 +use "Tools/nat_numeral_simprocs.ML"
    5.73 +
    5.74 +declaration {*
    5.75 +let
    5.76 +
    5.77 +val less_eq_rules = @{thms ring_distribs} @
    5.78 +  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
    5.79 +   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
    5.80 +   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
    5.81 +   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
    5.82 +   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
    5.83 +   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
    5.84 +   @{thm mult_Suc}, @{thm mult_Suc_right},
    5.85 +   @{thm add_Suc}, @{thm add_Suc_right},
    5.86 +   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
    5.87 +   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
    5.88 +
    5.89 +val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
    5.90 +
    5.91 +in
    5.92 +
    5.93 +K (Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    5.94 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    5.95 +    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    5.96 +    simpset = simpset addsimps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
    5.97 +      addsimps less_eq_rules
    5.98 +      addsimprocs simprocs}))
    5.99 +
   5.100 +end
   5.101 +*}
   5.102 +
   5.103  
   5.104  subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
   5.105  
     6.1 --- a/src/HOL/Tools/int_arith.ML	Fri May 08 08:01:09 2009 +0200
     6.2 +++ b/src/HOL/Tools/int_arith.ML	Fri May 08 09:48:07 2009 +0200
     6.3 @@ -1,420 +1,15 @@
     6.4 -(* Authors: Larry Paulson and Tobias Nipkow
     6.5 -
     6.6 -Simprocs and decision procedure for numerals and linear arithmetic.
     6.7 -*)
     6.8 -
     6.9 -structure Int_Numeral_Simprocs =
    6.10 -struct
    6.11 -
    6.12 -(** Utilities **)
    6.13 -
    6.14 -fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    6.15 -
    6.16 -fun find_first_numeral past (t::terms) =
    6.17 -        ((snd (HOLogic.dest_number t), rev past @ terms)
    6.18 -         handle TERM _ => find_first_numeral (t::past) terms)
    6.19 -  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    6.20 -
    6.21 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    6.22 -
    6.23 -fun mk_minus t = 
    6.24 -  let val T = Term.fastype_of t
    6.25 -  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
    6.26 -
    6.27 -(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    6.28 -fun mk_sum T []        = mk_number T 0
    6.29 -  | mk_sum T [t,u]     = mk_plus (t, u)
    6.30 -  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    6.31 -
    6.32 -(*this version ALWAYS includes a trailing zero*)
    6.33 -fun long_mk_sum T []        = mk_number T 0
    6.34 -  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    6.35 -
    6.36 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
    6.37 -
    6.38 -(*decompose additions AND subtractions as a sum*)
    6.39 -fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
    6.40 -        dest_summing (pos, t, dest_summing (pos, u, ts))
    6.41 -  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
    6.42 -        dest_summing (pos, t, dest_summing (not pos, u, ts))
    6.43 -  | dest_summing (pos, t, ts) =
    6.44 -        if pos then t::ts else mk_minus t :: ts;
    6.45 -
    6.46 -fun dest_sum t = dest_summing (true, t, []);
    6.47 -
    6.48 -val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
    6.49 -val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
    6.50 -
    6.51 -val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    6.52 -
    6.53 -fun one_of T = Const(@{const_name HOL.one},T);
    6.54 -
    6.55 -(* build product with trailing 1 rather than Numeral 1 in order to avoid the
    6.56 -   unnecessary restriction to type class number_ring
    6.57 -   which is not required for cancellation of common factors in divisions.
    6.58 -*)
    6.59 -fun mk_prod T = 
    6.60 -  let val one = one_of T
    6.61 -  fun mk [] = one
    6.62 -    | mk [t] = t
    6.63 -    | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
    6.64 -  in mk end;
    6.65 -
    6.66 -(*This version ALWAYS includes a trailing one*)
    6.67 -fun long_mk_prod T []        = one_of T
    6.68 -  | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
    6.69 -
    6.70 -val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
    6.71 -
    6.72 -fun dest_prod t =
    6.73 -      let val (t,u) = dest_times t
    6.74 -      in dest_prod t @ dest_prod u end
    6.75 -      handle TERM _ => [t];
    6.76 -
    6.77 -(*DON'T do the obvious simplifications; that would create special cases*)
    6.78 -fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
    6.79 -
    6.80 -(*Express t as a product of (possibly) a numeral with other sorted terms*)
    6.81 -fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
    6.82 -  | dest_coeff sign t =
    6.83 -    let val ts = sort TermOrd.term_ord (dest_prod t)
    6.84 -        val (n, ts') = find_first_numeral [] ts
    6.85 -                          handle TERM _ => (1, ts)
    6.86 -    in (sign*n, mk_prod (Term.fastype_of t) ts') end;
    6.87 -
    6.88 -(*Find first coefficient-term THAT MATCHES u*)
    6.89 -fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    6.90 -  | find_first_coeff past u (t::terms) =
    6.91 -        let val (n,u') = dest_coeff 1 t
    6.92 -        in if u aconv u' then (n, rev past @ terms)
    6.93 -                         else find_first_coeff (t::past) u terms
    6.94 -        end
    6.95 -        handle TERM _ => find_first_coeff (t::past) u terms;
    6.96 -
    6.97 -(*Fractions as pairs of ints. Can't use Rat.rat because the representation
    6.98 -  needs to preserve negative values in the denominator.*)
    6.99 -fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
   6.100 -
   6.101 -(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   6.102 -  Fractions are reduced later by the cancel_numeral_factor simproc.*)
   6.103 -fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   6.104 -
   6.105 -val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
   6.106 -
   6.107 -(*Build term (p / q) * t*)
   6.108 -fun mk_fcoeff ((p, q), t) =
   6.109 -  let val T = Term.fastype_of t
   6.110 -  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   6.111 -
   6.112 -(*Express t as a product of a fraction with other sorted terms*)
   6.113 -fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
   6.114 -  | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
   6.115 -    let val (p, t') = dest_coeff sign t
   6.116 -        val (q, u') = dest_coeff 1 u
   6.117 -    in (mk_frac (p, q), mk_divide (t', u')) end
   6.118 -  | dest_fcoeff sign t =
   6.119 -    let val (p, t') = dest_coeff sign t
   6.120 -        val T = Term.fastype_of t
   6.121 -    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
   6.122 -
   6.123 -
   6.124 -(** New term ordering so that AC-rewriting brings numerals to the front **)
   6.125 -
   6.126 -(*Order integers by absolute value and then by sign. The standard integer
   6.127 -  ordering is not well-founded.*)
   6.128 -fun num_ord (i,j) =
   6.129 -  (case int_ord (abs i, abs j) of
   6.130 -    EQUAL => int_ord (Int.sign i, Int.sign j) 
   6.131 -  | ord => ord);
   6.132 -
   6.133 -(*This resembles TermOrd.term_ord, but it puts binary numerals before other
   6.134 -  non-atomic terms.*)
   6.135 -local open Term 
   6.136 -in 
   6.137 -fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
   6.138 -      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
   6.139 -  | numterm_ord
   6.140 -     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
   6.141 -     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
   6.142 -  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
   6.143 -  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
   6.144 -  | numterm_ord (t, u) =
   6.145 -      (case int_ord (size_of_term t, size_of_term u) of
   6.146 -        EQUAL =>
   6.147 -          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   6.148 -            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   6.149 -          end
   6.150 -      | ord => ord)
   6.151 -and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
   6.152 -end;
   6.153 -
   6.154 -fun numtermless tu = (numterm_ord tu = LESS);
   6.155 -
   6.156 -val num_ss = HOL_ss settermless numtermless;
   6.157 -
   6.158 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
   6.159 -val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
   6.160 -
   6.161 -(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
   6.162 -val add_0s =  @{thms add_0s};
   6.163 -val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
   6.164 -
   6.165 -(*Simplify inverse Numeral1, a/Numeral1*)
   6.166 -val inverse_1s = [@{thm inverse_numeral_1}];
   6.167 -val divide_1s = [@{thm divide_numeral_1}];
   6.168 -
   6.169 -(*To perform binary arithmetic.  The "left" rewriting handles patterns
   6.170 -  created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *)
   6.171 -val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
   6.172 -                 @{thm add_number_of_left}, @{thm mult_number_of_left}] @
   6.173 -                @{thms arith_simps} @ @{thms rel_simps};
   6.174 -
   6.175 -(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   6.176 -  during re-arrangement*)
   6.177 -val non_add_simps =
   6.178 -  subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
   6.179 -
   6.180 -(*To evaluate binary negations of coefficients*)
   6.181 -val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
   6.182 -                   @{thms minus_bin_simps} @ @{thms pred_bin_simps};
   6.183 -
   6.184 -(*To let us treat subtraction as addition*)
   6.185 -val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
   6.186 -
   6.187 -(*To let us treat division as multiplication*)
   6.188 -val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   6.189 -
   6.190 -(*push the unary minus down: - x * y = x * - y *)
   6.191 -val minus_mult_eq_1_to_2 =
   6.192 -    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
   6.193 -
   6.194 -(*to extract again any uncancelled minuses*)
   6.195 -val minus_from_mult_simps =
   6.196 -    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
   6.197 -
   6.198 -(*combine unary minus with numeric literals, however nested within a product*)
   6.199 -val mult_minus_simps =
   6.200 -    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
   6.201 -
   6.202 -val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   6.203 -  diff_simps @ minus_simps @ @{thms add_ac}
   6.204 -val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   6.205 -val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   6.206 +(* Author: Tobias Nipkow
   6.207  
   6.208 -structure CancelNumeralsCommon =
   6.209 -  struct
   6.210 -  val mk_sum            = mk_sum
   6.211 -  val dest_sum          = dest_sum
   6.212 -  val mk_coeff          = mk_coeff
   6.213 -  val dest_coeff        = dest_coeff 1
   6.214 -  val find_first_coeff  = find_first_coeff []
   6.215 -  val trans_tac         = K Arith_Data.trans_tac
   6.216 -
   6.217 -  fun norm_tac ss =
   6.218 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   6.219 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   6.220 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   6.221 -
   6.222 -  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   6.223 -  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   6.224 -  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   6.225 -  end;
   6.226 -
   6.227 -
   6.228 -structure EqCancelNumerals = CancelNumeralsFun
   6.229 - (open CancelNumeralsCommon
   6.230 -  val prove_conv = Arith_Data.prove_conv
   6.231 -  val mk_bal   = HOLogic.mk_eq
   6.232 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   6.233 -  val bal_add1 = @{thm eq_add_iff1} RS trans
   6.234 -  val bal_add2 = @{thm eq_add_iff2} RS trans
   6.235 -);
   6.236 -
   6.237 -structure LessCancelNumerals = CancelNumeralsFun
   6.238 - (open CancelNumeralsCommon
   6.239 -  val prove_conv = Arith_Data.prove_conv
   6.240 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   6.241 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   6.242 -  val bal_add1 = @{thm less_add_iff1} RS trans
   6.243 -  val bal_add2 = @{thm less_add_iff2} RS trans
   6.244 -);
   6.245 -
   6.246 -structure LeCancelNumerals = CancelNumeralsFun
   6.247 - (open CancelNumeralsCommon
   6.248 -  val prove_conv = Arith_Data.prove_conv
   6.249 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   6.250 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   6.251 -  val bal_add1 = @{thm le_add_iff1} RS trans
   6.252 -  val bal_add2 = @{thm le_add_iff2} RS trans
   6.253 -);
   6.254 -
   6.255 -val cancel_numerals =
   6.256 -  map Arith_Data.prep_simproc
   6.257 -   [("inteq_cancel_numerals",
   6.258 -     ["(l::'a::number_ring) + m = n",
   6.259 -      "(l::'a::number_ring) = m + n",
   6.260 -      "(l::'a::number_ring) - m = n",
   6.261 -      "(l::'a::number_ring) = m - n",
   6.262 -      "(l::'a::number_ring) * m = n",
   6.263 -      "(l::'a::number_ring) = m * n"],
   6.264 -     K EqCancelNumerals.proc),
   6.265 -    ("intless_cancel_numerals",
   6.266 -     ["(l::'a::{ordered_idom,number_ring}) + m < n",
   6.267 -      "(l::'a::{ordered_idom,number_ring}) < m + n",
   6.268 -      "(l::'a::{ordered_idom,number_ring}) - m < n",
   6.269 -      "(l::'a::{ordered_idom,number_ring}) < m - n",
   6.270 -      "(l::'a::{ordered_idom,number_ring}) * m < n",
   6.271 -      "(l::'a::{ordered_idom,number_ring}) < m * n"],
   6.272 -     K LessCancelNumerals.proc),
   6.273 -    ("intle_cancel_numerals",
   6.274 -     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
   6.275 -      "(l::'a::{ordered_idom,number_ring}) <= m + n",
   6.276 -      "(l::'a::{ordered_idom,number_ring}) - m <= n",
   6.277 -      "(l::'a::{ordered_idom,number_ring}) <= m - n",
   6.278 -      "(l::'a::{ordered_idom,number_ring}) * m <= n",
   6.279 -      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   6.280 -     K LeCancelNumerals.proc)];
   6.281 -
   6.282 -
   6.283 -structure CombineNumeralsData =
   6.284 -  struct
   6.285 -  type coeff            = int
   6.286 -  val iszero            = (fn x => x = 0)
   6.287 -  val add               = op +
   6.288 -  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   6.289 -  val dest_sum          = dest_sum
   6.290 -  val mk_coeff          = mk_coeff
   6.291 -  val dest_coeff        = dest_coeff 1
   6.292 -  val left_distrib      = @{thm combine_common_factor} RS trans
   6.293 -  val prove_conv        = Arith_Data.prove_conv_nohyps
   6.294 -  val trans_tac         = K Arith_Data.trans_tac
   6.295 -
   6.296 -  fun norm_tac ss =
   6.297 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   6.298 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   6.299 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   6.300 -
   6.301 -  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   6.302 -  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   6.303 -  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   6.304 -  end;
   6.305 -
   6.306 -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   6.307 -
   6.308 -(*Version for fields, where coefficients can be fractions*)
   6.309 -structure FieldCombineNumeralsData =
   6.310 -  struct
   6.311 -  type coeff            = int * int
   6.312 -  val iszero            = (fn (p, q) => p = 0)
   6.313 -  val add               = add_frac
   6.314 -  val mk_sum            = long_mk_sum
   6.315 -  val dest_sum          = dest_sum
   6.316 -  val mk_coeff          = mk_fcoeff
   6.317 -  val dest_coeff        = dest_fcoeff 1
   6.318 -  val left_distrib      = @{thm combine_common_factor} RS trans
   6.319 -  val prove_conv        = Arith_Data.prove_conv_nohyps
   6.320 -  val trans_tac         = K Arith_Data.trans_tac
   6.321 -
   6.322 -  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   6.323 -  fun norm_tac ss =
   6.324 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
   6.325 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   6.326 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   6.327 -
   6.328 -  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   6.329 -  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   6.330 -  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   6.331 -  end;
   6.332 -
   6.333 -structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   6.334 -
   6.335 -val combine_numerals =
   6.336 -  Arith_Data.prep_simproc
   6.337 -    ("int_combine_numerals", 
   6.338 -     ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   6.339 -     K CombineNumerals.proc);
   6.340 -
   6.341 -val field_combine_numerals =
   6.342 -  Arith_Data.prep_simproc
   6.343 -    ("field_combine_numerals", 
   6.344 -     ["(i::'a::{number_ring,field,division_by_zero}) + j",
   6.345 -      "(i::'a::{number_ring,field,division_by_zero}) - j"], 
   6.346 -     K FieldCombineNumerals.proc);
   6.347 -
   6.348 -(** Constant folding for multiplication in semirings **)
   6.349 -
   6.350 -(*We do not need folding for addition: combine_numerals does the same thing*)
   6.351 -
   6.352 -structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   6.353 -struct
   6.354 -  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   6.355 -  val eq_reflection = eq_reflection
   6.356 -  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
   6.357 -    | is_numeral _ = false;
   6.358 -end;
   6.359 -
   6.360 -structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   6.361 -
   6.362 -val assoc_fold_simproc =
   6.363 -  Arith_Data.prep_simproc
   6.364 -   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   6.365 -    K Semiring_Times_Assoc.proc);
   6.366 -
   6.367 -end;
   6.368 -
   6.369 -Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   6.370 -Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   6.371 -Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
   6.372 -Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc];
   6.373 -
   6.374 -(*examples:
   6.375 -print_depth 22;
   6.376 -set timing;
   6.377 -set trace_simp;
   6.378 -fun test s = (Goal s, by (Simp_tac 1));
   6.379 -
   6.380 -test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   6.381 -
   6.382 -test "2*u = (u::int)";
   6.383 -test "(i + j + 12 + (k::int)) - 15 = y";
   6.384 -test "(i + j + 12 + (k::int)) - 5 = y";
   6.385 -
   6.386 -test "y - b < (b::int)";
   6.387 -test "y - (3*b + c) < (b::int) - 2*c";
   6.388 -
   6.389 -test "(2*x - (u*v) + y) - v*3*u = (w::int)";
   6.390 -test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
   6.391 -test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
   6.392 -test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
   6.393 -
   6.394 -test "(i + j + 12 + (k::int)) = u + 15 + y";
   6.395 -test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
   6.396 -
   6.397 -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)";
   6.398 -
   6.399 -test "a + -(b+c) + b = (d::int)";
   6.400 -test "a + -(b+c) - b = (d::int)";
   6.401 -
   6.402 -(*negative numerals*)
   6.403 -test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
   6.404 -test "(i + j + -3 + (k::int)) < u + 5 + y";
   6.405 -test "(i + j + 3 + (k::int)) < u + -6 + y";
   6.406 -test "(i + j + -12 + (k::int)) - 15 = y";
   6.407 -test "(i + j + 12 + (k::int)) - -15 = y";
   6.408 -test "(i + j + -12 + (k::int)) - -15 = y";
   6.409 -*)
   6.410 -
   6.411 -(*** decision procedure for linear arithmetic ***)
   6.412 -
   6.413 -(*---------------------------------------------------------------------------*)
   6.414 -(* Linear arithmetic                                                         *)
   6.415 -(*---------------------------------------------------------------------------*)
   6.416 -
   6.417 -(*
   6.418  Instantiation of the generic linear arithmetic package for int.
   6.419  *)
   6.420  
   6.421 -structure Int_Arith =
   6.422 +signature INT_ARITH =
   6.423 +sig
   6.424 +  val fast_int_arith_simproc: simproc
   6.425 +  val setup: Context.generic -> Context.generic
   6.426 +end
   6.427 +
   6.428 +structure Int_Arith : INT_ARITH =
   6.429  struct
   6.430  
   6.431  (* Update parameters of arithmetic prover *)
   6.432 @@ -491,9 +86,9 @@
   6.433  
   6.434  val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
   6.435  
   6.436 -val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   6.437 -  :: Int_Numeral_Simprocs.combine_numerals
   6.438 -  :: Int_Numeral_Simprocs.cancel_numerals;
   6.439 +val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
   6.440 +  :: Numeral_Simprocs.combine_numerals
   6.441 +  :: Numeral_Simprocs.cancel_numerals;
   6.442  
   6.443  val setup =
   6.444    Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   6.445 @@ -503,7 +98,7 @@
   6.446      lessD = lessD @ [@{thm zless_imp_add1_zle}],
   6.447      neqE = neqE,
   6.448      simpset = simpset addsimps add_rules
   6.449 -                      addsimprocs int_numeral_base_simprocs
   6.450 +                      addsimprocs numeral_base_simprocs
   6.451                        addcongs [if_weak_cong]}) #>
   6.452    arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   6.453    arith_discrete @{type_name Int.int}
     7.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Fri May 08 08:01:09 2009 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,391 +0,0 @@
     7.4 -(*  Title:      HOL/int_factor_simprocs.ML
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 -    Copyright   2000  University of Cambridge
     7.7 -
     7.8 -Factor cancellation simprocs for the integers (and for fields).
     7.9 -
    7.10 -This file can't be combined with int_arith1 because it requires IntDiv.thy.
    7.11 -*)
    7.12 -
    7.13 -
    7.14 -(*To quote from Provers/Arith/cancel_numeral_factor.ML:
    7.15 -
    7.16 -Cancels common coefficients in balanced expressions:
    7.17 -
    7.18 -     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    7.19 -
    7.20 -where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    7.21 -and d = gcd(m,m') and n=m/d and n'=m'/d.
    7.22 -*)
    7.23 -
    7.24 -val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
    7.25 -
    7.26 -local
    7.27 -  open Int_Numeral_Simprocs
    7.28 -in
    7.29 -
    7.30 -structure CancelNumeralFactorCommon =
    7.31 -  struct
    7.32 -  val mk_coeff          = mk_coeff
    7.33 -  val dest_coeff        = dest_coeff 1
    7.34 -  val trans_tac         = K Arith_Data.trans_tac
    7.35 -
    7.36 -  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    7.37 -  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    7.38 -  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
    7.39 -  fun norm_tac ss =
    7.40 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    7.41 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    7.42 -    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    7.43 -
    7.44 -  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
    7.45 -  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    7.46 -  val simplify_meta_eq = Arith_Data.simplify_meta_eq
    7.47 -    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
    7.48 -      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
    7.49 -  end
    7.50 -
    7.51 -(*Version for semiring_div*)
    7.52 -structure DivCancelNumeralFactor = CancelNumeralFactorFun
    7.53 - (open CancelNumeralFactorCommon
    7.54 -  val prove_conv = Arith_Data.prove_conv
    7.55 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
    7.56 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
    7.57 -  val cancel = @{thm div_mult_mult1} RS trans
    7.58 -  val neg_exchanges = false
    7.59 -)
    7.60 -
    7.61 -(*Version for fields*)
    7.62 -structure DivideCancelNumeralFactor = CancelNumeralFactorFun
    7.63 - (open CancelNumeralFactorCommon
    7.64 -  val prove_conv = Arith_Data.prove_conv
    7.65 -  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
    7.66 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
    7.67 -  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
    7.68 -  val neg_exchanges = false
    7.69 -)
    7.70 -
    7.71 -structure EqCancelNumeralFactor = CancelNumeralFactorFun
    7.72 - (open CancelNumeralFactorCommon
    7.73 -  val prove_conv = Arith_Data.prove_conv
    7.74 -  val mk_bal   = HOLogic.mk_eq
    7.75 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    7.76 -  val cancel = @{thm mult_cancel_left} RS trans
    7.77 -  val neg_exchanges = false
    7.78 -)
    7.79 -
    7.80 -structure LessCancelNumeralFactor = CancelNumeralFactorFun
    7.81 - (open CancelNumeralFactorCommon
    7.82 -  val prove_conv = Arith_Data.prove_conv
    7.83 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
    7.84 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
    7.85 -  val cancel = @{thm mult_less_cancel_left} RS trans
    7.86 -  val neg_exchanges = true
    7.87 -)
    7.88 -
    7.89 -structure LeCancelNumeralFactor = CancelNumeralFactorFun
    7.90 - (open CancelNumeralFactorCommon
    7.91 -  val prove_conv = Arith_Data.prove_conv
    7.92 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
    7.93 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
    7.94 -  val cancel = @{thm mult_le_cancel_left} RS trans
    7.95 -  val neg_exchanges = true
    7.96 -)
    7.97 -
    7.98 -val cancel_numeral_factors =
    7.99 -  map Arith_Data.prep_simproc
   7.100 -   [("ring_eq_cancel_numeral_factor",
   7.101 -     ["(l::'a::{idom,number_ring}) * m = n",
   7.102 -      "(l::'a::{idom,number_ring}) = m * n"],
   7.103 -     K EqCancelNumeralFactor.proc),
   7.104 -    ("ring_less_cancel_numeral_factor",
   7.105 -     ["(l::'a::{ordered_idom,number_ring}) * m < n",
   7.106 -      "(l::'a::{ordered_idom,number_ring}) < m * n"],
   7.107 -     K LessCancelNumeralFactor.proc),
   7.108 -    ("ring_le_cancel_numeral_factor",
   7.109 -     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
   7.110 -      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   7.111 -     K LeCancelNumeralFactor.proc),
   7.112 -    ("int_div_cancel_numeral_factors",
   7.113 -     ["((l::'a::{semiring_div,number_ring}) * m) div n",
   7.114 -      "(l::'a::{semiring_div,number_ring}) div (m * n)"],
   7.115 -     K DivCancelNumeralFactor.proc),
   7.116 -    ("divide_cancel_numeral_factor",
   7.117 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   7.118 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   7.119 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   7.120 -     K DivideCancelNumeralFactor.proc)];
   7.121 -
   7.122 -(* referenced by rat_arith.ML *)
   7.123 -val field_cancel_numeral_factors =
   7.124 -  map Arith_Data.prep_simproc
   7.125 -   [("field_eq_cancel_numeral_factor",
   7.126 -     ["(l::'a::{field,number_ring}) * m = n",
   7.127 -      "(l::'a::{field,number_ring}) = m * n"],
   7.128 -     K EqCancelNumeralFactor.proc),
   7.129 -    ("field_cancel_numeral_factor",
   7.130 -     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   7.131 -      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   7.132 -      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   7.133 -     K DivideCancelNumeralFactor.proc)]
   7.134 -
   7.135 -end;
   7.136 -
   7.137 -Addsimprocs cancel_numeral_factors;
   7.138 -
   7.139 -(*examples:
   7.140 -print_depth 22;
   7.141 -set timing;
   7.142 -set trace_simp;
   7.143 -fun test s = (Goal s; by (Simp_tac 1));
   7.144 -
   7.145 -test "9*x = 12 * (y::int)";
   7.146 -test "(9*x) div (12 * (y::int)) = z";
   7.147 -test "9*x < 12 * (y::int)";
   7.148 -test "9*x <= 12 * (y::int)";
   7.149 -
   7.150 -test "-99*x = 132 * (y::int)";
   7.151 -test "(-99*x) div (132 * (y::int)) = z";
   7.152 -test "-99*x < 132 * (y::int)";
   7.153 -test "-99*x <= 132 * (y::int)";
   7.154 -
   7.155 -test "999*x = -396 * (y::int)";
   7.156 -test "(999*x) div (-396 * (y::int)) = z";
   7.157 -test "999*x < -396 * (y::int)";
   7.158 -test "999*x <= -396 * (y::int)";
   7.159 -
   7.160 -test "-99*x = -81 * (y::int)";
   7.161 -test "(-99*x) div (-81 * (y::int)) = z";
   7.162 -test "-99*x <= -81 * (y::int)";
   7.163 -test "-99*x < -81 * (y::int)";
   7.164 -
   7.165 -test "-2 * x = -1 * (y::int)";
   7.166 -test "-2 * x = -(y::int)";
   7.167 -test "(-2 * x) div (-1 * (y::int)) = z";
   7.168 -test "-2 * x < -(y::int)";
   7.169 -test "-2 * x <= -1 * (y::int)";
   7.170 -test "-x < -23 * (y::int)";
   7.171 -test "-x <= -23 * (y::int)";
   7.172 -*)
   7.173 -
   7.174 -(*And the same examples for fields such as rat or real:
   7.175 -test "0 <= (y::rat) * -2";
   7.176 -test "9*x = 12 * (y::rat)";
   7.177 -test "(9*x) / (12 * (y::rat)) = z";
   7.178 -test "9*x < 12 * (y::rat)";
   7.179 -test "9*x <= 12 * (y::rat)";
   7.180 -
   7.181 -test "-99*x = 132 * (y::rat)";
   7.182 -test "(-99*x) / (132 * (y::rat)) = z";
   7.183 -test "-99*x < 132 * (y::rat)";
   7.184 -test "-99*x <= 132 * (y::rat)";
   7.185 -
   7.186 -test "999*x = -396 * (y::rat)";
   7.187 -test "(999*x) / (-396 * (y::rat)) = z";
   7.188 -test "999*x < -396 * (y::rat)";
   7.189 -test "999*x <= -396 * (y::rat)";
   7.190 -
   7.191 -test  "(- ((2::rat) * x) <= 2 * y)";
   7.192 -test "-99*x = -81 * (y::rat)";
   7.193 -test "(-99*x) / (-81 * (y::rat)) = z";
   7.194 -test "-99*x <= -81 * (y::rat)";
   7.195 -test "-99*x < -81 * (y::rat)";
   7.196 -
   7.197 -test "-2 * x = -1 * (y::rat)";
   7.198 -test "-2 * x = -(y::rat)";
   7.199 -test "(-2 * x) / (-1 * (y::rat)) = z";
   7.200 -test "-2 * x < -(y::rat)";
   7.201 -test "-2 * x <= -1 * (y::rat)";
   7.202 -test "-x < -23 * (y::rat)";
   7.203 -test "-x <= -23 * (y::rat)";
   7.204 -*)
   7.205 -
   7.206 -
   7.207 -(** Declarations for ExtractCommonTerm **)
   7.208 -
   7.209 -local
   7.210 -  open Int_Numeral_Simprocs
   7.211 -in
   7.212 -
   7.213 -(*Find first term that matches u*)
   7.214 -fun find_first_t past u []         = raise TERM ("find_first_t", [])
   7.215 -  | find_first_t past u (t::terms) =
   7.216 -        if u aconv t then (rev past @ terms)
   7.217 -        else find_first_t (t::past) u terms
   7.218 -        handle TERM _ => find_first_t (t::past) u terms;
   7.219 -
   7.220 -(** Final simplification for the CancelFactor simprocs **)
   7.221 -val simplify_one = Arith_Data.simplify_meta_eq  
   7.222 -  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
   7.223 -
   7.224 -fun cancel_simplify_meta_eq ss cancel_th th =
   7.225 -    simplify_one ss (([th, cancel_th]) MRS trans);
   7.226 -
   7.227 -local
   7.228 -  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
   7.229 -  fun Eq_True_elim Eq = 
   7.230 -    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   7.231 -in
   7.232 -fun sign_conv pos_th neg_th ss t =
   7.233 -  let val T = fastype_of t;
   7.234 -      val zero = Const(@{const_name HOL.zero}, T);
   7.235 -      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
   7.236 -      val pos = less $ zero $ t and neg = less $ t $ zero
   7.237 -      fun prove p =
   7.238 -        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
   7.239 -        handle THM _ => NONE
   7.240 -    in case prove pos of
   7.241 -         SOME th => SOME(th RS pos_th)
   7.242 -       | NONE => (case prove neg of
   7.243 -                    SOME th => SOME(th RS neg_th)
   7.244 -                  | NONE => NONE)
   7.245 -    end;
   7.246 -end
   7.247 -
   7.248 -structure CancelFactorCommon =
   7.249 -  struct
   7.250 -  val mk_sum            = long_mk_prod
   7.251 -  val dest_sum          = dest_prod
   7.252 -  val mk_coeff          = mk_coeff
   7.253 -  val dest_coeff        = dest_coeff
   7.254 -  val find_first        = find_first_t []
   7.255 -  val trans_tac         = K Arith_Data.trans_tac
   7.256 -  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   7.257 -  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   7.258 -  val simplify_meta_eq  = cancel_simplify_meta_eq 
   7.259 -  end;
   7.260 -
   7.261 -(*mult_cancel_left requires a ring with no zero divisors.*)
   7.262 -structure EqCancelFactor = ExtractCommonTermFun
   7.263 - (open CancelFactorCommon
   7.264 -  val prove_conv = Arith_Data.prove_conv
   7.265 -  val mk_bal   = HOLogic.mk_eq
   7.266 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   7.267 -  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
   7.268 -);
   7.269 -
   7.270 -(*for ordered rings*)
   7.271 -structure LeCancelFactor = ExtractCommonTermFun
   7.272 - (open CancelFactorCommon
   7.273 -  val prove_conv = Arith_Data.prove_conv
   7.274 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   7.275 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   7.276 -  val simp_conv = sign_conv
   7.277 -    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   7.278 -);
   7.279 -
   7.280 -(*for ordered rings*)
   7.281 -structure LessCancelFactor = ExtractCommonTermFun
   7.282 - (open CancelFactorCommon
   7.283 -  val prove_conv = Arith_Data.prove_conv
   7.284 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   7.285 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   7.286 -  val simp_conv = sign_conv
   7.287 -    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   7.288 -);
   7.289 -
   7.290 -(*for semirings with division*)
   7.291 -structure DivCancelFactor = ExtractCommonTermFun
   7.292 - (open CancelFactorCommon
   7.293 -  val prove_conv = Arith_Data.prove_conv
   7.294 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   7.295 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   7.296 -  val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
   7.297 -);
   7.298 -
   7.299 -structure ModCancelFactor = ExtractCommonTermFun
   7.300 - (open CancelFactorCommon
   7.301 -  val prove_conv = Arith_Data.prove_conv
   7.302 -  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   7.303 -  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
   7.304 -  val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
   7.305 -);
   7.306 -
   7.307 -(*for idoms*)
   7.308 -structure DvdCancelFactor = ExtractCommonTermFun
   7.309 - (open CancelFactorCommon
   7.310 -  val prove_conv = Arith_Data.prove_conv
   7.311 -  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   7.312 -  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   7.313 -  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
   7.314 -);
   7.315 -
   7.316 -(*Version for all fields, including unordered ones (type complex).*)
   7.317 -structure DivideCancelFactor = ExtractCommonTermFun
   7.318 - (open CancelFactorCommon
   7.319 -  val prove_conv = Arith_Data.prove_conv
   7.320 -  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   7.321 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   7.322 -  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
   7.323 -);
   7.324 -
   7.325 -val cancel_factors =
   7.326 -  map Arith_Data.prep_simproc
   7.327 -   [("ring_eq_cancel_factor",
   7.328 -     ["(l::'a::idom) * m = n",
   7.329 -      "(l::'a::idom) = m * n"],
   7.330 -     K EqCancelFactor.proc),
   7.331 -    ("ordered_ring_le_cancel_factor",
   7.332 -     ["(l::'a::ordered_ring) * m <= n",
   7.333 -      "(l::'a::ordered_ring) <= m * n"],
   7.334 -     K LeCancelFactor.proc),
   7.335 -    ("ordered_ring_less_cancel_factor",
   7.336 -     ["(l::'a::ordered_ring) * m < n",
   7.337 -      "(l::'a::ordered_ring) < m * n"],
   7.338 -     K LessCancelFactor.proc),
   7.339 -    ("int_div_cancel_factor",
   7.340 -     ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
   7.341 -     K DivCancelFactor.proc),
   7.342 -    ("int_mod_cancel_factor",
   7.343 -     ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
   7.344 -     K ModCancelFactor.proc),
   7.345 -    ("dvd_cancel_factor",
   7.346 -     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   7.347 -     K DvdCancelFactor.proc),
   7.348 -    ("divide_cancel_factor",
   7.349 -     ["((l::'a::{division_by_zero,field}) * m) / n",
   7.350 -      "(l::'a::{division_by_zero,field}) / (m * n)"],
   7.351 -     K DivideCancelFactor.proc)];
   7.352 -
   7.353 -end;
   7.354 -
   7.355 -Addsimprocs cancel_factors;
   7.356 -
   7.357 -
   7.358 -(*examples:
   7.359 -print_depth 22;
   7.360 -set timing;
   7.361 -set trace_simp;
   7.362 -fun test s = (Goal s; by (Asm_simp_tac 1));
   7.363 -
   7.364 -test "x*k = k*(y::int)";
   7.365 -test "k = k*(y::int)";
   7.366 -test "a*(b*c) = (b::int)";
   7.367 -test "a*(b*c) = d*(b::int)*(x*a)";
   7.368 -
   7.369 -test "(x*k) div (k*(y::int)) = (uu::int)";
   7.370 -test "(k) div (k*(y::int)) = (uu::int)";
   7.371 -test "(a*(b*c)) div ((b::int)) = (uu::int)";
   7.372 -test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   7.373 -*)
   7.374 -
   7.375 -(*And the same examples for fields such as rat or real:
   7.376 -print_depth 22;
   7.377 -set timing;
   7.378 -set trace_simp;
   7.379 -fun test s = (Goal s; by (Asm_simp_tac 1));
   7.380 -
   7.381 -test "x*k = k*(y::rat)";
   7.382 -test "k = k*(y::rat)";
   7.383 -test "a*(b*c) = (b::rat)";
   7.384 -test "a*(b*c) = d*(b::rat)*(x*a)";
   7.385 -
   7.386 -
   7.387 -test "(x*k) / (k*(y::rat)) = (uu::rat)";
   7.388 -test "(k) / (k*(y::rat)) = (uu::rat)";
   7.389 -test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   7.390 -test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   7.391 -
   7.392 -(*FIXME: what do we do about this?*)
   7.393 -test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   7.394 -*)
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri May 08 09:48:07 2009 +0200
     8.3 @@ -0,0 +1,538 @@
     8.4 +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
     8.5 +
     8.6 +Simprocs for nat numerals.
     8.7 +*)
     8.8 +
     8.9 +signature NAT_NUMERAL_SIMPROCS =
    8.10 +sig
    8.11 +  val combine_numerals: simproc
    8.12 +  val cancel_numerals: simproc list
    8.13 +  val cancel_factors: simproc list
    8.14 +  val cancel_numeral_factors: simproc list
    8.15 +end;
    8.16 +
    8.17 +structure Nat_Numeral_Simprocs =
    8.18 +struct
    8.19 +
    8.20 +(*Maps n to #n for n = 0, 1, 2*)
    8.21 +val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    8.22 +val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    8.23 +
    8.24 +fun rename_numerals th =
    8.25 +    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    8.26 +
    8.27 +(*Utilities*)
    8.28 +
    8.29 +fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
    8.30 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    8.31 +
    8.32 +fun find_first_numeral past (t::terms) =
    8.33 +        ((dest_number t, t, rev past @ terms)
    8.34 +         handle TERM _ => find_first_numeral (t::past) terms)
    8.35 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    8.36 +
    8.37 +val zero = mk_number 0;
    8.38 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    8.39 +
    8.40 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    8.41 +fun mk_sum []        = zero
    8.42 +  | mk_sum [t,u]     = mk_plus (t, u)
    8.43 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    8.44 +
    8.45 +(*this version ALWAYS includes a trailing zero*)
    8.46 +fun long_mk_sum []        = HOLogic.zero
    8.47 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    8.48 +
    8.49 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    8.50 +
    8.51 +
    8.52 +(** Other simproc items **)
    8.53 +
    8.54 +val bin_simps =
    8.55 +     [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    8.56 +      @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    8.57 +      @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    8.58 +      @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    8.59 +      @{thm less_nat_number_of}, 
    8.60 +      @{thm Let_number_of}, @{thm nat_number_of}] @
    8.61 +     @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
    8.62 +
    8.63 +
    8.64 +(*** CancelNumerals simprocs ***)
    8.65 +
    8.66 +val one = mk_number 1;
    8.67 +val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    8.68 +
    8.69 +fun mk_prod [] = one
    8.70 +  | mk_prod [t] = t
    8.71 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
    8.72 +                        else mk_times (t, mk_prod ts);
    8.73 +
    8.74 +val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
    8.75 +
    8.76 +fun dest_prod t =
    8.77 +      let val (t,u) = dest_times t
    8.78 +      in  dest_prod t @ dest_prod u  end
    8.79 +      handle TERM _ => [t];
    8.80 +
    8.81 +(*DON'T do the obvious simplifications; that would create special cases*)
    8.82 +fun mk_coeff (k,t) = mk_times (mk_number k, t);
    8.83 +
    8.84 +(*Express t as a product of (possibly) a numeral with other factors, sorted*)
    8.85 +fun dest_coeff t =
    8.86 +    let val ts = sort TermOrd.term_ord (dest_prod t)
    8.87 +        val (n, _, ts') = find_first_numeral [] ts
    8.88 +                          handle TERM _ => (1, one, ts)
    8.89 +    in (n, mk_prod ts') end;
    8.90 +
    8.91 +(*Find first coefficient-term THAT MATCHES u*)
    8.92 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    8.93 +  | find_first_coeff past u (t::terms) =
    8.94 +        let val (n,u') = dest_coeff t
    8.95 +        in  if u aconv u' then (n, rev past @ terms)
    8.96 +                          else find_first_coeff (t::past) u terms
    8.97 +        end
    8.98 +        handle TERM _ => find_first_coeff (t::past) u terms;
    8.99 +
   8.100 +
   8.101 +(*Split up a sum into the list of its constituent terms, on the way removing any
   8.102 +  Sucs and counting them.*)
   8.103 +fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
   8.104 +  | dest_Suc_sum (t, (k,ts)) = 
   8.105 +      let val (t1,t2) = dest_plus t
   8.106 +      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
   8.107 +      handle TERM _ => (k, t::ts);
   8.108 +
   8.109 +(*Code for testing whether numerals are already used in the goal*)
   8.110 +fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
   8.111 +  | is_numeral _ = false;
   8.112 +
   8.113 +fun prod_has_numeral t = exists is_numeral (dest_prod t);
   8.114 +
   8.115 +(*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
   8.116 +  an exception is raised unless the original expression contains at least one
   8.117 +  numeral in a coefficient position.  This prevents nat_combine_numerals from 
   8.118 +  introducing numerals to goals.*)
   8.119 +fun dest_Sucs_sum relaxed t = 
   8.120 +  let val (k,ts) = dest_Suc_sum (t,(0,[]))
   8.121 +  in
   8.122 +     if relaxed orelse exists prod_has_numeral ts then 
   8.123 +       if k=0 then ts
   8.124 +       else mk_number k :: ts
   8.125 +     else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   8.126 +  end;
   8.127 +
   8.128 +
   8.129 +(*Simplify 1*n and n*1 to n*)
   8.130 +val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
   8.131 +val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
   8.132 +
   8.133 +(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
   8.134 +
   8.135 +(*And these help the simproc return False when appropriate, which helps
   8.136 +  the arith prover.*)
   8.137 +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
   8.138 +  @{thm Suc_not_Zero}, @{thm le_0_eq}];
   8.139 +
   8.140 +val simplify_meta_eq =
   8.141 +    Arith_Data.simplify_meta_eq
   8.142 +        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
   8.143 +          @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
   8.144 +
   8.145 +
   8.146 +(*** Applying CancelNumeralsFun ***)
   8.147 +
   8.148 +structure CancelNumeralsCommon =
   8.149 +  struct
   8.150 +  val mk_sum            = (fn T:typ => mk_sum)
   8.151 +  val dest_sum          = dest_Sucs_sum true
   8.152 +  val mk_coeff          = mk_coeff
   8.153 +  val dest_coeff        = dest_coeff
   8.154 +  val find_first_coeff  = find_first_coeff []
   8.155 +  val trans_tac         = K Arith_Data.trans_tac
   8.156 +
   8.157 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   8.158 +    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   8.159 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   8.160 +  fun norm_tac ss = 
   8.161 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   8.162 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   8.163 +
   8.164 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   8.165 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   8.166 +  val simplify_meta_eq  = simplify_meta_eq
   8.167 +  end;
   8.168 +
   8.169 +
   8.170 +structure EqCancelNumerals = CancelNumeralsFun
   8.171 + (open CancelNumeralsCommon
   8.172 +  val prove_conv = Arith_Data.prove_conv
   8.173 +  val mk_bal   = HOLogic.mk_eq
   8.174 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   8.175 +  val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   8.176 +  val bal_add2 = @{thm nat_eq_add_iff2} RS trans
   8.177 +);
   8.178 +
   8.179 +structure LessCancelNumerals = CancelNumeralsFun
   8.180 + (open CancelNumeralsCommon
   8.181 +  val prove_conv = Arith_Data.prove_conv
   8.182 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   8.183 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   8.184 +  val bal_add1 = @{thm nat_less_add_iff1} RS trans
   8.185 +  val bal_add2 = @{thm nat_less_add_iff2} RS trans
   8.186 +);
   8.187 +
   8.188 +structure LeCancelNumerals = CancelNumeralsFun
   8.189 + (open CancelNumeralsCommon
   8.190 +  val prove_conv = Arith_Data.prove_conv
   8.191 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   8.192 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   8.193 +  val bal_add1 = @{thm nat_le_add_iff1} RS trans
   8.194 +  val bal_add2 = @{thm nat_le_add_iff2} RS trans
   8.195 +);
   8.196 +
   8.197 +structure DiffCancelNumerals = CancelNumeralsFun
   8.198 + (open CancelNumeralsCommon
   8.199 +  val prove_conv = Arith_Data.prove_conv
   8.200 +  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   8.201 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   8.202 +  val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   8.203 +  val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   8.204 +);
   8.205 +
   8.206 +
   8.207 +val cancel_numerals =
   8.208 +  map Arith_Data.prep_simproc
   8.209 +   [("nateq_cancel_numerals",
   8.210 +     ["(l::nat) + m = n", "(l::nat) = m + n",
   8.211 +      "(l::nat) * m = n", "(l::nat) = m * n",
   8.212 +      "Suc m = n", "m = Suc n"],
   8.213 +     K EqCancelNumerals.proc),
   8.214 +    ("natless_cancel_numerals",
   8.215 +     ["(l::nat) + m < n", "(l::nat) < m + n",
   8.216 +      "(l::nat) * m < n", "(l::nat) < m * n",
   8.217 +      "Suc m < n", "m < Suc n"],
   8.218 +     K LessCancelNumerals.proc),
   8.219 +    ("natle_cancel_numerals",
   8.220 +     ["(l::nat) + m <= n", "(l::nat) <= m + n",
   8.221 +      "(l::nat) * m <= n", "(l::nat) <= m * n",
   8.222 +      "Suc m <= n", "m <= Suc n"],
   8.223 +     K LeCancelNumerals.proc),
   8.224 +    ("natdiff_cancel_numerals",
   8.225 +     ["((l::nat) + m) - n", "(l::nat) - (m + n)",
   8.226 +      "(l::nat) * m - n", "(l::nat) - m * n",
   8.227 +      "Suc m - n", "m - Suc n"],
   8.228 +     K DiffCancelNumerals.proc)];
   8.229 +
   8.230 +
   8.231 +(*** Applying CombineNumeralsFun ***)
   8.232 +
   8.233 +structure CombineNumeralsData =
   8.234 +  struct
   8.235 +  type coeff            = int
   8.236 +  val iszero            = (fn x => x = 0)
   8.237 +  val add               = op +
   8.238 +  val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   8.239 +  val dest_sum          = dest_Sucs_sum false
   8.240 +  val mk_coeff          = mk_coeff
   8.241 +  val dest_coeff        = dest_coeff
   8.242 +  val left_distrib      = @{thm left_add_mult_distrib} RS trans
   8.243 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   8.244 +  val trans_tac         = K Arith_Data.trans_tac
   8.245 +
   8.246 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   8.247 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   8.248 +  fun norm_tac ss =
   8.249 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   8.250 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   8.251 +
   8.252 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   8.253 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   8.254 +  val simplify_meta_eq  = simplify_meta_eq
   8.255 +  end;
   8.256 +
   8.257 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   8.258 +
   8.259 +val combine_numerals =
   8.260 +  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   8.261 +
   8.262 +
   8.263 +(*** Applying CancelNumeralFactorFun ***)
   8.264 +
   8.265 +structure CancelNumeralFactorCommon =
   8.266 +  struct
   8.267 +  val mk_coeff          = mk_coeff
   8.268 +  val dest_coeff        = dest_coeff
   8.269 +  val trans_tac         = K Arith_Data.trans_tac
   8.270 +
   8.271 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps
   8.272 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   8.273 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   8.274 +  fun norm_tac ss =
   8.275 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   8.276 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   8.277 +
   8.278 +  val numeral_simp_ss = HOL_ss addsimps bin_simps
   8.279 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   8.280 +  val simplify_meta_eq  = simplify_meta_eq
   8.281 +  end
   8.282 +
   8.283 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
   8.284 + (open CancelNumeralFactorCommon
   8.285 +  val prove_conv = Arith_Data.prove_conv
   8.286 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   8.287 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   8.288 +  val cancel = @{thm nat_mult_div_cancel1} RS trans
   8.289 +  val neg_exchanges = false
   8.290 +)
   8.291 +
   8.292 +structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   8.293 + (open CancelNumeralFactorCommon
   8.294 +  val prove_conv = Arith_Data.prove_conv
   8.295 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   8.296 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   8.297 +  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
   8.298 +  val neg_exchanges = false
   8.299 +)
   8.300 +
   8.301 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
   8.302 + (open CancelNumeralFactorCommon
   8.303 +  val prove_conv = Arith_Data.prove_conv
   8.304 +  val mk_bal   = HOLogic.mk_eq
   8.305 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   8.306 +  val cancel = @{thm nat_mult_eq_cancel1} RS trans
   8.307 +  val neg_exchanges = false
   8.308 +)
   8.309 +
   8.310 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
   8.311 + (open CancelNumeralFactorCommon
   8.312 +  val prove_conv = Arith_Data.prove_conv
   8.313 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   8.314 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   8.315 +  val cancel = @{thm nat_mult_less_cancel1} RS trans
   8.316 +  val neg_exchanges = true
   8.317 +)
   8.318 +
   8.319 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
   8.320 + (open CancelNumeralFactorCommon
   8.321 +  val prove_conv = Arith_Data.prove_conv
   8.322 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   8.323 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   8.324 +  val cancel = @{thm nat_mult_le_cancel1} RS trans
   8.325 +  val neg_exchanges = true
   8.326 +)
   8.327 +
   8.328 +val cancel_numeral_factors =
   8.329 +  map Arith_Data.prep_simproc
   8.330 +   [("nateq_cancel_numeral_factors",
   8.331 +     ["(l::nat) * m = n", "(l::nat) = m * n"],
   8.332 +     K EqCancelNumeralFactor.proc),
   8.333 +    ("natless_cancel_numeral_factors",
   8.334 +     ["(l::nat) * m < n", "(l::nat) < m * n"],
   8.335 +     K LessCancelNumeralFactor.proc),
   8.336 +    ("natle_cancel_numeral_factors",
   8.337 +     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   8.338 +     K LeCancelNumeralFactor.proc),
   8.339 +    ("natdiv_cancel_numeral_factors",
   8.340 +     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   8.341 +     K DivCancelNumeralFactor.proc),
   8.342 +    ("natdvd_cancel_numeral_factors",
   8.343 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   8.344 +     K DvdCancelNumeralFactor.proc)];
   8.345 +
   8.346 +
   8.347 +
   8.348 +(*** Applying ExtractCommonTermFun ***)
   8.349 +
   8.350 +(*this version ALWAYS includes a trailing one*)
   8.351 +fun long_mk_prod []        = one
   8.352 +  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   8.353 +
   8.354 +(*Find first term that matches u*)
   8.355 +fun find_first_t past u []         = raise TERM("find_first_t", [])
   8.356 +  | find_first_t past u (t::terms) =
   8.357 +        if u aconv t then (rev past @ terms)
   8.358 +        else find_first_t (t::past) u terms
   8.359 +        handle TERM _ => find_first_t (t::past) u terms;
   8.360 +
   8.361 +(** Final simplification for the CancelFactor simprocs **)
   8.362 +val simplify_one = Arith_Data.simplify_meta_eq  
   8.363 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
   8.364 +
   8.365 +fun cancel_simplify_meta_eq ss cancel_th th =
   8.366 +    simplify_one ss (([th, cancel_th]) MRS trans);
   8.367 +
   8.368 +structure CancelFactorCommon =
   8.369 +  struct
   8.370 +  val mk_sum            = (fn T:typ => long_mk_prod)
   8.371 +  val dest_sum          = dest_prod
   8.372 +  val mk_coeff          = mk_coeff
   8.373 +  val dest_coeff        = dest_coeff
   8.374 +  val find_first        = find_first_t []
   8.375 +  val trans_tac         = K Arith_Data.trans_tac
   8.376 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   8.377 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   8.378 +  val simplify_meta_eq  = cancel_simplify_meta_eq
   8.379 +  end;
   8.380 +
   8.381 +structure EqCancelFactor = ExtractCommonTermFun
   8.382 + (open CancelFactorCommon
   8.383 +  val prove_conv = Arith_Data.prove_conv
   8.384 +  val mk_bal   = HOLogic.mk_eq
   8.385 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   8.386 +  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
   8.387 +);
   8.388 +
   8.389 +structure LessCancelFactor = ExtractCommonTermFun
   8.390 + (open CancelFactorCommon
   8.391 +  val prove_conv = Arith_Data.prove_conv
   8.392 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   8.393 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   8.394 +  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
   8.395 +);
   8.396 +
   8.397 +structure LeCancelFactor = ExtractCommonTermFun
   8.398 + (open CancelFactorCommon
   8.399 +  val prove_conv = Arith_Data.prove_conv
   8.400 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   8.401 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   8.402 +  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
   8.403 +);
   8.404 +
   8.405 +structure DivideCancelFactor = ExtractCommonTermFun
   8.406 + (open CancelFactorCommon
   8.407 +  val prove_conv = Arith_Data.prove_conv
   8.408 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   8.409 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   8.410 +  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
   8.411 +);
   8.412 +
   8.413 +structure DvdCancelFactor = ExtractCommonTermFun
   8.414 + (open CancelFactorCommon
   8.415 +  val prove_conv = Arith_Data.prove_conv
   8.416 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   8.417 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   8.418 +  val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
   8.419 +);
   8.420 +
   8.421 +val cancel_factor =
   8.422 +  map Arith_Data.prep_simproc
   8.423 +   [("nat_eq_cancel_factor",
   8.424 +     ["(l::nat) * m = n", "(l::nat) = m * n"],
   8.425 +     K EqCancelFactor.proc),
   8.426 +    ("nat_less_cancel_factor",
   8.427 +     ["(l::nat) * m < n", "(l::nat) < m * n"],
   8.428 +     K LessCancelFactor.proc),
   8.429 +    ("nat_le_cancel_factor",
   8.430 +     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   8.431 +     K LeCancelFactor.proc),
   8.432 +    ("nat_divide_cancel_factor",
   8.433 +     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   8.434 +     K DivideCancelFactor.proc),
   8.435 +    ("nat_dvd_cancel_factor",
   8.436 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   8.437 +     K DvdCancelFactor.proc)];
   8.438 +
   8.439 +end;
   8.440 +
   8.441 +
   8.442 +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   8.443 +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   8.444 +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   8.445 +Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
   8.446 +
   8.447 +
   8.448 +(*examples:
   8.449 +print_depth 22;
   8.450 +set timing;
   8.451 +set trace_simp;
   8.452 +fun test s = (Goal s; by (Simp_tac 1));
   8.453 +
   8.454 +(*cancel_numerals*)
   8.455 +test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
   8.456 +test "(2*length xs < 2*length xs + j)";
   8.457 +test "(2*length xs < length xs * 2 + j)";
   8.458 +test "2*u = (u::nat)";
   8.459 +test "2*u = Suc (u)";
   8.460 +test "(i + j + 12 + (k::nat)) - 15 = y";
   8.461 +test "(i + j + 12 + (k::nat)) - 5 = y";
   8.462 +test "Suc u - 2 = y";
   8.463 +test "Suc (Suc (Suc u)) - 2 = y";
   8.464 +test "(i + j + 2 + (k::nat)) - 1 = y";
   8.465 +test "(i + j + 1 + (k::nat)) - 2 = y";
   8.466 +
   8.467 +test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
   8.468 +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
   8.469 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
   8.470 +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
   8.471 +test "Suc ((u*v)*4) - v*3*u = w";
   8.472 +test "Suc (Suc ((u*v)*3)) - v*3*u = w";
   8.473 +
   8.474 +test "(i + j + 12 + (k::nat)) = u + 15 + y";
   8.475 +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
   8.476 +test "(i + j + 12 + (k::nat)) = u + 5 + y";
   8.477 +(*Suc*)
   8.478 +test "(i + j + 12 + k) = Suc (u + y)";
   8.479 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
   8.480 +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   8.481 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
   8.482 +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   8.483 +test "2*y + 3*z + 2*u = Suc (u)";
   8.484 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
   8.485 +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::nat)";
   8.486 +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
   8.487 +test "(2*n*m) < (3*(m*n)) + (u::nat)";
   8.488 +
   8.489 +test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
   8.490 + 
   8.491 +test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
   8.492 +
   8.493 +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
   8.494 +
   8.495 +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
   8.496 +
   8.497 +
   8.498 +(*negative numerals: FAIL*)
   8.499 +test "(i + j + -23 + (k::nat)) < u + 15 + y";
   8.500 +test "(i + j + 3 + (k::nat)) < u + -15 + y";
   8.501 +test "(i + j + -12 + (k::nat)) - 15 = y";
   8.502 +test "(i + j + 12 + (k::nat)) - -15 = y";
   8.503 +test "(i + j + -12 + (k::nat)) - -15 = y";
   8.504 +
   8.505 +(*combine_numerals*)
   8.506 +test "k + 3*k = (u::nat)";
   8.507 +test "Suc (i + 3) = u";
   8.508 +test "Suc (i + j + 3 + k) = u";
   8.509 +test "k + j + 3*k + j = (u::nat)";
   8.510 +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
   8.511 +test "(2*n*m) + (3*(m*n)) = (u::nat)";
   8.512 +(*negative numerals: FAIL*)
   8.513 +test "Suc (i + j + -3 + k) = u";
   8.514 +
   8.515 +(*cancel_numeral_factors*)
   8.516 +test "9*x = 12 * (y::nat)";
   8.517 +test "(9*x) div (12 * (y::nat)) = z";
   8.518 +test "9*x < 12 * (y::nat)";
   8.519 +test "9*x <= 12 * (y::nat)";
   8.520 +
   8.521 +(*cancel_factor*)
   8.522 +test "x*k = k*(y::nat)";
   8.523 +test "k = k*(y::nat)";
   8.524 +test "a*(b*c) = (b::nat)";
   8.525 +test "a*(b*c) = d*(b::nat)*(x*a)";
   8.526 +
   8.527 +test "x*k < k*(y::nat)";
   8.528 +test "k < k*(y::nat)";
   8.529 +test "a*(b*c) < (b::nat)";
   8.530 +test "a*(b*c) < d*(b::nat)*(x*a)";
   8.531 +
   8.532 +test "x*k <= k*(y::nat)";
   8.533 +test "k <= k*(y::nat)";
   8.534 +test "a*(b*c) <= (b::nat)";
   8.535 +test "a*(b*c) <= d*(b::nat)*(x*a)";
   8.536 +
   8.537 +test "(x*k) div (k*(y::nat)) = (uu::nat)";
   8.538 +test "(k) div (k*(y::nat)) = (uu::nat)";
   8.539 +test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
   8.540 +test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
   8.541 +*)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri May 08 09:48:07 2009 +0200
     9.3 @@ -0,0 +1,786 @@
     9.4 +(* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.5 +   Copyright   2000  University of Cambridge
     9.6 +
     9.7 +Simprocs for the integer numerals.
     9.8 +*)
     9.9 +
    9.10 +(*To quote from Provers/Arith/cancel_numeral_factor.ML:
    9.11 +
    9.12 +Cancels common coefficients in balanced expressions:
    9.13 +
    9.14 +     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
    9.15 +
    9.16 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
    9.17 +and d = gcd(m,m') and n=m/d and n'=m'/d.
    9.18 +*)
    9.19 +
    9.20 +signature NUMERAL_SIMPROCS =
    9.21 +sig
    9.22 +  val mk_sum: typ -> term list -> term
    9.23 +  val dest_sum: term -> term list
    9.24 +
    9.25 +  val assoc_fold_simproc: simproc
    9.26 +  val combine_numerals: simproc
    9.27 +  val cancel_numerals: simproc list
    9.28 +  val cancel_factors: simproc list
    9.29 +  val cancel_numeral_factors: simproc list
    9.30 +  val field_combine_numerals: simproc
    9.31 +  val field_cancel_numeral_factors: simproc list
    9.32 +  val num_ss: simpset
    9.33 +end;
    9.34 +
    9.35 +structure Numeral_Simprocs : NUMERAL_SIMPROCS =
    9.36 +struct
    9.37 +
    9.38 +fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    9.39 +
    9.40 +fun find_first_numeral past (t::terms) =
    9.41 +        ((snd (HOLogic.dest_number t), rev past @ terms)
    9.42 +         handle TERM _ => find_first_numeral (t::past) terms)
    9.43 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    9.44 +
    9.45 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    9.46 +
    9.47 +fun mk_minus t = 
    9.48 +  let val T = Term.fastype_of t
    9.49 +  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
    9.50 +
    9.51 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    9.52 +fun mk_sum T []        = mk_number T 0
    9.53 +  | mk_sum T [t,u]     = mk_plus (t, u)
    9.54 +  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    9.55 +
    9.56 +(*this version ALWAYS includes a trailing zero*)
    9.57 +fun long_mk_sum T []        = mk_number T 0
    9.58 +  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    9.59 +
    9.60 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT;
    9.61 +
    9.62 +(*decompose additions AND subtractions as a sum*)
    9.63 +fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
    9.64 +        dest_summing (pos, t, dest_summing (pos, u, ts))
    9.65 +  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
    9.66 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
    9.67 +  | dest_summing (pos, t, ts) =
    9.68 +        if pos then t::ts else mk_minus t :: ts;
    9.69 +
    9.70 +fun dest_sum t = dest_summing (true, t, []);
    9.71 +
    9.72 +val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
    9.73 +val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
    9.74 +
    9.75 +val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    9.76 +
    9.77 +fun one_of T = Const(@{const_name HOL.one},T);
    9.78 +
    9.79 +(* build product with trailing 1 rather than Numeral 1 in order to avoid the
    9.80 +   unnecessary restriction to type class number_ring
    9.81 +   which is not required for cancellation of common factors in divisions.
    9.82 +*)
    9.83 +fun mk_prod T = 
    9.84 +  let val one = one_of T
    9.85 +  fun mk [] = one
    9.86 +    | mk [t] = t
    9.87 +    | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
    9.88 +  in mk end;
    9.89 +
    9.90 +(*This version ALWAYS includes a trailing one*)
    9.91 +fun long_mk_prod T []        = one_of T
    9.92 +  | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
    9.93 +
    9.94 +val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
    9.95 +
    9.96 +fun dest_prod t =
    9.97 +      let val (t,u) = dest_times t
    9.98 +      in dest_prod t @ dest_prod u end
    9.99 +      handle TERM _ => [t];
   9.100 +
   9.101 +(*DON'T do the obvious simplifications; that would create special cases*)
   9.102 +fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   9.103 +
   9.104 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   9.105 +fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   9.106 +  | dest_coeff sign t =
   9.107 +    let val ts = sort TermOrd.term_ord (dest_prod t)
   9.108 +        val (n, ts') = find_first_numeral [] ts
   9.109 +                          handle TERM _ => (1, ts)
   9.110 +    in (sign*n, mk_prod (Term.fastype_of t) ts') end;
   9.111 +
   9.112 +(*Find first coefficient-term THAT MATCHES u*)
   9.113 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   9.114 +  | find_first_coeff past u (t::terms) =
   9.115 +        let val (n,u') = dest_coeff 1 t
   9.116 +        in if u aconv u' then (n, rev past @ terms)
   9.117 +                         else find_first_coeff (t::past) u terms
   9.118 +        end
   9.119 +        handle TERM _ => find_first_coeff (t::past) u terms;
   9.120 +
   9.121 +(*Fractions as pairs of ints. Can't use Rat.rat because the representation
   9.122 +  needs to preserve negative values in the denominator.*)
   9.123 +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
   9.124 +
   9.125 +(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   9.126 +  Fractions are reduced later by the cancel_numeral_factor simproc.*)
   9.127 +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   9.128 +
   9.129 +val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
   9.130 +
   9.131 +(*Build term (p / q) * t*)
   9.132 +fun mk_fcoeff ((p, q), t) =
   9.133 +  let val T = Term.fastype_of t
   9.134 +  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   9.135 +
   9.136 +(*Express t as a product of a fraction with other sorted terms*)
   9.137 +fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
   9.138 +  | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
   9.139 +    let val (p, t') = dest_coeff sign t
   9.140 +        val (q, u') = dest_coeff 1 u
   9.141 +    in (mk_frac (p, q), mk_divide (t', u')) end
   9.142 +  | dest_fcoeff sign t =
   9.143 +    let val (p, t') = dest_coeff sign t
   9.144 +        val T = Term.fastype_of t
   9.145 +    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
   9.146 +
   9.147 +
   9.148 +(** New term ordering so that AC-rewriting brings numerals to the front **)
   9.149 +
   9.150 +(*Order integers by absolute value and then by sign. The standard integer
   9.151 +  ordering is not well-founded.*)
   9.152 +fun num_ord (i,j) =
   9.153 +  (case int_ord (abs i, abs j) of
   9.154 +    EQUAL => int_ord (Int.sign i, Int.sign j) 
   9.155 +  | ord => ord);
   9.156 +
   9.157 +(*This resembles TermOrd.term_ord, but it puts binary numerals before other
   9.158 +  non-atomic terms.*)
   9.159 +local open Term 
   9.160 +in 
   9.161 +fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
   9.162 +      (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord)
   9.163 +  | numterm_ord
   9.164 +     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
   9.165 +     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
   9.166 +  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
   9.167 +  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
   9.168 +  | numterm_ord (t, u) =
   9.169 +      (case int_ord (size_of_term t, size_of_term u) of
   9.170 +        EQUAL =>
   9.171 +          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
   9.172 +            (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
   9.173 +          end
   9.174 +      | ord => ord)
   9.175 +and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
   9.176 +end;
   9.177 +
   9.178 +fun numtermless tu = (numterm_ord tu = LESS);
   9.179 +
   9.180 +val num_ss = HOL_ss settermless numtermless;
   9.181 +
   9.182 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
   9.183 +val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
   9.184 +
   9.185 +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
   9.186 +val add_0s =  @{thms add_0s};
   9.187 +val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
   9.188 +
   9.189 +(*Simplify inverse Numeral1, a/Numeral1*)
   9.190 +val inverse_1s = [@{thm inverse_numeral_1}];
   9.191 +val divide_1s = [@{thm divide_numeral_1}];
   9.192 +
   9.193 +(*To perform binary arithmetic.  The "left" rewriting handles patterns
   9.194 +  created by the Numeral_Simprocs, such as 3 * (5 * x). *)
   9.195 +val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
   9.196 +                 @{thm add_number_of_left}, @{thm mult_number_of_left}] @
   9.197 +                @{thms arith_simps} @ @{thms rel_simps};
   9.198 +
   9.199 +(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   9.200 +  during re-arrangement*)
   9.201 +val non_add_simps =
   9.202 +  subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
   9.203 +
   9.204 +(*To evaluate binary negations of coefficients*)
   9.205 +val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
   9.206 +                   @{thms minus_bin_simps} @ @{thms pred_bin_simps};
   9.207 +
   9.208 +(*To let us treat subtraction as addition*)
   9.209 +val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
   9.210 +
   9.211 +(*To let us treat division as multiplication*)
   9.212 +val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
   9.213 +
   9.214 +(*push the unary minus down: - x * y = x * - y *)
   9.215 +val minus_mult_eq_1_to_2 =
   9.216 +    [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
   9.217 +
   9.218 +(*to extract again any uncancelled minuses*)
   9.219 +val minus_from_mult_simps =
   9.220 +    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
   9.221 +
   9.222 +(*combine unary minus with numeric literals, however nested within a product*)
   9.223 +val mult_minus_simps =
   9.224 +    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
   9.225 +
   9.226 +val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   9.227 +  diff_simps @ minus_simps @ @{thms add_ac}
   9.228 +val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   9.229 +val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   9.230 +
   9.231 +structure CancelNumeralsCommon =
   9.232 +  struct
   9.233 +  val mk_sum            = mk_sum
   9.234 +  val dest_sum          = dest_sum
   9.235 +  val mk_coeff          = mk_coeff
   9.236 +  val dest_coeff        = dest_coeff 1
   9.237 +  val find_first_coeff  = find_first_coeff []
   9.238 +  val trans_tac         = K Arith_Data.trans_tac
   9.239 +
   9.240 +  fun norm_tac ss =
   9.241 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   9.242 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   9.243 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   9.244 +
   9.245 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   9.246 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   9.247 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   9.248 +  end;
   9.249 +
   9.250 +
   9.251 +structure EqCancelNumerals = CancelNumeralsFun
   9.252 + (open CancelNumeralsCommon
   9.253 +  val prove_conv = Arith_Data.prove_conv
   9.254 +  val mk_bal   = HOLogic.mk_eq
   9.255 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   9.256 +  val bal_add1 = @{thm eq_add_iff1} RS trans
   9.257 +  val bal_add2 = @{thm eq_add_iff2} RS trans
   9.258 +);
   9.259 +
   9.260 +structure LessCancelNumerals = CancelNumeralsFun
   9.261 + (open CancelNumeralsCommon
   9.262 +  val prove_conv = Arith_Data.prove_conv
   9.263 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   9.264 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   9.265 +  val bal_add1 = @{thm less_add_iff1} RS trans
   9.266 +  val bal_add2 = @{thm less_add_iff2} RS trans
   9.267 +);
   9.268 +
   9.269 +structure LeCancelNumerals = CancelNumeralsFun
   9.270 + (open CancelNumeralsCommon
   9.271 +  val prove_conv = Arith_Data.prove_conv
   9.272 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   9.273 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   9.274 +  val bal_add1 = @{thm le_add_iff1} RS trans
   9.275 +  val bal_add2 = @{thm le_add_iff2} RS trans
   9.276 +);
   9.277 +
   9.278 +val cancel_numerals =
   9.279 +  map Arith_Data.prep_simproc
   9.280 +   [("inteq_cancel_numerals",
   9.281 +     ["(l::'a::number_ring) + m = n",
   9.282 +      "(l::'a::number_ring) = m + n",
   9.283 +      "(l::'a::number_ring) - m = n",
   9.284 +      "(l::'a::number_ring) = m - n",
   9.285 +      "(l::'a::number_ring) * m = n",
   9.286 +      "(l::'a::number_ring) = m * n"],
   9.287 +     K EqCancelNumerals.proc),
   9.288 +    ("intless_cancel_numerals",
   9.289 +     ["(l::'a::{ordered_idom,number_ring}) + m < n",
   9.290 +      "(l::'a::{ordered_idom,number_ring}) < m + n",
   9.291 +      "(l::'a::{ordered_idom,number_ring}) - m < n",
   9.292 +      "(l::'a::{ordered_idom,number_ring}) < m - n",
   9.293 +      "(l::'a::{ordered_idom,number_ring}) * m < n",
   9.294 +      "(l::'a::{ordered_idom,number_ring}) < m * n"],
   9.295 +     K LessCancelNumerals.proc),
   9.296 +    ("intle_cancel_numerals",
   9.297 +     ["(l::'a::{ordered_idom,number_ring}) + m <= n",
   9.298 +      "(l::'a::{ordered_idom,number_ring}) <= m + n",
   9.299 +      "(l::'a::{ordered_idom,number_ring}) - m <= n",
   9.300 +      "(l::'a::{ordered_idom,number_ring}) <= m - n",
   9.301 +      "(l::'a::{ordered_idom,number_ring}) * m <= n",
   9.302 +      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   9.303 +     K LeCancelNumerals.proc)];
   9.304 +
   9.305 +structure CombineNumeralsData =
   9.306 +  struct
   9.307 +  type coeff            = int
   9.308 +  val iszero            = (fn x => x = 0)
   9.309 +  val add               = op +
   9.310 +  val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
   9.311 +  val dest_sum          = dest_sum
   9.312 +  val mk_coeff          = mk_coeff
   9.313 +  val dest_coeff        = dest_coeff 1
   9.314 +  val left_distrib      = @{thm combine_common_factor} RS trans
   9.315 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   9.316 +  val trans_tac         = K Arith_Data.trans_tac
   9.317 +
   9.318 +  fun norm_tac ss =
   9.319 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   9.320 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   9.321 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   9.322 +
   9.323 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   9.324 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   9.325 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
   9.326 +  end;
   9.327 +
   9.328 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   9.329 +
   9.330 +(*Version for fields, where coefficients can be fractions*)
   9.331 +structure FieldCombineNumeralsData =
   9.332 +  struct
   9.333 +  type coeff            = int * int
   9.334 +  val iszero            = (fn (p, q) => p = 0)
   9.335 +  val add               = add_frac
   9.336 +  val mk_sum            = long_mk_sum
   9.337 +  val dest_sum          = dest_sum
   9.338 +  val mk_coeff          = mk_fcoeff
   9.339 +  val dest_coeff        = dest_fcoeff 1
   9.340 +  val left_distrib      = @{thm combine_common_factor} RS trans
   9.341 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   9.342 +  val trans_tac         = K Arith_Data.trans_tac
   9.343 +
   9.344 +  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   9.345 +  fun norm_tac ss =
   9.346 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
   9.347 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   9.348 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   9.349 +
   9.350 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   9.351 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   9.352 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
   9.353 +  end;
   9.354 +
   9.355 +structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   9.356 +
   9.357 +val combine_numerals =
   9.358 +  Arith_Data.prep_simproc
   9.359 +    ("int_combine_numerals", 
   9.360 +     ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
   9.361 +     K CombineNumerals.proc);
   9.362 +
   9.363 +val field_combine_numerals =
   9.364 +  Arith_Data.prep_simproc
   9.365 +    ("field_combine_numerals", 
   9.366 +     ["(i::'a::{number_ring,field,division_by_zero}) + j",
   9.367 +      "(i::'a::{number_ring,field,division_by_zero}) - j"], 
   9.368 +     K FieldCombineNumerals.proc);
   9.369 +
   9.370 +(** Constant folding for multiplication in semirings **)
   9.371 +
   9.372 +(*We do not need folding for addition: combine_numerals does the same thing*)
   9.373 +
   9.374 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   9.375 +struct
   9.376 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   9.377 +  val eq_reflection = eq_reflection
   9.378 +  fun is_numeral (Const(@{const_name Int.number_of}, _) $ _) = true
   9.379 +    | is_numeral _ = false;
   9.380 +end;
   9.381 +
   9.382 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
   9.383 +
   9.384 +val assoc_fold_simproc =
   9.385 +  Arith_Data.prep_simproc
   9.386 +   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
   9.387 +    K Semiring_Times_Assoc.proc);
   9.388 +
   9.389 +structure CancelNumeralFactorCommon =
   9.390 +  struct
   9.391 +  val mk_coeff          = mk_coeff
   9.392 +  val dest_coeff        = dest_coeff 1
   9.393 +  val trans_tac         = K Arith_Data.trans_tac
   9.394 +
   9.395 +  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   9.396 +  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
   9.397 +  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
   9.398 +  fun norm_tac ss =
   9.399 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   9.400 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   9.401 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   9.402 +
   9.403 +  val numeral_simp_ss = HOL_ss addsimps
   9.404 +    [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
   9.405 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   9.406 +  val simplify_meta_eq = Arith_Data.simplify_meta_eq
   9.407 +    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
   9.408 +      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
   9.409 +  end
   9.410 +
   9.411 +(*Version for semiring_div*)
   9.412 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
   9.413 + (open CancelNumeralFactorCommon
   9.414 +  val prove_conv = Arith_Data.prove_conv
   9.415 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   9.416 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   9.417 +  val cancel = @{thm div_mult_mult1} RS trans
   9.418 +  val neg_exchanges = false
   9.419 +)
   9.420 +
   9.421 +(*Version for fields*)
   9.422 +structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   9.423 + (open CancelNumeralFactorCommon
   9.424 +  val prove_conv = Arith_Data.prove_conv
   9.425 +  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   9.426 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   9.427 +  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   9.428 +  val neg_exchanges = false
   9.429 +)
   9.430 +
   9.431 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
   9.432 + (open CancelNumeralFactorCommon
   9.433 +  val prove_conv = Arith_Data.prove_conv
   9.434 +  val mk_bal   = HOLogic.mk_eq
   9.435 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   9.436 +  val cancel = @{thm mult_cancel_left} RS trans
   9.437 +  val neg_exchanges = false
   9.438 +)
   9.439 +
   9.440 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
   9.441 + (open CancelNumeralFactorCommon
   9.442 +  val prove_conv = Arith_Data.prove_conv
   9.443 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   9.444 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   9.445 +  val cancel = @{thm mult_less_cancel_left} RS trans
   9.446 +  val neg_exchanges = true
   9.447 +)
   9.448 +
   9.449 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
   9.450 + (open CancelNumeralFactorCommon
   9.451 +  val prove_conv = Arith_Data.prove_conv
   9.452 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   9.453 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   9.454 +  val cancel = @{thm mult_le_cancel_left} RS trans
   9.455 +  val neg_exchanges = true
   9.456 +)
   9.457 +
   9.458 +val cancel_numeral_factors =
   9.459 +  map Arith_Data.prep_simproc
   9.460 +   [("ring_eq_cancel_numeral_factor",
   9.461 +     ["(l::'a::{idom,number_ring}) * m = n",
   9.462 +      "(l::'a::{idom,number_ring}) = m * n"],
   9.463 +     K EqCancelNumeralFactor.proc),
   9.464 +    ("ring_less_cancel_numeral_factor",
   9.465 +     ["(l::'a::{ordered_idom,number_ring}) * m < n",
   9.466 +      "(l::'a::{ordered_idom,number_ring}) < m * n"],
   9.467 +     K LessCancelNumeralFactor.proc),
   9.468 +    ("ring_le_cancel_numeral_factor",
   9.469 +     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
   9.470 +      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
   9.471 +     K LeCancelNumeralFactor.proc),
   9.472 +    ("int_div_cancel_numeral_factors",
   9.473 +     ["((l::'a::{semiring_div,number_ring}) * m) div n",
   9.474 +      "(l::'a::{semiring_div,number_ring}) div (m * n)"],
   9.475 +     K DivCancelNumeralFactor.proc),
   9.476 +    ("divide_cancel_numeral_factor",
   9.477 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   9.478 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   9.479 +      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   9.480 +     K DivideCancelNumeralFactor.proc)];
   9.481 +
   9.482 +val field_cancel_numeral_factors =
   9.483 +  map Arith_Data.prep_simproc
   9.484 +   [("field_eq_cancel_numeral_factor",
   9.485 +     ["(l::'a::{field,number_ring}) * m = n",
   9.486 +      "(l::'a::{field,number_ring}) = m * n"],
   9.487 +     K EqCancelNumeralFactor.proc),
   9.488 +    ("field_cancel_numeral_factor",
   9.489 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
   9.490 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
   9.491 +      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
   9.492 +     K DivideCancelNumeralFactor.proc)]
   9.493 +
   9.494 +
   9.495 +(** Declarations for ExtractCommonTerm **)
   9.496 +
   9.497 +(*Find first term that matches u*)
   9.498 +fun find_first_t past u []         = raise TERM ("find_first_t", [])
   9.499 +  | find_first_t past u (t::terms) =
   9.500 +        if u aconv t then (rev past @ terms)
   9.501 +        else find_first_t (t::past) u terms
   9.502 +        handle TERM _ => find_first_t (t::past) u terms;
   9.503 +
   9.504 +(** Final simplification for the CancelFactor simprocs **)
   9.505 +val simplify_one = Arith_Data.simplify_meta_eq  
   9.506 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
   9.507 +
   9.508 +fun cancel_simplify_meta_eq ss cancel_th th =
   9.509 +    simplify_one ss (([th, cancel_th]) MRS trans);
   9.510 +
   9.511 +local
   9.512 +  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
   9.513 +  fun Eq_True_elim Eq = 
   9.514 +    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
   9.515 +in
   9.516 +fun sign_conv pos_th neg_th ss t =
   9.517 +  let val T = fastype_of t;
   9.518 +      val zero = Const(@{const_name HOL.zero}, T);
   9.519 +      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
   9.520 +      val pos = less $ zero $ t and neg = less $ t $ zero
   9.521 +      fun prove p =
   9.522 +        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
   9.523 +        handle THM _ => NONE
   9.524 +    in case prove pos of
   9.525 +         SOME th => SOME(th RS pos_th)
   9.526 +       | NONE => (case prove neg of
   9.527 +                    SOME th => SOME(th RS neg_th)
   9.528 +                  | NONE => NONE)
   9.529 +    end;
   9.530 +end
   9.531 +
   9.532 +structure CancelFactorCommon =
   9.533 +  struct
   9.534 +  val mk_sum            = long_mk_prod
   9.535 +  val dest_sum          = dest_prod
   9.536 +  val mk_coeff          = mk_coeff
   9.537 +  val dest_coeff        = dest_coeff
   9.538 +  val find_first        = find_first_t []
   9.539 +  val trans_tac         = K Arith_Data.trans_tac
   9.540 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   9.541 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   9.542 +  val simplify_meta_eq  = cancel_simplify_meta_eq 
   9.543 +  end;
   9.544 +
   9.545 +(*mult_cancel_left requires a ring with no zero divisors.*)
   9.546 +structure EqCancelFactor = ExtractCommonTermFun
   9.547 + (open CancelFactorCommon
   9.548 +  val prove_conv = Arith_Data.prove_conv
   9.549 +  val mk_bal   = HOLogic.mk_eq
   9.550 +  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   9.551 +  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
   9.552 +);
   9.553 +
   9.554 +(*for ordered rings*)
   9.555 +structure LeCancelFactor = ExtractCommonTermFun
   9.556 + (open CancelFactorCommon
   9.557 +  val prove_conv = Arith_Data.prove_conv
   9.558 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   9.559 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   9.560 +  val simp_conv = sign_conv
   9.561 +    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   9.562 +);
   9.563 +
   9.564 +(*for ordered rings*)
   9.565 +structure LessCancelFactor = ExtractCommonTermFun
   9.566 + (open CancelFactorCommon
   9.567 +  val prove_conv = Arith_Data.prove_conv
   9.568 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   9.569 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   9.570 +  val simp_conv = sign_conv
   9.571 +    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   9.572 +);
   9.573 +
   9.574 +(*for semirings with division*)
   9.575 +structure DivCancelFactor = ExtractCommonTermFun
   9.576 + (open CancelFactorCommon
   9.577 +  val prove_conv = Arith_Data.prove_conv
   9.578 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   9.579 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
   9.580 +  val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
   9.581 +);
   9.582 +
   9.583 +structure ModCancelFactor = ExtractCommonTermFun
   9.584 + (open CancelFactorCommon
   9.585 +  val prove_conv = Arith_Data.prove_conv
   9.586 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   9.587 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
   9.588 +  val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
   9.589 +);
   9.590 +
   9.591 +(*for idoms*)
   9.592 +structure DvdCancelFactor = ExtractCommonTermFun
   9.593 + (open CancelFactorCommon
   9.594 +  val prove_conv = Arith_Data.prove_conv
   9.595 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   9.596 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
   9.597 +  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
   9.598 +);
   9.599 +
   9.600 +(*Version for all fields, including unordered ones (type complex).*)
   9.601 +structure DivideCancelFactor = ExtractCommonTermFun
   9.602 + (open CancelFactorCommon
   9.603 +  val prove_conv = Arith_Data.prove_conv
   9.604 +  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   9.605 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   9.606 +  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
   9.607 +);
   9.608 +
   9.609 +val cancel_factors =
   9.610 +  map Arith_Data.prep_simproc
   9.611 +   [("ring_eq_cancel_factor",
   9.612 +     ["(l::'a::idom) * m = n",
   9.613 +      "(l::'a::idom) = m * n"],
   9.614 +     K EqCancelFactor.proc),
   9.615 +    ("ordered_ring_le_cancel_factor",
   9.616 +     ["(l::'a::ordered_ring) * m <= n",
   9.617 +      "(l::'a::ordered_ring) <= m * n"],
   9.618 +     K LeCancelFactor.proc),
   9.619 +    ("ordered_ring_less_cancel_factor",
   9.620 +     ["(l::'a::ordered_ring) * m < n",
   9.621 +      "(l::'a::ordered_ring) < m * n"],
   9.622 +     K LessCancelFactor.proc),
   9.623 +    ("int_div_cancel_factor",
   9.624 +     ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
   9.625 +     K DivCancelFactor.proc),
   9.626 +    ("int_mod_cancel_factor",
   9.627 +     ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
   9.628 +     K ModCancelFactor.proc),
   9.629 +    ("dvd_cancel_factor",
   9.630 +     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   9.631 +     K DvdCancelFactor.proc),
   9.632 +    ("divide_cancel_factor",
   9.633 +     ["((l::'a::{division_by_zero,field}) * m) / n",
   9.634 +      "(l::'a::{division_by_zero,field}) / (m * n)"],
   9.635 +     K DivideCancelFactor.proc)];
   9.636 +
   9.637 +end;
   9.638 +
   9.639 +Addsimprocs Numeral_Simprocs.cancel_numerals;
   9.640 +Addsimprocs [Numeral_Simprocs.combine_numerals];
   9.641 +Addsimprocs [Numeral_Simprocs.field_combine_numerals];
   9.642 +Addsimprocs [Numeral_Simprocs.assoc_fold_simproc];
   9.643 +
   9.644 +(*examples:
   9.645 +print_depth 22;
   9.646 +set timing;
   9.647 +set trace_simp;
   9.648 +fun test s = (Goal s, by (Simp_tac 1));
   9.649 +
   9.650 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   9.651 +
   9.652 +test "2*u = (u::int)";
   9.653 +test "(i + j + 12 + (k::int)) - 15 = y";
   9.654 +test "(i + j + 12 + (k::int)) - 5 = y";
   9.655 +
   9.656 +test "y - b < (b::int)";
   9.657 +test "y - (3*b + c) < (b::int) - 2*c";
   9.658 +
   9.659 +test "(2*x - (u*v) + y) - v*3*u = (w::int)";
   9.660 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
   9.661 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
   9.662 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
   9.663 +
   9.664 +test "(i + j + 12 + (k::int)) = u + 15 + y";
   9.665 +test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
   9.666 +
   9.667 +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)";
   9.668 +
   9.669 +test "a + -(b+c) + b = (d::int)";
   9.670 +test "a + -(b+c) - b = (d::int)";
   9.671 +
   9.672 +(*negative numerals*)
   9.673 +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
   9.674 +test "(i + j + -3 + (k::int)) < u + 5 + y";
   9.675 +test "(i + j + 3 + (k::int)) < u + -6 + y";
   9.676 +test "(i + j + -12 + (k::int)) - 15 = y";
   9.677 +test "(i + j + 12 + (k::int)) - -15 = y";
   9.678 +test "(i + j + -12 + (k::int)) - -15 = y";
   9.679 +*)
   9.680 +
   9.681 +Addsimprocs Numeral_Simprocs.cancel_numeral_factors;
   9.682 +
   9.683 +(*examples:
   9.684 +print_depth 22;
   9.685 +set timing;
   9.686 +set trace_simp;
   9.687 +fun test s = (Goal s; by (Simp_tac 1));
   9.688 +
   9.689 +test "9*x = 12 * (y::int)";
   9.690 +test "(9*x) div (12 * (y::int)) = z";
   9.691 +test "9*x < 12 * (y::int)";
   9.692 +test "9*x <= 12 * (y::int)";
   9.693 +
   9.694 +test "-99*x = 132 * (y::int)";
   9.695 +test "(-99*x) div (132 * (y::int)) = z";
   9.696 +test "-99*x < 132 * (y::int)";
   9.697 +test "-99*x <= 132 * (y::int)";
   9.698 +
   9.699 +test "999*x = -396 * (y::int)";
   9.700 +test "(999*x) div (-396 * (y::int)) = z";
   9.701 +test "999*x < -396 * (y::int)";
   9.702 +test "999*x <= -396 * (y::int)";
   9.703 +
   9.704 +test "-99*x = -81 * (y::int)";
   9.705 +test "(-99*x) div (-81 * (y::int)) = z";
   9.706 +test "-99*x <= -81 * (y::int)";
   9.707 +test "-99*x < -81 * (y::int)";
   9.708 +
   9.709 +test "-2 * x = -1 * (y::int)";
   9.710 +test "-2 * x = -(y::int)";
   9.711 +test "(-2 * x) div (-1 * (y::int)) = z";
   9.712 +test "-2 * x < -(y::int)";
   9.713 +test "-2 * x <= -1 * (y::int)";
   9.714 +test "-x < -23 * (y::int)";
   9.715 +test "-x <= -23 * (y::int)";
   9.716 +*)
   9.717 +
   9.718 +(*And the same examples for fields such as rat or real:
   9.719 +test "0 <= (y::rat) * -2";
   9.720 +test "9*x = 12 * (y::rat)";
   9.721 +test "(9*x) / (12 * (y::rat)) = z";
   9.722 +test "9*x < 12 * (y::rat)";
   9.723 +test "9*x <= 12 * (y::rat)";
   9.724 +
   9.725 +test "-99*x = 132 * (y::rat)";
   9.726 +test "(-99*x) / (132 * (y::rat)) = z";
   9.727 +test "-99*x < 132 * (y::rat)";
   9.728 +test "-99*x <= 132 * (y::rat)";
   9.729 +
   9.730 +test "999*x = -396 * (y::rat)";
   9.731 +test "(999*x) / (-396 * (y::rat)) = z";
   9.732 +test "999*x < -396 * (y::rat)";
   9.733 +test "999*x <= -396 * (y::rat)";
   9.734 +
   9.735 +test  "(- ((2::rat) * x) <= 2 * y)";
   9.736 +test "-99*x = -81 * (y::rat)";
   9.737 +test "(-99*x) / (-81 * (y::rat)) = z";
   9.738 +test "-99*x <= -81 * (y::rat)";
   9.739 +test "-99*x < -81 * (y::rat)";
   9.740 +
   9.741 +test "-2 * x = -1 * (y::rat)";
   9.742 +test "-2 * x = -(y::rat)";
   9.743 +test "(-2 * x) / (-1 * (y::rat)) = z";
   9.744 +test "-2 * x < -(y::rat)";
   9.745 +test "-2 * x <= -1 * (y::rat)";
   9.746 +test "-x < -23 * (y::rat)";
   9.747 +test "-x <= -23 * (y::rat)";
   9.748 +*)
   9.749 +
   9.750 +Addsimprocs Numeral_Simprocs.cancel_factors;
   9.751 +
   9.752 +
   9.753 +(*examples:
   9.754 +print_depth 22;
   9.755 +set timing;
   9.756 +set trace_simp;
   9.757 +fun test s = (Goal s; by (Asm_simp_tac 1));
   9.758 +
   9.759 +test "x*k = k*(y::int)";
   9.760 +test "k = k*(y::int)";
   9.761 +test "a*(b*c) = (b::int)";
   9.762 +test "a*(b*c) = d*(b::int)*(x*a)";
   9.763 +
   9.764 +test "(x*k) div (k*(y::int)) = (uu::int)";
   9.765 +test "(k) div (k*(y::int)) = (uu::int)";
   9.766 +test "(a*(b*c)) div ((b::int)) = (uu::int)";
   9.767 +test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
   9.768 +*)
   9.769 +
   9.770 +(*And the same examples for fields such as rat or real:
   9.771 +print_depth 22;
   9.772 +set timing;
   9.773 +set trace_simp;
   9.774 +fun test s = (Goal s; by (Asm_simp_tac 1));
   9.775 +
   9.776 +test "x*k = k*(y::rat)";
   9.777 +test "k = k*(y::rat)";
   9.778 +test "a*(b*c) = (b::rat)";
   9.779 +test "a*(b*c) = d*(b::rat)*(x*a)";
   9.780 +
   9.781 +
   9.782 +test "(x*k) / (k*(y::rat)) = (uu::rat)";
   9.783 +test "(k) / (k*(y::rat)) = (uu::rat)";
   9.784 +test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
   9.785 +test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
   9.786 +
   9.787 +(*FIXME: what do we do about this?*)
   9.788 +test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
   9.789 +*)
    10.1 --- a/src/HOL/Tools/rat_arith.ML	Fri May 08 08:01:09 2009 +0200
    10.2 +++ b/src/HOL/Tools/rat_arith.ML	Fri May 08 09:48:07 2009 +0200
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOL/Real/rat_arith.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Lawrence C Paulson
    10.7      Copyright   2004 University of Cambridge
    10.8  
    10.9 @@ -10,8 +9,6 @@
   10.10  
   10.11  local
   10.12  
   10.13 -val simprocs = field_cancel_numeral_factors
   10.14 -
   10.15  val simps =
   10.16   [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
   10.17    read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
   10.18 @@ -42,7 +39,7 @@
   10.19      lessD = lessD,  (*Can't change lessD: the rats are dense!*)
   10.20      neqE =  neqE,
   10.21      simpset = simpset addsimps simps
   10.22 -                      addsimprocs simprocs}) #>
   10.23 +                      addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
   10.24    arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
   10.25    arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
   10.26