# HG changeset patch
# User paulson
# Date 931855453 -7200
# Node ID cac1e4e9c821780bb93d7006bcc0a54afc1aa2f6
# Parent  dd3e8bd86cc63b52d2cea1fc5e355157a8473a07
new monotonicity theorems

diff -r dd3e8bd86cc6 -r cac1e4e9c821 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Tue Jul 13 10:43:31 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Tue Jul 13 10:44:13 1999 +0200
@@ -292,15 +292,12 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
 qed "zmult_zle_mono2_neg";
 
-(*<=monotonicity, BOTH arguments*)
+(* <= monotonicity, BOTH arguments*)
 Goal "[| i <= j;  k <= l;  int 0 <= j;  int 0 <= k |] ==> i*k <= j*l";
 by (etac (zmult_zle_mono1 RS order_trans) 1);
 by (assume_tac 1);
-by (rtac order_trans 1);
-by (stac zmult_commute 2);
-by (etac zmult_zle_mono1 2);
-by (assume_tac 2);
-by (simp_tac (simpset() addsimps [zmult_commute]) 1);
+by (etac zmult_zle_mono2 1);
+by (assume_tac 1);
 qed "zmult_zle_mono";
 
 
@@ -329,6 +326,14 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
 qed "zmult_zless_mono1";
 
+(* < monotonicity, BOTH arguments*)
+Goal "[| i < j;  k < l;  int 0 < j;  int 0 < k |] ==> i*k < j*l";
+by (etac (zmult_zless_mono1 RS order_less_trans) 1);
+by (assume_tac 1);
+by (etac zmult_zless_mono2 1);
+by (assume_tac 1);
+qed "zmult_zless_mono";
+
 Goal "[| i<j;  k < int 0 |] ==> j*k < i*k";
 by (rtac (zminus_zless_zminus RS iffD1) 1);
 by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym,
@@ -350,7 +355,7 @@
 by (REPEAT 
     (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], 
 		simpset()) 1));
-qed "zmult_eq_iff";
+qed "zmult_eq_int0_iff";
 
 
 Goal "int 0 < k ==> (m*k < n*k) = (m<n)";