# HG changeset patch
# User paulson
# Date 960997501 -7200
# Node ID 0d76289660691949b076697b4e36ec5f748e1c11
# Parent  7b34ffecaaa80504c67b01f6be8f392f14366039
new lemmas for signs of products

diff -r 7b34ffecaaa8 -r 0d7628966069 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Wed Jun 14 17:44:43 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Wed Jun 14 17:45:01 2000 +0200
@@ -31,14 +31,6 @@
 
 (** For cancel_numerals **)
 
-Goal "!!i::int. ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
-qed "diff_add_eq1";
-
-Goal "!!i::int. ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
-qed "diff_add_eq2";
-
 val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
 			   zle_iff_zdiff_zle_0] @
@@ -171,8 +163,7 @@
 val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
 
 (*To perform binary arithmetic*)
-val bin_simps = [number_of_add RS sym, add_number_of_left] @ 
-                bin_arith_simps @ bin_rel_simps;
+val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
 
 (*To evaluate binary negations of coefficients*)
 val zminus_simps = NCons_simps @
@@ -478,33 +469,11 @@
 
 (** Simplification of inequalities involving numerical constants **)
 
-Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
-by (arith_tac 1);
-qed "zle_add1_eq";
-
 Goal "(w <= z - (#1::int)) = (w<(z::int))";
 by (arith_tac 1);
 qed "zle_diff1_eq";
 Addsimps [zle_diff1_eq];
 
-(*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
-by (fast_arith_tac 1);
-qed "zle_imp_zle_zadd";
-
-Goal "w <= z ==> w <= z + (#1::int)";
-by (fast_arith_tac 1);
-qed "zle_imp_zle_zadd1";
-
-(*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
-by (fast_arith_tac 1);
-qed "zless_imp_zless_zadd";
-
-Goal "w < z ==> w < z + (#1::int)";
-by (fast_arith_tac 1);
-qed "zless_imp_zless_zadd1";
-
 Goal "(w < z + #1) = (w<=(z::int))";
 by (arith_tac 1);
 qed "zle_add1_eq_le";
@@ -515,20 +484,6 @@
 qed "zadd_left_cancel0";
 Addsimps [zadd_left_cancel0];
 
-(*LOOPS as a simprule!*)
-Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
-by (fast_arith_tac 1);
-qed "zless_zadd_imp_zless";
-
-(*LOOPS as a simprule!  Analogous to Suc_lessD*)
-Goal "w + #1 < z ==> w < (z::int)";
-by (fast_arith_tac 1);
-qed "zless_zadd1_imp_zless";
-
-Goal "w + #-1 = w - (#1::int)";
-by (Simp_tac 1);
-qed "zplus_minus1_conv";
-
 
 (* nat *)
 
@@ -602,62 +557,53 @@
 qed_spec_mp "zdiff_int";
 
 
-(** Products of signs **)
+(*** Some convenient biconditionals for products of signs ***)
 
-Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
-by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1_neg], 
-	       simpset()addsimps [order_le_less, zmult_commute]) 1);
-qed "neg_imp_zmult_pos_iff";
+Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac; 
+qed "zmult_pos";
 
-Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
-by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
-	       simpset() addsimps [order_le_less]) 1);
-qed "neg_imp_zmult_neg_iff";
+Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac; 
+qed "zmult_neg";
 
-Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
-by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [zmult_zless_mono1], 
-	       simpset() addsimps [order_le_less]) 1);
-qed "pos_imp_zmult_neg_iff";
+Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac; 
+qed "zmult_pos_neg";
 
-Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
-by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1], 
-	       simpset() addsimps [order_le_less, zmult_commute]) 1);
-qed "pos_imp_zmult_pos_iff";
-
-(** <= versions of the theorems above **)
+Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)";
+by (auto_tac (claset(), 
+              simpset() addsimps [order_le_less, linorder_not_less,
+	                          zmult_pos, zmult_neg]));
+by (ALLGOALS (rtac ccontr)); 
+by (auto_tac (claset(), 
+	      simpset() addsimps [order_le_less, linorder_not_less]));
+by (ALLGOALS (etac rev_mp)); 
+by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
+by (auto_tac (claset() addDs [order_less_not_sym], 
+              simpset() addsimps [zmult_commute]));  
+qed "int_0_less_mult_iff";
 
-Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
-				      neg_imp_zmult_pos_iff]) 1);
-qed "neg_imp_zmult_nonpos_iff";
-
-Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
-				      neg_imp_zmult_neg_iff]) 1);
-qed "neg_imp_zmult_nonneg_iff";
+Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)";
+by (auto_tac (claset(), 
+              simpset() addsimps [order_le_less, linorder_not_less,  
+                                  int_0_less_mult_iff]));
+qed "int_0_le_mult_iff";
 
-Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
-				      pos_imp_zmult_pos_iff]) 1);
-qed "pos_imp_zmult_nonpos_iff";
+Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
+by (auto_tac (claset(), 
+              simpset() addsimps [int_0_le_mult_iff, 
+                                  linorder_not_le RS sym]));
+by (auto_tac (claset() addDs [order_less_not_sym],  
+              simpset() addsimps [linorder_not_le]));
+qed "zmult_less_0_iff";
 
-Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
-				      pos_imp_zmult_neg_iff]) 1);
-qed "pos_imp_zmult_nonneg_iff";
+Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)";
+by (auto_tac (claset() addDs [order_less_not_sym], 
+              simpset() addsimps [int_0_less_mult_iff, 
+                                  linorder_not_less RS sym]));
+qed "zmult_le_0_iff";
+
diff -r 7b34ffecaaa8 -r 0d7628966069 src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Wed Jun 14 17:44:43 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Wed Jun 14 17:45:01 2000 +0200
@@ -115,9 +115,7 @@
 Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
 by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
 by Auto_tac;
-by (ALLGOALS 
-    (asm_full_simp_tac (simpset() addsimps [quorem_def,
-					    pos_imp_zmult_pos_iff])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
 (*base case: a<b*)
 by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
 (*main argument*)
@@ -156,9 +154,7 @@
 Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
 by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
 by Auto_tac;
-by (ALLGOALS 
-    (asm_full_simp_tac (simpset() addsimps [quorem_def,
-					    pos_imp_zmult_pos_iff])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
 (*base case: 0<=a+b*)
 by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
 (*main argument*)
@@ -325,13 +321,13 @@
 Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q";
 by (subgoal_tac "#0 < a*q" 1);
 by (arith_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
 val lemma1 = result();
 
 Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1";
 by (subgoal_tac "#0 <= a*(#1-q)" 1);
 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
-by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_nonneg_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
 val lemma2 = result();
 
 Goal "[| quorem((a,a),(q,r));  a ~= (#0::int) |] ==> q = #1";
@@ -494,7 +490,7 @@
 by (subgoal_tac "#0 <= q'" 1);
  by (subgoal_tac "#0 < b'*(q' + #1)" 2);
   by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
- by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 2);
+ 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 (subgoal_tac "b*q = r' - r + b'*q'" 1);
@@ -523,7 +519,7 @@
 by (subgoal_tac "q' < #0" 1);
  by (subgoal_tac "b'*q' < #0" 2);
   by (arith_tac 3);
- by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_neg_iff]) 2);
+ 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_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
@@ -683,15 +679,13 @@
 Goal "[| (#0::int) < c;   b < r;  r <= #0 |] ==> b * (q mod c) + r <= #0";
 by (subgoal_tac "b * (q mod c) <= #0" 1);
 by (arith_tac 1);
-by (asm_simp_tac (simpset() addsimps [neg_imp_zmult_nonpos_iff, 
-				      pos_mod_sign]) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
 val lemma2 = result();
 
 Goal "[| (#0::int) < c;  #0 <= r;  r < b |] ==> #0 <= b * (q mod c) + r";
 by (subgoal_tac "#0 <= b * (q mod c)" 1);
 by (arith_tac 1);
-by (asm_simp_tac
-    (simpset() addsimps [pos_imp_zmult_nonneg_iff, pos_mod_sign]) 1);
+by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
 val lemma3 = result();
 
 Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
@@ -712,8 +706,7 @@
     (claset(),
      simpset() addsimps zmult_ac@
                         [zmod_zdiv_equality, quorem_def, linorder_neq_iff,
-			 pos_imp_zmult_pos_iff,
-			 neg_imp_zmult_pos_iff,
+			 int_0_less_mult_iff,
 			 zadd_zmult_distrib2 RS sym,
 			 lemma1, lemma2, lemma3, lemma4]));
 val lemma = result();
@@ -816,12 +809,12 @@
 by (subgoal_tac "#0 <= b mod a" 1);
  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
 by (arith_tac 1);
-qed "pos_zdiv_times_2";
+qed "pos_zdiv_mult_2";
 
 
 Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a";
 by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1);
-by (rtac pos_zdiv_times_2 2);
+by (rtac pos_zdiv_mult_2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zmult_zminus_right]));
 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
@@ -829,7 +822,7 @@
 by (asm_full_simp_tac (HOL_ss
 		       addsimps [zdiv_zminus_zminus, zdiff_def,
 				 zminus_zadd_distrib RS sym]) 1);
-qed "neg_zdiv_times_2";
+qed "neg_zdiv_mult_2";
 
 
 (*Not clear why this must be proved separately; probably number_of causes
@@ -847,7 +840,7 @@
 by (asm_simp_tac (simpset()
                   delsimps bin_arith_extra_simps@bin_rel_simps
 		  addsimps [zdiv_zmult_zmult1,
-			    pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
+			    pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
 qed "zdiv_number_of_BIT";
 
 Addsimps [zdiv_number_of_BIT];
@@ -878,13 +871,13 @@
 by (subgoal_tac "#0 <= b mod a" 1);
  by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
 by (arith_tac 1);
-qed "pos_zmod_times_2";
+qed "pos_zmod_mult_2";
 
 
 Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1";
 by (subgoal_tac 
     "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1);
-by (rtac pos_zmod_times_2 2);
+by (rtac pos_zmod_mult_2 2);
 by (auto_tac (claset(),
 	      simpset() addsimps [zmult_zminus_right]));
 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
@@ -894,7 +887,7 @@
 				 zminus_zadd_distrib RS sym]) 1);
 by (dtac (zminus_equation RS iffD1 RS sym) 1);
 by Auto_tac;
-qed "neg_zmod_times_2";
+qed "neg_zmod_mult_2";
 
 Goal "number_of (v BIT b) mod number_of (w BIT False) = \
 \         (if b then \
@@ -907,7 +900,7 @@
 by (asm_simp_tac (simpset()
 		  delsimps bin_arith_extra_simps@bin_rel_simps
 		  addsimps [zmod_zmult_zmult1,
-			    pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);
+			    pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
 qed "zmod_number_of_BIT";
 
 Addsimps [zmod_number_of_BIT];