# HG changeset patch
# User nipkow
# Date 950894968 -3600
# Node ID fe9bf28e8a584a533c4ad8cd65174959d10230bd
# Parent  6ba8fa2b063893c1e4b7931d8a0c8c752722feae
installed lin arith for nat numerals.

diff -r 6ba8fa2b0638 -r fe9bf28e8a58 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Fri Feb 18 15:37:08 2000 +0100
+++ b/src/HOL/Integ/IntArith.ML	Fri Feb 18 18:29:28 2000 +0100
@@ -113,11 +113,6 @@
 
 (*
 Instantiation of the generic linear arithmetic package for int.
-FIXME: multiplication with constants (eg #2 * i) does not work yet.
-Solution: the cancellation simprocs in Int_Cancel should be able to deal with
-it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should
-include rules for turning multiplication with constants into addition.
-(The latter option is very inefficient!)
 *)
 
 (* Update parameters of arithmetic prover *)
@@ -188,6 +183,9 @@
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
 by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> #6*a <= #5*l+i";
+by (fast_arith_tac 1);
 *)
 
 (*---------------------------------------------------------------------------*)
diff -r 6ba8fa2b0638 -r fe9bf28e8a58 src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Fri Feb 18 15:37:08 2000 +0100
+++ b/src/HOL/Integ/IntDiv.ML	Fri Feb 18 18:29:28 2000 +0100
@@ -83,10 +83,6 @@
 
 (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
 
-(*Unfold all "let"s involving constants*)
-Addsimps [read_instantiate_sg (sign_of IntDiv.thy)
-	          [("s", "number_of ?v")] Let_def];
-
 
 Goal "adjust a b (q,r) = (let diff = r-b in \
 \                         if #0 <= diff then (#2*q + #1, diff)  \
diff -r 6ba8fa2b0638 -r fe9bf28e8a58 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Fri Feb 18 15:37:08 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML	Fri Feb 18 18:29:28 2000 +0100
@@ -463,5 +463,26 @@
 	  less_number_of_Suc, less_Suc_number_of, 
 	  le_number_of_Suc, le_Suc_number_of];
 
-(* Pusch int(.) inwards: *)
+(* Push int(.) inwards: *)
 Addsimps [int_Suc,zadd_int RS sym];
+
+(*** Prepare linear arithmetic for nat numerals ***)
+
+let
+
+(* reduce contradictory <= to False *)
+val add_rules =
+  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
+   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
+   le_Suc_number_of,le_number_of_Suc,
+   less_Suc_number_of,less_number_of_Suc,
+   Suc_eq_number_of,eq_number_of_Suc,
+   eq_number_of_0, eq_0_number_of, less_0_number_of,
+   nat_number_of, Let_number_of, if_True, if_False];
+
+val simprocs = [Nat_Plus_Assoc.conv,Nat_Times_Assoc.conv];
+
+in
+LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
+                      addsimprocs simprocs
+end;