# HG changeset patch
# User paulson
# Date 1196263563 -3600
# Node ID 4cc7976948ac155f9fed429a1c3132fc8b097b22
# Parent  5760991891dd062df7af63ac663744df33a3ad31
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
output of a structured proof.

diff -r 5760991891dd -r 4cc7976948ac src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Nov 28 16:16:01 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Nov 28 16:26:03 2007 +0100
@@ -823,8 +823,11 @@
 
 fun sledgehammer state =
   let
-    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state);
-    val thy = ProofContext.theory_of ctxt;
+    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
+    val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
+                    (*Mark the chained theorems to keep them out of metis calls;
+                      their original "name hints" may be bad anyway.*)
+    val thy = ProofContext.theory_of ctxt
   in
     Output.debug (fn () => "subgoals in isar_atp:\n" ^
                   Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
diff -r 5760991891dd -r 4cc7976948ac src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Nov 28 16:16:01 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Nov 28 16:26:03 2007 +0100
@@ -11,6 +11,7 @@
   datatype atp = E | SPASS | Vampire
   val modulus:     int ref
   val recon_sorts: bool ref
+  val chained_hint: string
   val checkEProofFound:
 	TextIO.instream * TextIO.outstream * Posix.Process.pid *
 	string * Proof.context * thm * int * string Vector.vector -> bool
@@ -447,7 +448,8 @@
   in
     app (fn th => Output.debug (fn () => string_of_thm th)) ccls;
     isar_header (map #1 fixes) ^
-    String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines))
+    String.concat (isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)) ^
+    "qed\n"
   end
   handle e => (*FIXME: exn handler is too general!*)
     "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e;
@@ -540,17 +542,24 @@
 fun metis_line [] = "apply metis"
   | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
 
+(*Used to label theorems chained into the sledgehammer call*)
+val chained_hint = "CHAINED";
+
+val nochained = filter_out (fn y => y = chained_hint);
+
 (*The signal handler in watcher.ML must be able to read the output of this.*)
 fun lemma_list atp proofextract thm_names probfile toParent ppid =
   signal_success probfile toParent ppid 
-                 (metis_line (get_axiom_names_for atp proofextract thm_names));
+                 (metis_line (nochained (get_axiom_names_for atp proofextract thm_names)));
 
 fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno =
   let val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
-      val line1 = metis_line (get_axiom_names_tstp proofextract thm_names)
+      val names = get_axiom_names_tstp proofextract thm_names
+      val line1 = metis_line (nochained names)
+      val line2 = if chained_hint mem_string names then ""
+                  else decode_tstp_file cnfs ctxt th sgno thm_names
   in
-    signal_success probfile toParent ppid
-      (line1 ^ "\n" ^ decode_tstp_file cnfs ctxt th sgno thm_names)
+    signal_success probfile toParent ppid (line1 ^ "\n" ^ line2)
   end;
 
 (**** Extracting proofs from an ATP's output ****)