more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
authorwenzelm
Fri Aug 16 21:33:36 2013 +0200 (2013-08-16)
changeset 530438cbfbeb566a4
parent 53042 aa0322a65bea
child 53044 be27b6be8027
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
src/HOL/Probability/Measurable.thy
src/HOL/Probability/measurable.ML
     1.1 --- a/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:28:05 2013 +0200
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Fri Aug 16 21:33:36 2013 +0200
     1.3 @@ -46,10 +46,24 @@
     1.4  
     1.5  ML_file "measurable.ML"
     1.6  
     1.7 -attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
     1.8 -attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
     1.9 -attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
    1.10 -method_setup measurable = {* Measurable.method *} "measurability prover"
    1.11 +attribute_setup measurable = {*
    1.12 +  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    1.13 +    Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    1.14 +    (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
    1.15 +*} "declaration of measurability theorems"
    1.16 +
    1.17 +attribute_setup measurable_dest = {*
    1.18 +  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
    1.19 +*} "add dest rule for measurability prover"
    1.20 +
    1.21 +attribute_setup measurable_app = {*
    1.22 +  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
    1.23 +*} "add application rule for measurability prover"
    1.24 +
    1.25 +method_setup measurable = {*
    1.26 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
    1.27 +*} "measurability prover"
    1.28 +
    1.29  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.30  
    1.31  declare
     2.1 --- a/src/HOL/Probability/measurable.ML	Fri Aug 16 21:28:05 2013 +0200
     2.2 +++ b/src/HOL/Probability/measurable.ML	Fri Aug 16 21:33:36 2013 +0200
     2.3 @@ -8,13 +8,13 @@
     2.4  sig
     2.5    datatype level = Concrete | Generic
     2.6  
     2.7 -  val simproc : Proof.context -> cterm -> thm option
     2.8 -  val method : (Proof.context -> Method.method) context_parser
     2.9 +  val add_app : thm -> Context.generic -> Context.generic
    2.10 +  val add_dest : thm -> Context.generic -> Context.generic
    2.11 +  val add_thm : bool * level -> thm -> Context.generic -> Context.generic
    2.12 +
    2.13    val measurable_tac : Proof.context -> thm list -> tactic
    2.14  
    2.15 -  val attr : attribute context_parser
    2.16 -  val dest_attr : attribute context_parser
    2.17 -  val app_attr : attribute context_parser
    2.18 +  val simproc : Proof.context -> cterm -> thm option
    2.19  
    2.20    val get : level -> Proof.context -> thm list
    2.21    val get_all : Proof.context -> thm list
    2.22 @@ -213,21 +213,6 @@
    2.23  fun measurable_tac ctxt facts =
    2.24    TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
    2.25  
    2.26 -val attr_add = Thm.declaration_attribute o add_thm;
    2.27 -
    2.28 -val attr : attribute context_parser =
    2.29 -  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    2.30 -     Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add);
    2.31 -
    2.32 -val dest_attr : attribute context_parser =
    2.33 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
    2.34 -
    2.35 -val app_attr : attribute context_parser =
    2.36 -  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
    2.37 -
    2.38 -val method : (Proof.context -> Method.method) context_parser =
    2.39 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
    2.40 -
    2.41  fun simproc ctxt redex =
    2.42    let
    2.43      val t = HOLogic.mk_Trueprop (term_of redex);