# HG changeset patch # User haftmann # Date 1241853465 -7200 # Node ID 31b4cbe16debfddcdaa75193321434a71d61a997 # Parent aee96acd5e7911cd94e9e9cf73f20783fb1fed15# Parent 54a442b2d7274e9c3db6f74ffa34ee4e9b2794a4 merged diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/HoareParallel/Graph.thy --- a/src/HOL/HoareParallel/Graph.thy Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/HoareParallel/Graph.thy Sat May 09 09:17:45 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) diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Sat May 09 09:17:45 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 diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/NSA/hypreal_arith.ML --- a/src/HOL/NSA/hypreal_arith.ML Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/NSA/hypreal_arith.ML Sat May 09 09:17:45 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; diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/Tools/int_arith.ML Sat May 09 09:17:45 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 ()) diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/Tools/lin_arith.ML Sat May 09 09:17:45 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))) diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/Tools/rat_arith.ML --- a/src/HOL/Tools/rat_arith.ML Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/Tools/rat_arith.ML Sat May 09 09:17:45 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; diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/Tools/real_arith.ML --- a/src/HOL/Tools/real_arith.ML Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/Tools/real_arith.ML Sat May 09 09:17:45 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; diff -r aee96acd5e79 -r 31b4cbe16deb src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Sat May 09 07:25:45 2009 +0200 +++ b/src/HOL/ex/Arith_Examples.thy Sat May 09 09:17:45 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