generalize method list further to list of list (clustering preferred methods together)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -105,6 +105,9 @@
 fun tac_of_method meth type_enc lam_trans ctxt facts =
   (case meth of
     Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
+  | Metis_New_Skolem_Method =>
+    tac_of_method Metis_Method type_enc lam_trans (Config.put Metis_Tactic.new_skolem true ctxt)
+      facts
   | Meson_Method => Meson.meson_tac ctxt facts
   | _ =>
     Method.insert_tac facts THEN'
@@ -120,7 +123,7 @@
 (* main function for preplaying Isar steps; may throw exceptions *)
 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
   | preplay_raw debug type_enc lam_trans ctxt timeout
-      (step as Prove (_, xs, _, t, subproofs, (fact_names, meth :: _))) =
+      (step as Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
     let
       val goal =
         (case xs of
@@ -144,7 +147,6 @@
 
       val ctxt' = ctxt
         |> debug ? (Config.put Metis_Tactic.verbose true #> Config.put Lin_Arith.verbose true)
-        |> use_metis_new_skolem step ? Config.put Metis_Tactic.new_skolem true
 
       val prove = Goal.prove ctxt' [] [] goal
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -12,11 +12,8 @@
   type one_line_params = Sledgehammer_Reconstructor.one_line_params
 
   val string_of_reconstructor : reconstructor -> string
-
   val one_line_proof_text : int -> one_line_params -> string
-
-  val string_of_proof :
-    Proof.context -> string -> string -> int -> int -> isar_proof -> string
+  val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
 end;
 
 structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
@@ -34,12 +31,10 @@
 
 (** reconstructors **)
 
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
-    metis_call type_enc lam_trans
+fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
   | string_of_reconstructor SMT = smtN
 
 
-
 (** one-liner reconstructor proofs **)
 
 fun show_time NONE = ""
@@ -59,8 +54,7 @@
     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 fun using_labels [] = ""
-  | using_labels ls =
-    "using " ^ space_implode " " (map string_of_label ls) ^ " "
+  | using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " "
 
 fun command_call name [] =
     name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
@@ -68,8 +62,7 @@
 
 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
   (* unusing_chained_facts used_chaineds num_chained ^ *)
-  using_labels ls ^ apply_on_subgoal i n ^
-  command_call (string_of_reconstructor reconstr) ss
+  using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
 
 fun try_command_line banner time command =
   banner ^ ": " ^
@@ -105,8 +98,7 @@
       | Failed_to_Play reconstr => (true, reconstr, NONE)
     val try_line =
       ([], map fst extra)
-      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
-                               num_chained
+      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
       |> (if failed then
             enclose "One-line proof reconstruction failed: "
                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
@@ -186,16 +178,18 @@
     fun using_facts [] [] = ""
       | using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
 
-    fun of_method ls ss Metis_Method =
-        reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
+    fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
+
+    fun of_method ls ss Metis_Method = of_metis ls ss
+      | of_method ls ss Metis_New_Skolem_Method = "using [[metis_new_skolem]] " ^ of_metis ls ss
       | of_method ls ss meth = using_facts ls ss ^ by_method meth
 
-    fun of_byline ind options (ls, ss) meth =
+    fun of_byline ind (ls, ss) meth =
       let
         val ls = ls |> sort_distinct label_ord
         val ss = ss |> sort_distinct string_ord
       in
-        "\n" ^ of_indent (ind + 1) ^ options ^ of_method ls ss meth
+        "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
       end
 
     fun of_free (s, T) =
@@ -218,10 +212,10 @@
 
     fun add_assms ind assms = fold (add_assm ind) assms
 
-    fun add_step_post ind l t facts meth options =
+    fun add_step_post ind l t facts meth =
       add_suffix (of_label l)
       #> add_term t
-      #> add_suffix (of_byline ind options facts meth ^ "\n")
+      #> add_suffix (of_byline ind facts meth ^ "\n")
 
     fun of_subproof ind ctxt proof =
       let
@@ -231,8 +225,7 @@
         val suffix = " }"
       in
         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
-        String.extract (s, ind * indent_size,
-                        SOME (size s - ind * indent_size - 1)) ^
+        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
         suffix ^ "\n"
       end
     and of_subproofs _ _ _ [] = ""
@@ -247,19 +240,15 @@
         #> add_suffix " = "
         #> add_term t2
         #> add_suffix "\n"
-      | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, meth :: _))) =
-        (case xs of
-          [] => (* have *)
-          add_step_pre ind qs subproofs
-          #> add_suffix (of_have qs (length subproofs) ^ " ")
-          #> add_step_post ind l t facts meth ""
-        | _ => (* obtain *)
-          add_step_pre ind qs subproofs
-          #> add_suffix (of_obtain qs (length subproofs) ^ " ")
-          #> add_frees xs
-          #> add_suffix " where "
-          #> add_step_post ind l t facts meth
-            (if use_metis_new_skolem step then "using [[metis_new_skolem]] " else ""))
+      | add_step ind (step as Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
+        add_step_pre ind qs subproofs
+        #> (case xs of
+            [] => add_suffix (of_have qs (length subproofs) ^ " ")
+          | _ =>
+            add_suffix (of_obtain qs (length subproofs) ^ " ")
+            #> add_frees xs
+            #> add_suffix " where ")
+        #> add_step_post ind l t facts meth
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
       ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
@@ -267,7 +256,7 @@
     (* One-step Metis proofs are pointless; better use the one-liner directly. *)
     (case proof of
       Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method :: _))]) => ""
+    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
     | _ =>
       (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -18,10 +18,10 @@
   and isar_step =
     Let of term * term |
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
-      (facts * proof_method list)
+      (facts * proof_method list list)
   and proof_method =
-    Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
-    Blast_Method | Meson_Method
+    Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
+    Force_Method | Arith_Method | Blast_Method | Meson_Method
 
   val no_label : label
   val no_facts : facts
@@ -38,8 +38,7 @@
 
   val label_of_step : isar_step -> label option
   val subproofs_of_step : isar_step -> isar_proof list option
-  val byline_of_step : isar_step -> (facts * proof_method list) option
-  val use_metis_new_skolem : isar_step -> bool
+  val byline_of_step : isar_step -> (facts * proof_method list list) option
 
   val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
@@ -68,10 +67,10 @@
 and isar_step =
   Let of term * term |
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
-    (facts * proof_method list)
+    (facts * proof_method list list)
 and proof_method =
-  Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
-  Blast_Method | Meson_Method
+  Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
+  Force_Method | Arith_Method | Blast_Method | Meson_Method
 
 val no_label = ("", ~1)
 val no_facts = ([],[])
@@ -95,16 +94,9 @@
 fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
   | byline_of_step _ = NONE
 
-(* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see
-   also "atp_proof_reconstruct.ML" concerning Vampire). *)
-fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth :: _))) =
-    meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs
-  | use_metis_new_skolem _ = false
-
 fun fold_isar_steps f = fold (fold_isar_step f)
 and fold_isar_step f step =
-  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step))
-  #> f step
+  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
 
 fun map_isar_steps f =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -230,9 +230,9 @@
     fun chain_qs_lfs NONE lfs = ([], lfs)
       | chain_qs_lfs (SOME l0) lfs =
         if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-    fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
+    fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
         let val (qs', lfs) = chain_qs_lfs lbl lfs in
-          Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), meths))
+          Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
         end
       | chain_step _ step = step
     and chain_steps _ [] = []
@@ -242,20 +242,23 @@
     and chain_proof (Proof (fix, assms, steps)) =
       Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
     and chain_proofs proofs = map (chain_proof) proofs
-  in chain_proof end
+  in
+    chain_proof
+  end
 
 type isar_params =
   bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
   thm
 
-val arith_methods =
-  [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
-   Metis_Method]
-val metislike_methods =
-  [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
-   Force_Method, Meson_Method]
-val rewrite_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method]
-val skolem_methods = [Metis_Method, Meson_Method]
+val arith_methodss =
+  [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
+    Metis_Method], [Meson_Method]]
+val metislike_methodss =
+  [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+    Force_Method], [Meson_Method]]
+val rewrite_methodss =
+  [[Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
+val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]]
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, isar_try0,
@@ -296,12 +299,12 @@
           map_filter (get_role (curry (op =) Lemma)) atp_proof
           |> map (fn ((l, t), rule) =>
             let
-              val (skos, meths) =
-                if is_skolemize_rule rule then (skolems_of t, skolem_methods)
-                else if is_arith_rule rule then ([], arith_methods)
-                else ([], rewrite_methods)
+              val (skos, methss) =
+                if is_skolemize_rule rule then (skolems_of t, skolem_methodss)
+                else if is_arith_rule rule then ([], arith_methodss)
+                else ([], rewrite_methodss)
             in
-              Prove ([], skos, l, t, [], (([], []), meths))
+              Prove ([], skos, l, t, [], (([], []), methss))
             end)
 
         val bot = atp_proof |> List.last |> #1
@@ -349,7 +352,7 @@
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                               ((the_list predecessor, []), metislike_methods)))
+                               ((the_list predecessor, []), metislike_methodss)))
                 else
                   I)
             |> rev
@@ -364,15 +367,15 @@
               fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
 
               val deps = fold add_fact_of_dependencies gamma no_facts
-              val meths = if is_arith_rule rule then arith_methods else metislike_methods
-              val by = (deps, meths)
+              val methss = if is_arith_rule rule then arith_methodss else metislike_methodss
+              val by = (deps, methss)
             in
               if is_clause_tainted c then
                 (case gamma of
                   [g] =>
                   if skolem andalso is_clause_tainted g then
                     let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
-                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] []
+                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] []
                     end
                   else
                     do_rest l (prove [] by)
@@ -390,7 +393,7 @@
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  ((the_list predecessor, []), metislike_methods))
+                  ((the_list predecessor, []), metislike_methodss))
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -21,8 +21,8 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, _ :: meths))) =
-    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) meths
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
+    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
   | variants_of_step _ = raise Fail "Sledgehammer_Try0: variants_of_step"
 
 val slack = seconds 0.05