Defined abs on int.

--- a/src/HOL/Integ/Bin.ML	Fri Jun 30 21:21:11 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Sat Jul 01 17:52:52 2000 +0200
@@ -397,6 +397,15 @@
 by (rtac (linorder_not_less RS sym) 1);
 qed "le_number_of_eq_not_less"; 
 
+(** Absolute value (abs) **)
+
+Goalw [zabs_def]
+ "abs(number_of x::int) = \
+\ (if number_of x < (0::int) then -number_of x else number_of x)";
+by(rtac refl 1);
+qed "abs_number_of";
+
+
 (*Delete the original rewrites, with their clumsy conditional expressions*)
 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
           NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
@@ -418,7 +427,7 @@
      bin_minus_1, bin_minus_0,  
      bin_add_Pls_right, bin_add_Min_right,
      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
-     diff_number_of_eq, 
+     diff_number_of_eq, abs_number_of,
      bin_mult_1, bin_mult_0] @ NCons_simps);
 
 (*For making a minimal simpset, one must include these default simprules

--- a/src/HOL/Integ/Int.thy	Fri Jun 30 21:21:11 2000 +0200
+++ b/src/HOL/Integ/Int.thy	Sat Jul 01 17:52:52 2000 +0200
@@ -16,4 +16,7 @@
   nat  :: int => nat
   "nat(Z) == if neg Z then 0 else (@ m. Z = int m)"
 
+defs
+  zabs_def  "abs(i::int) == if i < 0 then -i else i"
+
 end

--- a/src/HOL/Integ/IntArith.ML	Fri Jun 30 21:21:11 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Sat Jul 01 17:52:52 2000 +0200
@@ -558,6 +558,19 @@
 qed_spec_mp "zdiff_int";
 
 
+(*** abs: absolute value, as an integer ****)
+
+Goalw [zabs_def] "abs(abs(x::int)) = abs(x)";
+by(Simp_tac 1);
+qed "abs_abs";
+Addsimps [abs_abs];
+
+Goalw [zabs_def] "abs(-(x::int)) = abs(x)";
+by(Simp_tac 1);
+qed "abs_minus";
+Addsimps [abs_minus];
+
+
 (*** Some convenient biconditionals for products of signs ***)
 
 Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";

--- a/src/HOL/Integ/IntArith.thy	Fri Jun 30 21:21:11 2000 +0200
+++ b/src/HOL/Integ/IntArith.thy	Sat Jul 01 17:52:52 2000 +0200
@@ -1,3 +1,2 @@
-
 theory IntArith = Bin:
 end