# HG changeset patch
# User blanchet
# Date 1290806527 -3600
# Node ID a82badd0e6ef003589df797fd78a743c925fa237
# Parent  88f2955a111e0971250875b1fc13a0644a9ee718
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs

diff -r 88f2955a111e -r a82badd0e6ef src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 26 22:22:07 2010 +0100
@@ -440,7 +440,7 @@
 val smt_iter_timeout_divisor = 2
 val smt_monomorph_limit = 4
 
-fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
+fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
   let
     val ctxt = Proof.context_of state
     fun iter timeout iter_num outcome0 msecs_so_far facts =
@@ -534,6 +534,7 @@
     val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+    val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
     val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
@@ -547,8 +548,9 @@
         in
           try_command_line (proof_banner auto)
                            (apply_on_subgoal subgoal subgoal_count ^
-                            command_call method (map (fst o fst) used_facts)) ^
-          minimize_line minimize_command (map (fst o fst) used_facts)
+                            command_call method (map fst other_lemmas)) ^
+          minimize_line minimize_command
+                        (map fst (other_lemmas @ chained_lemmas))
         end
       | SOME failure => string_for_failure "SMT solver" failure
   in
diff -r 88f2955a111e -r a82badd0e6ef src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 26 22:22:07 2010 +0100
@@ -24,7 +24,9 @@
   val command_call : string -> string list -> string
   val try_command_line : string -> string -> string
   val minimize_line : ('a list -> string) -> 'a list -> string
-  val metis_proof_text : metis_params -> text_result
+  val split_used_facts :
+    (string * locality) list
+    -> (string * locality) list * (string * locality) list
   val isar_proof_text : isar_params -> metis_params -> text_result
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
@@ -159,15 +161,15 @@
 fun used_facts_in_tstplike_proof fact_names =
   atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
 
-fun used_facts fact_names =
-  used_facts_in_tstplike_proof fact_names
-  #> List.partition (curry (op =) Chained o snd)
+val split_used_facts =
+  List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
 fun metis_proof_text (banner, full_types, minimize_command,
                       tstplike_proof, fact_names, goal, i) =
   let
-    val (chained_lemmas, other_lemmas) = used_facts fact_names tstplike_proof
+    val (chained_lemmas, other_lemmas) =
+      split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
     val n = Logic.count_prems (prop_of goal)
   in
     (metis_line banner full_types i n (map fst other_lemmas) ^
@@ -912,14 +914,14 @@
   in do_proof end
 
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-                    (other_params as (_, full_types, _, tstplike_proof,
+                    (metis_params as (_, full_types, _, tstplike_proof,
                                       fact_names, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
     val n = Logic.count_prems (prop_of goal)
-    val (one_line_proof, lemma_names) = metis_proof_text other_params
+    val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
       case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
                isar_shrink_factor tstplike_proof conjecture_shape fact_names
@@ -940,8 +942,8 @@
         |> the_default "\nWarning: The Isar proof construction failed."
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof isar_params other_params =
+fun proof_text isar_proof isar_params metis_params =
   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
-      other_params
+      metis_params
 
 end;