src/HOL/Tools/lin_arith.ML
changeset 31101 26c7bb764a38
parent 31100 6a2e67fe4488
child 31510 e0f2bb4b0021
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Mon May 11 15:18:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon May 11 15:57:29 2009 +0200
     1.3 @@ -4,19 +4,12 @@
     1.4  HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
     1.5  *)
     1.6  
     1.7 -signature BASIC_LIN_ARITH =
     1.8 -sig
     1.9 -  val lin_arith_simproc: simpset -> term -> thm option
    1.10 -  val fast_nat_arith_simproc: simproc
    1.11 -  val fast_arith_tac: Proof.context -> int -> tactic
    1.12 -  val fast_ex_arith_tac: Proof.context -> bool -> int -> tactic
    1.13 -  val linear_arith_tac: Proof.context -> int -> tactic
    1.14 -end;
    1.15 -
    1.16  signature LIN_ARITH =
    1.17  sig
    1.18 -  include BASIC_LIN_ARITH
    1.19    val pre_tac: Proof.context -> int -> tactic
    1.20 +  val simple_tac: Proof.context -> int -> tactic
    1.21 +  val tac: Proof.context -> int -> tactic
    1.22 +  val simproc: simpset -> term -> thm option
    1.23    val add_inj_thms: thm list -> Context.generic -> Context.generic
    1.24    val add_lessD: thm -> Context.generic -> Context.generic
    1.25    val add_simps: thm list -> Context.generic -> Context.generic
    1.26 @@ -240,15 +233,12 @@
    1.27  end handle Rat.DIVZERO => NONE;
    1.28  
    1.29  fun of_lin_arith_sort thy U =
    1.30 -  Sign.of_sort thy (U, ["Ring_and_Field.ordered_idom"]);
    1.31 +  Sign.of_sort thy (U, @{sort Ring_and_Field.ordered_idom});
    1.32  
    1.33 -fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
    1.34 -  if of_lin_arith_sort sg U then
    1.35 -    (true, D mem discrete)
    1.36 -  else (* special cases *)
    1.37 -    if D mem discrete then  (true, true)  else  (false, false)
    1.38 -  | allows_lin_arith sg discrete U =
    1.39 -  (of_lin_arith_sort sg U, false);
    1.40 +fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
    1.41 +      if of_lin_arith_sort thy U then (true, member (op =) discrete D)
    1.42 +      else if member (op =) discrete D then (true, true) else (false, false)
    1.43 +  | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
    1.44  
    1.45  fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
    1.46    case T of
    1.47 @@ -284,7 +274,7 @@
    1.48    | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
    1.49    | domain_is_nat _                                                 = false;
    1.50  
    1.51 -fun number_of (n, T) = HOLogic.mk_number T n;
    1.52 +val mk_number = HOLogic.mk_number;
    1.53  
    1.54  (*---------------------------------------------------------------------------*)
    1.55  (* the following code performs splitting of certain constants (e.g. min,     *)
    1.56 @@ -779,8 +769,8 @@
    1.57  fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
    1.58  fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    1.59  
    1.60 -fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    1.61 -val fast_ex_arith_tac = Fast_Arith.lin_arith_tac;
    1.62 +fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    1.63 +val lin_arith_tac = Fast_Arith.lin_arith_tac;
    1.64  val trace = Fast_Arith.trace;
    1.65  val warning_count = Fast_Arith.warning_count;
    1.66  
    1.67 @@ -811,17 +801,7 @@
    1.68  fun add_arith_facts ss =
    1.69    add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
    1.70  
    1.71 -val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    1.72 -
    1.73 -val fast_nat_arith_simproc =
    1.74 -  Simplifier.simproc (the_context ()) "fast_nat_arith"
    1.75 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
    1.76 -
    1.77 -(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
    1.78 -useful to detect inconsistencies among the premises for subgoals which are
    1.79 -*not* themselves (in)equalities, because the latter activate
    1.80 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
    1.81 -solver all the time rather than add the additional check. *)
    1.82 +val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    1.83  
    1.84  
    1.85  (* generic refutation procedure *)
    1.86 @@ -871,7 +851,7 @@
    1.87  
    1.88  local
    1.89  
    1.90 -fun raw_arith_tac ctxt ex =
    1.91 +fun raw_tac ctxt ex =
    1.92    (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
    1.93       decomp sg"? -- but note that the test is applied to terms already before
    1.94       they are split/normalized) to speed things up in case there are lots of
    1.95 @@ -880,21 +860,21 @@
    1.96       (l <= min m n + k) = (l <= m+k & l <= n+k)
    1.97    *)
    1.98    refute_tac (K true)
    1.99 -    (* Splitting is also done inside fast_arith_tac, but not completely --   *)
   1.100 +    (* Splitting is also done inside simple_tac, but not completely --   *)
   1.101      (* split_tac may use split theorems that have not been implemented in    *)
   1.102 -    (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
   1.103 +    (* simple_tac (cf. pre_decomp and split_once_items above), and       *)
   1.104      (* split_limit may trigger.                                   *)
   1.105 -    (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
   1.106 -    (* some goals that fast_arith_tac alone would fail on.                   *)
   1.107 +    (* Therefore splitting outside of simple_tac may allow us to prove   *)
   1.108 +    (* some goals that simple_tac alone would fail on.                   *)
   1.109      (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   1.110 -    (fast_ex_arith_tac ctxt ex);
   1.111 +    (lin_arith_tac ctxt ex);
   1.112  
   1.113  in
   1.114  
   1.115 -fun gen_linear_arith_tac ex ctxt = FIRST' [fast_arith_tac ctxt,
   1.116 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt ex];
   1.117 +fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
   1.118 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
   1.119  
   1.120 -val linear_arith_tac = gen_linear_arith_tac true;
   1.121 +val tac = gen_tac true;
   1.122  
   1.123  end;
   1.124  
   1.125 @@ -903,7 +883,13 @@
   1.126  
   1.127  val setup =
   1.128    init_arith_data #>
   1.129 -  Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
   1.130 +  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
   1.131 +    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
   1.132 +    (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   1.133 +    useful to detect inconsistencies among the premises for subgoals which are
   1.134 +    *not* themselves (in)equalities, because the latter activate
   1.135 +    fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   1.136 +    solver all the time rather than add the additional check. *)
   1.137      addSolver (mk_solver' "lin_arith"
   1.138        (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)))
   1.139  
   1.140 @@ -915,10 +901,7 @@
   1.141      (Args.bang_facts >> (fn prems => fn ctxt =>
   1.142        METHOD (fn facts =>
   1.143          HEADGOAL (Method.insert_tac (prems @ Arith_Data.get_arith_facts ctxt @ facts)
   1.144 -          THEN' linear_arith_tac ctxt)))) "linear arithmetic" #>
   1.145 -  Arith_Data.add_tactic "linear arithmetic" gen_linear_arith_tac;
   1.146 +          THEN' tac ctxt)))) "linear arithmetic" #>
   1.147 +  Arith_Data.add_tactic "linear arithmetic" gen_tac;
   1.148  
   1.149  end;
   1.150 -
   1.151 -structure Basic_Lin_Arith: BASIC_LIN_ARITH = Lin_Arith;
   1.152 -open Basic_Lin_Arith;