added simproc_setup;
authorwenzelm
Sun Jan 28 23:29:16 2007 +0100 (2007-01-28 ago)
changeset 222020544af1a5117
parent 22201 6fe46a7259ec
child 22203 efc0cdc01307
added simproc_setup;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jan 28 23:29:15 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jan 28 23:29:16 2007 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
     1.5    val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
     1.6    val declaration: string -> local_theory -> local_theory
     1.7 +  val simproc_setup: string * string list * string -> local_theory -> local_theory
     1.8    val have: ((string * Attrib.src list) * (string * string list) list) list ->
     1.9      bool -> Proof.state -> Proof.state
    1.10    val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    1.11 @@ -238,6 +239,16 @@
    1.12    #> Context.proof_map;
    1.13  
    1.14  
    1.15 +(* simprocs *)
    1.16 +
    1.17 +fun simproc_setup (name, pats, proc) =
    1.18 +  ML_Context.use_let
    1.19 +    "val simproc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
    1.20 +  ("Context.map_proof (Simplifier.def_simproc " ^ ML_Syntax.print_string name ^ " " ^
    1.21 +    ML_Syntax.print_list ML_Syntax.print_string pats ^ " simproc)") proc
    1.22 +  |> Context.proof_map;
    1.23 +
    1.24 +
    1.25  (* goals *)
    1.26  
    1.27  fun goal opt_chain goal stmt int =
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:15 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:16 2007 +0100
     2.3 @@ -311,6 +311,12 @@
     2.4      (P.opt_target -- P.text
     2.5      >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
     2.6  
     2.7 +val simproc_setupP =
     2.8 +  OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     2.9 +    (P.opt_target --
    2.10 +      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text
    2.11 +    >> (fn (((loc, x), y), z) => Toplevel.local_theory loc (IsarCmd.simproc_setup (x, y, z))));
    2.12 +
    2.13  
    2.14  (* translation functions *)
    2.15  
    2.16 @@ -929,9 +935,10 @@
    2.17    constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
    2.18    theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
    2.19    ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
    2.20 -  parse_ast_translationP, parse_translationP, print_translationP,
    2.21 -  typed_print_translationP, print_ast_translationP,
    2.22 -  token_translationP, oracleP, contextP, localeP,
    2.23 +  simproc_setupP, parse_ast_translationP, parse_translationP,
    2.24 +  print_translationP, typed_print_translationP,
    2.25 +  print_ast_translationP, token_translationP, oracleP, contextP,
    2.26 +  localeP,
    2.27    (*proof commands*)
    2.28    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    2.29    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,