author chaieb Tue Jun 12 10:15:40 2007 +0200 (2007-06-12) changeset 23333 ec5b4ab52026 parent 23332 b91295432e6d child 23334 2443224cf6d7
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
 src/HOL/Presburger.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Presburger.thy	Tue Jun 12 10:15:32 2007 +0200
1.2 +++ b/src/HOL/Presburger.thy	Tue Jun 12 10:15:40 2007 +0200
1.3 @@ -433,16 +433,28 @@
1.5      (mk_arith_tactic "presburger" (fn i => fn st =>
1.6         (warning "Trying Presburger arithmetic ...";
1.7 -    Presburger.cooper_tac true ((ProofContext.init o theory_of_thm) st) i st)))
1.8 +    Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
1.9    (* FIXME!!!!!!! get the right context!!*)
1.10  *}
1.11 -method_setup presburger = {* Method.simple_args (Scan.optional (Args.\$\$\$ "elim" >> K false) true)
1.12 -  (fn q => fn ctxt =>  Method.SIMPLE_METHOD' (Presburger.cooper_tac q ctxt))*} ""
1.13 -(*
1.14 +
1.15  method_setup presburger = {*
1.16 -  Method.ctxt_args (Method.SIMPLE_METHOD' o (Presburger.cooper_tac true))
1.17 +let
1.18 + fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
1.19 + fun simple_keyword k = Scan.lift (Args.\$\$\$ k) >> K ()
1.21 + val delN = "del"
1.22 + val elimN = "elim"
1.23 + val any_keyword = keyword addN || keyword delN || simple_keyword elimN
1.24 + val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
1.25 +in
1.26 +  fn src => Method.syntax
1.27 +   ((Scan.optional (simple_keyword elimN >> K false) true) --
1.28 +    (Scan.optional (keyword addN |-- thms) []) --
1.29 +    (Scan.optional (keyword delN |-- thms) [])) src
1.30 +  #> (fn (((elim, add_ths), del_ths),ctxt) =>
1.31 +         Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
1.32 +end
1.33  *} ""
1.34 -*)
1.35
1.36  subsection {* Code generator setup *}
1.37  text {*
```