--- 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) #>
--- 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,
--- 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}) #>
--- 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 "";
-
-*)
-
-
-
--- 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
--- 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];
--- 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