1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sun Feb 09 21:37:27 2014 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Mon Feb 10 21:51:15 2014 +0100
     1.3 @@ -285,7 +285,8 @@
     1.4         @{simproc int_combine_numerals},
     1.5         @{simproc inteq_cancel_numerals},
     1.6         @{simproc intless_cancel_numerals},
     1.7 -       @{simproc intle_cancel_numerals}]
     1.8 +       @{simproc intle_cancel_numerals},
     1.9 +       @{simproc field_combine_numerals}]
    1.10    #> Lin_Arith.add_simprocs
    1.11        [@{simproc nat_combine_numerals},
    1.12         @{simproc nateq_cancel_numerals},

     2.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Feb 09 21:37:27 2014 +0100
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Feb 10 21:51:15 2014 +0100
     2.3 @@ -158,20 +158,19 @@
     2.4           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
     2.5           if we choose to do so here, the simpset used by arith must be able to
     2.6           perform the same simplifications. *)
     2.7 -      (* FIXME: Currently we treat the numerator as atomic unless the
     2.8 -         denominator can be reduced to a numeric constant.  It might be better
     2.9 -         to demult the numerator in any case, and invent a new term of the form
    2.10 -         '1 / t' if the numerator can be reduced, but the denominator cannot. *)
    2.11 -      (* FIXME: Currently we even treat the whole fraction as atomic unless the
    2.12 -         denominator can be reduced to a numeric constant.  It might be better
    2.13 -         to use the partially reduced denominator (i.e. 's / (2*t)' could be
    2.14 -         demult'ed to 's / t' with multiplicity .5).   This would require a
    2.15 -         very simple change only below, but it breaks existing proofs. *)
    2.16        (* quotient 's / t', where the denominator t can be NONE *)
    2.17        (* Note: will raise Rat.DIVZERO iff m' is Rat.zero *)
    2.18 -      (case demult (t, Rat.one) of
    2.19 -        (SOME _, _) => (SOME (mC $ s $ t), m)
    2.20 -      | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
    2.21 +      let val (os',m') = demult (s, m);
    2.22 +          val (ot',p) = demult (t, Rat.one)
    2.23 +      in (case (os',ot') of
    2.24 +            (SOME s', SOME t') => SOME (mC $ s' $ t')
    2.25 +          | (SOME s', NONE) => SOME s'
    2.26 +          | (NONE, SOME t') =>
    2.27 +               let val Const(_,T) = mC
    2.28 +               in SOME (mC $ Const (@{const_name Groups.one}, domain_type T) $ t') end
    2.29 +          | (NONE, NONE) => NONE,
    2.30 +          Rat.mult m' (Rat.inv p))
    2.31 +      end
    2.32      (* terms that evaluate to numeric constants *)
    2.33      | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
    2.34      | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)