updated to named_theorems;
authorwenzelm
Sat Aug 16 20:46:59 2014 +0200 (2014-08-16)
changeset 579620284a7d083be
parent 57961 10b2f60b70f0
child 57963 cb67fac9bd89
updated to named_theorems;
src/HOL/HOL.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 16 20:27:51 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 20:46:59 2014 +0200
     1.3 @@ -1965,29 +1965,12 @@
     1.4  
     1.5  subsection {* Preprocessing for the predicate compiler *}
     1.6  
     1.7 -ML {*
     1.8 -structure Predicate_Compile_Alternative_Defs = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding code_pred_def}
    1.11 -  val description = "alternative definitions of constants for the Predicate Compiler"
    1.12 -)
    1.13 -structure Predicate_Compile_Inline_Defs = Named_Thms
    1.14 -(
    1.15 -  val name = @{binding code_pred_inline}
    1.16 -  val description = "inlining definitions for the Predicate Compiler"
    1.17 -)
    1.18 -structure Predicate_Compile_Simps = Named_Thms
    1.19 -(
    1.20 -  val name = @{binding code_pred_simp}
    1.21 -  val description = "simplification rules for the optimisations in the Predicate Compiler"
    1.22 -)
    1.23 -*}
    1.24 -
    1.25 -setup {*
    1.26 -  Predicate_Compile_Alternative_Defs.setup
    1.27 -  #> Predicate_Compile_Inline_Defs.setup
    1.28 -  #> Predicate_Compile_Simps.setup
    1.29 -*}
    1.30 +named_theorems code_pred_def
    1.31 +  "alternative definitions of constants for the Predicate Compiler"
    1.32 +named_theorems code_pred_inline
    1.33 +  "inlining definitions for the Predicate Compiler"
    1.34 +named_theorems code_pred_simp
    1.35 +  "simplification rules for the optimisations in the Predicate Compiler"
    1.36  
    1.37  
    1.38  subsection {* Legacy tactics and ML bindings *}
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 16 20:27:51 2014 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 16 20:46:59 2014 +0200
     2.3 @@ -1047,7 +1047,8 @@
     2.4      val thy = Proof_Context.theory_of ctxt
     2.5      val ((((full_constname, constT), vs'), intro), thy1) =
     2.6        Predicate_Compile_Aux.define_quickcheck_predicate t' thy
     2.7 -    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     2.8 +    val thy2 =
     2.9 +      Context.theory_map (Named_Theorems.add_thm @{named_theorems code_pred_def} intro) thy1
    2.10      val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
    2.11      val ctxt' = Proof_Context.init_global thy3
    2.12      val _ = tracing "Generating prolog program..."
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 16 20:27:51 2014 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Aug 16 20:46:59 2014 +0200
     3.3 @@ -1042,7 +1042,7 @@
     3.4    let
     3.5      val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     3.6      val process =
     3.7 -      rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
     3.8 +      rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp})
     3.9      fun process_False intro_t =
    3.10        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
    3.11        then NONE else SOME intro_t
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 16 20:27:51 2014 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 16 20:46:59 2014 +0200
     4.3 @@ -161,8 +161,8 @@
     4.4  fun inline_equations thy th =
     4.5    let
     4.6      val ctxt = Proof_Context.init_global thy
     4.7 -    val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
     4.8 -    val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
     4.9 +    val inline_defs = Named_Theorems.get ctxt @{named_theorems code_pred_inline}
    4.10 +    val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th
    4.11      (*val _ = print_step options
    4.12        ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
    4.13         ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
    4.14 @@ -208,12 +208,12 @@
    4.15            NONE
    4.16      fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
    4.17      val spec =
    4.18 -      (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
    4.19 +      (case filter_defs (Named_Theorems.get ctxt @{named_theorems code_pred_def}) of
    4.20          [] =>
    4.21            (case Spec_Rules.retrieve ctxt t of
    4.22              [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
    4.23            | ((_, (_, ths)) :: _) => filter_defs ths)
    4.24 -      | ths => rev ths)
    4.25 +      | ths => ths)
    4.26      val _ =
    4.27        if show_intermediate_results options then
    4.28          tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Aug 16 20:27:51 2014 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Aug 16 20:46:59 2014 +0200
     5.3 @@ -231,7 +231,8 @@
     5.4      val thy = Proof_Context.theory_of ctxt
     5.5      val ((((full_constname, constT), vs'), intro), thy1) =
     5.6        Predicate_Compile_Aux.define_quickcheck_predicate t' thy
     5.7 -    val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     5.8 +    val thy2 =
     5.9 +      Context.theory_map (Named_Theorems.add_thm @{named_theorems code_pred_def} intro) thy1
    5.10      val (thy3, _) = cpu_time "predicate preprocessing"
    5.11          (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)
    5.12      val (thy4, _) = cpu_time "random_dseq core compilation"