more integer theorems, better simplification

--- a/src/HOL/Integ/Bin.ML	Wed Sep 13 18:46:45 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed Sep 13 18:47:30 2000 +0200
@@ -329,7 +329,18 @@
 by Auto_tac;
 qed "int_eq_0_conv'";
 
-Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
+Goal "(#0 < int k) = (0<k)";
+by (Simp_tac 1);
+qed "zero_less_int_conv";
+
+Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv',
+          zero_less_int_conv];
+
+Goal "(0 < nat z) = (#0 < z)";
+by (cut_inst_tac [("w","#0")] zless_nat_conj 1);
+by Auto_tac;  
+qed "zero_less_nat_eq";
+Addsimps [zero_less_nat_eq];
 
 
 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)

--- a/src/HOL/Integ/Int.ML	Wed Sep 13 18:46:45 2000 +0200
+++ b/src/HOL/Integ/Int.ML	Wed Sep 13 18:47:30 2000 +0200
@@ -255,6 +255,11 @@
 by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
 qed "not_neg_eq_ge_int0"; 
 
+Goal "abs (int m) = int m";
+by (simp_tac (simpset() addsimps [zabs_def]) 1); 
+qed "abs_int_eq";
+Addsimps [abs_int_eq];
+
 
 (**** nat: magnitide of an integer, as a natural number ****)
 

--- a/src/HOL/Integ/IntDiv.ML	Wed Sep 13 18:46:45 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML	Wed Sep 13 18:47:30 2000 +0200
@@ -297,7 +297,7 @@
 (*There is no mod_neg_pos_trivial...*)
 
 
-(*Simpler laws such as -a div b = -(a div b) FAIL*)
+(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
 Goal "(-a) div (-b) = a div (b::int)";
 by (zdiv_undefined_case_tac "b = #0" 1);
 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
@@ -306,7 +306,7 @@
 qed "zdiv_zminus_zminus";
 Addsimps [zdiv_zminus_zminus];
 
-(*Simpler laws such as -a mod b = -(a mod b) FAIL*)
+(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
 Goal "(-a) mod (-b) = - (a mod (b::int))";
 by (zdiv_undefined_case_tac "b = #0" 1);
 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) 
@@ -316,6 +316,50 @@
 Addsimps [zmod_zminus_zminus];
 
 
+(*** div, mod and unary minus ***)
+
+Goal "quorem((a,b),(q,r)) \
+\     ==> quorem ((-a,b), (if r=#0 then -q else -q-#1), \
+\                         (if r=#0 then #0 else b-r))";
+by (auto_tac
+    (claset(),
+     simpset() addsimps split_ifs@
+                        [quorem_def, linorder_neq_iff, 
+			 zdiff_zmult_distrib2]));
+val lemma = result();
+
+Goal "b ~= (#0::int) \
+\     \\<Longrightarrow> (-a) div b = \
+\         (if a mod b = #0 then - (a div b) else  - (a div b) - #1)";
+by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
+qed "zdiv_zminus1_eq_if";
+
+Goal "(-a::int) mod b = (if a mod b = #0 then #0 else  b - (a mod b))";
+by (zdiv_undefined_case_tac "b = #0" 1);
+by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
+qed "zmod_zminus1_eq_if";
+
+Goal "a div (-b) = (-a::int) div b";
+by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1);
+by Auto_tac;  
+qed "zdiv_zminus2";
+
+Goal "a mod (-b) = - ((-a::int) mod b)";
+by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1);
+by Auto_tac;  
+qed "zmod_zminus2";
+
+Goal "b ~= (#0::int) \
+\     \\<Longrightarrow> a div (-b) = \
+\         (if a mod b = #0 then - (a div b) else  - (a div b) - #1)";
+by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); 
+qed "zdiv_zminus2_eq_if";
+
+Goal "a mod (-b::int) = (if a mod b = #0 then #0 else  (a mod b) - b)";
+by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); 
+qed "zmod_zminus2_eq_if";
+
+
 (*** division of a number by itself ***)
 
 Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q";

--- a/src/HOL/Integ/NatBin.ML	Wed Sep 13 18:46:45 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Wed Sep 13 18:47:30 2000 +0200
@@ -132,6 +132,12 @@
 				      int_0_le_mult_iff]) 1);
 qed "nat_mult_distrib";
 
+Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
+by (rtac trans 1); 
+by (rtac nat_mult_distrib 2); 
+by Auto_tac;  
+qed "nat_mult_distrib_neg";
+
 Goal "(number_of v :: nat) * number_of v' = \
 \      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
 by (simp_tac
@@ -154,14 +160,15 @@
 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
 by (rename_tac "m m'" 1);
 by (subgoal_tac "#0 <= int m div int m'" 1);
- by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
-				       pos_imp_zdiv_nonneg_iff]) 2);
+ by (asm_full_simp_tac 
+     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
 by (rtac (inj_int RS injD) 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
  by (Force_tac 2);
-by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
-				      numeral_0_eq_0, zadd_int, zmult_int]) 1);
+by (asm_full_simp_tac 
+    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
+	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
 by (rtac (mod_div_equality RS sym RS trans) 1);
 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
 qed "nat_div_distrib";
@@ -186,14 +193,15 @@
 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
 by (rename_tac "m m'" 1);
 by (subgoal_tac "#0 <= int m mod int m'" 1);
- by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
-				       pos_mod_sign]) 2);
+ by (asm_full_simp_tac 
+     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
 by (rtac (inj_int RS injD) 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
  by (Force_tac 2);
-by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
-				      numeral_0_eq_0, zadd_int, zmult_int]) 1);
+by (asm_full_simp_tac 
+     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
+		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
 by (rtac (mod_div_equality RS sym RS trans) 1);
 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
 qed "nat_mod_distrib";
@@ -517,3 +525,14 @@
 Goal "(number_of Pls ::int) ~= number_of Min"; 
 by Auto_tac;
 qed "eq_number_of_Pls_Min"; 
+
+
+(*** Further lemmas about "nat" ***)
+
+Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
+by (case_tac "z=#0 | w=#0" 1);
+by Auto_tac;  
+by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
+                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
+by (arith_tac 1);
+qed "nat_abs_mult_distrib";

--- a/src/HOL/Integ/int_arith2.ML	Wed Sep 13 18:46:45 2000 +0200
+++ b/src/HOL/Integ/int_arith2.ML	Wed Sep 13 18:47:30 2000 +0200
@@ -41,11 +41,11 @@
 by (rtac (major RS nat_0_le RS sym RS minor) 1);
 qed "nonneg_eq_int"; 
 
-Goal "#0 <= w ==> (nat w = m) = (w = int m)";
+Goal "(nat w = m) = (if #0 <= w then w = int m else m=0)";
 by Auto_tac;
 qed "nat_eq_iff";
 
-Goal "#0 <= w ==> (m = nat w) = (w = int m)";
+Goal "(m = nat w) = (if #0 <= w then w = int m else m=0)";
 by Auto_tac;
 qed "nat_eq_iff2";
 
@@ -57,6 +57,12 @@
 by (Simp_tac 1);
 qed "nat_less_iff";
 
+Goal "(int m = z) = (m = nat z & #0 \\<le> z)";
+by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));  
+qed "int_eq_iff";
+
+Addsimps [inst "z" "number_of ?v" int_eq_iff];
+
 
 (*Users don't want to see (int 0), int(Suc 0) or w + - z*)
 Addsimps [int_0, int_Suc, symmetric zdiff_def];
@@ -104,4 +110,9 @@
 by(Simp_tac 1);
 qed "zabs_split";
 
+Goal "#0 <= abs (z::int)";
+by (simp_tac (simpset() addsimps [zabs_def]) 1); 
+qed "zero_le_zabs";
+AddIffs [zero_le_zabs];
+
 (*continued in IntArith.ML ...*)