src/HOL/Decision_Procs/mir_tac.ML
changeset 31240 2c20bcd70fbe
parent 30939 207ec81543f6
child 31790 05c92381363c
     1.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon May 25 12:29:29 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon May 25 12:46:14 2009 +0200
     1.3 @@ -2,6 +2,13 @@
     1.4      Author:     Amine Chaieb, TU Muenchen
     1.5  *)
     1.6  
     1.7 +signature MIR_TAC =
     1.8 +sig
     1.9 +  val trace: bool ref
    1.10 +  val mir_tac: Proof.context -> bool -> int -> tactic
    1.11 +  val setup: theory -> theory
    1.12 +end
    1.13 +
    1.14  structure Mir_Tac =
    1.15  struct
    1.16  
    1.17 @@ -82,9 +89,9 @@
    1.18  
    1.19  
    1.20  fun mir_tac ctxt q i = 
    1.21 -    (ObjectLogic.atomize_prems_tac i)
    1.22 -        THEN (simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i)
    1.23 -        THEN (REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"},@{thm "abs_split"}] i))
    1.24 +    ObjectLogic.atomize_prems_tac i
    1.25 +        THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
    1.26 +        THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
    1.27          THEN (fn st =>
    1.28    let
    1.29      val g = List.nth (prems_of st, i - 1)
    1.30 @@ -143,22 +150,15 @@
    1.31        THEN tac) st
    1.32    end handle Subscript => no_tac st);
    1.33  
    1.34 -fun mir_args meth =
    1.35 - let val parse_flag = 
    1.36 -         Args.$$$ "no_quantify" >> (K (K false));
    1.37 - in
    1.38 -   Method.simple_args 
    1.39 -  (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
    1.40 -    curry (Library.foldl op |>) true)
    1.41 -    (fn q => fn ctxt => meth ctxt q)
    1.42 -  end;
    1.43 -
    1.44 -fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
    1.45 -
    1.46  val setup =
    1.47 -  Method.add_method ("mir",
    1.48 -     mir_args mir_method,
    1.49 -     "decision procedure for MIR arithmetic");
    1.50 -
    1.51 +  Method.setup @{binding mir}
    1.52 +    let
    1.53 +      val parse_flag = Args.$$$ "no_quantify" >> K (K false)
    1.54 +    in
    1.55 +      Scan.lift (Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
    1.56 +        curry (Library.foldl op |>) true) >>
    1.57 +      (fn q => fn ctxt => SIMPLE_METHOD' (mir_tac ctxt q))
    1.58 +    end
    1.59 +    "decision procedure for MIR arithmetic";
    1.60  
    1.61  end