# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 017e5dac8642727b3bd3c9117398c6fe5743dedd
# Parent  2a9dcff63b8098ced156f78d7b406557a35df968
added unfold set constant functionality to Meson/Metis -- disabled by default for now

diff -r 2a9dcff63b80 -r 017e5dac8642 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
@@ -9,12 +9,14 @@
 signature MESON =
 sig
   val trace : bool Config.T
+  val unfold_set_consts : bool Config.T
   val max_clauses : int Config.T
   val term_pair_of: indexname * (typ * 'a) -> term * 'a
   val size_of_subgoals: thm -> int
   val has_too_many_clauses: Proof.context -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
+  val unfold_set_const_simps : Proof.context -> thm list
   val presimplify: thm -> thm
   val make_nnf: Proof.context -> thm -> thm
   val choice_theorems : theory -> thm list
@@ -49,8 +51,10 @@
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
-val max_clauses_default = 60
-val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
+val unfold_set_consts =
+  Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false)
+
+val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60)
 
 (*No known example (on 1-5-2007) needs even thirty*)
 val iter_deepen_limit = 50;
@@ -555,6 +559,10 @@
     handle THM ("tryres", _, _) => th
   else th
 
+fun unfold_set_const_simps ctxt =
+  if Config.get ctxt unfold_set_consts then @{thms Collect_def_raw mem_def_raw}
+  else []
+
 (*The simplification removes defined quantifiers and occurrences of True and False.
   nnf_ss also includes the one-point simprocs,
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
diff -r 2a9dcff63b80 -r 017e5dac8642 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 12 15:29:19 2011 +0200
@@ -320,6 +320,7 @@
          |> new_skolemizer ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule Object_Logic.atomize
+                |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
                 |> extensionalize_theorem
                 |> make_nnf ctxt
   in
diff -r 2a9dcff63b80 -r 017e5dac8642 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu May 12 15:29:19 2011 +0200
@@ -141,10 +141,11 @@
     else th :: Meson.make_clauses_unsorted [th']
   end
 
-val neg_clausify =
+fun neg_clausify ctxt =
   single
   #> Meson.make_clauses_unsorted
-  #> maps also_extensionalize_theorem
+  #> maps (Raw_Simplifier.rewrite_rule (Meson.unfold_set_const_simps ctxt)
+           #> also_extensionalize_theorem)
   #> map Meson_Clausify.introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
@@ -168,7 +169,7 @@
       (verbose_warning ctxt "Proof state contains the universal sort {}";
        Seq.empty)
     else
-      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+      Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt))
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
   end