better rules for cancellation of common factors across comparisons

--- a/src/HOL/Integ/Bin.ML	Thu Aug 17 10:42:57 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Thu Aug 17 11:55:47 2000 +0200
@@ -226,6 +226,12 @@
 (*Moving negation out of products*)
 Addsimps [zmult_zminus, zmult_zminus_right];
 
+(*Cancellation of constant factors in comparisons (< and <=) *)
+Addsimps (map (inst "k" "number_of ?v")
+	  [zmult_zless_cancel1, zmult_zless_cancel2,
+	   zmult_zle_cancel1, zmult_zle_cancel2]);
+
+
 (** Special-case simplification for small constants **)
 
 Goal "#0 * z = (#0::int)";

--- a/src/HOL/Integ/Int.ML	Thu Aug 17 10:42:57 2000 +0200
+++ b/src/HOL/Integ/Int.ML	Thu Aug 17 11:55:47 2000 +0200
@@ -427,61 +427,51 @@
 qed "zmult_eq_int0_iff";
 
 
-Goal "int 0 < k ==> (m*k < n*k) = (m<n)";
-by (safe_tac (claset() addSIs [zmult_zless_mono1]));
-by (cut_facts_tac [linorder_less_linear] 1);
-by (blast_tac (claset() addIs [zmult_zless_mono1] addEs [order_less_asym]) 1);
+(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
+    but not (yet?) for k*m < n*k. **)
+
+Goal "(m*k < n*k) = ((int 0 < k & m<n) | (k < int 0 & n<m))";
+by (case_tac "k = int 0" 1);
+by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, 
+                              zmult_zless_mono1, zmult_zless_mono1_neg]));  
+by (auto_tac (claset(), 
+              simpset() addsimps [linorder_not_less,
+				  inst "y1" "m*k" (linorder_not_le RS sym),
+                                  inst "y1" "m" (linorder_not_le RS sym)]));
+by (ALLGOALS (etac notE));
+by (auto_tac (claset(), simpset() addsimps [zless_imp_zle, zmult_zle_mono1,
+                                            zmult_zle_mono1_neg]));  
 qed "zmult_zless_cancel2";
 
-Goal "int 0 < k ==> (k*m < k*n) = (m<n)";
-by (dtac zmult_zless_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
-qed "zmult_zless_cancel1";
-Addsimps [zmult_zless_cancel1, zmult_zless_cancel2];
 
-Goal "k < int 0 ==> (m*k < n*k) = (n<m)";
-by (safe_tac (claset() addSIs [zmult_zless_mono1_neg]));
-by (cut_facts_tac [linorder_less_linear] 1);
-by (blast_tac (claset() addIs [zmult_zless_mono1_neg] 
-                        addEs [order_less_asym]) 1);
-qed "zmult_zless_cancel2_neg";
+Goal "(k*m < k*n) = ((int 0 < k & m<n) | (k < int 0 & n<m))";
+by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
+                                  zmult_zless_cancel2]) 1);
+qed "zmult_zless_cancel1";
 
-Goal "k < int 0 ==> (k*m < k*n) = (n<m)";
-by (dtac zmult_zless_cancel2_neg 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
-qed "zmult_zless_cancel1_neg";
-Addsimps [zmult_zless_cancel1_neg, zmult_zless_cancel2_neg];
-
-Goal "int 0 < k ==> (m*k <= n*k) = (m<=n)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+Goal "(m*k <= n*k) = ((int 0 < k --> m<=n) & (k < int 0 --> n<=m))";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
+                                  zmult_zless_cancel2]) 1);
 qed "zmult_zle_cancel2";
 
-Goal "int 0 < k ==> (k*m <= k*n) = (m<=n)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+Goal "(k*m <= k*n) = ((int 0 < k --> m<=n) & (k < int 0 --> n<=m))";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
+                                  zmult_zless_cancel1]) 1);
 qed "zmult_zle_cancel1";
-Addsimps [zmult_zle_cancel1, zmult_zle_cancel2];
 
-Goal "k < int 0 ==> (m*k <= n*k) = (n<=m)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "zmult_zle_cancel2_neg";
-
-Goal "k < int 0 ==> (k*m <= k*n) = (n<=m)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "zmult_zle_cancel1_neg";
-Addsimps [zmult_zle_cancel1_neg, zmult_zle_cancel2_neg];
-
-Goal "k ~= int 0 ==> (m*k = n*k) = (m=n)";
+Goal "(m*k = n*k) = (k = int 0 | m=n)";
 by (cut_facts_tac [linorder_less_linear] 1);
 by Safe_tac;
-by (assume_tac 2);
+by Auto_tac;  
 by (REPEAT 
     (force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg)
                          addD2 ("mono_pos", zmult_zless_mono1), 
 		simpset() addsimps [linorder_neq_iff]) 1));
+
 qed "zmult_cancel2";
 
-Goal "k ~= int 0 ==> (k*m = k*n) = (m=n)";
-by (dtac zmult_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
+Goal "(k*m = k*n) = (k = int 0 | m=n)";
+by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
+                                  zmult_cancel2]) 1);
 qed "zmult_cancel1";
 Addsimps [zmult_cancel1, zmult_cancel2];

--- a/src/HOL/Integ/IntArith.ML	Thu Aug 17 10:42:57 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Thu Aug 17 11:55:47 2000 +0200
@@ -73,7 +73,8 @@
 
 Goal "(m = m*(n::int)) = (n = #1 | m = #0)";
 by Auto_tac;
-by (stac (zmult_cancel1 RS sym) 1);
+by (subgoal_tac "m*#1 = m*n" 1);
+by (dtac (zmult_cancel1 RS iffD1) 1); 
 by Auto_tac;
 qed "zmult_eq_self_iff";
 

--- a/src/HOL/Integ/IntDiv.ML	Thu Aug 17 10:42:57 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Thu Aug 17 11:55:47 2000 +0200
@@ -45,7 +45,7 @@
 by (subgoal_tac "b * q' < b * (#1 + q)" 1);
 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
 				       zadd_zmult_distrib2]) 2);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
 qed "unique_quotient_lemma";
 
 Goal "[| b*q' + r' <= b*q + r;  r <= #0;  b < #0;  b < r' |] \
@@ -492,7 +492,7 @@
   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
  by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
 by (subgoal_tac "b*q < b*(q' + #1)" 1);
- by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
 by (subgoal_tac "b*q = r' - r + b'*q'" 1);
  by (Simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
@@ -521,7 +521,7 @@
   by (arith_tac 3);
  by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
 by (subgoal_tac "b*q' < b*(q + #1)" 1);
- by (Asm_full_simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); 
 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
 by (subgoal_tac "b*q' <= b'*q'" 1);
  by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2);

--- a/src/HOL/Integ/NatBin.ML	Thu Aug 17 10:42:57 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Thu Aug 17 11:55:47 2000 +0200
@@ -305,7 +305,7 @@
 (*Non-trivial simplifications*)	 
 val other_renamed_arith_simps =
     map rename_numerals
-	[add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
+	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
 	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
 
 Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);