# HG changeset patch
# User wenzelm
# Date 1185903624 -7200
# Node ID 5d0ecd0c8f3c679336f95a129c54eb41d13808a2
# Parent  71c27b320610f3019a90ee71db2a153125e39170
tuned LinArith setup;

diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/Hyperreal/hypreal_arith.ML
--- a/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -30,14 +30,14 @@
     Simplifier.simproc (the_context ())
       "fast_hypreal_arith" 
       ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
-    (K Fast_Arith.lin_arith_simproc);
+    (K LinArith.lin_arith_simproc);
 
 val hypreal_arith_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = real_inj_thms @ inj_thms,
-    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
+    lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
     neqE = neqE,
     simpset = simpset addsimps simps}) #>
   arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/NatBin.thy	Tue Jul 31 19:40:24 2007 +0200
@@ -656,7 +656,7 @@
 val numeral_ss = simpset() addsimps numerals;
 
 val nat_bin_arith_setup =
- Fast_Arith.map_data
+ LinArith.map_data
    (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
       inj_thms = inj_thms,
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -36,11 +36,11 @@
 val ratT = Type ("Rational.rat", [])
 
 val rat_arith_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
-    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
+    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
     neqE =  neqE,
     simpset = simpset addsimps simps
                       addsimprocs simprocs}) #>
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -29,74 +29,14 @@
 in
 
 val real_arith_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
-    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
+    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
     neqE = neqE,
     simpset = simpset addsimps simps}) #>
   arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
   arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT)
 
 end;
-
-
-(* Some test data [omitting examples that assume the ordering to be discrete!]
-Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by (arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a <= l";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a <= l+l+l+l";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| 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 <= l+l+l+l+i";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "!!a::real. [| 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);
-qed "";
-
-Goal "!!a::real. [| 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);
-qed "";
-
-Goal "a<=b ==> a < b+(1::real)";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "a<=b ==> a-(3::real) < b";
-by (fast_arith_tac 1);
-qed "";
-
-Goal "a<=b ==> a-(1::real) < b";
-by (fast_arith_tac 1);
-qed "";
-
-*)
-
-
-
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/ex/Arith_Examples.thy
--- a/src/HOL/ex/Arith_Examples.thy	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy	Tue Jul 31 19:40:24 2007 +0200
@@ -19,12 +19,12 @@
   method combines them both, and tries other methods (e.g.~@{text presburger})
   as well.  This is the one that you should use in your proofs!
 
-  An @{text arith}-based simproc is available as well
-  (see @{ML Fast_Arith.lin_arith_simproc}),
-  which---for performance reasons---however
-  does even less splitting than @{ML fast_arith_tac} at the moment (namely
-  inequalities only).  (On the other hand, it does take apart conjunctions,
-  which @{ML fast_arith_tac} currently does not do.)
+  An @{text arith}-based simproc is available as well (see @{ML
+  LinArith.lin_arith_simproc}), which---for performance
+  reasons---however does even less splitting than @{ML fast_arith_tac}
+  at the moment (namely inequalities only).  (On the other hand, it
+  does take apart conjunctions, which @{ML fast_arith_tac} currently
+  does not do.)
 *}
 
 (*
@@ -122,12 +122,12 @@
   (* FIXME: need to replace 1 by its numeral representation *)
   apply (subst numeral_1_eq_1 [symmetric])
   (* FIXME: arith does not know about iszero *)
-  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
+  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
 oops
 
 lemma "(i::int) mod 42 <= 41"
   (* FIXME: arith does not know about iszero *)
-  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
+  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
 oops
 
 
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/int_arith1.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -591,7 +591,7 @@
 in
 
 val int_arith_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms,
     mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
     inj_thms = nat_inj_thms @ inj_thms,
@@ -610,6 +610,6 @@
   "fast_int_arith" 
      ["(m::'a::{ordered_idom,number_ring}) < n",
       "(m::'a::{ordered_idom,number_ring}) <= n",
-      "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
+      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
 
 Addsimprocs [fast_int_arith_simproc];
diff -r 71c27b320610 -r 5d0ecd0c8f3c src/HOL/nat_simprocs.ML
--- a/src/HOL/nat_simprocs.ML	Tue Jul 31 19:40:23 2007 +0200
+++ b/src/HOL/nat_simprocs.ML	Tue Jul 31 19:40:24 2007 +0200
@@ -564,7 +564,7 @@
 in
 
 val nat_simprocs_setup =
-  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms, lessD = lessD, neqE = neqE,
     simpset = simpset addsimps add_rules