make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri May 28 13:49:21 2010 +0200
@@ -121,9 +121,8 @@
          : problem) =
   let
     (* get clauses and prepare them for writing *)
-    val (ctxt, (chain_ths, th)) = goal;
+    val (ctxt, (chained_ths, th)) = goal;
     val thy = ProofContext.theory_of ctxt;
-    val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
     val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
     val goal_cls = List.concat goal_clss
     val the_filtered_clauses =
@@ -135,7 +134,7 @@
         NONE => the_filtered_clauses
       | SOME axcls => axcls);
     val (internal_thm_names, clauses) =
-      prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
+      prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri May 28 13:49:21 2010 +0200
@@ -352,7 +352,7 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (mk_clause_table ax_clauses) o prop_of)
 
-fun all_valid_thms respect_no_atp ctxt chain_ths =
+fun all_valid_thms respect_no_atp ctxt chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
@@ -372,12 +372,13 @@
           val ths = filter_out bad_for_atp ths0;
         in
           if Facts.is_concealed facts name orelse
-             forall (member Thm.eq_thm chain_ths) ths orelse
              (respect_no_atp andalso is_package_def name) then
             I
           else case find_first check_thms [name1, name2, name] of
             NONE => I
-          | SOME a => cons (a, ths)
+          | SOME name' =>
+            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+                           ? prefix chained_prefix, ths)
         end);
   in valid_facts global_facts @ valid_facts local_facts end;
 
@@ -397,10 +398,10 @@
 
 (* The single-name theorems go after the multiple-name ones, so that single
    names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt chain_ths =
+fun name_thm_pairs respect_no_atp ctxt chained_ths =
   let
     val (mults, singles) =
-      List.partition is_multi (all_valid_thms respect_no_atp ctxt chain_ths)
+      List.partition is_multi (all_valid_thms respect_no_atp ctxt chained_ths)
     val ps = [] |> fold add_single_names singles
                 |> fold add_multi_names mults
   in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
@@ -409,11 +410,11 @@
       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   | check_named _ = true;
 
-fun get_all_lemmas respect_no_atp ctxt chain_ths =
+fun get_all_lemmas respect_no_atp ctxt chained_ths =
   let val included_thms =
         tap (fn ths => trace_msg
                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
-            (name_thm_pairs respect_no_atp ctxt chain_ths)
+            (name_thm_pairs respect_no_atp ctxt chained_ths)
   in
     filter check_named included_thms
   end;
@@ -510,14 +511,14 @@
 fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
                        defs_relevant max_new theory_relevant
                        (relevance_override as {add, only, ...})
-                       (ctxt, (chain_ths, _)) goal_cls =
+                       (ctxt, (chained_ths, _)) goal_cls =
   if (only andalso null add) orelse relevance_threshold > 1.0 then
     []
   else
     let
       val thy = ProofContext.theory_of ctxt
       val is_FO = is_first_order thy goal_cls
-      val included_cls = get_all_lemmas respect_no_atp ctxt chain_ths
+      val included_cls = get_all_lemmas respect_no_atp ctxt chained_ths
         |> cnf_rules_pairs thy |> make_unique
         |> restrict_to_logic thy is_FO
         |> remove_unwanted_clauses
@@ -529,14 +530,8 @@
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
   let
-    (* add chain thms *)
-    val chain_cls =
-      cnf_rules_pairs thy (filter check_named
-                                  (map (`Thm.get_name_hint) chain_ths))
-    val axcls = chain_cls @ axcls
-    val extra_cls = chain_cls @ extra_cls
     val is_FO = is_first_order thy goal_cls
     val ccls = subtract_cls extra_cls goal_cls
     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri May 28 13:49:21 2010 +0200
@@ -7,6 +7,7 @@
 
 signature SLEDGEHAMMER_FACT_PREPROCESSOR =
 sig
+  val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
   val skolem_prefix: string
@@ -31,6 +32,9 @@
 
 open Sledgehammer_FOL_Clause
 
+(* Used to label theorems chained into the goal. *)
+val chained_prefix = "Sledgehammer.chained_"
+
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 28 13:49:21 2010 +0200
@@ -233,13 +233,19 @@
                                          state) atps
       in () end
 
-fun minimize override_params i fact_refs state =
+fun minimize override_params i frefs state =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val theorems_from_refs =
-      map o pairf Facts.string_of_ref o ProofContext.get_fact
-    val name_thms_pairs = theorems_from_refs ctxt fact_refs
+    val chained_ths = #facts (Proof.goal state)
+    fun theorems_from_ref ctxt fref =
+      let
+        val ths = ProofContext.get_fact ctxt fref
+        val name = Facts.string_of_ref fref
+                   |> forall (member Thm.eq_thm chained_ths) ths
+                      ? prefix chained_prefix
+      in (name, ths) end
+    val name_thms_pairs = map (theorems_from_ref ctxt) frefs
   in
     case subgoal_count state of
       0 => priority "No subgoal!"
@@ -267,11 +273,11 @@
 fun string_for_raw_param (key, values) =
   key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
 
-fun minimize_command override_params i atp_name facts =
+fun minimize_command override_params i atp_name fact_names =
   sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
   (override_params |> filter is_raw_param_relevant_for_minimize
                    |> implode o map (prefix ", " o string_for_raw_param)) ^
-  "] (" ^ space_implode " " facts ^ ")" ^
+  "] (" ^ space_implode " " fact_names ^ ")" ^
   (if i = 1 then "" else " " ^ string_of_int i)
 
 fun hammer_away override_params subcommand opt_i relevance_override state =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:22:16 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri May 28 13:49:21 2010 +0200
@@ -10,7 +10,6 @@
   type minimize_command = string list -> string
   type name_pool = Sledgehammer_FOL_Clause.name_pool
 
-  val chained_hint: string
   val invert_const: string -> string
   val invert_type_const: string -> string
   val num_type_args: theory -> string -> int
@@ -582,9 +581,6 @@
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
   
-(* Used to label theorems chained into the goal. *)
-val chained_hint = "sledgehammer_chained"
-
 fun apply_command _ 1 = "by "
   | apply_command 1 _ = "apply "
   | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
@@ -602,16 +598,24 @@
       "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback command ^ ".\n"
 
+val unprefix_chained = perhaps (try (unprefix chained_prefix))
+
 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
   let
-    val lemmas =
+    val raw_lemmas =
       atp_proof |> extract_clause_numbers_in_atp_proof
                 |> filter (is_axiom_clause_number thm_names)
                 |> map (fn i => Vector.sub (thm_names, i - 1))
-                |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint)
-                |> sort_distinct string_ord
+    val (chained_lemmas, other_lemmas) =
+      raw_lemmas |> List.partition (String.isPrefix chained_prefix)
+                 |>> map (unprefix chained_prefix)
+                 |> pairself (sort_distinct string_ord)
+    val lemmas = other_lemmas @ chained_lemmas
     val n = Logic.count_prems (prop_of goal)
-  in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
+  in
+    (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas,
+     lemmas)
+  end
 
 (** Isar proof construction and manipulation **)
 
@@ -929,7 +933,7 @@
     fun do_facts (ls, ss) =
       let
         val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
-        val ss = ss |> sort_distinct string_ord
+        val ss = ss |> map unprefix_chained |> sort_distinct string_ord
       in metis_command 1 1 (map string_for_label ls @ ss) end
     and do_step ind (Fix xs) =
         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"