New simplification ordering to move numerals together. Fixes a bug in the
nat cancellation simprocs

--- a/src/HOL/Integ/int_arith1.ML	Fri Mar 19 10:44:20 2004 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Fri Mar 19 10:46:25 2004 +0100
@@ -157,7 +157,43 @@
   isn't complicated by the abstract 0 and 1.*)
 val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
 
-(*Utilities*)
+(** New term ordering so that AC-rewriting brings numerals to the front **)
+
+(*Order integers by absolute value and then by sign. The standard integer
+  ordering is not well-founded.*)
+fun num_ord (i,j) =
+      (case Int.compare (abs i, abs j) of
+            EQUAL => Int.compare (Int.sign i, Int.sign j) 
+          | ord => ord);
+
+(*This resembles Term.term_ord, but it puts binary numerals before other
+  non-atomic terms.*)
+local open Term 
+in 
+fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
+      (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
+  | numterm_ord
+     (Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
+     num_ord (HOLogic.dest_binum v, HOLogic.dest_binum w)
+  | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
+  | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
+  | numterm_ord (t, u) =
+      (case Int.compare (size_of_term t, size_of_term u) of
+        EQUAL =>
+          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
+            (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
+          end
+      | ord => ord)
+and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
+end;
+
+fun numtermless tu = (numterm_ord tu = LESS);
+
+(*Defined in this file, but perhaps needed only for simprocs of type nat.*)
+val num_ss = HOL_ss settermless numtermless;
+
+
+(** Utilities **)
 
 fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n;
 

--- a/src/HOL/Integ/nat_simprocs.ML	Fri Mar 19 10:44:20 2004 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri Mar 19 10:46:25 2004 +0100
@@ -155,6 +155,10 @@
     else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", [t]);
 
 
+(*Like HOL_ss but with an ordering that brings numerals to the front
+  under AC-rewriting.*)
+val num_ss = Int_Numeral_Simprocs.num_ss;
+
 (*** Applying CancelNumeralsFun ***)
 
 structure CancelNumeralsCommon =
@@ -166,10 +170,10 @@
   val find_first_coeff  = find_first_coeff []
   val trans_tac          = trans_tac
   val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
-                                [Suc_eq_add_numeral_1] @ add_ac))
+                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+                                [Suc_eq_add_numeral_1_left] @ add_ac))
                  THEN ALLGOALS (simp_tac
-                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
+                                (num_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac  = ALLGOALS
                 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
@@ -250,10 +254,10 @@
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac          = trans_tac
   val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
+                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
                               [Suc_eq_add_numeral_1] @ add_ac))
                  THEN ALLGOALS (simp_tac
-                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
+                                (num_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac  = ALLGOALS
                 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
@@ -273,9 +277,10 @@
   val dest_coeff        = dest_coeff
   val trans_tac         = trans_tac
   val norm_tac = ALLGOALS
-                    (simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
-                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
+                   (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+                                [Suc_eq_add_numeral_1_left] @ add_ac))
+                 THEN ALLGOALS (simp_tac
+                                (num_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
   val simplify_meta_eq  = simplify_meta_eq
   end
@@ -459,6 +464,15 @@
 test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
 test "(2*n*m) < (3*(m*n)) + (u::nat)";
 
+test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
+ 
+test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
+
+test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
+
+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))";
+
+
 (*negative numerals: FAIL*)
 test "(i + j + -23 + (k::nat)) < u + 15 + y";
 test "(i + j + 3 + (k::nat)) < u + -15 + y";