author paulson Tue, 21 Mar 2006 12:17:38 +0100 changeset 19298 741b8138c2b3 parent 19297 8f6e097d7b23 child 19299 5f0610aafc48
Now SML/NJ-friendly (IntInf)
```--- a/src/HOL/Integ/nat_simprocs.ML	Tue Mar 21 12:16:43 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue Mar 21 12:17:38 2006 +0100
@@ -52,20 +52,6 @@

val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;

-(*Split up a sum into the list of its constituent terms, on the way removing any
-  Sucs and counting them.*)
-fun dest_Suc_sum (Const ("Suc", _) \$ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
-  | dest_Suc_sum (t, (k,ts)) =
-      let val (t1,t2) = dest_plus t
-      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
-      handle TERM _ => (k, t::ts);
-
-(*The Sucs found in the term are converted to a binary numeral*)
-fun dest_Sucs_sum t =
-  case dest_Suc_sum (t,(0,[])) of
-      (0,ts) => ts
-    | (k,ts) => mk_numeral k :: ts
-

(** Other simproc items **)

@@ -121,6 +107,34 @@
handle TERM _ => find_first_coeff (t::past) u terms;

+(*Split up a sum into the list of its constituent terms, on the way removing any
+  Sucs and counting them.*)
+fun dest_Suc_sum (Const ("Suc", _) \$ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
+  | dest_Suc_sum (t, (k,ts)) =
+      let val (t1,t2) = dest_plus t
+      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
+      handle TERM _ => (k, t::ts);
+
+(*Code for testing whether numerals are already used in the goal*)
+fun is_numeral (Const("Numeral.number_of", _) \$ w) = true
+  | is_numeral _ = false;
+
+fun prod_has_numeral t = exists is_numeral (dest_prod t);
+
+(*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
+  an exception is raised unless the original expression contains at least one
+  numeral in a coefficient position.  This prevents nat_combine_numerals from
+  introducing numerals to goals.*)
+fun dest_Sucs_sum relaxed t =
+  let val (k,ts) = dest_Suc_sum (t,(0,[]))
+  in
+     if relaxed orelse exists prod_has_numeral ts then
+       if k=0 then ts
+       else mk_numeral (IntInf.fromInt k) :: ts
+     else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
+  end;
+
+
(*Simplify 1*n and n*1 to n*)
val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
@@ -138,27 +152,6 @@
mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules);

-(** Restricted version of dest_Sucs_sum for nat_combine_numerals:
-    Simprocs never apply unless the original expression contains at least one
-    numeral in a coefficient position. This avoids replacing x+x by
-    2*x, for example, unless numerals have been used already.
-**)
-
-fun is_numeral (Const("Numeral.number_of", _) \$ w) = true
-  | is_numeral _ = false;
-
-fun prod_has_numeral t = exists is_numeral (dest_prod t);
-
-fun require_has_numeral ts =
-    if exists prod_has_numeral ts then ts
-    else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", ts);
-
-fun restricted_dest_Sucs_sum t =
-  case dest_Suc_sum (t,(0,[])) of
-      (0,ts) => require_has_numeral ts
-    | (k,ts) => mk_numeral k :: require_has_numeral ts
-
-
(*Like HOL_ss but with an ordering that brings numerals to the front
under AC-rewriting.*)
val num_ss = Int_Numeral_Simprocs.num_ss;
@@ -168,7 +161,7 @@
structure CancelNumeralsCommon =
struct
val mk_sum            = (fn T:typ => mk_sum)
-  val dest_sum          = dest_Sucs_sum
+  val dest_sum          = dest_Sucs_sum true
val mk_coeff          = mk_coeff
val dest_coeff        = dest_coeff
val find_first_coeff  = find_first_coeff []
@@ -254,7 +247,7 @@
struct