src/HOL/Probability/measurable.ML
changeset 51717 9e7d1c139569
parent 50387 3d8863c41fe8
child 53043 8cbfbeb566a4
     1.1 --- a/src/HOL/Probability/measurable.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Probability/measurable.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    datatype level = Concrete | Generic
     1.6  
     1.7 -  val simproc : simpset -> cterm -> thm option
     1.8 +  val simproc : Proof.context -> cterm -> thm option
     1.9    val method : (Proof.context -> Method.method) context_parser
    1.10    val measurable_tac : Proof.context -> thm list -> tactic
    1.11  
    1.12 @@ -151,7 +151,8 @@
    1.13      in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
    1.14      handle TERM _ => no_tac) 1)
    1.15  
    1.16 -fun measurable_tac' ctxt ss facts = let
    1.17 +fun measurable_tac' ctxt facts =
    1.18 +  let
    1.19  
    1.20      val imported_thms =
    1.21        (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
    1.22 @@ -202,7 +203,7 @@
    1.23  
    1.24      val depth_measurable_tac = REPEAT_cnt (fn n =>
    1.25         (COND (is_cond_formula 1)
    1.26 -        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ss) 1))
    1.27 +        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ctxt) 1))
    1.28          ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
    1.29            (split_app_tac ctxt 1) APPEND
    1.30            (splitter 1)))) 0
    1.31 @@ -210,7 +211,7 @@
    1.32    in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
    1.33  
    1.34  fun measurable_tac ctxt facts =
    1.35 -  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
    1.36 +  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
    1.37  
    1.38  val attr_add = Thm.declaration_attribute o add_thm;
    1.39  
    1.40 @@ -227,11 +228,11 @@
    1.41  val method : (Proof.context -> Method.method) context_parser =
    1.42    Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
    1.43  
    1.44 -fun simproc ss redex = let
    1.45 -    val ctxt = Simplifier.the_context ss;
    1.46 +fun simproc ctxt redex =
    1.47 +  let
    1.48      val t = HOLogic.mk_Trueprop (term_of redex);
    1.49      fun tac {context = ctxt, prems = _ } =
    1.50 -      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
    1.51 +      SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt));
    1.52    in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
    1.53  
    1.54  end