better rules for cancellation of common factors across comparisons

--- a/src/ZF/ArithSimp.ML	Fri Aug 18 12:31:20 2000 +0200
+++ b/src/ZF/ArithSimp.ML	Fri Aug 18 12:34:13 2000 +0200
@@ -353,6 +353,64 @@
 qed "mult_eq_1_iff";
 AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
 
+
+(** Cancellation laws for common factors in comparisons **)
+
+Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k < n#*k) <-> (0<k & m<n)";
+by (safe_tac (claset() addSIs [mult_lt_mono1]));
+by (etac natE 1);
+by Auto_tac;  
+by (rtac (not_le_iff_lt RS iffD1) 1); 
+by (dtac (not_le_iff_lt RSN (2,rev_iffD2)) 3); 
+by (blast_tac (claset() addIs [mult_le_mono1]) 5); 
+by Auto_tac;  
+val lemma = result();
+
+Goal "(m#*k < n#*k) <-> (0 < natify(k) & natify(m) < natify(n))";
+by (rtac iff_trans 1);
+by (rtac lemma 2);
+by Auto_tac;  
+qed "mult_less_cancel2";
+
+Goal "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))";
+by (simp_tac (simpset() addsimps [mult_less_cancel2, 
+                                  inst "m" "k" mult_commute]) 1);
+qed "mult_less_cancel1";
+Addsimps [mult_less_cancel1, mult_less_cancel2];
+
+Goal "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))";
+by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1);
+by Auto_tac;  
+qed "mult_le_cancel2";
+
+Goal "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))";
+by (asm_simp_tac (simpset() addsimps [not_lt_iff_le RS iff_sym]) 1);
+by Auto_tac;  
+qed "mult_le_cancel1";
+Addsimps [mult_le_cancel1, mult_le_cancel2];
+
+Goal "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)";
+by (blast_tac (claset() addIs [le_anti_sym]) 1); 
+qed "Ord_eq_iff_le";
+
+Goal "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)";
+by (asm_simp_tac (simpset() addsimps [inst "m" "m#*k" Ord_eq_iff_le,
+                                      inst "m" "m" Ord_eq_iff_le]) 1); 
+by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff]));  
+val lemma = result();
+
+Goal "(m#*k = n#*k) <-> (natify(m) = natify(n) | natify(k) = 0)";
+by (rtac iff_trans 1);
+by (rtac lemma 2);
+by Auto_tac;  
+qed "mult_cancel2";
+
+Goal "(k#*m = k#*n) <-> (natify(m) = natify(n) | natify(k) = 0)";
+by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
+qed "mult_cancel1";
+Addsimps [mult_cancel1, mult_cancel2];
+
+
 (*Cancellation law for division*)
 Goal "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
 by (eres_inst_tac [("i","m")] complete_induct 1);

--- a/src/ZF/Integ/IntDiv.ML	Fri Aug 18 12:31:20 2000 +0200
+++ b/src/ZF/Integ/IntDiv.ML	Fri Aug 18 12:34:13 2000 +0200
@@ -69,22 +69,12 @@
 by Auto_tac;  
 qed "zadd_succ_zle_iff";
 
-(** USED??
-Goal "w $< $# succ(m) <-> w $< $# m | intify(w) = $# m";
-by (cut_inst_tac [("z","#0")] zless_add_succ_iff 1);
-by Auto_tac;  
-qed "zless_succ_iff";
-
-Goal "(w $<= $# succ(m)) <-> (w $<= $#m | intify(w) = $# succ(m))";
-by (simp_tac (simpset_of Int.thy addsimps [zless_succ_iff, zle_def]) 1);
-qed "zle_succ_iff";
-**)
-
 (** Inequality reasoning **)
 
 Goal "(w $< z $+ #1) <-> (w$<=z)";
 by (subgoal_tac "#1 = $# 1" 1);
-by (asm_simp_tac (simpset_of Int.thy addsimps [zless_add_succ_iff, zle_def]) 1);
+by (asm_simp_tac (simpset_of Int.thy 
+                  addsimps [zless_add_succ_iff, zle_def]) 1);
 by Auto_tac;  
 qed "zless_add1_iff_zle";
 
@@ -260,89 +250,67 @@
 qed "zmult_eq_0_iff";
 
 
-Goal "[| m: int; n: int |] ==> #0 $< k ==> (m$*k $< n$*k) <-> (m$<n)";
-by (safe_tac (claset() addSIs [zmult_zless_mono1]));
-by (cut_facts_tac  [zless_linear] 1);
-by Auto_tac;  
-by (blast_tac (claset() addIs [zmult_zless_mono1] addEs [zless_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 "[| k: int; m: int; n: int |] \
+\     ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))";
+by (case_tac "k = #0" 1);
+by (auto_tac (claset(), simpset() addsimps [neq_iff_zless, 
+                              zmult_zless_mono1, zmult_zless_mono1_neg]));  
+by (auto_tac (claset(), 
+      simpset() addsimps [not_zless_iff_zle,
+			  inst "w1" "m$*k" (not_zle_iff_zless RS iff_sym),
+			  inst "w1" "m" (not_zle_iff_zless RS iff_sym)]));
+by (ALLGOALS (etac notE));
+by (auto_tac (claset(), simpset() addsimps [zless_imp_zle, zmult_zle_mono1,
+                                            zmult_zle_mono1_neg]));  
 val lemma = result();
 
-Goal "#0 $< k ==> (m$*k $< n$*k) <-> (m$<n)";
-by (cut_inst_tac [("m","intify(m)"),("n","intify(n)")] lemma 1);
+Goal "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))";
+by (cut_inst_tac [("k","intify(k)"),("m","intify(m)"),("n","intify(n)")]
+                 lemma 1);
 by Auto_tac;  
 qed "zmult_zless_cancel2";
 
-Goal "#0 $< k ==> (k$*m $< k$*n) <-> (m$<n)";
-by (dtac zmult_zless_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
+Goal "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))";
+by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
+                                  zmult_zless_cancel2]) 1);
 qed "zmult_zless_cancel1";
-Addsimps [zmult_zless_cancel1, zmult_zless_cancel2];
-
-Goal "[| m: int; n: int |] ==> k $< #0 ==> (m$*k $< n$*k) <-> (n$<m)";
-by (safe_tac (claset() addSIs [zmult_zless_mono1_neg]));
-by (cut_facts_tac [zless_linear] 1);
-by Auto_tac;  
-by (blast_tac (claset() addIs [zmult_zless_mono1_neg] 
-                        addEs [zless_asym]) 1);
-val lemma = result();
 
-Goal "k $< #0 ==> (m$*k $< n$*k) <-> (n$<m)";
-by (cut_inst_tac [("m","intify(m)"),("n","intify(n)")] lemma 1);
+Goal "(m$*k $<= n$*k) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
+                                  zmult_zless_cancel2]) 1);
 by Auto_tac;  
-qed "zmult_zless_cancel2_neg";
-
-Goal "k $< #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 "#0 $< k ==> (m$*k $<= n$*k) <-> (m$<=n)";
-by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
 qed "zmult_zle_cancel2";
 
-Goal "#0 $< k ==> (k$*m $<= k$*n) <-> (m$<=n)";
-by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+Goal "(k$*m $<= k$*n) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
+                                  zmult_zless_cancel1]) 1);
+by Auto_tac;  
 qed "zmult_zle_cancel1";
-Addsimps [zmult_zle_cancel1, zmult_zle_cancel2];
 
-Goal "k $< #0 ==> (m$*k $<= n$*k) <-> (n$<=m)";
-by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-qed "zmult_zle_cancel2_neg";
+Goal "[| m: int; n: int |] ==> m=n <-> (m $<= n & n $<= m)";
+by (blast_tac (claset() addIs [zle_refl,zle_anti_sym]) 1); 
+qed "int_eq_iff_zle";
 
-Goal "k $< #0 ==> (k$*m $<= k$*n) <-> (n$<=m)";
-by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-qed "zmult_zle_cancel1_neg";
-Addsimps [zmult_zle_cancel1_neg, zmult_zle_cancel2_neg];
+Goal "[| k: int; m: int; n: int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)";
+by (asm_simp_tac (simpset() addsimps [inst "m" "m$*k" int_eq_iff_zle,
+                                      inst "m" "m" int_eq_iff_zle]) 1); 
+by (auto_tac (claset(), 
+              simpset() addsimps [zmult_zle_cancel2, neq_iff_zless]));  
+val lemma = result();
 
-Goal "[| k ~= #0; k: int; m: int; n: int |] ==> (m$*k = n$*k) <-> (m=n)";
-by (rotate_tac 1 1); 
-by (cut_inst_tac [("z","m"),("w","n")] zless_linear 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps []) 2);
-by (REPEAT 
-    (force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg)
-                         addD2 ("mono_pos", zmult_zless_mono1), 
-		simpset() addsimps [neq_iff_zless]) 1));
+Goal "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))";
+by (rtac iff_trans 1);
+by (rtac lemma 2);
+by Auto_tac;  
 qed "zmult_cancel2";
 
-Goal "intify(k) ~= #0 ==> (m$*k = n$*k) <-> (intify(m) = intify(n))";
-by (rtac iff_trans 1);
-by (rtac zmult_cancel2 2);
-by Auto_tac;  
-qed "zmult_cancel2_intify";
-
-Goal "[| k ~= #0; k: int; m: int; n: int |] ==> (k$*m = k$*n) <-> (m=n)";
-by (dtac zmult_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 4);
-by Auto_tac;  
+Goal "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))";
+by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, 
+                                  zmult_cancel2]) 1);
 qed "zmult_cancel1";
-
-Goal "intify(k) ~= #0 ==> (k$*m = k$*n) <-> (intify(m) = intify(n))";
-by (rtac iff_trans 1);
-by (rtac zmult_cancel1 2);
-by Auto_tac;  
-qed "zmult_cancel1_intify";
 Addsimps [zmult_cancel1, zmult_cancel2];
 
 
@@ -352,18 +320,22 @@
 Goal "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |] \
 \     ==> q' $<= q";
 by (subgoal_tac "r' $+ b $* (q'$-q) $<= r" 1);
-by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
+by (full_simp_tac 
+    (simpset() addsimps [zdiff_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
 by (subgoal_tac "#0 $< b $* (#1 $+ q $- q')" 1);
 by (etac zle_zless_trans 2);
-by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
-				       zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
+by (full_simp_tac 
+    (simpset() addsimps [zdiff_zmult_distrib2,
+			 zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
 by (etac zle_zless_trans 2);
 by (Asm_simp_tac 2);
 by (subgoal_tac "b $* q' $< b $* (#1 $+ q)" 1);
-by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2,
-				       zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
-by (asm_full_simp_tac (simpset() addsimps [zless_add1_iff_zle]@
-                                          zadd_ac@zcompare_rls) 1);
+by (full_simp_tac
+    (simpset() addsimps [zdiff_zmult_distrib2,
+			 zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2);
+by (auto_tac (claset() addEs [zless_asym], 
+              simpset() addsimps [zmult_zless_cancel1, zless_add1_iff_zle]@
+                                 zadd_ac@zcompare_rls));
 qed "unique_quotient_lemma";
 
 Goal "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |] \
@@ -391,7 +363,6 @@
 				sym]) 1));
 qed "unique_quotient";
 
-
 Goal "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b: int; b ~= #0; \
 \        q: int; q' : int; \
 \        r: int; r' : int |] ==> r = r'";

--- a/src/ZF/Integ/int_arith.ML	Fri Aug 18 12:31:20 2000 +0200
+++ b/src/ZF/Integ/int_arith.ML	Fri Aug 18 12:34:13 2000 +0200
@@ -168,7 +168,7 @@
                zmult_minus1, zmult_minus1_right];
 
 val tc_rules = [integ_of_type, intify_in_int, 
-                zadd_type, zdiff_type, zmult_type] @ bin.intrs;
+                int_of_type, zadd_type, zdiff_type, zmult_type] @ bin.intrs;
 val intifys = [intify_ident, zadd_intify1, zadd_intify2,
                zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
                zless_intify1, zless_intify2, zle_intify1, zle_intify2];
@@ -204,7 +204,8 @@
                                     bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
   val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
 			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
+  val numeral_simp_tac	= 
+         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   end;
 
@@ -213,7 +214,7 @@
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
-  val dest_bal = FOLogic.dest_bin "op =" iT
+  val dest_bal = FOLogic.dest_eq
   val bal_add1 = eq_add_iff1 RS iff_trans
   val bal_add2 = eq_add_iff2 RS iff_trans
 );
@@ -274,7 +275,8 @@
                                     bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
   val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
 			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps))
+  val numeral_simp_tac	= 
+         ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   end;
 
@@ -291,13 +293,16 @@
 
 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   the "sum" of #3, x, #4; the literals are then multiplied*)
+
+
 structure CombineNumeralsProdData =
   struct
   val add		= op * : int*int -> int
   val mk_sum    	= mk_prod
   val dest_sum		= dest_prod
-  fun mk_coeff (k, t) = mk_numeral k
-  val dest_coeff	= dest_coeff 1
+  fun mk_coeff(k,t) = if t=one then mk_numeral k 
+                      else raise TERM("mk_coeff", [])
+  fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   val left_distrib	= zmult_assoc RS sym RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   val trans_tac         = ArithData.gen_trans_tac trans
@@ -306,7 +311,8 @@
                                     bin_simps@zmult_ac@tc_rules@intifys
   val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
 			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
-  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps bin_simps))
+  val numeral_simp_tac	= 
+         ALLGOALS (simp_tac (ZF_ss addsimps bin_simps@tc_rules@intifys))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
   end;
 
@@ -387,5 +393,9 @@
 test "(i $+ j $+ #-12 $+ k) $- #15 = y";
 test "(i $+ j $+ #12 $+ k) $- #-15 = y";
 test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
+
+(*Multiplying separated numerals*)
+Goal "#6 $* ($# x $* #2) =  uu";
+Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
 *)