--- a/src/HOL/Int.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Int.thy Mon May 11 15:18:32 2009 +0200
@@ -1521,6 +1521,7 @@
use "Tools/numeral_simprocs.ML"
use "Tools/int_arith.ML"
+setup {* Int_Arith.global_setup *}
declaration {* K Int_Arith.setup *}
setup {*
--- a/src/HOL/IsaMakefile Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/IsaMakefile Mon May 11 15:18:32 2009 +0200
@@ -295,8 +295,6 @@
Real.thy \
RealVector.thy \
Tools/float_syntax.ML \
- Tools/rat_arith.ML \
- Tools/real_arith.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
Tools/Qelim/langford_data.ML \
@@ -1051,7 +1049,6 @@
NSA/HyperDef.thy \
NSA/HyperNat.thy \
NSA/Hyperreal.thy \
- NSA/hypreal_arith.ML \
NSA/Filter.thy \
NSA/NatStar.thy \
NSA/NSA.thy \
--- a/src/HOL/NSA/HyperDef.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon May 11 15:18:32 2009 +0200
@@ -8,7 +8,6 @@
theory HyperDef
imports HyperNat Real
-uses ("hypreal_arith.ML")
begin
types hypreal = "real star"
@@ -343,8 +342,17 @@
Addsimps [symmetric hypreal_diff_def]
*)
-use "hypreal_arith.ML"
-declaration {* K hypreal_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
+ @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
+ #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
+ @{thm star_of_number_of}, @{thm star_of_add}, @{thm star_of_minus},
+ @{thm star_of_diff}, @{thm star_of_mult}]
+ #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})
+ #> Simplifier.map_ss (fn simpset => simpset addsimprocs [Simplifier.simproc @{theory}
+ "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
+ (K Lin_Arith.lin_arith_simproc)]))
+*}
subsection {* Exponentials on the Hyperreals *}
--- a/src/HOL/NSA/hypreal_arith.ML Mon May 11 11:53:21 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/NSA/hypreal_arith.ML
- Author: Tobias Nipkow, TU Muenchen
- Copyright 1999 TU Muenchen
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type hypreal.
-*)
-
-local
-
-val simps = [thm "star_of_zero",
- thm "star_of_one",
- thm "star_of_number_of",
- thm "star_of_add",
- thm "star_of_minus",
- thm "star_of_diff",
- thm "star_of_mult"]
-
-val real_inj_thms = [thm "star_of_le" RS iffD2,
- thm "star_of_less" RS iffD2,
- thm "star_of_eq" RS iffD2]
-
-in
-
-val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
-
-val fast_hypreal_arith_simproc =
- Simplifier.simproc (the_context ())
- "fast_hypreal_arith"
- ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- (K Lin_Arith.lin_arith_simproc);
-
-val hypreal_arith_setup =
- Lin_Arith.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 lessD: the hypreals are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps}) #>
- Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, HOLogic.realT --> hyprealT) #>
- Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
-
-end;
--- a/src/HOL/Nat.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Nat.thy Mon May 11 15:18:32 2009 +0200
@@ -1410,6 +1410,7 @@
declaration {* K Nat_Arith.setup *}
use "Tools/lin_arith.ML"
+setup {* Lin_Arith.global_setup *}
declaration {* K Lin_Arith.setup *}
lemmas [arith_split] = nat_diff_split split_min split_max
--- a/src/HOL/Nat_Numeral.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Mon May 11 15:18:32 2009 +0200
@@ -874,33 +874,21 @@
use "Tools/nat_numeral_simprocs.ML"
-declaration {*
-let
-
-val less_eq_rules = @{thms ring_distribs} @
- [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
- @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
- @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
- @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
- @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
- @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
- @{thm mult_Suc}, @{thm mult_Suc_right},
- @{thm add_Suc}, @{thm add_Suc_right},
- @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
- @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
-
-val simprocs = Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals;
-
-in
-
-K (Lin_Arith.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 (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
- addsimps less_eq_rules
- addsimprocs simprocs}))
-
-end
+declaration {*
+ K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
+ #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
+ @{thm nat_0}, @{thm nat_1},
+ @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
+ @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
+ @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
+ @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
+ @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
+ @{thm mult_Suc}, @{thm mult_Suc_right},
+ @{thm add_Suc}, @{thm add_Suc_right},
+ @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
+ @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
+ @{thm if_True}, @{thm if_False}])
+ #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
*}
--- a/src/HOL/Rational.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Rational.thy Mon May 11 15:18:32 2009 +0200
@@ -6,7 +6,6 @@
theory Rational
imports GCD Archimedean_Field
-uses ("Tools/rat_arith.ML")
begin
subsection {* Rational numbers as quotient *}
@@ -582,10 +581,25 @@
by (simp add: floor_unique)
-subsection {* Arithmetic setup *}
+subsection {* Linear arithmetic setup *}
-use "Tools/rat_arith.ML"
-declaration {* K rat_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
+ (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
+ #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2]
+ (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
+ #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
+ @{thm True_implies_equals},
+ read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
+ @{thm divide_1}, @{thm divide_zero_left},
+ @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
+ @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
+ @{thm of_int_minus}, @{thm of_int_diff},
+ @{thm of_int_of_nat_eq}]
+ #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors
+ #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
+ #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
+*}
subsection {* Embedding from Rationals to other Fields *}
--- a/src/HOL/RealDef.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/RealDef.thy Mon May 11 15:18:32 2009 +0200
@@ -9,7 +9,6 @@
theory RealDef
imports PReal
-uses ("Tools/real_arith.ML")
begin
definition
@@ -960,10 +959,20 @@
(if neg (number_of v :: int) then 0
else (number_of v :: real))"
by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of)
-
-use "Tools/real_arith.ML"
-declaration {* K real_arith_setup *}
+declaration {*
+ K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
+ (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)
+ #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]
+ (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)
+ #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
+ @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
+ @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
+ @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
+ @{thm real_of_nat_number_of}, @{thm real_number_of}]
+ #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT)
+ #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT))
+*}
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
--- a/src/HOL/Tools/int_arith.ML Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML Mon May 11 15:18:32 2009 +0200
@@ -5,8 +5,8 @@
signature INT_ARITH =
sig
- val fast_int_arith_simproc: simproc
val setup: Context.generic -> Context.generic
+ val global_setup: theory -> theory
end
structure Int_Arith : INT_ARITH =
@@ -49,17 +49,15 @@
make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
proc = proc1, identifier = []};
-val allowed_consts =
- [@{const_name "op ="}, @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
- @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
- @{const_name "HOL.zero"}, @{const_name "HOL.one"}, @{const_name "HOL.less"},
- @{const_name "HOL.less_eq"}];
-
-fun check t = case t of
- Const(s,t) => if s = @{const_name "HOL.one"} then not (t = @{typ int})
- else s mem_string allowed_consts
- | a$b => check a andalso check b
- | _ => false;
+fun check (Const (@{const_name "HOL.one"}, @{typ int})) = false
+ | check (Const (@{const_name "HOL.one"}, _)) = true
+ | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+ @{const_name "HOL.times"}, @{const_name "HOL.uminus"},
+ @{const_name "HOL.minus"}, @{const_name "HOL.plus"},
+ @{const_name "HOL.zero"},
+ @{const_name "HOL.less"}, @{const_name "HOL.less_eq"}] s
+ | check (a $ b) = check a andalso check b
+ | check _ = false;
val conv =
Simplifier.rewrite
@@ -80,35 +78,24 @@
make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
proc = sproc, identifier = []}
-val add_rules =
- simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
- @{thms int_arith_rules}
-
-val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
-
-val numeral_base_simprocs = Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
- :: Numeral_Simprocs.combine_numerals
- :: Numeral_Simprocs.cancel_numerals;
-
-val setup =
- Lin_Arith.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,
- lessD = lessD @ [@{thm zless_imp_add1_zle}],
- neqE = neqE,
- simpset = simpset addsimps add_rules
- addsimprocs numeral_base_simprocs}) #>
- Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
- Lin_Arith.add_discrete_type @{type_name Int.int}
-
val fast_int_arith_simproc =
- Simplifier.simproc (the_context ())
- "fast_int_arith"
+ Simplifier.simproc @{theory} "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 Lin_Arith.lin_arith_simproc);
-end;
+val global_setup = Simplifier.map_simpset
+ (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
-Addsimprocs [Int_Arith.fast_int_arith_simproc];
+val setup =
+ Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
+ #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
+ #> Lin_Arith.add_simps (@{thms simp_thms} @ @{thms arith_simps} @ @{thms rel_simps}
+ @ @{thms arith_special} @ @{thms int_arith_rules})
+ #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
+ :: Numeral_Simprocs.combine_numerals
+ :: Numeral_Simprocs.cancel_numerals)
+ #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
+ #> Lin_Arith.add_discrete_type @{type_name Int.int}
+
+end;
--- a/src/HOL/Tools/lin_arith.ML Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Mon May 11 15:18:32 2009 +0200
@@ -6,27 +6,25 @@
signature BASIC_LIN_ARITH =
sig
- val arith_split_add: attribute
- val lin_arith_pre_tac: Proof.context -> int -> tactic
+ val lin_arith_simproc: simpset -> term -> thm option
+ val fast_nat_arith_simproc: simproc
val fast_arith_tac: Proof.context -> int -> tactic
val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
- val lin_arith_simproc: simpset -> term -> thm option
- val fast_nat_arith_simproc: simproc
val linear_arith_tac: Proof.context -> int -> tactic
end;
signature LIN_ARITH =
sig
include BASIC_LIN_ARITH
- val add_discrete_type: string -> Context.generic -> Context.generic
+ val pre_tac: Proof.context -> int -> tactic
+ val add_inj_thms: thm list -> Context.generic -> Context.generic
+ val add_lessD: thm -> Context.generic -> Context.generic
+ val add_simps: thm list -> Context.generic -> Context.generic
+ val add_simprocs: simproc list -> Context.generic -> Context.generic
val add_inj_const: string * typ -> Context.generic -> Context.generic
- val map_data:
- ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ->
- {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
- lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
- Context.generic -> Context.generic
+ val add_discrete_type: string -> Context.generic -> Context.generic
val setup: Context.generic -> Context.generic
+ val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
val warning_count: int ref
@@ -47,37 +45,38 @@
val sym = sym;
val not_lessD = @{thm linorder_not_less} RS iffD1;
val not_leD = @{thm linorder_not_le} RS iffD1;
-val le0 = thm "le0";
-fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
+fun mk_Eq thm = thm RS Eq_FalseI handle THM _ => thm RS Eq_TrueI;
val mk_Trueprop = HOLogic.mk_Trueprop;
fun atomize thm = case Thm.prop_of thm of
- Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
- atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
+ Const ("Trueprop", _) $ (Const (@{const_name "op &"}, _) $ _ $ _) =>
+ atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop",_)) $ (Const("Not",_) $ t)) = TP $ t
- | neg_prop ((TP as Const("Trueprop",_)) $ t) = TP $ (HOLogic.Not $t)
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+ | neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);
fun is_False thm =
let val _ $ t = Thm.prop_of thm
- in t = Const("False",HOLogic.boolT) end;
+ in t = HOLogic.false_const end;
fun is_nat t = (fastype_of1 t = HOLogic.natT);
-fun mk_nat_thm sg t =
- let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
- in instantiate ([],[(cn,ct)]) le0 end;
+fun mk_nat_thm thy t =
+ let
+ val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
+ and ct = cterm_of thy t
+ in instantiate ([], [(cn, ct)]) @{thm le0} end;
end;
(* arith context data *)
-structure ArithContextData = GenericDataFun
+structure Lin_Arith_Data = GenericDataFun
(
type T = {splits: thm list,
inj_consts: (string * typ) list,
@@ -92,27 +91,25 @@
discrete = Library.merge (op =) (discrete1, discrete2)};
);
-val get_arith_data = ArithContextData.get o Context.Proof;
+val get_arith_data = Lin_Arith_Data.get o Context.Proof;
-val arith_split_add = Thm.declaration_attribute (fn thm =>
- ArithContextData.map (fn {splits, inj_consts, discrete} =>
- {splits = update Thm.eq_thm_prop thm splits,
- inj_consts = inj_consts, discrete = discrete}));
+fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
+ {splits = update Thm.eq_thm_prop thm splits,
+ inj_consts = inj_consts, discrete = discrete});
-fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = inj_consts,
discrete = update (op =) d discrete});
-fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = update (op =) c inj_consts,
discrete = discrete});
-val (split_limit, setup1) = Attrib.config_int "linarith_split_limit" 9;
-val (neq_limit, setup2) = Attrib.config_int "linarith_neq_limit" 9;
-val setup_options = setup1 #> setup2;
+val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
+val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
-structure LA_Data_Ref =
+structure LA_Data =
struct
val fast_arith_neq_limit = neq_limit;
@@ -756,15 +753,32 @@
)
end;
-end; (* LA_Data_Ref *)
+end; (* LA_Data *)
-val lin_arith_pre_tac = LA_Data_Ref.pre_tac;
+val pre_tac = LA_Data.pre_tac;
-structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data_Ref);
+structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
val map_data = Fast_Arith.map_data;
+fun map_inj_thms f {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 = f inj_thms,
+ lessD = lessD, neqE = neqE, simpset = simpset};
+
+fun map_lessD f {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 = f lessD, neqE = neqE, simpset = simpset};
+
+fun map_simpset f {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 = f simpset};
+
+fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
+fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
+fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
+fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
+
fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
val trace = Fast_Arith.trace;
@@ -774,7 +788,7 @@
Most of the work is done by the cancel tactics. *)
val init_arith_data =
- map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
{add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
inj_thms = inj_thms,
@@ -891,17 +905,18 @@
init_arith_data #>
Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
addSolver (mk_solver' "lin_arith"
- (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
- Context.mapping
- (setup_options #>
- Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac #>
- Method.setup @{binding linarith}
- (Args.bang_facts >> (fn prems => fn ctxt =>
- METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
- THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
- Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
- "declaration of split rules for arithmetic procedure") I;
+ (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
+
+val global_setup =
+ setup_split_limit #> setup_neq_limit #>
+ Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
+ "declaration of split rules for arithmetic procedure" #>
+ Method.setup @{binding linarith}
+ (Args.bang_facts >> (fn prems => fn ctxt =>
+ METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
+ THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
+ Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac;
end;
--- a/src/HOL/Tools/rat_arith.ML Mon May 11 11:53:21 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/Real/rat_arith.ML
- Author: Lawrence C Paulson
- Copyright 2004 University of Cambridge
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type rat.
-*)
-
-local
-
-val simps =
- [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
- read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
- @{thm divide_1}, @{thm divide_zero_left},
- @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
- @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
- @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
- @{thm of_int_minus}, @{thm of_int_diff},
- @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
-
-val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
- @{thm of_nat_eq_iff} RS iffD2]
-(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
- of_nat_less_iff RS iffD2 *)
-
-val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
- @{thm of_int_eq_iff} RS iffD2]
-(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
- of_int_less_iff RS iffD2 *)
-
-in
-
-val rat_arith_setup =
- Lin_Arith.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 lessD: the rats are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps
- addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
- Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
- Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})
-
-end;
--- a/src/HOL/Tools/real_arith.ML Mon May 11 11:53:21 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: HOL/Real/real_arith.ML
- ID: $Id$
- Author: Tobias Nipkow, TU Muenchen
- Copyright 1999 TU Muenchen
-
-Simprocs for common factor cancellation & Rational coefficient handling
-
-Instantiation of the generic linear arithmetic package for type real.
-*)
-
-local
-
-val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
- @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
- @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
- @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
- @{thm real_of_nat_number_of}, @{thm real_number_of}]
-
-val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
- @{thm real_of_nat_inject} RS iffD2]
-(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
- real_of_nat_less_iff RS iffD2 *)
-
-val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
- @{thm real_of_int_inject} RS iffD2]
-(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
- real_of_int_less_iff RS iffD2 *)
-
-in
-
-val real_arith_setup =
- Lin_Arith.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 lessD: the reals are dense!*)
- neqE = neqE,
- simpset = simpset addsimps simps}) #>
- Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
- Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
-
-end;
--- a/src/HOL/ex/Arith_Examples.thy Mon May 11 11:53:21 2009 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Mon May 11 15:18:32 2009 +0200
@@ -123,12 +123,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 {* lin_arith_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 {* lin_arith_pre_tac @{context} 1 *})
+ apply (tactic {* Lin_Arith.pre_tac @{context} 1 *})
oops
lemma "-(i::int) * 1 = 0 ==> i = 0"