added unfold set constant functionality to Meson/Metis -- disabled by default for now
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42739017e5dac8642
parent 42738 2a9dcff63b80
child 42740 31334a7b109d
added unfold set constant functionality to Meson/Metis -- disabled by default for now
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactics.ML
     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.*)
     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -320,6 +320,7 @@
     2.4           |> new_skolemizer ? forall_intr_vars
     2.5      val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     2.6      val th = th |> Conv.fconv_rule Object_Logic.atomize
     2.7 +                |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
     2.8                  |> extensionalize_theorem
     2.9                  |> make_nnf ctxt
    2.10    in
     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
     3.3 @@ -141,10 +141,11 @@
     3.4      else th :: Meson.make_clauses_unsorted [th']
     3.5    end
     3.6  
     3.7 -val neg_clausify =
     3.8 +fun neg_clausify ctxt =
     3.9    single
    3.10    #> Meson.make_clauses_unsorted
    3.11 -  #> maps also_extensionalize_theorem
    3.12 +  #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
    3.13 +           #> also_extensionalize_theorem)
    3.14    #> map Meson_Clausify.introduce_combinators_in_theorem
    3.15    #> Meson.finish_cnf
    3.16  
    3.17 @@ -168,7 +169,7 @@
    3.18        (verbose_warning ctxt "Proof state contains the universal sort {}";
    3.19         Seq.empty)
    3.20      else
    3.21 -      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
    3.22 +      Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
    3.23                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
    3.24                    ctxt i st0
    3.25    end