# HG changeset patch # User haftmann # Date 1242047912 -7200 # Node ID 6a2e67fe448806608e4ecc3341b2b20b90254e39 # Parent 27a6558e64b62aef9feffcb77f38b410ee4fabf2 tuned interface of Lin_Arith diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Int.thy --- 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 {* diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/IsaMakefile --- 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 \ diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/NSA/HyperDef.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 \ 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 *} diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/NSA/hypreal_arith.ML --- 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; diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Nat.thy --- 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 diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Nat_Numeral.thy --- 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)) *} diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Rational.thy --- 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 *} diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/RealDef.thy --- 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?*} diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Tools/int_arith.ML --- 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; diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Tools/lin_arith.ML --- 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; diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Tools/rat_arith.ML --- 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; diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/Tools/real_arith.ML --- 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; diff -r 27a6558e64b6 -r 6a2e67fe4488 src/HOL/ex/Arith_Examples.thy --- 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"