arith method setup: proper context;
authorwenzelm
Tue Jul 31 00:56:29 2007 +0200 (2007-07-31)
changeset 24076ae946f751c44
parent 24075 366d4d234814
child 24077 e7ba448bc571
arith method setup: proper context;
turned fast_arith_split/neq_limit into configuration options;
tuned signatures;
misc cleanup;
src/HOL/arith_data.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/arith_data.ML	Tue Jul 31 00:56:26 2007 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Tue Jul 31 00:56:29 2007 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5  val mk_Trueprop = HOLogic.mk_Trueprop;
     1.6  
     1.7 -fun atomize thm = case #prop(rep_thm thm) of
     1.8 +fun atomize thm = case Thm.prop_of thm of
     1.9      Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
    1.10      atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
    1.11    | _ => [thm];
    1.12 @@ -186,7 +186,7 @@
    1.13    | neg_prop t = raise TERM ("neg_prop", [t]);
    1.14  
    1.15  fun is_False thm =
    1.16 -  let val _ $ t = #prop(rep_thm thm)
    1.17 +  let val _ $ t = Thm.prop_of thm
    1.18    in t = Const("False",HOLogic.boolT) end;
    1.19  
    1.20  fun is_nat(t) = fastype_of1 t = HOLogic.natT;
    1.21 @@ -206,14 +206,13 @@
    1.22  
    1.23  fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
    1.24  
    1.25 -structure ArithTheoryData = TheoryDataFun
    1.26 +structure ArithContextData = GenericDataFun
    1.27  (
    1.28    type T = {splits: thm list,
    1.29              inj_consts: (string * typ) list,
    1.30              discrete: string list,
    1.31              tactics: arithtactic list};
    1.32    val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
    1.33 -  val copy = I;
    1.34    val extend = I;
    1.35    fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
    1.36               {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) =
    1.37 @@ -223,29 +222,41 @@
    1.38      tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
    1.39  );
    1.40  
    1.41 +val get_arith_data = ArithContextData.get o Context.Proof;
    1.42 +
    1.43  val arith_split_add = Thm.declaration_attribute (fn thm =>
    1.44 -  Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    1.45 -    {splits= insert Thm.eq_thm_prop thm splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I);
    1.46 +  ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    1.47 +    {splits = insert Thm.eq_thm_prop thm splits,
    1.48 +     inj_consts = inj_consts, discrete = discrete, tactics = tactics}));
    1.49  
    1.50 -fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    1.51 -  {splits = splits, inj_consts = inj_consts, discrete = insert (op =) d discrete, tactics= tactics});
    1.52 +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    1.53 +  {splits = splits, inj_consts = inj_consts,
    1.54 +   discrete = insert (op =) d discrete, tactics = tactics});
    1.55  
    1.56 -fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    1.57 -  {splits = splits, inj_consts = insert (op =) c inj_consts, discrete = discrete, tactics= tactics});
    1.58 +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    1.59 +  {splits = splits, inj_consts = insert (op =) c inj_consts,
    1.60 +   discrete = discrete, tactics= tactics});
    1.61  
    1.62 -fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
    1.63 -  {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= insert eq_arith_tactic tac tactics});
    1.64 +fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} =>
    1.65 +  {splits = splits, inj_consts = inj_consts, discrete = discrete,
    1.66 +   tactics = insert eq_arith_tactic tac tactics});
    1.67  
    1.68  
    1.69  signature HOL_LIN_ARITH_DATA =
    1.70  sig
    1.71    include LIN_ARITH_DATA
    1.72 -  val fast_arith_split_limit : int ref
    1.73 +  val fast_arith_split_limit: int ConfigOption.T
    1.74 +  val setup_options: theory -> theory
    1.75  end;
    1.76  
    1.77  structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
    1.78  struct
    1.79  
    1.80 +val (fast_arith_split_limit, setup1) = ConfigOption.int "fast_arith_split_limit" 9;
    1.81 +val (fast_arith_neq_limit, setup2) = ConfigOption.int "fast_arith_neq_limit" 9;
    1.82 +val setup_options = setup1 #> setup2;
    1.83 +
    1.84 +
    1.85  (* internal representation of linear (in-)equations *)
    1.86  type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
    1.87  
    1.88 @@ -387,10 +398,10 @@
    1.89    | allows_lin_arith sg discrete U =
    1.90    (of_lin_arith_sort sg U, false);
    1.91  
    1.92 -fun decomp_typecheck (sg, discrete, inj_consts) (T : typ, xxx) : decompT option =
    1.93 +fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decompT option =
    1.94    case T of
    1.95      Type ("fun", [U, _]) =>
    1.96 -      (case allows_lin_arith sg discrete U of
    1.97 +      (case allows_lin_arith thy discrete U of
    1.98          (true, d) =>
    1.99            (case decomp0 inj_consts xxx of
   1.100              NONE                   => NONE
   1.101 @@ -411,12 +422,11 @@
   1.102    | decomp_negation data _ =
   1.103        NONE;
   1.104  
   1.105 -fun decomp sg : term -> decompT option =
   1.106 -let
   1.107 -  val {discrete, inj_consts, ...} = ArithTheoryData.get sg
   1.108 -in
   1.109 -  decomp_negation (sg, discrete, inj_consts)
   1.110 -end;
   1.111 +fun decomp ctxt : term -> decompT option =
   1.112 +  let
   1.113 +    val thy = ProofContext.theory_of ctxt
   1.114 +    val {discrete, inj_consts, ...} = get_arith_data ctxt
   1.115 +  in decomp_negation (thy, discrete, inj_consts) end;
   1.116  
   1.117  fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
   1.118    | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
   1.119 @@ -425,23 +435,11 @@
   1.120  fun number_of (n, T) = HOLogic.mk_number T n;
   1.121  
   1.122  (*---------------------------------------------------------------------------*)
   1.123 -(* code that performs certain goal transformations for linear arithmetic     *)
   1.124 -(*---------------------------------------------------------------------------*)
   1.125 -
   1.126 -(* A "do nothing" variant of pre_decomp and pre_tac:
   1.127 -
   1.128 -fun pre_decomp sg Ts termitems = [termitems];
   1.129 -fun pre_tac i = all_tac;
   1.130 -*)
   1.131 -
   1.132 -(*---------------------------------------------------------------------------*)
   1.133  (* the following code performs splitting of certain constants (e.g. min,     *)
   1.134  (* max) in a linear arithmetic problem; similar to what split_tac later does *)
   1.135  (* to the proof state                                                        *)
   1.136  (*---------------------------------------------------------------------------*)
   1.137  
   1.138 -val fast_arith_split_limit = ref 9;
   1.139 -
   1.140  (* checks if splitting with 'thm' is implemented                             *)
   1.141  
   1.142  fun is_split_thm (thm : thm) : bool =
   1.143 @@ -493,24 +491,24 @@
   1.144  (*        former can have a faster implementation as it does not need to be  *)
   1.145  (*        proof-producing).                                                  *)
   1.146  
   1.147 -fun split_once_items (sg : theory) (Ts : typ list, terms : term list) :
   1.148 +fun split_once_items ctxt (Ts : typ list, terms : term list) :
   1.149                       (typ list * term list) list option =
   1.150  let
   1.151 +  val thy = ProofContext.theory_of ctxt
   1.152    (* takes a list  [t1, ..., tn]  to the term                                *)
   1.153    (*   tn' --> ... --> t1' --> False  ,                                      *)
   1.154    (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   1.155 -  (* term list -> term *)
   1.156    fun REPEAT_DETERM_etac_rev_mp terms' =
   1.157      fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
   1.158 -  val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
   1.159 +  val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   1.160    val cmap       = Splitter.cmap_of_split_thms split_thms
   1.161 -  val splits     = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
   1.162 +  val splits     = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
   1.163 +  val split_limit = ConfigOption.get ctxt fast_arith_split_limit
   1.164  in
   1.165 -  if length splits > !fast_arith_split_limit then (
   1.166 -    tracing ("fast_arith_split_limit exceeded (current value is " ^
   1.167 -              string_of_int (!fast_arith_split_limit) ^ ")");
   1.168 -    NONE
   1.169 -  ) else (
   1.170 +  if length splits > split_limit then
   1.171 +   (tracing ("fast_arith_split_limit exceeded (current value is " ^
   1.172 +      string_of_int split_limit ^ ")"); NONE)
   1.173 +  else (
   1.174    case splits of [] =>
   1.175      (* split_tac would fail: no possible split *)
   1.176      NONE
   1.177 @@ -784,8 +782,8 @@
   1.178      (* implemented above, or 'is_split_thm' should be modified to filter it  *)
   1.179      (* out                                                                   *)
   1.180      | (t, ts) => (
   1.181 -      warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^
   1.182 -               " (with " ^ Int.toString (length ts) ^
   1.183 +      warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^
   1.184 +               " (with " ^ string_of_int (length ts) ^
   1.185                 " argument(s)) not implemented; proof reconstruction is likely to fail");
   1.186        NONE
   1.187      ))
   1.188 @@ -813,17 +811,17 @@
   1.189        | _                                   => false)
   1.190      terms;
   1.191  
   1.192 -fun pre_decomp sg (Ts : typ list, terms : term list) : (typ list * term list) list =
   1.193 +fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
   1.194  let
   1.195    (* repeatedly split (including newly emerging subgoals) until no further   *)
   1.196    (* splitting is possible                                                   *)
   1.197    fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
   1.198      | split_loop (subgoal::subgoals)                = (
   1.199 -        case split_once_items sg subgoal of
   1.200 +        case split_once_items ctxt subgoal of
   1.201            SOME new_subgoals => split_loop (new_subgoals @ subgoals)
   1.202          | NONE              => subgoal :: split_loop subgoals
   1.203        )
   1.204 -  fun is_relevant t  = isSome (decomp sg t)
   1.205 +  fun is_relevant t  = isSome (decomp ctxt t)
   1.206    (* filter_prems_tac is_relevant: *)
   1.207    val relevant_terms = filter_prems_tac_items is_relevant terms
   1.208    (* split_tac, NNF normalization: *)
   1.209 @@ -855,30 +853,29 @@
   1.210      full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
   1.211  in
   1.212  
   1.213 -fun split_once_tac (split_thms : thm list) (i : int) : tactic =
   1.214 -let
   1.215 -  fun cond_split_tac i st =
   1.216 -    let
   1.217 -      val subgoal = Logic.nth_prem (i, Thm.prop_of st)
   1.218 -      val Ts      = rev (map snd (Logic.strip_params subgoal))
   1.219 -      val concl   = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
   1.220 -      val cmap    = Splitter.cmap_of_split_thms split_thms
   1.221 -      val splits  = Splitter.split_posns cmap (theory_of_thm st) Ts concl
   1.222 -    in
   1.223 -      if length splits > !fast_arith_split_limit then
   1.224 -        no_tac st
   1.225 -      else
   1.226 -        split_tac split_thms i st
   1.227 -    end
   1.228 -in
   1.229 -  EVERY' [
   1.230 -    REPEAT_DETERM o etac rev_mp,
   1.231 -    cond_split_tac,
   1.232 -    rtac ccontr,
   1.233 -    prem_nnf_tac,
   1.234 -    TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
   1.235 -  ] i
   1.236 -end
   1.237 +fun split_once_tac ctxt split_thms =
   1.238 +  let
   1.239 +    val thy = ProofContext.theory_of ctxt
   1.240 +    val cond_split_tac = SUBGOAL (fn (subgoal, i) =>
   1.241 +      let
   1.242 +        val Ts = rev (map snd (Logic.strip_params subgoal))
   1.243 +        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
   1.244 +        val cmap = Splitter.cmap_of_split_thms split_thms
   1.245 +        val splits = Splitter.split_posns cmap thy Ts concl
   1.246 +        val split_limit = ConfigOption.get ctxt fast_arith_split_limit
   1.247 +      in
   1.248 +        if length splits > split_limit then no_tac
   1.249 +        else split_tac split_thms i
   1.250 +      end)
   1.251 +  in
   1.252 +    EVERY' [
   1.253 +      REPEAT_DETERM o etac rev_mp,
   1.254 +      cond_split_tac,
   1.255 +      rtac ccontr,
   1.256 +      prem_nnf_tac,
   1.257 +      TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
   1.258 +    ]
   1.259 +  end;
   1.260  
   1.261  end;  (* local *)
   1.262  
   1.263 @@ -887,22 +884,21 @@
   1.264  (* subgoals and finally attempt to solve them by finding an immediate        *)
   1.265  (* contradiction (i.e. a term and its negation) in their premises.           *)
   1.266  
   1.267 -fun pre_tac i st =
   1.268 +fun pre_tac ctxt i =
   1.269  let
   1.270 -  val sg            = theory_of_thm st
   1.271 -  val split_thms    = filter is_split_thm (#splits (ArithTheoryData.get sg))
   1.272 -  fun is_relevant t = isSome (decomp sg t)
   1.273 +  val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   1.274 +  fun is_relevant t = isSome (decomp ctxt t)
   1.275  in
   1.276    DETERM (
   1.277      TRY (filter_prems_tac is_relevant i)
   1.278        THEN (
   1.279 -        (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
   1.280 +        (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms))
   1.281            THEN_ALL_NEW
   1.282              (CONVERSION Drule.beta_eta_conversion
   1.283                THEN'
   1.284              (TRY o (etac notE THEN' eq_assume_tac)))
   1.285        ) i
   1.286 -  ) st
   1.287 +  )
   1.288  end;
   1.289  
   1.290  end;  (* LA_Data_Ref *)
   1.291 @@ -911,16 +907,14 @@
   1.292  structure Fast_Arith =
   1.293    Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
   1.294  
   1.295 -val fast_arith_tac         = Fast_Arith.lin_arith_tac false;
   1.296 +fun fast_arith_tac ctxt    = Fast_Arith.lin_arith_tac ctxt false;
   1.297  val fast_ex_arith_tac      = Fast_Arith.lin_arith_tac;
   1.298  val trace_arith            = Fast_Arith.trace;
   1.299 -val fast_arith_neq_limit   = Fast_Arith.fast_arith_neq_limit;
   1.300 -val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
   1.301  
   1.302  (* reduce contradictory <= to False.
   1.303     Most of the work is done by the cancel tactics. *)
   1.304  
   1.305 -val init_lin_arith_data =
   1.306 +val init_arith_data =
   1.307   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   1.308     {add_mono_thms = add_mono_thms @
   1.309      @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field},
   1.310 @@ -929,7 +923,9 @@
   1.311      lessD = lessD @ [thm "Suc_leI"],
   1.312      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
   1.313      simpset = HOL_basic_ss
   1.314 -      addsimps [@{thm "monoid_add_class.zero_plus.add_0_left"}, @{thm "monoid_add_class.zero_plus.add_0_right"},
   1.315 +      addsimps
   1.316 +       [@{thm "monoid_add_class.zero_plus.add_0_left"},
   1.317 +        @{thm "monoid_add_class.zero_plus.add_0_right"},
   1.318          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
   1.319          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
   1.320          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
   1.321 @@ -941,7 +937,7 @@
   1.322  
   1.323  val fast_nat_arith_simproc =
   1.324    Simplifier.simproc (the_context ()) "fast_nat_arith"
   1.325 -    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
   1.326 +    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc);
   1.327  
   1.328  (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   1.329  useful to detect inconsistencies among the premises for subgoals which are
   1.330 @@ -954,7 +950,7 @@
   1.331  
   1.332  local
   1.333  
   1.334 -fun raw_arith_tac ex i st =
   1.335 +fun raw_arith_tac ctxt ex =
   1.336    (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
   1.337       decomp sg"? -- but note that the test is applied to terms already before
   1.338       they are split/normalized) to speed things up in case there are lots of
   1.339 @@ -969,32 +965,30 @@
   1.340      (* fast_arith_split_limit may trigger.                                   *)
   1.341      (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
   1.342      (* some goals that fast_arith_tac alone would fail on.                   *)
   1.343 -    (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
   1.344 -    (fast_ex_arith_tac ex)
   1.345 -    i st;
   1.346 +    (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
   1.347 +    (fast_ex_arith_tac ctxt ex);
   1.348  
   1.349 -fun arith_theory_tac i st =
   1.350 -let
   1.351 -  val tactics = #tactics (ArithTheoryData.get (Thm.theory_of_thm st))
   1.352 -in
   1.353 -  FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) i st
   1.354 -end;
   1.355 +fun more_arith_tacs ctxt =
   1.356 +  let val tactics = #tactics (get_arith_data ctxt)
   1.357 +  in FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) end;
   1.358  
   1.359  in
   1.360  
   1.361 -  val simple_arith_tac = FIRST' [fast_arith_tac,
   1.362 -    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true];
   1.363 +fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   1.364 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true];
   1.365  
   1.366 -  val arith_tac = FIRST' [fast_arith_tac,
   1.367 -    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true,
   1.368 -    arith_theory_tac];
   1.369 +fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   1.370 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true,
   1.371 +  more_arith_tacs ctxt];
   1.372  
   1.373 -  val silent_arith_tac = FIRST' [fast_arith_tac,
   1.374 -    ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac false,
   1.375 -    arith_theory_tac];
   1.376 +fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt,
   1.377 +  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false,
   1.378 +  more_arith_tacs ctxt];
   1.379  
   1.380 -  fun arith_method prems =
   1.381 -    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
   1.382 +fun arith_method src =
   1.383 +  Method.syntax Args.bang_facts src
   1.384 +  #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
   1.385 +      HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt)));
   1.386  
   1.387  end;
   1.388  
   1.389 @@ -1045,12 +1039,14 @@
   1.390  (* theory setup *)
   1.391  
   1.392  val arith_setup =
   1.393 -  init_lin_arith_data #>
   1.394 -  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
   1.395 +  init_arith_data #>
   1.396 +  Simplifier.map_ss (fn ss => ss
   1.397      addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
   1.398 -    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
   1.399 -  Method.add_methods
   1.400 -    [("arith", (arith_method o fst) oo Method.syntax Args.bang_facts,
   1.401 -      "decide linear arithmethic")] #>
   1.402 -  Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
   1.403 -    "declaration of split rules for arithmetic procedure")];
   1.404 +    addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)) #>
   1.405 +  Context.mapping
   1.406 +   (LA_Data_Ref.setup_options #>
   1.407 +    Method.add_methods
   1.408 +      [("arith", arith_method,
   1.409 +        "decide linear arithmethic")] #>
   1.410 +    Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
   1.411 +      "declaration of split rules for arithmetic procedure")]) I;
     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jul 31 00:56:26 2007 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Jul 31 00:56:29 2007 +0200
     2.3 @@ -1,20 +1,14 @@
     2.4  (*  Title:      Provers/Arith/fast_lin_arith.ML
     2.5      ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1998  TU Munich
     2.8 -
     2.9 -A generic linear arithmetic package.
    2.10 -It provides two tactics
    2.11 +    Author:     Tobias Nipkow and Tjark Weber
    2.12  
    2.13 -    lin_arith_tac:         int -> tactic
    2.14 -cut_lin_arith_tac: thms -> int -> tactic
    2.15 -
    2.16 -and a simplification procedure
    2.17 +A generic linear arithmetic package.  It provides two tactics
    2.18 +(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
    2.19 +(lin_arith_simproc).
    2.20  
    2.21 -    lin_arith_prover: theory -> simpset -> term -> thm option
    2.22 -
    2.23 -Only take premises and conclusions into account that are already (negated)
    2.24 -(in)equations. lin_arith_prover tries to prove or disprove the term.
    2.25 +Only take premises and conclusions into account that are already
    2.26 +(negated) (in)equations. lin_arith_simproc tries to prove or disprove
    2.27 +the term.
    2.28  *)
    2.29  
    2.30  (* Debugging: set Fast_Arith.trace *)
    2.31 @@ -54,15 +48,21 @@
    2.32  
    2.33  signature LIN_ARITH_DATA =
    2.34  sig
    2.35 -  (* internal representation of linear (in-)equations: *)
    2.36 +  (*internal representation of linear (in-)equations:*)
    2.37    type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool
    2.38 -  val decomp: theory -> term -> decompT option
    2.39 -  val domain_is_nat : term -> bool
    2.40 -  (* preprocessing, performed on a representation of subgoals as list of premises: *)
    2.41 -  val pre_decomp: theory -> typ list * term list -> (typ list * term list) list
    2.42 -  (* preprocessing, performed on the goal -- must do the same as 'pre_decomp': *)
    2.43 -  val pre_tac   : int -> Tactical.tactic
    2.44 -  val number_of : IntInf.int * typ -> term
    2.45 +  val decomp: Proof.context -> term -> decompT option
    2.46 +  val domain_is_nat: term -> bool
    2.47 +
    2.48 +  (*preprocessing, performed on a representation of subgoals as list of premises:*)
    2.49 +  val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list
    2.50 +
    2.51 +  (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
    2.52 +  val pre_tac: Proof.context -> int -> tactic
    2.53 +  val number_of: IntInf.int * typ -> term
    2.54 +
    2.55 +  (*the limit on the number of ~= allowed; because each ~= is split
    2.56 +    into two cases, this can lead to an explosion*)
    2.57 +  val fast_arith_neq_limit: int ConfigOption.T
    2.58  end;
    2.59  (*
    2.60  decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
    2.61 @@ -92,31 +92,33 @@
    2.62                   lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
    2.63                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    2.64                       lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
    2.65 -                -> theory -> theory
    2.66 +                -> Context.generic -> Context.generic
    2.67    val trace: bool ref
    2.68 -  val fast_arith_neq_limit: int ref
    2.69 -  val lin_arith_prover: theory -> simpset -> term -> thm option
    2.70 -  val     lin_arith_tac:    bool -> int -> tactic
    2.71    val cut_lin_arith_tac: simpset -> int -> tactic
    2.72 +  val lin_arith_tac: Proof.context -> bool -> int -> tactic
    2.73 +  val lin_arith_simproc: simpset -> term -> thm option
    2.74  end;
    2.75  
    2.76 -functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC
    2.77 -                       and       LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH =
    2.78 +functor Fast_Lin_Arith
    2.79 +  (structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH =
    2.80  struct
    2.81  
    2.82  
    2.83  (** theory data **)
    2.84  
    2.85 -structure Data = TheoryDataFun
    2.86 +structure Data = GenericDataFun
    2.87  (
    2.88 -  type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    2.89 -            lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
    2.90 +  type T =
    2.91 +   {add_mono_thms: thm list,
    2.92 +    mult_mono_thms: thm list,
    2.93 +    inj_thms: thm list,
    2.94 +    lessD: thm list,
    2.95 +    neqE: thm list,
    2.96 +    simpset: Simplifier.simpset};
    2.97  
    2.98    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    2.99                 lessD = [], neqE = [], simpset = Simplifier.empty_ss};
   2.100 -  val copy = I;
   2.101    val extend = I;
   2.102 -
   2.103    fun merge _
   2.104      ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
   2.105        lessD = lessD1, neqE=neqE1, simpset = simpset1},
   2.106 @@ -131,6 +133,7 @@
   2.107  );
   2.108  
   2.109  val map_data = Data.map;
   2.110 +val get_data = Data.get o Context.Proof;
   2.111  
   2.112  
   2.113  
   2.114 @@ -409,11 +412,14 @@
   2.115  (* Translate back a proof.                                                   *)
   2.116  (* ------------------------------------------------------------------------- *)
   2.117  
   2.118 -fun trace_thm (msg : string) (th : thm) : thm =
   2.119 -    (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
   2.120 +fun trace_thm msg th =
   2.121 +  (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
   2.122  
   2.123 -fun trace_msg (msg : string) : unit =
   2.124 -    if !trace then tracing msg else ();
   2.125 +fun trace_term ctxt msg t =
   2.126 +  (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t)
   2.127 +
   2.128 +fun trace_msg msg =
   2.129 +  if !trace then tracing msg else ();
   2.130  
   2.131  (* FIXME OPTIMIZE!!!! (partly done already)
   2.132     Addition/Multiplication need i*t representation rather than t+t+...
   2.133 @@ -425,16 +431,18 @@
   2.134  with 0 <= n.
   2.135  *)
   2.136  local
   2.137 - exception FalseE of thm
   2.138 +  exception FalseE of thm
   2.139  in
   2.140 -fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm =
   2.141 -  let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
   2.142 -          Data.get sg;
   2.143 -      val simpset' = Simplifier.inherit_context ss simpset;
   2.144 -      val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
   2.145 +fun mkthm ss asms (just: injust) =
   2.146 +  let
   2.147 +    val ctxt = Simplifier.the_context ss;
   2.148 +    val thy = ProofContext.theory_of ctxt;
   2.149 +    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;
   2.150 +    val simpset' = Simplifier.inherit_context ss simpset;
   2.151 +    val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
   2.152                              map fst lhs  union  (map fst rhs  union  ats))
   2.153                          ([], List.mapPartial (fn thm => if Thm.no_prems thm
   2.154 -                                              then LA_Data.decomp sg (concl_of thm)
   2.155 +                                              then LA_Data.decomp ctxt (Thm.concl_of thm)
   2.156                                                else NONE) asms)
   2.157  
   2.158        fun add2 thm1 thm2 =
   2.159 @@ -465,15 +473,15 @@
   2.160                get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
   2.161              fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
   2.162              val cv = cvar(mth, hd(prems_of mth));
   2.163 -            val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
   2.164 +            val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv)))
   2.165          in instantiate ([],[(cv,ct)]) mth end
   2.166  
   2.167        fun simp thm =
   2.168          let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
   2.169          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
   2.170  
   2.171 -      fun mk (Asm i)              = trace_thm ("Asm " ^ Int.toString i) (nth asms i)
   2.172 -        | mk (Nat i)              = trace_thm ("Nat " ^ Int.toString i) (LA_Logic.mk_nat_thm sg (nth atoms i))
   2.173 +      fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
   2.174 +        | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   2.175          | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
   2.176          | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
   2.177          | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   2.178 @@ -550,22 +558,24 @@
   2.179    #> commas
   2.180    #> curry (op ^) "Counterexample (possibly spurious):\n";
   2.181  
   2.182 -fun trace_ex (sg, params, atoms, discr, n, hist : history) =
   2.183 +fun trace_ex ctxt params atoms discr n (hist: history) =
   2.184    case hist of
   2.185      [] => ()
   2.186    | (v, lineqs) :: hist' =>
   2.187 -    let val frees = map Free params
   2.188 -        fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
   2.189 -        val start = if v = ~1 then (hist', findex0 discr n lineqs)
   2.190 +      let
   2.191 +        val frees = map Free params
   2.192 +        fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t))
   2.193 +        val start =
   2.194 +          if v = ~1 then (hist', findex0 discr n lineqs)
   2.195            else (hist, replicate n Rat.zero)
   2.196 -        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr)
   2.197 -          (uncurry (fold (findex1 discr)) start))
   2.198 +        val ex = SOME (produce_ex (map show_term atoms ~~ discr)
   2.199 +            (uncurry (fold (findex1 discr)) start))
   2.200            handle NoEx => NONE
   2.201 -    in
   2.202 -      case ex of
   2.203 -        SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
   2.204 -      | NONE => warning "arith failed"
   2.205 -    end;
   2.206 +      in
   2.207 +        case ex of
   2.208 +          SOME s => (warning "arith failed - see trace for a counterexample"; tracing s)
   2.209 +        | NONE => warning "arith failed"
   2.210 +      end;
   2.211  
   2.212  (* ------------------------------------------------------------------------- *)
   2.213  
   2.214 @@ -594,8 +604,7 @@
   2.215  (*        failure as soon as a case could not be refuted; i.e. delay further *)
   2.216  (*        splitting until after a refutation for other cases has been found. *)
   2.217  
   2.218 -fun split_items sg (do_pre : bool) (Ts, terms) :
   2.219 -                (typ list * (LA_Data.decompT * int) list) list =
   2.220 +fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decompT * int) list) list =
   2.221  let
   2.222    (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
   2.223    (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
   2.224 @@ -632,11 +641,11 @@
   2.225  
   2.226    val result = (Ts, terms)
   2.227      |> (* user-defined preprocessing of the subgoal *)
   2.228 -       (if do_pre then LA_Data.pre_decomp sg else Library.single)
   2.229 +       (if do_pre then LA_Data.pre_decomp ctxt else Library.single)
   2.230      |> tap (fn subgoals => trace_msg ("Preprocessing yields " ^
   2.231           string_of_int (length subgoals) ^ " subgoal(s) total."))
   2.232      |> (* produce the internal encoding of (in-)equalities *)
   2.233 -       map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t))))
   2.234 +       map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t))))
   2.235      |> (* splitting of inequalities *)
   2.236         map (apsnd elim_neq)
   2.237      |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals)
   2.238 @@ -658,21 +667,22 @@
   2.239  fun discr (initems : (LA_Data.decompT * int) list) : bool list =
   2.240    map fst (Library.foldl add_datoms ([],initems));
   2.241  
   2.242 -fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) :
   2.243 +fun refutes ctxt params show_ex :
   2.244    (typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option =
   2.245  let
   2.246    fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss)
   2.247               (js : injust list) : injust list option =
   2.248 -    let val atoms = Library.foldl add_atoms ([], initems)
   2.249 -        val n = length atoms
   2.250 -        val mkleq = mklineq n atoms
   2.251 -        val ixs = 0 upto (n-1)
   2.252 -        val iatoms = atoms ~~ ixs
   2.253 -        val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
   2.254 -        val ineqs = map mkleq initems @ natlineqs
   2.255 +    let
   2.256 +      val atoms = Library.foldl add_atoms ([], initems)
   2.257 +      val n = length atoms
   2.258 +      val mkleq = mklineq n atoms
   2.259 +      val ixs = 0 upto (n - 1)
   2.260 +      val iatoms = atoms ~~ ixs
   2.261 +      val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
   2.262 +      val ineqs = map mkleq initems @ natlineqs
   2.263      in case elim (ineqs, []) of
   2.264           Success j =>
   2.265 -           (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")");
   2.266 +           (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")");
   2.267              refute initemss (js@[j]))
   2.268         | Failure hist =>
   2.269             (if not show_ex then
   2.270 @@ -685,25 +695,18 @@
   2.271                val new_names = map Name.bound (0 upto new_count)
   2.272                val params'   = (new_names @ map fst params) ~~ Ts
   2.273              in
   2.274 -              trace_ex (sg, params', atoms, discr initems, n, hist)
   2.275 +              trace_ex ctxt params' atoms (discr initems) n hist
   2.276              end; NONE)
   2.277      end
   2.278      | refute [] js = SOME js
   2.279  in refute end;
   2.280  
   2.281 -fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool)
   2.282 -           (do_pre : bool) (terms : term list) : injust list option =
   2.283 -  refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
   2.284 +fun refute ctxt params show_ex do_pre terms : injust list option =
   2.285 +  refutes ctxt params show_ex (split_items ctxt do_pre (map snd params, terms)) [];
   2.286  
   2.287  fun count P xs = length (filter P xs);
   2.288  
   2.289 -(* The limit on the number of ~= allowed.
   2.290 -   Because each ~= is split into two cases, this can lead to an explosion.
   2.291 -*)
   2.292 -val fast_arith_neq_limit = ref 9;
   2.293 -
   2.294 -fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool)
   2.295 -          (do_pre : bool) (Hs : term list) (concl : term) : injust list option =
   2.296 +fun prove ctxt (params : (string * Term.typ) list) show_ex do_pre Hs concl : injust list option =
   2.297    let
   2.298      val _ = trace_msg "prove:"
   2.299      (* append the negated conclusion to 'Hs' -- this corresponds to     *)
   2.300 @@ -712,14 +715,13 @@
   2.301      val Hs' = Hs @ [LA_Logic.neg_prop concl]
   2.302      fun is_neq NONE                 = false
   2.303        | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
   2.304 +    val neq_limit = ConfigOption.get ctxt LA_Data.fast_arith_neq_limit;
   2.305    in
   2.306 -    if count is_neq (map (LA_Data.decomp sg) Hs')
   2.307 -      > !fast_arith_neq_limit then (
   2.308 -      trace_msg ("fast_arith_neq_limit exceeded (current value is " ^
   2.309 -                   string_of_int (!fast_arith_neq_limit) ^ ")");
   2.310 -      NONE
   2.311 -    ) else
   2.312 -      refute sg params show_ex do_pre Hs'
   2.313 +    if count is_neq (map (LA_Data.decomp ctxt) Hs') > neq_limit then
   2.314 +     (trace_msg ("fast_arith_neq_limit exceeded (current value is " ^
   2.315 +        string_of_int neq_limit ^ ")"); NONE)
   2.316 +    else
   2.317 +      refute ctxt params show_ex do_pre Hs'
   2.318    end handle TERM ("neg_prop", _) =>
   2.319      (* since no meta-logic negation is available, we can only fail if   *)
   2.320      (* the conclusion is not of the form 'Trueprop $ _' (simply         *)
   2.321 @@ -729,48 +731,52 @@
   2.322  
   2.323  fun refute_tac ss (i, justs) =
   2.324    fn state =>
   2.325 -    let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^
   2.326 -                             Int.toString (length justs) ^ " justification(s)):") state
   2.327 -        val sg          = theory_of_thm state
   2.328 -        val {neqE, ...} = Data.get sg
   2.329 -        fun just1 j =
   2.330 -          (* eliminate inequalities *)
   2.331 -          REPEAT_DETERM (eresolve_tac neqE i) THEN
   2.332 -            PRIMITIVE (trace_thm "State after neqE:") THEN
   2.333 -            (* use theorems generated from the actual justifications *)
   2.334 -            METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
   2.335 -    in (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
   2.336 -       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
   2.337 -       (* user-defined preprocessing of the subgoal *)
   2.338 -       DETERM (LA_Data.pre_tac i) THEN
   2.339 -       PRIMITIVE (trace_thm "State after pre_tac:") THEN
   2.340 -       (* prove every resulting subgoal, using its justification *)
   2.341 -       EVERY (map just1 justs)
   2.342 +    let
   2.343 +      val ctxt = Simplifier.the_context ss;
   2.344 +      val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
   2.345 +                             string_of_int (length justs) ^ " justification(s)):") state
   2.346 +      val {neqE, ...} = get_data ctxt;
   2.347 +      fun just1 j =
   2.348 +        (* eliminate inequalities *)
   2.349 +        REPEAT_DETERM (eresolve_tac neqE i) THEN
   2.350 +          PRIMITIVE (trace_thm "State after neqE:") THEN
   2.351 +          (* use theorems generated from the actual justifications *)
   2.352 +          METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
   2.353 +    in
   2.354 +      (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
   2.355 +      DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
   2.356 +      (* user-defined preprocessing of the subgoal *)
   2.357 +      DETERM (LA_Data.pre_tac ctxt i) THEN
   2.358 +      PRIMITIVE (trace_thm "State after pre_tac:") THEN
   2.359 +      (* prove every resulting subgoal, using its justification *)
   2.360 +      EVERY (map just1 justs)
   2.361      end  state;
   2.362  
   2.363  (*
   2.364  Fast but very incomplete decider. Only premises and conclusions
   2.365  that are already (negated) (in)equations are taken into account.
   2.366  *)
   2.367 -fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) =
   2.368 -  SUBGOAL (fn (A,_) =>
   2.369 -  let val params = rev (Logic.strip_params A)
   2.370 -      val Hs     = Logic.strip_assums_hyp A
   2.371 -      val concl  = Logic.strip_assums_concl A
   2.372 -  in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
   2.373 -     case prove (Thm.theory_of_thm st) params show_ex true Hs concl of
   2.374 -       NONE => (trace_msg "Refutation failed."; no_tac)
   2.375 -     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
   2.376 -  end) i st;
   2.377 +fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) =>
   2.378 +  let
   2.379 +    val ctxt = Simplifier.the_context ss
   2.380 +    val params = rev (Logic.strip_params A)
   2.381 +    val Hs = Logic.strip_assums_hyp A
   2.382 +    val concl = Logic.strip_assums_concl A
   2.383 +    val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A
   2.384 +  in
   2.385 +    case prove ctxt params show_ex true Hs concl of
   2.386 +      NONE => (trace_msg "Refutation failed."; no_tac)
   2.387 +    | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
   2.388 +  end);
   2.389  
   2.390 -fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) =
   2.391 -  simpset_lin_arith_tac
   2.392 -    (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
   2.393 -    show_ex i st;
   2.394 +fun cut_lin_arith_tac ss =
   2.395 +  cut_facts_tac (Simplifier.prems_of_ss ss) THEN'
   2.396 +  simpset_lin_arith_tac ss false;
   2.397  
   2.398 -fun cut_lin_arith_tac (ss : simpset) (i : int) =
   2.399 -  cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
   2.400 -  simpset_lin_arith_tac ss false i;
   2.401 +fun lin_arith_tac ctxt =
   2.402 +  simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss);
   2.403 +
   2.404 +
   2.405  
   2.406  (** Forward proof from theorems **)
   2.407  
   2.408 @@ -794,8 +800,8 @@
   2.409      val (_, ct2)   = Thm.dest_comb Ict2
   2.410  in (ct1, ct2) end;
   2.411  
   2.412 -fun splitasms (sg : theory) (asms : thm list) : splittree =
   2.413 -let val {neqE, ...} = Data.get sg
   2.414 +fun splitasms ctxt (asms : thm list) : splittree =
   2.415 +let val {neqE, ...} = get_data ctxt
   2.416      fun elim_neq (asms', []) = Tip (rev asms')
   2.417        | elim_neq (asms', asm::asms) =
   2.418        (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
   2.419 @@ -808,70 +814,52 @@
   2.420        | NONE => elim_neq (asm::asms', asms))
   2.421  in elim_neq ([], asms) end;
   2.422  
   2.423 -fun fwdproof (ctxt : theory * simpset) (Tip asms : splittree) (j::js : injust list) =
   2.424 -    (mkthm ctxt asms j, js)
   2.425 -  | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js =
   2.426 -    let val (thm1, js1) = fwdproof ctxt tree1 js
   2.427 -        val (thm2, js2) = fwdproof ctxt tree2 js1
   2.428 +fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js)
   2.429 +  | fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js =
   2.430 +      let
   2.431 +        val (thm1, js1) = fwdproof ss tree1 js
   2.432 +        val (thm2, js2) = fwdproof ss tree2 js1
   2.433          val thm1' = implies_intr ct1 thm1
   2.434          val thm2' = implies_intr ct2 thm2
   2.435 -    in (thm2' COMP (thm1' COMP thm), js2) end;
   2.436 -(* needs handle THM _ => NONE ? *)
   2.437 +      in (thm2' COMP (thm1' COMP thm), js2) end;
   2.438 +      (* FIXME needs handle THM _ => NONE ? *)
   2.439  
   2.440 -fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option =
   2.441 -let
   2.442 -(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *)
   2.443 -(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *)
   2.444 -(* but beware: this can be a significant performance issue.                      *)
   2.445 -    (* There is no "forward version" of 'pre_tac'.  Therefore we combine the     *)
   2.446 -    (* available theorems into a single proof state and perform "backward proof" *)
   2.447 -    (* using 'refute_tac'.                                                       *)
   2.448 -(*
   2.449 -    val Hs    = map prop_of thms
   2.450 -    val Prop  = fold (curry Logic.mk_implies) (rev Hs) Tconcl
   2.451 -    val cProp = cterm_of sg Prop
   2.452 -    val concl = Goal.init cProp
   2.453 -                  |> refute_tac ss (1, js)
   2.454 -                  |> Seq.hd
   2.455 -                  |> Goal.finish
   2.456 -                  |> fold (fn thA => fn thAB => implies_elim thAB thA) thms
   2.457 -*)
   2.458 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
   2.459 -    val nTconcl       = LA_Logic.neg_prop Tconcl
   2.460 -    val cnTconcl      = cterm_of sg nTconcl
   2.461 -    val nTconclthm    = assume cnTconcl
   2.462 -    val tree          = splitasms sg (thms @ [nTconclthm])
   2.463 -    val (Falsethm, _) = fwdproof ctxt tree js
   2.464 -    val contr         = if pos then LA_Logic.ccontr else LA_Logic.notI
   2.465 -    val concl         = implies_intr cnTconcl Falsethm COMP contr
   2.466 -in SOME (trace_thm "Proved by lin. arith. prover:"
   2.467 -          (LA_Logic.mk_Eq concl)) end
   2.468 -(* in case concl contains ?-var, which makes assume fail: *)
   2.469 -handle THM _ => NONE;
   2.470 +fun prover ss thms Tconcl (js : injust list) pos : thm option =
   2.471 +  let
   2.472 +    val ctxt = Simplifier.the_context ss
   2.473 +    val thy = ProofContext.theory_of ctxt
   2.474 +    val nTconcl = LA_Logic.neg_prop Tconcl
   2.475 +    val cnTconcl = cterm_of thy nTconcl
   2.476 +    val nTconclthm = assume cnTconcl
   2.477 +    val tree = splitasms ctxt (thms @ [nTconclthm])
   2.478 +    val (Falsethm, _) = fwdproof ss tree js
   2.479 +    val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
   2.480 +    val concl = implies_intr cnTconcl Falsethm COMP contr
   2.481 +  in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
   2.482 +  (*in case concl contains ?-var, which makes assume fail:*)   (* FIXME Variable.import_terms *)
   2.483 +  handle THM _ => NONE;
   2.484  
   2.485  (* PRE: concl is not negated!
   2.486     This assumption is OK because
   2.487 -   1. lin_arith_prover tries both to prove and disprove concl and
   2.488 -   2. lin_arith_prover is applied by the simplifier which
   2.489 +   1. lin_arith_simproc tries both to prove and disprove concl and
   2.490 +   2. lin_arith_simproc is applied by the Simplifier which
   2.491        dives into terms and will thus try the non-negated concl anyway.
   2.492  *)
   2.493 -
   2.494 -fun lin_arith_prover sg ss (concl : term) : thm option =
   2.495 -let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
   2.496 -    val Hs = map prop_of thms
   2.497 +fun lin_arith_simproc ss concl =
   2.498 +  let
   2.499 +    val ctxt = Simplifier.the_context ss
   2.500 +    val thms = List.concat (map LA_Logic.atomize (Simplifier.prems_of_ss ss))
   2.501 +    val Hs = map Thm.prop_of thms
   2.502      val Tconcl = LA_Logic.mk_Trueprop concl
   2.503 -(*
   2.504 -    val _ = trace_msg "lin_arith_prover"
   2.505 -    val _ = map (trace_thm "thms:") thms
   2.506 -    val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl)
   2.507 -*)
   2.508 -in case prove sg [] false false Hs Tconcl of (* concl provable? *)
   2.509 -     SOME js => prover (sg, ss) thms Tconcl js true
   2.510 -   | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl
   2.511 -          in case prove sg [] false false Hs nTconcl of (* ~concl provable? *)
   2.512 -               SOME js => prover (sg, ss) thms nTconcl js false
   2.513 -             | NONE => NONE
   2.514 -          end
   2.515 -end;
   2.516 +  in
   2.517 +    case prove ctxt [] false false Hs Tconcl of (* concl provable? *)
   2.518 +      SOME js => prover ss thms Tconcl js true
   2.519 +    | NONE =>
   2.520 +        let val nTconcl = LA_Logic.neg_prop Tconcl in
   2.521 +          case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *)
   2.522 +            SOME js => prover ss thms nTconcl js false
   2.523 +          | NONE => NONE
   2.524 +        end
   2.525 +  end;
   2.526  
   2.527  end;