interface changes in linarith.ML
authorhaftmann
Sat May 09 09:17:29 2009 +0200 (2009-05-09)
changeset 3108254a442b2d727
parent 31072 796d3d42c873
child 31083 31b4cbe16deb
interface changes in linarith.ML
src/HOL/HoareParallel/Graph.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/NSA/hypreal_arith.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/rat_arith.ML
src/HOL/Tools/real_arith.ML
src/HOL/ex/Arith_Examples.thy
     1.1 --- a/src/HOL/HoareParallel/Graph.thy	Fri May 08 13:38:21 2009 +0200
     1.2 +++ b/src/HOL/HoareParallel/Graph.thy	Sat May 09 09:17:29 2009 +0200
     1.3 @@ -172,9 +172,9 @@
     1.4   prefer 2 apply arith
     1.5   apply(drule_tac n = "Suc nata" in Compl_lemma)
     1.6   apply clarify
     1.7 - using [[fast_arith_split_limit = 0]]
     1.8 + using [[linarith_split_limit = 0]]
     1.9   apply force
    1.10 - using [[fast_arith_split_limit = 9]]
    1.11 + using [[linarith_split_limit = 9]]
    1.12  apply(drule leI)
    1.13  apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
    1.14   apply(erule_tac x = "m - (Suc nata)" in allE)
     2.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri May 08 13:38:21 2009 +0200
     2.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat May 09 09:17:29 2009 +0200
     2.3 @@ -454,7 +454,7 @@
     2.4  apply (simp add: max_of_list_def)
     2.5  apply (induct xs)
     2.6  apply simp
     2.7 -using [[fast_arith_split_limit = 0]]
     2.8 +using [[linarith_split_limit = 0]]
     2.9  apply simp
    2.10  apply arith
    2.11  done
     3.1 --- a/src/HOL/NSA/hypreal_arith.ML	Fri May 08 13:38:21 2009 +0200
     3.2 +++ b/src/HOL/NSA/hypreal_arith.ML	Sat May 09 09:17:29 2009 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/NSA/hypreal_arith.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Tobias Nipkow, TU Muenchen
     3.7      Copyright   1999 TU Muenchen
     3.8  
     3.9 @@ -24,7 +23,7 @@
    3.10  
    3.11  in
    3.12  
    3.13 -val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
    3.14 +val hyprealT = Type (@{type_name StarDef.star}, [HOLogic.realT]);
    3.15  
    3.16  val fast_hypreal_arith_simproc =
    3.17      Simplifier.simproc (the_context ())
    3.18 @@ -40,7 +39,7 @@
    3.19      lessD = lessD,  (*Can't change lessD: the hypreals are dense!*)
    3.20      neqE = neqE,
    3.21      simpset = simpset addsimps simps}) #>
    3.22 -  arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
    3.23 +  Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, HOLogic.realT --> hyprealT) #>
    3.24    Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
    3.25  
    3.26  end;
     4.1 --- a/src/HOL/Tools/int_arith.ML	Fri May 08 13:38:21 2009 +0200
     4.2 +++ b/src/HOL/Tools/int_arith.ML	Sat May 09 09:17:29 2009 +0200
     4.3 @@ -93,15 +93,14 @@
     4.4  val setup =
     4.5    Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     4.6     {add_mono_thms = add_mono_thms,
     4.7 -    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
     4.8 +    mult_mono_thms = (*@{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: *)mult_mono_thms,
     4.9      inj_thms = nat_inj_thms @ inj_thms,
    4.10      lessD = lessD @ [@{thm zless_imp_add1_zle}],
    4.11      neqE = neqE,
    4.12      simpset = simpset addsimps add_rules
    4.13 -                      addsimprocs numeral_base_simprocs
    4.14 -                      addcongs [if_weak_cong]}) #>
    4.15 -  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    4.16 -  arith_discrete @{type_name Int.int}
    4.17 +                      addsimprocs numeral_base_simprocs}) #>
    4.18 +  Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
    4.19 +  Lin_Arith.add_discrete_type @{type_name Int.int}
    4.20  
    4.21  val fast_int_arith_simproc =
    4.22    Simplifier.simproc (the_context ())
     5.1 --- a/src/HOL/Tools/lin_arith.ML	Fri May 08 13:38:21 2009 +0200
     5.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat May 09 09:17:29 2009 +0200
     5.3 @@ -7,14 +7,9 @@
     5.4  signature BASIC_LIN_ARITH =
     5.5  sig
     5.6    val arith_split_add: attribute
     5.7 -  val arith_discrete: string -> Context.generic -> Context.generic
     5.8 -  val arith_inj_const: string * typ -> Context.generic -> Context.generic
     5.9 -  val fast_arith_split_limit: int Config.T
    5.10 -  val fast_arith_neq_limit: int Config.T
    5.11    val lin_arith_pre_tac: Proof.context -> int -> tactic
    5.12    val fast_arith_tac: Proof.context -> int -> tactic
    5.13    val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
    5.14 -  val trace_arith: bool ref
    5.15    val lin_arith_simproc: simpset -> term -> thm option
    5.16    val fast_nat_arith_simproc: simproc
    5.17    val linear_arith_tac: Proof.context -> int -> tactic
    5.18 @@ -23,14 +18,19 @@
    5.19  signature LIN_ARITH =
    5.20  sig
    5.21    include BASIC_LIN_ARITH
    5.22 +  val add_discrete_type: string -> Context.generic -> Context.generic
    5.23 +  val add_inj_const: string * typ -> Context.generic -> Context.generic
    5.24    val map_data:
    5.25      ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    5.26        lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} ->
    5.27       {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    5.28        lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) ->
    5.29      Context.generic -> Context.generic
    5.30 +  val setup: Context.generic -> Context.generic
    5.31 +  val split_limit: int Config.T
    5.32 +  val neq_limit: int Config.T
    5.33    val warning_count: int ref
    5.34 -  val setup: Context.generic -> Context.generic
    5.35 +  val trace: bool ref
    5.36  end;
    5.37  
    5.38  structure Lin_Arith: LIN_ARITH =
    5.39 @@ -99,23 +99,23 @@
    5.40      {splits = update Thm.eq_thm_prop thm splits,
    5.41       inj_consts = inj_consts, discrete = discrete}));
    5.42  
    5.43 -fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
    5.44 +fun add_discrete_type d = ArithContextData.map (fn {splits, inj_consts, discrete} =>
    5.45    {splits = splits, inj_consts = inj_consts,
    5.46     discrete = update (op =) d discrete});
    5.47  
    5.48 -fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
    5.49 +fun add_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete} =>
    5.50    {splits = splits, inj_consts = update (op =) c inj_consts,
    5.51     discrete = discrete});
    5.52  
    5.53 -val (fast_arith_split_limit, setup1) = Attrib.config_int "fast_arith_split_limit" 9;
    5.54 -val (fast_arith_neq_limit, setup2) = Attrib.config_int "fast_arith_neq_limit" 9;
    5.55 +val (split_limit, setup1) = Attrib.config_int "linarith_split_limit" 9;
    5.56 +val (neq_limit, setup2) = Attrib.config_int "linarith_neq_limit" 9;
    5.57  val setup_options = setup1 #> setup2;
    5.58  
    5.59  
    5.60  structure LA_Data_Ref =
    5.61  struct
    5.62  
    5.63 -val fast_arith_neq_limit = fast_arith_neq_limit;
    5.64 +val fast_arith_neq_limit = neq_limit;
    5.65  
    5.66  
    5.67  (* Decomposition of terms *)
    5.68 @@ -358,10 +358,10 @@
    5.69    val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
    5.70    val cmap       = Splitter.cmap_of_split_thms split_thms
    5.71    val splits     = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
    5.72 -  val split_limit = Config.get ctxt fast_arith_split_limit
    5.73 +  val split_limit = Config.get ctxt split_limit
    5.74  in
    5.75    if length splits > split_limit then
    5.76 -   (tracing ("fast_arith_split_limit exceeded (current value is " ^
    5.77 +   (tracing ("linarith_split_limit exceeded (current value is " ^
    5.78        string_of_int split_limit ^ ")"); NONE)
    5.79    else (
    5.80    case splits of [] =>
    5.81 @@ -696,7 +696,7 @@
    5.82  (* disjunctions and existential quantifiers from the premises, possibly (in  *)
    5.83  (* the case of disjunctions) resulting in several new subgoals, each of the  *)
    5.84  (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
    5.85 -(* !fast_arith_split_limit splits are possible.                              *)
    5.86 +(* !split_limit splits are possible.                              *)
    5.87  
    5.88  local
    5.89    val nnf_simpset =
    5.90 @@ -717,7 +717,7 @@
    5.91          val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
    5.92          val cmap = Splitter.cmap_of_split_thms split_thms
    5.93          val splits = Splitter.split_posns cmap thy Ts concl
    5.94 -        val split_limit = Config.get ctxt fast_arith_split_limit
    5.95 +        val split_limit = Config.get ctxt split_limit
    5.96        in
    5.97          if length splits > split_limit then no_tac
    5.98          else split_tac split_thms i
    5.99 @@ -767,7 +767,7 @@
   5.100  
   5.101  fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
   5.102  val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
   5.103 -val trace_arith = Fast_Arith.trace;
   5.104 +val trace = Fast_Arith.trace;
   5.105  val warning_count = Fast_Arith.warning_count;
   5.106  
   5.107  (* reduce contradictory <= to False.
   5.108 @@ -775,11 +775,10 @@
   5.109  
   5.110  val init_arith_data =
   5.111   map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   5.112 -   {add_mono_thms = add_mono_thms @
   5.113 -    @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
   5.114 -    mult_mono_thms = mult_mono_thms,
   5.115 +   {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
   5.116 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
   5.117      inj_thms = inj_thms,
   5.118 -    lessD = lessD @ [thm "Suc_leI"],
   5.119 +    lessD = lessD @ [@{thm "Suc_leI"}],
   5.120      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
   5.121      simpset = HOL_basic_ss
   5.122        addsimps
   5.123 @@ -791,8 +790,9 @@
   5.124          @{thm "not_one_less_zero"}]
   5.125        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
   5.126         (*abel_cancel helps it work in abstract algebraic domains*)
   5.127 -      addsimprocs Nat_Arith.nat_cancel_sums_add}) #>
   5.128 -  arith_discrete "nat";
   5.129 +      addsimprocs Nat_Arith.nat_cancel_sums_add
   5.130 +      addcongs [if_weak_cong]}) #>
   5.131 +  add_discrete_type @{type_name nat};
   5.132  
   5.133  fun add_arith_facts ss =
   5.134    add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
   5.135 @@ -869,7 +869,7 @@
   5.136      (* Splitting is also done inside fast_arith_tac, but not completely --   *)
   5.137      (* split_tac may use split theorems that have not been implemented in    *)
   5.138      (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
   5.139 -    (* fast_arith_split_limit may trigger.                                   *)
   5.140 +    (* split_limit may trigger.                                   *)
   5.141      (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
   5.142      (* some goals that fast_arith_tac alone would fail on.                   *)
   5.143      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
     6.1 --- a/src/HOL/Tools/rat_arith.ML	Fri May 08 13:38:21 2009 +0200
     6.2 +++ b/src/HOL/Tools/rat_arith.ML	Sat May 09 09:17:29 2009 +0200
     6.3 @@ -40,7 +40,7 @@
     6.4      neqE =  neqE,
     6.5      simpset = simpset addsimps simps
     6.6                        addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
     6.7 -  arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
     6.8 -  arith_inj_const (@{const_name of_int}, @{typ "int => rat"})
     6.9 +  Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
    6.10 +  Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})
    6.11  
    6.12  end;
     7.1 --- a/src/HOL/Tools/real_arith.ML	Fri May 08 13:38:21 2009 +0200
     7.2 +++ b/src/HOL/Tools/real_arith.ML	Sat May 09 09:17:29 2009 +0200
     7.3 @@ -36,7 +36,7 @@
     7.4      lessD = lessD,  (*Can't change lessD: the reals are dense!*)
     7.5      neqE = neqE,
     7.6      simpset = simpset addsimps simps}) #>
     7.7 -  arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
     7.8 -  arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
     7.9 +  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
    7.10 +  Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
    7.11  
    7.12  end;
     8.1 --- a/src/HOL/ex/Arith_Examples.thy	Fri May 08 13:38:21 2009 +0200
     8.2 +++ b/src/HOL/ex/Arith_Examples.thy	Sat May 09 09:17:29 2009 +0200
     8.3 @@ -29,7 +29,7 @@
     8.4  *}
     8.5  
     8.6  (*
     8.7 -ML {* set trace_arith; *}
     8.8 +ML {* set Lin_Arith.trace; *}
     8.9  *)
    8.10  
    8.11  subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    8.12 @@ -244,7 +244,7 @@
    8.13    by linarith
    8.14  
    8.15  (*
    8.16 -ML {* reset trace_arith; *}
    8.17 +ML {* reset Lin_Arith.trace; *}
    8.18  *)
    8.19  
    8.20  end