add del option to measurable;
authorAndreas Lochbihler
Tue Nov 11 08:57:46 2014 +0100 (2014-11-11)
changeset 58965a62cdcc5344b
parent 58964 a93d114eaa5d
child 58966 0297e1277ed2
child 58971 8c9a319821b3
add del option to measurable;
make measurability rules available as dynamic theorem;
src/HOL/Probability/Measurable.thy
src/HOL/Probability/measurable.ML
     1.1 --- a/src/HOL/Probability/Measurable.thy	Tue Nov 11 00:11:11 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Tue Nov 11 08:57:46 2014 +0100
     1.3 @@ -51,9 +51,10 @@
     1.4  ML_file "measurable.ML"
     1.5  
     1.6  attribute_setup measurable = {*
     1.7 -  Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
     1.8 -    Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
     1.9 -    (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm))
    1.10 +  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
    1.11 +    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
    1.12 +      Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    1.13 +    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
    1.14  *} "declaration of measurability theorems"
    1.15  
    1.16  attribute_setup measurable_dest = {*
    1.17 @@ -70,6 +71,10 @@
    1.18  
    1.19  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.20  
    1.21 +setup {*
    1.22 +  Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of)
    1.23 +*}
    1.24 +
    1.25  declare
    1.26    measurable_compose_rev[measurable_dest]
    1.27    pred_sets1[measurable_dest]
     2.1 --- a/src/HOL/Probability/measurable.ML	Tue Nov 11 00:11:11 2014 +0100
     2.2 +++ b/src/HOL/Probability/measurable.ML	Tue Nov 11 08:57:46 2014 +0100
     2.3 @@ -11,6 +11,8 @@
     2.4    val add_app : thm -> Context.generic -> Context.generic
     2.5    val add_dest : thm -> Context.generic -> Context.generic
     2.6    val add_thm : bool * level -> thm -> Context.generic -> Context.generic
     2.7 +  val del_thm : bool * level -> thm -> Context.generic -> Context.generic
     2.8 +  val add_del_thm : bool -> (bool * level) -> thm -> Context.generic -> Context.generic
     2.9  
    2.10    val measurable_tac : Proof.context -> thm list -> tactic
    2.11  
    2.12 @@ -20,7 +22,6 @@
    2.13    val get_all : Proof.context -> thm list
    2.14  
    2.15    val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
    2.16 -
    2.17  end ;
    2.18  
    2.19  structure Measurable : MEASURABLE =
    2.20 @@ -77,6 +78,7 @@
    2.21  
    2.22  fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
    2.23  fun add thms' = update (fold Item_Net.update thms');
    2.24 +fun del thms' = update (fold Item_Net.remove thms');
    2.25  
    2.26  val get_dest = Item_Net.content o #dest_thms o Data.get;
    2.27  val add_dest = Data.map o map_dest_thms o Item_Net.update;
    2.28 @@ -93,7 +95,12 @@
    2.29  fun import_theorem ctxt thm = if is_too_generic thm then [] else
    2.30    [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
    2.31  
    2.32 -fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
    2.33 +fun add_del_thm_gen f (raw, lv) thm ctxt = f (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
    2.34 +
    2.35 +val add_thm = add_del_thm_gen add;
    2.36 +val del_thm = add_del_thm_gen del;
    2.37 +fun add_del_thm true = add_thm
    2.38 +  | add_del_thm false = del_thm
    2.39  
    2.40  fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
    2.41