use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
authorblanchet
Thu Sep 02 11:29:02 2010 +0200 (2010-09-02)
changeset 39036dff91b90d74c
parent 39035 094848cf7ef3
child 39037 5146d640aa4a
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
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/SAT.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/clausifier.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Sep 02 11:02:13 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Sep 02 11:29:02 2010 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    ("Tools/recfun_codegen.ML")
     1.5    "Tools/async_manager.ML"
     1.6    "Tools/try.ML"
     1.7 +  ("Tools/cnf_funcs.ML")
     1.8  begin
     1.9  
    1.10  setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.11 @@ -1645,7 +1646,6 @@
    1.12    "(\<not> \<not>(P)) = P"
    1.13  by blast+
    1.14  
    1.15 -
    1.16  subsection {* Basic ML bindings *}
    1.17  
    1.18  ML {*
    1.19 @@ -1699,6 +1699,7 @@
    1.20  val trans = @{thm trans}
    1.21  *}
    1.22  
    1.23 +use "Tools/cnf_funcs.ML"
    1.24  
    1.25  subsection {* Code generator setup *}
    1.26  
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:02:13 2010 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:29:02 2010 +0200
     2.3 @@ -7,7 +7,8 @@
     2.4  
     2.5  theory Hilbert_Choice
     2.6  imports Nat Wellfounded Plain
     2.7 -uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
     2.8 +uses ("Tools/meson.ML")
     2.9 +     ("Tools/choice_specification.ML")
    2.10  begin
    2.11  
    2.12  subsection {* Hilbert's epsilon *}
     3.1 --- a/src/HOL/SAT.thy	Thu Sep 02 11:02:13 2010 +0200
     3.2 +++ b/src/HOL/SAT.thy	Thu Sep 02 11:29:02 2010 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4  theory SAT
     3.5  imports Refute
     3.6  uses
     3.7 -  "Tools/cnf_funcs.ML"
     3.8    "Tools/sat_funcs.ML"
     3.9  begin
    3.10  
     4.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 02 11:02:13 2010 +0200
     4.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 02 11:29:02 2010 +0200
     4.3 @@ -26,6 +26,9 @@
     4.4    ("Tools/Sledgehammer/sledgehammer_isar.ML")
     4.5  begin
     4.6  
     4.7 +lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
     4.8 +by simp
     4.9 +
    4.10  definition skolem_id :: "'a \<Rightarrow> 'a" where
    4.11  [no_atp]: "skolem_id = (\<lambda>x. x)"
    4.12  
     5.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 02 11:02:13 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 02 11:29:02 2010 +0200
     5.3 @@ -228,19 +228,26 @@
     5.4                    |> Meson.make_nnf ctxt
     5.5    in (th3, ctxt) end
     5.6  
     5.7 +fun to_definitional_cnf_with_quantifiers thy th =
     5.8 +  let
     5.9 +    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
    5.10 +    val eqth = eqth RS @{thm eq_reflection}
    5.11 +    val eqth = eqth RS @{thm TruepropI}
    5.12 +  in Thm.equal_elim eqth th end
    5.13 +
    5.14  (* Convert a theorem to CNF, with Skolem functions as additional premises. *)
    5.15  fun cnf_axiom thy th =
    5.16    let
    5.17      val ctxt0 = Variable.global_thm_context th
    5.18 -    val (nnfth, ctxt) = to_nnf th ctxt0
    5.19 -    val sko_ths = map (skolem_theorem_of_def thy)
    5.20 -                      (assume_skolem_funs nnfth)
    5.21 -    val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
    5.22 +    val (nnf_th, ctxt) = to_nnf th ctxt0
    5.23 +    val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
    5.24 +    val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
    5.25 +    val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
    5.26    in
    5.27 -    cnfs |> map introduce_combinators_in_theorem
    5.28 -         |> Variable.export ctxt ctxt0
    5.29 -         |> Meson.finish_cnf
    5.30 -         |> map Thm.close_derivation
    5.31 +    cnf_ths |> map introduce_combinators_in_theorem
    5.32 +            |> Variable.export ctxt ctxt0
    5.33 +            |> Meson.finish_cnf
    5.34 +            |> map Thm.close_derivation
    5.35    end
    5.36    handle THM _ => []
    5.37