# HG changeset patch
# User blanchet
# Date 1277801805 -7200
# Node ID 78334f400ae6a14e630165b02e224f32aa8c6a49
# Parent  1d1754ccd233a516b897982d82313f617dc4dc92
Sledgehammer can save some msecs by cheating

diff -r 1d1754ccd233 -r 78334f400ae6 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 29 10:56:45 2010 +0200
@@ -185,7 +185,7 @@
 
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
-  #> (if raw then  map (apfst (rpair 0)) else cnf_rules_pairs thy)
+  #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true)
 
 val optional_helpers =
   [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
@@ -264,7 +264,7 @@
                     relevance_convergence defs_relevant max_axiom_clauses
                     (the_default prefers_theory_relevant theory_relevant)
                     relevance_override goal goal_cls
-                |> cnf_rules_pairs thy
+                |> cnf_rules_pairs thy true
     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
     val (internal_thm_names, clauses) =
       prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
diff -r 1d1754ccd233 -r 78334f400ae6 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jun 29 10:56:45 2010 +0200
@@ -7,9 +7,9 @@
 
 signature CLAUSIFIER =
 sig
-  val cnf_axiom: theory -> thm -> thm list
+  val cnf_axiom: theory -> bool -> thm -> thm list
   val cnf_rules_pairs :
-    theory -> (string * thm) list -> ((string * int) * thm) list
+    theory -> bool -> (string * thm) list -> ((string * int) * thm) list
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -193,7 +193,7 @@
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
-fun skolem_theorem_of_def thy rhs0 =
+fun skolem_theorem_of_def thy cheat rhs0 =
   let
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
@@ -213,10 +213,13 @@
       THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
                  RS @{thm someI_ex}) 1
   in
-    Goal.prove_internal [ex_tm] conc tacf
-    |> forall_intr_list frees
-    |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
-    |> Thm.varifyT_global
+    (if cheat then
+      Skip_Proof.make_thm thy (Logic.mk_implies (pairself term_of (ex_tm, conc)))
+    else
+      Goal.prove_internal [ex_tm] conc tacf
+      |> forall_intr_list frees
+      |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
+      |> Thm.varifyT_global)
   end
 
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
@@ -229,11 +232,12 @@
   in  (th3, ctxt)  end;
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolemize_theorem thy th =
+fun skolemize_theorem thy cheat 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 sko_ths = map (skolem_theorem_of_def thy cheat)
+                      (assume_skolem_funs nnfth)
     val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   in
     cnfs |> map introduce_combinators
@@ -245,13 +249,13 @@
 
 (* Convert Isabelle theorems into axiom clauses. *)
 (* FIXME: is transfer necessary? *)
-fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
+fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
 
 
 (**** Translate a set of theorems into CNF ****)
 
 (*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy =
+fun cnf_rules_pairs thy cheat =
   let
     fun do_one _ [] = []
       | do_one ((name, k), th) (cls :: clss) =
@@ -259,7 +263,7 @@
     fun do_all pairs [] = pairs
       | do_all pairs ((name, th) :: ths) =
         let
-          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
+          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
                           handle THM _ => []
         in do_all (new_pairs @ pairs) ths end
   in do_all [] o rev end
diff -r 1d1754ccd233 -r 78334f400ae6 src/HOL/Tools/Sledgehammer/meson_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Tue Jun 29 10:56:45 2010 +0200
@@ -18,7 +18,7 @@
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
+  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) ths) end
 
 val setup =
   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
diff -r 1d1754ccd233 -r 78334f400ae6 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 29 10:56:45 2010 +0200
@@ -608,7 +608,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnf_helper_theorem thy raw th =
-  if raw then th else the_single (cnf_axiom thy th)
+  if raw then th else the_single (cnf_axiom thy false th)
 
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
@@ -724,7 +724,7 @@
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
       val th_cls_pairs =
-        map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
+        map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
       val ths = maps #2 th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
diff -r 1d1754ccd233 -r 78334f400ae6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 29 10:56:45 2010 +0200
@@ -51,11 +51,12 @@
 fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
                                filtered_clauses name_thms_pairs =
   let
+    val thy = Proof.theory_of state
     val num_theorems = length name_thms_pairs
     val _ = priority ("Testing " ^ string_of_int num_theorems ^
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
-    val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+    val axclauses = cnf_rules_pairs thy true name_thm_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),