tuned LinArith setup;
authorwenzelm
Tue Jul 31 19:40:24 2007 +0200 (2007-07-31)
changeset 240935d0ecd0c8f3c
parent 24092 71c27b320610
child 24094 6db35c14146d
tuned LinArith setup;
src/HOL/Hyperreal/hypreal_arith.ML
src/HOL/NatBin.thy
src/HOL/Real/rat_arith.ML
src/HOL/Real/real_arith.ML
src/HOL/ex/Arith_Examples.thy
src/HOL/int_arith1.ML
src/HOL/nat_simprocs.ML
     1.1 --- a/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:23 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 19:40:24 2007 +0200
     1.3 @@ -30,14 +30,14 @@
     1.4      Simplifier.simproc (the_context ())
     1.5        "fast_hypreal_arith" 
     1.6        ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     1.7 -    (K Fast_Arith.lin_arith_simproc);
     1.8 +    (K LinArith.lin_arith_simproc);
     1.9  
    1.10  val hypreal_arith_setup =
    1.11 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.12 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    1.13     {add_mono_thms = add_mono_thms,
    1.14      mult_mono_thms = mult_mono_thms,
    1.15      inj_thms = real_inj_thms @ inj_thms,
    1.16 -    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
    1.17 +    lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    1.18      neqE = neqE,
    1.19      simpset = simpset addsimps simps}) #>
    1.20    arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
     2.1 --- a/src/HOL/NatBin.thy	Tue Jul 31 19:40:23 2007 +0200
     2.2 +++ b/src/HOL/NatBin.thy	Tue Jul 31 19:40:24 2007 +0200
     2.3 @@ -656,7 +656,7 @@
     2.4  val numeral_ss = simpset() addsimps numerals;
     2.5  
     2.6  val nat_bin_arith_setup =
     2.7 - Fast_Arith.map_data
     2.8 + LinArith.map_data
     2.9     (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    2.10       {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    2.11        inj_thms = inj_thms,
     3.1 --- a/src/HOL/Real/rat_arith.ML	Tue Jul 31 19:40:23 2007 +0200
     3.2 +++ b/src/HOL/Real/rat_arith.ML	Tue Jul 31 19:40:24 2007 +0200
     3.3 @@ -36,11 +36,11 @@
     3.4  val ratT = Type ("Rational.rat", [])
     3.5  
     3.6  val rat_arith_setup =
     3.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     3.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     3.9     {add_mono_thms = add_mono_thms,
    3.10      mult_mono_thms = mult_mono_thms,
    3.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    3.12 -    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
    3.13 +    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
    3.14      neqE =  neqE,
    3.15      simpset = simpset addsimps simps
    3.16                        addsimprocs simprocs}) #>
     4.1 --- a/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:23 2007 +0200
     4.2 +++ b/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:24 2007 +0200
     4.3 @@ -29,74 +29,14 @@
     4.4  in
     4.5  
     4.6  val real_arith_setup =
     4.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     4.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     4.9     {add_mono_thms = add_mono_thms,
    4.10      mult_mono_thms = mult_mono_thms,
    4.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    4.12 -    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
    4.13 +    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
    4.14      neqE = neqE,
    4.15      simpset = simpset addsimps simps}) #>
    4.16    arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
    4.17    arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT)
    4.18  
    4.19  end;
    4.20 -
    4.21 -
    4.22 -(* Some test data [omitting examples that assume the ordering to be discrete!]
    4.23 -Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    4.24 -by (fast_arith_tac 1);
    4.25 -qed "";
    4.26 -
    4.27 -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
    4.28 -by (fast_arith_tac 1);
    4.29 -qed "";
    4.30 -
    4.31 -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
    4.32 -by (fast_arith_tac 1);
    4.33 -qed "";
    4.34 -
    4.35 -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    4.36 -by (arith_tac 1);
    4.37 -qed "";
    4.38 -
    4.39 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    4.40 -\     ==> a <= l";
    4.41 -by (fast_arith_tac 1);
    4.42 -qed "";
    4.43 -
    4.44 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    4.45 -\     ==> a+a+a+a <= l+l+l+l";
    4.46 -by (fast_arith_tac 1);
    4.47 -qed "";
    4.48 -
    4.49 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    4.50 -\     ==> a+a+a+a+a <= l+l+l+l+i";
    4.51 -by (fast_arith_tac 1);
    4.52 -qed "";
    4.53 -
    4.54 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    4.55 -\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
    4.56 -by (fast_arith_tac 1);
    4.57 -qed "";
    4.58 -
    4.59 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    4.60 -\     ==> 6*a <= 5*l+i";
    4.61 -by (fast_arith_tac 1);
    4.62 -qed "";
    4.63 -
    4.64 -Goal "a<=b ==> a < b+(1::real)";
    4.65 -by (fast_arith_tac 1);
    4.66 -qed "";
    4.67 -
    4.68 -Goal "a<=b ==> a-(3::real) < b";
    4.69 -by (fast_arith_tac 1);
    4.70 -qed "";
    4.71 -
    4.72 -Goal "a<=b ==> a-(1::real) < b";
    4.73 -by (fast_arith_tac 1);
    4.74 -qed "";
    4.75 -
    4.76 -*)
    4.77 -
    4.78 -
    4.79 -
     5.1 --- a/src/HOL/ex/Arith_Examples.thy	Tue Jul 31 19:40:23 2007 +0200
     5.2 +++ b/src/HOL/ex/Arith_Examples.thy	Tue Jul 31 19:40:24 2007 +0200
     5.3 @@ -19,12 +19,12 @@
     5.4    method combines them both, and tries other methods (e.g.~@{text presburger})
     5.5    as well.  This is the one that you should use in your proofs!
     5.6  
     5.7 -  An @{text arith}-based simproc is available as well
     5.8 -  (see @{ML Fast_Arith.lin_arith_simproc}),
     5.9 -  which---for performance reasons---however
    5.10 -  does even less splitting than @{ML fast_arith_tac} at the moment (namely
    5.11 -  inequalities only).  (On the other hand, it does take apart conjunctions,
    5.12 -  which @{ML fast_arith_tac} currently does not do.)
    5.13 +  An @{text arith}-based simproc is available as well (see @{ML
    5.14 +  LinArith.lin_arith_simproc}), which---for performance
    5.15 +  reasons---however does even less splitting than @{ML fast_arith_tac}
    5.16 +  at the moment (namely inequalities only).  (On the other hand, it
    5.17 +  does take apart conjunctions, which @{ML fast_arith_tac} currently
    5.18 +  does not do.)
    5.19  *}
    5.20  
    5.21  (*
    5.22 @@ -122,12 +122,12 @@
    5.23    (* FIXME: need to replace 1 by its numeral representation *)
    5.24    apply (subst numeral_1_eq_1 [symmetric])
    5.25    (* FIXME: arith does not know about iszero *)
    5.26 -  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
    5.27 +  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
    5.28  oops
    5.29  
    5.30  lemma "(i::int) mod 42 <= 41"
    5.31    (* FIXME: arith does not know about iszero *)
    5.32 -  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
    5.33 +  apply (tactic {* lin_arith_pre_tac @{context} 1 *})
    5.34  oops
    5.35  
    5.36  
     6.1 --- a/src/HOL/int_arith1.ML	Tue Jul 31 19:40:23 2007 +0200
     6.2 +++ b/src/HOL/int_arith1.ML	Tue Jul 31 19:40:24 2007 +0200
     6.3 @@ -591,7 +591,7 @@
     6.4  in
     6.5  
     6.6  val int_arith_setup =
     6.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     6.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     6.9     {add_mono_thms = add_mono_thms,
    6.10      mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
    6.11      inj_thms = nat_inj_thms @ inj_thms,
    6.12 @@ -610,6 +610,6 @@
    6.13    "fast_int_arith" 
    6.14       ["(m::'a::{ordered_idom,number_ring}) < n",
    6.15        "(m::'a::{ordered_idom,number_ring}) <= n",
    6.16 -      "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
    6.17 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K LinArith.lin_arith_simproc);
    6.18  
    6.19  Addsimprocs [fast_int_arith_simproc];
     7.1 --- a/src/HOL/nat_simprocs.ML	Tue Jul 31 19:40:23 2007 +0200
     7.2 +++ b/src/HOL/nat_simprocs.ML	Tue Jul 31 19:40:24 2007 +0200
     7.3 @@ -564,7 +564,7 @@
     7.4  in
     7.5  
     7.6  val nat_simprocs_setup =
     7.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     7.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     7.9     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
    7.10      inj_thms = inj_thms, lessD = lessD, neqE = neqE,
    7.11      simpset = simpset addsimps add_rules