src/HOL/Tools/lin_arith.ML
changeset 47108 2a1953f0d20d
parent 46709 65a9b30bff00
child 48556 62a3fbf9d35b
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -174,14 +174,17 @@
     1.4        | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
     1.5      (* terms that evaluate to numeric constants *)
     1.6      | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
     1.7 -    | demult (Const (@{const_name Groups.zero}, _), m) = (NONE, Rat.zero)
     1.8 +    | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, Rat.zero)
     1.9      | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
    1.10 -    (*Warning: in rare cases number_of encloses a non-numeral,
    1.11 -      in which case dest_numeral raises TERM; hence all the handles below.
    1.12 +    (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
    1.13 +      in which case dest_num raises TERM; hence all the handles below.
    1.14        Same for Suc-terms that turn out not to be numerals -
    1.15        although the simplifier should eliminate those anyway ...*)
    1.16 -    | demult (t as Const ("Int.number_class.number_of", _) $ n, m) =
    1.17 -      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_numeral n)))
    1.18 +    | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) =
    1.19 +      ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_num n)))
    1.20 +        handle TERM _ => (SOME t, m))
    1.21 +    | demult (t as Const ("Num.neg_numeral_class.neg_numeral", _) $ n, m) =
    1.22 +      ((NONE, Rat.mult m (Rat.rat_of_int (~ (HOLogic.dest_num n))))
    1.23          handle TERM _ => (SOME t, m))
    1.24      | demult (t as Const (@{const_name Suc}, _) $ _, m) =
    1.25        ((NONE, Rat.mult m (Rat.rat_of_int (HOLogic.dest_nat t)))
    1.26 @@ -219,10 +222,13 @@
    1.27          (case demult inj_consts (all, m) of
    1.28             (NONE,   m') => (p, Rat.add i m')
    1.29           | (SOME u, m') => add_atom u m' pi)
    1.30 -    | poly (all as Const ("Int.number_class.number_of", Type(_,[_,T])) $ t, m, pi as (p, i)) =
    1.31 -        (let val k = HOLogic.dest_numeral t
    1.32 -            val k2 = if k < 0 andalso T = HOLogic.natT then 0 else k
    1.33 -        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k2))) end
    1.34 +    | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
    1.35 +        (let val k = HOLogic.dest_num t
    1.36 +        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int k))) end
    1.37 +        handle TERM _ => add_atom all m pi)
    1.38 +    | poly (all as Const ("Num.neg_numeral_class.neg_numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) =
    1.39 +        (let val k = HOLogic.dest_num t
    1.40 +        in (p, Rat.add i (Rat.mult m (Rat.rat_of_int (~ k)))) end
    1.41          handle TERM _ => add_atom all m pi)
    1.42      | poly (all as Const f $ x, m, pi) =
    1.43          if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
    1.44 @@ -464,9 +470,9 @@
    1.45        in
    1.46          SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
    1.47        end
    1.48 -    (* ?P ((?n::nat) mod (number_of ?k)) =
    1.49 -         ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
    1.50 -           (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
    1.51 +    (* ?P ((?n::nat) mod (numeral ?k)) =
    1.52 +         ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) -->
    1.53 +           (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *)
    1.54      | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
    1.55        let
    1.56          val rev_terms               = rev terms
    1.57 @@ -496,9 +502,9 @@
    1.58        in
    1.59          SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
    1.60        end
    1.61 -    (* ?P ((?n::nat) div (number_of ?k)) =
    1.62 -         ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
    1.63 -           (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
    1.64 +    (* ?P ((?n::nat) div (numeral ?k)) =
    1.65 +         ((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) -->
    1.66 +           (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *)
    1.67      | (Const ("Divides.div_class.div", Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
    1.68        let
    1.69          val rev_terms               = rev terms
    1.70 @@ -528,14 +534,14 @@
    1.71        in
    1.72          SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
    1.73        end
    1.74 -    (* ?P ((?n::int) mod (number_of ?k)) =
    1.75 -         ((number_of ?k = 0 --> ?P ?n) &
    1.76 -          (0 < number_of ?k -->
    1.77 +    (* ?P ((?n::int) mod (numeral ?k)) =
    1.78 +         ((numeral ?k = 0 --> ?P ?n) &
    1.79 +          (0 < numeral ?k -->
    1.80              (ALL i j.
    1.81 -              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
    1.82 -          (number_of ?k < 0 -->
    1.83 +              0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P j)) &
    1.84 +          (numeral ?k < 0 -->
    1.85              (ALL i j.
    1.86 -              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
    1.87 +              numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *)
    1.88      | (Const ("Divides.div_class.mod",
    1.89          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
    1.90        let
    1.91 @@ -582,14 +588,14 @@
    1.92        in
    1.93          SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
    1.94        end
    1.95 -    (* ?P ((?n::int) div (number_of ?k)) =
    1.96 -         ((number_of ?k = 0 --> ?P 0) &
    1.97 -          (0 < number_of ?k -->
    1.98 +    (* ?P ((?n::int) div (numeral ?k)) =
    1.99 +         ((numeral ?k = 0 --> ?P 0) &
   1.100 +          (0 < numeral ?k -->
   1.101              (ALL i j.
   1.102 -              0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P i)) &
   1.103 -          (number_of ?k < 0 -->
   1.104 +              0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P i)) &
   1.105 +          (numeral ?k < 0 -->
   1.106              (ALL i j.
   1.107 -              number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P i))) *)
   1.108 +              numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *)
   1.109      | (Const ("Divides.div_class.div",
   1.110          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
   1.111        let