src/HOL/Tools/Meson/meson.ML
changeset 42739 017e5dac8642
parent 42616 92715b528e78
child 42747 f132d13fcf75
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -9,12 +9,14 @@
     1.4  signature MESON =
     1.5  sig
     1.6    val trace : bool Config.T
     1.7 +  val unfold_set_consts : bool Config.T
     1.8    val max_clauses : int Config.T
     1.9    val term_pair_of: indexname * (typ * 'a) -> term * 'a
    1.10    val size_of_subgoals: thm -> int
    1.11    val has_too_many_clauses: Proof.context -> term -> bool
    1.12    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
    1.13    val finish_cnf: thm list -> thm list
    1.14 +  val unfold_set_const_simps : Proof.context -> thm list
    1.15    val presimplify: thm -> thm
    1.16    val make_nnf: Proof.context -> thm -> thm
    1.17    val choice_theorems : theory -> thm list
    1.18 @@ -49,8 +51,10 @@
    1.19  
    1.20  fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.21  
    1.22 -val max_clauses_default = 60
    1.23 -val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
    1.24 +val unfold_set_consts =
    1.25 +  Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false)
    1.26 +
    1.27 +val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60)
    1.28  
    1.29  (*No known example (on 1-5-2007) needs even thirty*)
    1.30  val iter_deepen_limit = 50;
    1.31 @@ -555,6 +559,10 @@
    1.32      handle THM ("tryres", _, _) => th
    1.33    else th
    1.34  
    1.35 +fun unfold_set_const_simps ctxt =
    1.36 +  if Config.get ctxt unfold_set_consts then @{thms Collect_def_raw mem_def_raw}
    1.37 +  else []
    1.38 +
    1.39  (*The simplification removes defined quantifiers and occurrences of True and False.
    1.40    nnf_ss also includes the one-point simprocs,
    1.41    which are needed to avoid the various one-point theorems from generating junk clauses.*)