Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
authorchaieb
Tue Jun 12 10:15:40 2007 +0200 (2007-06-12)
changeset 23333ec5b4ab52026
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
     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.4    arith_tactic_add 
     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.20 + val addN = "add"
    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 {*