clean handling of whether a fact is chained or not;
more elegant and reliable than encoding it in the name

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -30,16 +30,16 @@
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
      relevance_override: relevance_override,
-     axioms: (string * thm) list option}
+     axioms: ((string * bool) * thm) list option}
   type prover_result =
     {outcome: failure option,
      message: string,
      pool: string Symtab.table,
-     used_thm_names: string list,
+     used_thm_names: (string * bool) list,
      atp_run_time_in_msecs: int,
      output: string,
      proof: string,
-     axiom_names: string Vector.vector,
+     axiom_names: (string * bool) vector,
      conjecture_shape: int list list}
   type prover = params -> minimize_command -> problem -> prover_result
 
@@ -100,17 +100,17 @@
   {subgoal: int,
    goal: Proof.context * (thm list * thm),
    relevance_override: relevance_override,
-   axioms: (string * thm) list option}
+   axioms: ((string * bool) * thm) list option}
 
 type prover_result =
   {outcome: failure option,
    message: string,
    pool: string Symtab.table,
-   used_thm_names: string list,
+   used_thm_names: (string * bool) list,
    atp_run_time_in_msecs: int,
    output: string,
    proof: string,
-   axiom_names: string Vector.vector,
+   axiom_names: (string * bool) vector,
    conjecture_shape: int list list}
 
 type prover = params -> minimize_command -> problem -> prover_result
@@ -180,11 +180,11 @@
   #> parse_clause_formula_relation #> fst
 
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
-                                              thm_names =
+                                              axiom_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     (* This is a hack required for keeping track of axioms after they have been
-       clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
-       part of this hack. *)
+       clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is
+       also part of this hack. *)
     let
       val j0 = hd (hd conjecture_shape)
       val seq = extract_clause_sequence output
@@ -193,15 +193,20 @@
         conjecture_prefix ^ Int.toString (j - j0)
         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
         |> map (fn s => find_index (curry (op =) s) seq + 1)
+      fun name_for_number j =
+        let
+          val axioms =
+            j |> AList.lookup (op =) name_map
+              |> these |> map_filter (try (unprefix axiom_prefix))
+              |> map undo_ascii_of
+          val chained = forall (is_true_for axiom_names) axioms
+        in (axioms |> space_implode " ", chained) end
     in
       (conjecture_shape |> map (maps renumber_conjecture),
-       seq |> map (AList.lookup (op =) name_map #> these
-                   #> map_filter (try (unprefix axiom_prefix))
-                   #> map undo_ascii_of #> space_implode " ")
-           |> Vector.fromList)
+       seq |> map name_for_number |> Vector.fromList)
     end
   else
-    (conjecture_shape, thm_names)
+    (conjecture_shape, axiom_names)
 
 
 (* generic TPTP-based provers *)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -11,14 +11,13 @@
      only: bool}
 
   val trace : bool Unsynchronized.ref
-  val chained_prefix : string
   val name_thms_pair_from_ref :
     Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-    -> string * thm list
+    -> (string * bool) * thm list
   val relevant_facts :
     bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> term list -> term
-    -> (string * thm) list
+    -> ((string * bool) * thm) list
 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -37,17 +36,14 @@
    only: bool}
 
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-(* Used to label theorems chained into the goal. *)
-val chained_prefix = sledgehammer_prefix ^ "chained_"
 
 fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
   let
     val ths = ProofContext.get_fact ctxt xref
     val name = Facts.string_of_ref xref
     val name = name |> Symtab.defined reserved name ? quote
-                    |> forall (member Thm.eq_thm chained_ths) ths
-                       ? prefix chained_prefix
-  in (name, ths) end
+    val chained = forall (member Thm.eq_thm chained_ths) ths
+  in ((name, chained), ths) end
 
 
 (***************************************************************)
@@ -282,7 +278,7 @@
         | _ => false
     end;
 
-type annotated_thm = (string * thm) * (string * const_typ list) list
+type annotated_thm = ((string * bool) * thm) * (string * const_typ list) list
 
 (*For a reverse sort, putting the largest values first.*)
 fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
@@ -301,7 +297,7 @@
                        ", exceeds the limit of " ^ Int.toString max_new));
         trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
         trace_msg (fn () => "Actually passed: " ^
-          space_implode ", " (map (fst o fst o fst) accepted));
+          space_implode ", " (map (fst o fst o fst o fst) accepted));
         (map #1 accepted, List.drop (new_pairs, max_new))
       end
   end;
@@ -343,7 +339,7 @@
                 if null add_thms then
                   []
                 else
-                  map_filter (fn ((p as (name, th), _), _) =>
+                  map_filter (fn ((p as ((name, _), th), _), _) =>
                                  if member Thm.eq_thm add_thms th then SOME p
                                  else NONE) rejects
             | relevant (new_pairs, rejects) [] =
@@ -367,8 +363,8 @@
                 map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
               end
             | relevant (new_rels, rejects)
-                       (((ax as ((name, th), axiom_consts)), cached_weight)
-                        :: rest) =
+                       (((ax as (((name, chained), th), axiom_consts)),
+                         cached_weight) :: rest) =
               let
                 val weight =
                   case cached_weight of
@@ -537,15 +533,15 @@
 fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
   let
     val is_chained = member Thm.eq_thm chained_ths
-    fun is_bad_unnamed_local th =
-      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
-      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt)
     val local_facts = ProofContext.facts_of ctxt
     val named_locals = local_facts |> Facts.dest_static []
     (* Unnamed, not chained formulas with schematic variables are omitted,
        because they are rejected by the backticks (`...`) parser for some
        reason. *)
+    fun is_bad_unnamed_local th =
+      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
+      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
     val unnamed_locals =
       local_facts |> Facts.props |> filter_out is_bad_unnamed_local
                   |> map (pair "" o single)
@@ -579,25 +575,22 @@
                 SOME name' => name' |> Symtab.defined reserved name' ? quote
               | NONE => ths |> map_filter (try backquotify) |> space_implode " "
           in
-            if name' = "" then
-              I
-            else
-              cons (name' |> forall is_chained ths0 ? prefix chained_prefix,
-                    ths)
+            if name' = "" then I
+            else cons ((name', forall is_chained ths0), ths)
           end)
   in
     [] |> add_valid_facts fold local_facts (unnamed_locals @ named_locals)
        |> add_valid_facts Facts.fold_static global_facts global_facts
   end
 
-fun multi_name a th (n, pairs) =
-  (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
-
+fun multi_name (name, chained) th (n, pairs) =
+  (n + 1, ((name ^ "(" ^ Int.toString n ^ ")", chained), th) :: pairs)
 fun add_names (_, []) pairs = pairs
-  | add_names (a, [th]) pairs = (a, th) :: pairs
-  | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
+  | add_names (p, [th]) pairs = (p, th) :: pairs
+  | add_names (p, ths) pairs = #2 (fold (multi_name p) ths (1, pairs))
 
-fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
+fun is_multi ((name, _), ths) =
+  length ths > 1 orelse String.isSuffix ".axioms" name
 
 (* The single-name theorems go after the multiple-name ones, so that single
    names are preferred when both are available. *)
@@ -629,7 +622,7 @@
     relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
                      axioms (concl_t :: hyp_ts)
-    |> sort_wrt fst
+    |> sort_wrt (fst o fst)
   end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -10,8 +10,8 @@
   type params = Sledgehammer.params
 
   val minimize_theorems :
-    params -> int -> int -> Proof.state -> (string * thm list) list
-    -> (string * thm list) list option * string
+    params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
+    -> ((string * bool) * thm list) list option * string
   val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
 end;
 
@@ -30,14 +30,12 @@
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure _ = "Unknown error."
 
-fun n_theorems name_thms_pairs =
-  let val n = length name_thms_pairs in
+fun n_theorems names =
+  let val n = length names in
     string_of_int n ^ " theorem" ^ plural_s n ^
     (if n > 0 then
-       ": " ^ space_implode " "
-                  (name_thms_pairs
-                   |> map (perhaps (try (unprefix chained_prefix)))
-                   |> sort_distinct string_ord)
+       ": " ^ (names |> map fst
+                     |> sort_distinct string_ord |> space_implode " ")
      else
        "")
   end
@@ -65,8 +63,7 @@
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},
       axioms = SOME axioms}
-    val result as {outcome, used_thm_names, ...} =
-      prover params (K "") problem
+    val result as {outcome, used_thm_names, ...} = prover params (K "") problem
   in
     priority (case outcome of
                 NONE =>
@@ -80,8 +77,7 @@
 
 (* minimalization of thms *)
 
-fun filter_used_facts used =
-  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
+fun filter_used_facts used = filter (member (op =) used o fst)
 
 fun sublinear_minimize _ [] p = p
   | sublinear_minimize test (x :: xs) (seen, result) =
@@ -130,10 +126,9 @@
          val n = length min_thms
          val _ = priority (cat_lines
            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
-            (case filter (String.isPrefix chained_prefix o fst) min_thms of
-               [] => ""
-             | chained => " (including " ^ Int.toString (length chained) ^
-                          " chained)") ^ ".")
+            (case length (filter (snd o fst) min_thms) of
+               0 => ""
+             | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
        in
          (SOME min_thms,
           proof_text isar_proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -11,16 +11,16 @@
   type minimize_command = string list -> string
 
   val metis_proof_text:
-    bool * minimize_command * string * string vector * thm * int
-    -> string * string list
+    bool * minimize_command * string * (string * bool) vector * thm * int
+    -> string * (string * bool) list
   val isar_proof_text:
     string Symtab.table * bool * int * Proof.context * int list list
-    -> bool * minimize_command * string * string vector * thm * int
-    -> string * string list
+    -> bool * minimize_command * string * (string * bool) vector * thm * int
+    -> string * (string * bool) list
   val proof_text:
     bool -> string Symtab.table * bool * int * Proof.context * int list list
-    -> bool * minimize_command * string * string vector * thm * int
-    -> string * string list
+    -> bool * minimize_command * string * (string * bool) vector * thm * int
+    -> string * (string * bool) list
 end;
 
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -60,7 +60,7 @@
 fun index_in_shape x = find_index (exists (curry (op =) x))
 fun is_axiom_number axiom_names num =
   num > 0 andalso num <= Vector.length axiom_names andalso
-  Vector.sub (axiom_names, num - 1) <> ""
+  fst (Vector.sub (axiom_names, num - 1)) <> ""
 fun is_conjecture_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0
 
@@ -564,7 +564,7 @@
    "108. ... [input]". *)
 fun used_facts_in_atp_proof axiom_names atp_proof =
   let
-    fun axiom_name num =
+    fun axiom_name_at_index num =
       let val j = Int.fromString num |> the_default ~1 in
         if is_axiom_number axiom_names j then
           SOME (Vector.sub (axiom_names, j - 1))
@@ -573,18 +573,20 @@
       end
     val tokens_of =
       String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
-    val thm_name_list = Vector.foldr (op ::) [] axiom_names
     fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
         if tag = "cnf" orelse tag = "fof" then
           (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
              SOME name =>
-             if member (op =) rest "file" then SOME name else axiom_name num
-           | NONE => axiom_name num)
+             if member (op =) rest "file" then
+               SOME (name, is_true_for axiom_names name)
+             else
+               axiom_name_at_index num
+           | NONE => axiom_name_at_index num)
         else
           NONE
-      | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
+      | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num
       | do_line (num :: rest) =
-        (case List.last rest of "input" => axiom_name num | _ => NONE)
+        (case List.last rest of "input" => axiom_name_at_index num | _ => NONE)
       | do_line _ = NONE
   in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
 
@@ -620,23 +622,20 @@
       "\nTo minimize the number of lemmas, try this: " ^
       Markup.markup Markup.sendback command ^ "."
 
-val unprefix_chained = perhaps (try (unprefix chained_prefix))
-
 fun used_facts axiom_names =
   used_facts_in_atp_proof axiom_names
-  #> List.partition (String.isPrefix chained_prefix)
-  #>> map (unprefix chained_prefix)
-  #> pairself (sort_distinct string_ord)
+  #> List.partition snd
+  #> pairself (sort_distinct (string_ord) o map fst)
 
 fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names,
                       goal, i) =
   let
     val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
-    val lemmas = other_lemmas @ chained_lemmas
     val n = Logic.count_prems (prop_of goal)
   in
     (metis_line full_types i n other_lemmas ^
-     minimize_line minimize_command lemmas, lemmas)
+     minimize_line minimize_command (other_lemmas @ chained_lemmas),
+     map (rpair false) other_lemmas @ map (rpair true) chained_lemmas)
   end
 
 (** Isar proof construction and manipulation **)
@@ -663,7 +662,7 @@
 
 fun add_fact_from_dep axiom_names num =
   if is_axiom_number axiom_names num then
-    apsnd (insert (op =) (Vector.sub (axiom_names, num - 1)))
+    apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1))))
   else
     apfst (insert (op =) (raw_prefix, num))
 
@@ -964,10 +963,9 @@
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     fun do_facts (ls, ss) =
-      let
-        val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
-        val ss = ss |> map unprefix_chained |> sort_distinct string_ord
-      in metis_command full_types 1 1 (ls, ss) end
+      metis_command full_types 1 1
+                    (ls |> sort_distinct (prod_ord string_ord int_ord),
+                     ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
       | do_step ind (Let (t1, t2)) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -18,8 +18,8 @@
   val tfrees_name : string
   val prepare_problem :
     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
-    -> (string * thm) list
-    -> string problem * string Symtab.table * int * string Vector.vector
+    -> ((string * bool) * thm) list
+    -> string problem * string Symtab.table * int * (string * bool) vector
 end;
 
 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
@@ -194,11 +194,11 @@
                 ctypes_sorts = ctypes_sorts}
   end
 
-fun make_axiom ctxt presimp (name, th) =
+fun make_axiom ctxt presimp ((name, chained), th) =
   case make_formula ctxt presimp name Axiom (prop_of th) of
     FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
     NONE
-  | formula => SOME (name, formula)
+  | formula => SOME ((name, chained), formula)
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
     map2 (fn j => make_formula ctxt true (Int.toString j)
@@ -235,20 +235,20 @@
   let
     val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
     fun is_needed c = the (Symtab.lookup ct c) > 0
+    fun baptize th = ((Thm.get_name_hint th, false), th)
   in
     (optional_helpers
      |> full_types ? append optional_typed_helpers
      |> maps (fn (ss, ths) =>
-                 if exists is_needed ss then map (`Thm.get_name_hint) ths
-                 else [])) @
-    (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+                 if exists is_needed ss then map baptize ths else [])) @
+    (if is_FO then [] else map baptize mandatory_helpers)
     |> map_filter (Option.map snd o make_axiom ctxt false)
   end
 
-fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs =
   let
     val thy = ProofContext.theory_of ctxt
-    val axiom_ts = map (prop_of o snd) axioms
+    val axiom_ts = map (prop_of o snd) axiom_pairs
     val hyp_ts =
       if null hyp_ts then
         []
@@ -267,7 +267,7 @@
     (* TFrees in the conjecture; TVars in the axioms *)
     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
     val (axiom_names, axioms) =
-      ListPair.unzip (map_filter (make_axiom ctxt true) axioms)
+      ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
@@ -500,12 +500,12 @@
       (const_table_for_problem explicit_apply problem) problem
 
 fun prepare_problem ctxt readable_names explicit_forall full_types
-                    explicit_apply hyp_ts concl_t axiom_ts =
+                    explicit_apply hyp_ts concl_t axiom_pairs =
   let
     val thy = ProofContext.theory_of ctxt
     val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
                        arity_clauses)) =
-      prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts
+      prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs
     val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
     val helper_lines =
       map (problem_line_for_fact helper_prefix full_types) helper_facts

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 16:43:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 18:03:43 2010 +0200
@@ -6,6 +6,7 @@
 
 signature SLEDGEHAMMER_UTIL =
 sig
+  val is_true_for : (string * bool) vector -> string -> bool
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val strip_spaces : string -> string
@@ -27,6 +28,9 @@
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
 struct
 
+fun is_true_for v s =
+  Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
+
 fun plural_s n = if n = 1 then "" else "s"
 
 fun serial_commas _ [] = ["??"]