--- a/src/HOL/HoareParallel/Graph.thy Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Sat May 09 09:17:29 2009 +0200
@@ -172,9 +172,9 @@
prefer 2 apply arith
apply(drule_tac n = "Suc nata" in Compl_lemma)
apply clarify
- using [[fast_arith_split_limit = 0]]
+ using [[linarith_split_limit = 0]]
apply force
- using [[fast_arith_split_limit = 9]]
+ using [[linarith_split_limit = 9]]
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
apply(erule_tac x = "m - (Suc nata)" in allE)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 09 09:17:29 2009 +0200
@@ -454,7 +454,7 @@
apply (simp add: max_of_list_def)
apply (induct xs)
apply simp
-using [[fast_arith_split_limit = 0]]
+using [[linarith_split_limit = 0]]
apply simp
apply arith
done
--- a/src/HOL/NSA/hypreal_arith.ML Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/NSA/hypreal_arith.ML Sat May 09 09:17:29 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/NSA/hypreal_arith.ML
- ID: $Id$
Author: Tobias Nipkow, TU Muenchen
Copyright 1999 TU Muenchen
@@ -24,7 +23,7 @@
in
-val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
+val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
val fast_hypreal_arith_simproc =
Simplifier.simproc (the_context ())
@@ -40,7 +39,7 @@
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) #>
+ 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/Tools/int_arith.ML Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML Sat May 09 09:17:29 2009 +0200
@@ -93,15 +93,14 @@
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,
+ 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
- addcongs [if_weak_cong]}) #>
- arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
- arith_discrete @{type_name Int.int}
+ 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 ())
--- a/src/HOL/Tools/lin_arith.ML Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sat May 09 09:17:29 2009 +0200
@@ -7,14 +7,9 @@
signature BASIC_LIN_ARITH =
sig
val arith_split_add: attribute
- val arith_discrete: string -> Context.generic -> Context.generic
- val arith_inj_const: string * typ -> Context.generic -> Context.generic
- val fast_arith_split_limit: int Config.T
- val fast_arith_neq_limit: int Config.T
val lin_arith_pre_tac: Proof.context -> int -> tactic
val fast_arith_tac: Proof.context -> int -> tactic
val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
- val trace_arith: bool ref
val lin_arith_simproc: simpset -> term -> thm option
val fast_nat_arith_simproc: simproc
val linear_arith_tac: Proof.context -> int -> tactic
@@ -23,14 +18,19 @@
signature LIN_ARITH =
sig
include BASIC_LIN_ARITH
+ val add_discrete_type: string -> 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 setup: Context.generic -> Context.generic
+ val split_limit: int Config.T
+ val neq_limit: int Config.T
val warning_count: int ref
- val setup: Context.generic -> Context.generic
+ val trace: bool ref
end;
structure Lin_Arith: LIN_ARITH =
@@ -99,23 +99,23 @@
{splits = update Thm.eq_thm_prop thm splits,
inj_consts = inj_consts, discrete = discrete}));
-fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = inj_consts,
discrete = update (op =) d discrete});
-fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
+fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
{splits = splits, inj_consts = update (op =) c inj_consts,
discrete = discrete});
-val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
-val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
+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;
structure LA_Data_Ref =
struct
-val fast_arith_neq_limit = fast_arith_neq_limit;
+val fast_arith_neq_limit = neq_limit;
(* Decomposition of terms *)
@@ -358,10 +358,10 @@
val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
val cmap = Splitter.cmap_of_split_thms split_thms
val splits = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
- val split_limit = Config.get ctxt fast_arith_split_limit
+ val split_limit = Config.get ctxt split_limit
in
if length splits > split_limit then
- (tracing ("fast_arith_split_limit exceeded (current value is " ^
+ (tracing ("linarith_split_limit exceeded (current value is " ^
string_of_int split_limit ^ ")"); NONE)
else (
case splits of [] =>
@@ -696,7 +696,7 @@
(* disjunctions and existential quantifiers from the premises, possibly (in *)
(* the case of disjunctions) resulting in several new subgoals, each of the *)
(* general form [| Q1; ...; Qm |] ==> False. Fails if more than *)
-(* !fast_arith_split_limit splits are possible. *)
+(* !split_limit splits are possible. *)
local
val nnf_simpset =
@@ -717,7 +717,7 @@
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
val cmap = Splitter.cmap_of_split_thms split_thms
val splits = Splitter.split_posns cmap thy Ts concl
- val split_limit = Config.get ctxt fast_arith_split_limit
+ val split_limit = Config.get ctxt split_limit
in
if length splits > split_limit then no_tac
else split_tac split_thms i
@@ -767,7 +767,7 @@
fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
-val trace_arith = Fast_Arith.trace;
+val trace = Fast_Arith.trace;
val warning_count = Fast_Arith.warning_count;
(* reduce contradictory <= to False.
@@ -775,11 +775,10 @@
val init_arith_data =
map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
- {add_mono_thms = add_mono_thms @
- @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
- mult_mono_thms = mult_mono_thms,
+ {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,
- lessD = lessD @ [thm "Suc_leI"],
+ lessD = lessD @ [@{thm "Suc_leI"}],
neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
simpset = HOL_basic_ss
addsimps
@@ -791,8 +790,9 @@
@{thm "not_one_less_zero"}]
addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
- addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
- arith_discrete "nat";
+ addsimprocs Nat_Arith.nat_cancel_sums_add
+ addcongs [if_weak_cong]}) #>
+ add_discrete_type @{type_name nat};
fun add_arith_facts ss =
add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
@@ -869,7 +869,7 @@
(* Splitting is also done inside fast_arith_tac, but not completely -- *)
(* split_tac may use split theorems that have not been implemented in *)
(* fast_arith_tac (cf. pre_decomp and split_once_items above), and *)
- (* fast_arith_split_limit may trigger. *)
+ (* split_limit may trigger. *)
(* Therefore splitting outside of fast_arith_tac may allow us to prove *)
(* some goals that fast_arith_tac alone would fail on. *)
(REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
--- a/src/HOL/Tools/rat_arith.ML Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/Tools/rat_arith.ML Sat May 09 09:17:29 2009 +0200
@@ -40,7 +40,7 @@
neqE = neqE,
simpset = simpset addsimps simps
addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
- arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
- arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
+ 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 Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/Tools/real_arith.ML Sat May 09 09:17:29 2009 +0200
@@ -36,7 +36,7 @@
lessD = lessD, (*Can't change lessD: the reals are dense!*)
neqE = neqE,
simpset = simpset addsimps simps}) #>
- arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
- arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
+ 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 Fri May 08 13:38:21 2009 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Sat May 09 09:17:29 2009 +0200
@@ -29,7 +29,7 @@
*}
(*
-ML {* set trace_arith; *}
+ML {* set Lin_Arith.trace; *}
*)
subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
@@ -244,7 +244,7 @@
by linarith
(*
-ML {* reset trace_arith; *}
+ML {* reset Lin_Arith.trace; *}
*)
end