# HG changeset patch
# User blanchet
# Date 1283419742 -7200
# Node ID dff91b90d74cb168725ab7e6314a02523dbe8c00
# Parent  094848cf7ef3b8485a641e3f70fa81b7a25fa8f0
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine

diff -r 094848cf7ef3 -r dff91b90d74c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -32,6 +32,7 @@
   ("Tools/recfun_codegen.ML")
   "Tools/async_manager.ML"
   "Tools/try.ML"
+  ("Tools/cnf_funcs.ML")
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -1645,7 +1646,6 @@
   "(\<not> \<not>(P)) = P"
 by blast+
 
-
 subsection {* Basic ML bindings *}
 
 ML {*
@@ -1699,6 +1699,7 @@
 val trans = @{thm trans}
 *}
 
+use "Tools/cnf_funcs.ML"
 
 subsection {* Code generator setup *}
 
diff -r 094848cf7ef3 -r dff91b90d74c src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -7,7 +7,8 @@
 
 theory Hilbert_Choice
 imports Nat Wellfounded Plain
-uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
+uses ("Tools/meson.ML")
+     ("Tools/choice_specification.ML")
 begin
 
 subsection {* Hilbert's epsilon *}
diff -r 094848cf7ef3 -r dff91b90d74c src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/SAT.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -10,7 +10,6 @@
 theory SAT
 imports Refute
 uses
-  "Tools/cnf_funcs.ML"
   "Tools/sat_funcs.ML"
 begin
 
diff -r 094848cf7ef3 -r dff91b90d74c src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Sep 02 11:29:02 2010 +0200
@@ -26,6 +26,9 @@
   ("Tools/Sledgehammer/sledgehammer_isar.ML")
 begin
 
+lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by simp
+
 definition skolem_id :: "'a \<Rightarrow> 'a" where
 [no_atp]: "skolem_id = (\<lambda>x. x)"
 
diff -r 094848cf7ef3 -r dff91b90d74c src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 02 11:02:13 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 02 11:29:02 2010 +0200
@@ -228,19 +228,26 @@
                   |> Meson.make_nnf ctxt
   in (th3, ctxt) end
 
+fun to_definitional_cnf_with_quantifiers thy th =
+  let
+    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+    val eqth = eqth RS @{thm eq_reflection}
+    val eqth = eqth RS @{thm TruepropI}
+  in Thm.equal_elim eqth th end
+
 (* Convert a theorem to CNF, with Skolem functions as additional premises. *)
 fun cnf_axiom thy th =
   let
     val ctxt0 = Variable.global_thm_context th
-    val (nnfth, ctxt) = to_nnf th ctxt0
-    val sko_ths = map (skolem_theorem_of_def thy)
-                      (assume_skolem_funs nnfth)
-    val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+    val (nnf_th, ctxt) = to_nnf th ctxt0
+    val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+    val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
+    val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
   in
-    cnfs |> map introduce_combinators_in_theorem
-         |> Variable.export ctxt ctxt0
-         |> Meson.finish_cnf
-         |> map Thm.close_derivation
+    cnf_ths |> map introduce_combinators_in_theorem
+            |> Variable.export ctxt ctxt0
+            |> Meson.finish_cnf
+            |> map Thm.close_derivation
   end
   handle THM _ => []