merged
authorwenzelm
Fri, 31 Jan 2014 19:32:13 +0100
changeset 55226 46c8969a995b
parent 55223 3c593bad6b31 (diff)
parent 55225 22a1f3813d67 (current diff)
child 55227 653de351d21c
merged
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -13,6 +13,8 @@
   type stature = ATP_Problem_Generate.stature
   type one_line_params = Sledgehammer_Reconstructor.one_line_params
 
+  val trace : bool Config.T
+
   type isar_params =
     bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
 
@@ -42,6 +44,8 @@
 
 open String_Redirect
 
+val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
+
 val e_skolemize_rules = ["skolemize", "shift_quantors"]
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
@@ -103,99 +107,16 @@
         add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
     end
 
-val add_labels_of_proof =
-  steps_of_proof
-  #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
-
-fun kill_useless_labels_in_proof proof =
-  let
-    val used_ls = add_labels_of_proof proof []
-
-    fun kill_label l = if member (op =) used_ls l then l else no_label
-    fun kill_assms assms = map (apfst kill_label) assms
-
-    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
-        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
-      | kill_step step = step
-    and kill_proof (Proof (fix, assms, steps)) =
-      Proof (fix, kill_assms assms, map kill_step steps)
-  in
-    kill_proof proof
-  end
-
-val assume_prefix = "a"
-val have_prefix = "f"
-
-val relabel_proof =
-  let
-    fun fresh_label depth prefix (accum as (l, subst, next)) =
-      if l = no_label then
-        accum
-      else
-        let val l' = (replicate_string (depth + 1) prefix, next) in
-          (l', (l, l') :: subst, next + 1)
-        end
-
-    fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
-
-    fun relabel_assm depth (l, t) (subst, next) =
-      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
-        ((l, t), (subst, next))
-      end
-
-    fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
-
-    fun relabel_steps _ _ _ [] = []
-      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
-        let
-          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
-          val sub = relabel_proofs subst depth sub
-          val by = apfst (relabel_facts subst) by
-        in
-          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
-        end
-      | relabel_steps subst depth next (step :: steps) =
-        step :: relabel_steps subst depth next steps
-    and relabel_proof subst depth (Proof (fix, assms, steps)) =
-      let val (assms, subst) = relabel_assms subst depth assms in
-        Proof (fix, assms, relabel_steps subst depth 1 steps)
-      end
-    and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
-  in
-    relabel_proof [] 0
-  end
-
-val chain_direct_proof =
-  let
-    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), methss))) =
-        let val (qs', lfs) = chain_qs_lfs lbl lfs in
-          Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
-        end
-      | chain_step _ step = step
-    and chain_steps _ [] = []
-      | chain_steps (prev as SOME _) (i :: is) =
-        chain_step prev i :: chain_steps (label_of_step i) is
-      | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
-    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
-
 type isar_params =
   bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
 
 val arith_methodss =
   [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
-    Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
+    Algebra_Method], [Metis_Method], [Meson_Method]]
+val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
 val metislike_methodss =
   [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
-    Force_Method], [Meson_Method]]
+    Force_Method, Algebra_Method], [Meson_Method]]
 val rewrite_methodss =
   [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
 val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
@@ -345,7 +266,7 @@
         val string_of_isar_proof =
           string_of_isar_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count
 
-        val trace = false
+        val trace = Config.get ctxt trace
 
         val isar_proof =
           refute_graph
@@ -356,13 +277,21 @@
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
-        val preplay_data as {overall_preplay_outcome, ...} =
+        val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
           preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
             preplay_timeout isar_proof
 
+        fun str_of_preplay_outcome outcome =
+          if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
+
+        fun str_of_meth l meth =
+          string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
+        fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
+
         fun trace_isar_proof label proof =
           if trace then
-            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof proof ^ "\n")
+            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^
+              "\n")
           else
             ()
 
@@ -378,9 +307,11 @@
                (try0_isar ? minimize_isar_step_dependencies preplay_data)
           |> tap (trace_isar_proof "Minimized")
           |> `overall_preplay_outcome
-          ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
+          ||> chain_isar_proof
+          ||> kill_useless_labels_in_isar_proof
+          ||> relabel_isar_proof_finally
       in
-        (case string_of_isar_proof isar_proof of
+        (case string_of_isar_proof (K (K "")) isar_proof of
           "" =>
           if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
           else ""
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -79,14 +79,15 @@
     | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
   end
 
-(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+(* Tries merging the first step into the second step.
+   FIXME: Arbitrarily picks the second step's method. *)
 fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
-      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
     let
       val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
       val gfs = union (op =) gfs1 gfs2
     in
-      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
     end
   | try_merge _ _ = NONE
 
@@ -96,7 +97,7 @@
 (* Precondition: The proof must be labeled canonically
    (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
 fun compress_isar_proof compress_isar
-    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
+    ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
   if compress_isar <= 1.0 then
     proof
   else
@@ -136,57 +137,55 @@
 
       (** elimination of trivial, one-step subproofs **)
 
-      fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+      fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
         if null subs orelse not (compress_further ()) then
-          (set_preplay_outcome l (Played time);
-           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+          (set_preplay_outcome l meth (Played time);
+           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
         else
           (case subs of
             (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
-              (* trivial subproofs have exactly one Prove step *)
-              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+              (* trivial subproofs have exactly one "Prove" step *)
+              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
+                try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val Played time' = get_preplay_outcome l'
+              val Played time' = Lazy.force (preplay_outcome l' meth')
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
-              val lfs'' =
-                subtract (op =) (map fst assms) lfs'
-                |> union (op =) lfs
+              val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
               val gfs'' = union (op =) gfs' gfs
-              val by = ((lfs'', gfs''), meth)
+              val by = ((lfs'', gfs''), methss(*FIXME*))
               val step'' = Prove (qs, fix, l, t, subs'', by)
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
               val Played time'' = preplay_quietly timeout step''
-
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+              elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
             end
             handle Bind =>
-              elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+            elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
 
       fun elim_subproofs (step as Let _) = step
-        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
+            ((lfs, gfs), methss as (meth :: _) :: _))) =
           if subproofs = [] then
             step
           else
-            (case get_preplay_outcome l of
-              Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+            (case Lazy.force (preplay_outcome l meth) of
+              Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
             | _ => step)
 
       (** top_level compression: eliminate steps by merging them into their successors **)
-
       fun compress_top_level steps =
         let
           (* (#successors, (size_of_term t, position)) *)
-          fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+          fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
 
           val compression_ord =
             prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
@@ -207,33 +206,36 @@
                 | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
             in
               (steps
-              |> split_last |> fst (* keep last step *)
-              |> fold_index add_cand) []
+               |> split_last |> fst (* keep last step *)
+               |> fold_index add_cand) []
             end
 
           fun try_eliminate (i, l, _) succ_lbls steps =
             let
+              val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
+                drop i steps
+
+              val succs = collect_successors steps' succ_lbls
+              val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
+
               (* only touch steps that can be preplayed successfully *)
-              val Played time = get_preplay_outcome l
+              val Played time = Lazy.force (preplay_outcome l meth)
+
+              val succs' = map (try_merge cand #> the) succs
 
               val succ_times =
-                map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
+                map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
               val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
               val timeouts =
                 map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
 
-              val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
-
               (* FIXME: debugging *)
               val _ =
-                if the (label_of_step cand) <> l then
+                if the (label_of_isar_step cand) <> l then
                   raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
                 else
                   ()
 
-              val succs = collect_successors steps' succ_lbls
-              val succs' = map (try_merge cand #> the) succs
-
               (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
               val play_outcomes = map2 preplay_quietly timeouts succs'
 
@@ -245,7 +247,7 @@
               val steps2 = update_steps steps2 succs'
             in
               decrement_step_count (); (* candidate successfully eliminated *)
-              map2 set_preplay_outcome succ_lbls play_outcomes;
+              map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
               map (replace_successor l succ_lbls) lfs;
               (* removing the step would mess up the indices -> replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -26,12 +26,12 @@
 val slack = seconds 0.1
 
 fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
-  | minimize_isar_step_dependencies {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
-    (case get_preplay_outcome l of
+  | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
+    (case Lazy.force (preplay_outcome l meth) of
       Played time =>
       let
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
         val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
@@ -43,7 +43,7 @@
         val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
         val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
       in
-        set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+        set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
       end
     | _ => step (* don't touch steps that time out or fail *))
 
@@ -62,7 +62,7 @@
           fold_rev do_step steps (refed, [concl])
         end
     and do_step step (refed, accu) =
-      (case label_of_step step of
+      (case label_of_isar_step step of
         NONE => (refed, step :: accu)
       | SOME l =>
         if Ord_List.member label_ord refed l then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -8,6 +8,7 @@
 signature SLEDGEHAMMER_ISAR_PREPLAY =
 sig
   type play_outcome = Sledgehammer_Reconstructor.play_outcome
+  type proof_method = Sledgehammer_Isar_Proof.proof_method
   type isar_step = Sledgehammer_Isar_Proof.isar_step
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type label = Sledgehammer_Isar_Proof.label
@@ -15,8 +16,8 @@
   val trace : bool Config.T
 
   type isar_preplay_data =
-    {get_preplay_outcome: label -> play_outcome,
-     set_preplay_outcome: label -> play_outcome -> unit,
+    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
      preplay_quietly: Time.time -> isar_step -> play_outcome,
      overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -101,12 +102,12 @@
     | Force_Method => Clasimp.force_tac ctxt
     | Arith_Method => Arith_Data.arith_tac ctxt
     | Blast_Method => blast_tac ctxt
+    | Algebra_Method => Groebner.algebra_tac [] [] ctxt
     | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
-  | preplay_raw debug type_enc lam_trans ctxt timeout
-      (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
+fun preplay_raw debug type_enc lam_trans ctxt timeout meth
+      (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
     let
       val goal =
         (case xs of
@@ -144,12 +145,9 @@
        play_outcome)
     end
 
-
-(*** proof preplay interface ***)
-
 type isar_preplay_data =
-  {get_preplay_outcome: label -> play_outcome,
-   set_preplay_outcome: label -> play_outcome -> unit,
+  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
+   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    preplay_quietly: Time.time -> isar_step -> play_outcome,
    overall_preplay_outcome: isar_proof -> play_outcome}
 
@@ -188,16 +186,16 @@
 fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   if not do_preplay then
     (* the "dont_preplay" option pretends that everything works just fine *)
-    {get_preplay_outcome = K (Played Time.zeroTime),
-     set_preplay_outcome = K (K ()),
+    {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
+     set_preplay_outcome = K (K (K ())),
      preplay_quietly = K (K (Played Time.zeroTime)),
      overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
   else
     let
       val ctxt = enrich_context_with_local_facts proof ctxt
 
-      fun preplay quietly timeout step =
-        preplay_raw debug type_enc lam_trans ctxt timeout step
+      fun preplay quietly timeout meth step =
+        preplay_raw debug type_enc lam_trans ctxt timeout meth step
         handle exn =>
           if Exn.is_interrupt exn then
             reraise exn
@@ -209,39 +207,41 @@
              Play_Failed)
 
       (* preplay steps treating exceptions like timeouts *)
-      fun preplay_quietly timeout = preplay true timeout
+      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
+          preplay true timeout meth step
+        | preplay_quietly _ _ = Played Time.zeroTime
+
+      fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
+          Canonical_Label_Tab.update_new
+            (l, maps (map (fn meth =>
+               (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
+        | add_step_to_tab _ = I
 
       val preplay_tab =
-        let
-          fun add_step_to_tab step tab =
-            (case label_of_step step of
-              NONE => tab
-            | SOME l =>
-              Canonical_Label_Tab.update_new
-                (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
-            handle Canonical_Label_Tab.DUP _ =>
-              raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
-        in
-          Canonical_Label_Tab.empty
-          |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
-          |> Unsynchronized.ref
-        end
+        Canonical_Label_Tab.empty
+        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+        |> Unsynchronized.ref
 
-      fun get_preplay_outcome l =
-        Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
-        handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+      fun preplay_outcome l meth =
+        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
+          SOME meths_outcomes =>
+          (case AList.lookup (op =) meths_outcomes meth of
+            SOME outcome => outcome
+          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
+        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
 
-      fun set_preplay_outcome l result =
-        preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
+      fun set_preplay_outcome l meth result =
+        preplay_tab := Canonical_Label_Tab.map_entry l
+          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
 
-      val result_of_step =
-        try (label_of_step #> the #> get_preplay_outcome)
-        #> the_default (Played Time.zeroTime)
+      fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
+          Lazy.force (preplay_outcome l meth)
+        | result_of_step _ = Played Time.zeroTime
 
       fun overall_preplay_outcome (Proof (_, _, steps)) =
         fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
     in
-      {get_preplay_outcome = get_preplay_outcome,
+      {preplay_outcome = preplay_outcome,
        set_preplay_outcome = set_preplay_outcome,
        preplay_quietly = preplay_quietly,
        overall_preplay_outcome = overall_preplay_outcome}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -13,15 +13,16 @@
 
   datatype isar_qualifier = Show | Then
 
+  datatype proof_method =
+    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+    Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+
   datatype isar_proof =
     Proof of (string * typ) list * (label * term) list * isar_step list
   and isar_step =
     Let of term * term |
     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
       (facts * proof_method list list)
-  and proof_method =
-    Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
-    Arith_Method | Blast_Method | Meson_Method
 
   val no_label : label
   val no_facts : facts
@@ -29,10 +30,12 @@
   val label_ord : label * label -> order
   val string_of_label : label -> string
 
+  val string_of_proof_method : proof_method -> string
+
   val steps_of_proof : isar_proof -> isar_step list
 
-  val label_of_step : isar_step -> label option
-  val byline_of_step : isar_step -> (facts * proof_method list list) option
+  val label_of_isar_step : isar_step -> label option
+  val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
 
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -41,9 +44,14 @@
   structure Canonical_Label_Tab : TABLE
 
   val canonical_label_ord : (label * label) -> order
-  val relabel_isar_proof_canonically : isar_proof -> isar_proof
 
-  val string_of_isar_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
+  val chain_isar_proof : isar_proof -> isar_proof
+  val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
+  val relabel_isar_proof_canonically : isar_proof -> isar_proof
+  val relabel_isar_proof_finally : isar_proof -> isar_proof
+
+  val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
+    (label -> proof_method list list -> string) -> isar_proof -> string
 end;
 
 structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
@@ -62,15 +70,16 @@
 
 datatype isar_qualifier = Show | Then
 
+datatype proof_method =
+  Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+  Arith_Method | Blast_Method | Meson_Method | Algebra_Method
+
 datatype isar_proof =
   Proof of (string * typ) list * (label * term) list * isar_step list
 and isar_step =
   Let of term * term |
   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     (facts * proof_method list list)
-and proof_method =
-  Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
-  Arith_Method | Blast_Method | Meson_Method
 
 val no_label = ("", ~1)
 val no_facts = ([],[])
@@ -79,19 +88,32 @@
 
 fun string_of_label (s, num) = s ^ string_of_int num
 
+fun string_of_proof_method meth =
+  (case meth of
+    Metis_Method => "metis"
+  | Simp_Method => "simp"
+  | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
+  | Auto_Method => "auto"
+  | Fastforce_Method => "fastforce"
+  | Force_Method => "force"
+  | Arith_Method => "arith"
+  | Blast_Method => "blast"
+  | Meson_Method => "meson"
+  | Algebra_Method => "algebra")
+
 fun steps_of_proof (Proof (_, _, steps)) = steps
 
-fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
-  | label_of_step _ = NONE
+fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
+  | label_of_isar_step _ = NONE
 
-fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
-  | subproofs_of_step _ = NONE
+fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+  | subproofs_of_isar_step _ = NONE
 
-fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
-  | byline_of_step _ = NONE
+fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
+  | byline_of_isar_step _ = NONE
 
 fun 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_isar_step step)) #> f step
 and fold_isar_steps f = fold (fold_isar_step f)
 
 fun map_isar_steps f =
@@ -111,6 +133,38 @@
   type key = label
   val ord = canonical_label_ord)
 
+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_isar_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, map chain_isar_proof subproofs, ((lfs, gfs), methss))
+    end
+  | chain_isar_step _ step = step
+and chain_isar_steps _ [] = []
+  | chain_isar_steps (prev as SOME _) (i :: is) =
+    chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
+  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
+and chain_isar_proof (Proof (fix, assms, steps)) =
+  Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
+
+fun kill_useless_labels_in_isar_proof proof =
+  let
+    val used_ls =
+      fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+        (steps_of_proof proof) []
+
+    fun kill_label l = if member (op =) used_ls l then l else no_label
+
+    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
+        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
+      | kill_step step = step
+    and kill_proof (Proof (fix, assms, steps)) =
+      Proof (fix, map (apfst kill_label) assms, map kill_step steps)
+  in
+    kill_proof proof
+  end
+
 fun relabel_isar_proof_canonically proof =
   let
     fun next_label l (next, subst) =
@@ -146,9 +200,51 @@
     fst (do_proof proof (0, []))
   end
 
+val assume_prefix = "a"
+val have_prefix = "f"
+
+val relabel_isar_proof_finally =
+  let
+    fun fresh_label depth prefix (accum as (l, subst, next)) =
+      if l = no_label then
+        accum
+      else
+        let val l' = (replicate_string (depth + 1) prefix, next) in
+          (l', (l, l') :: subst, next + 1)
+        end
+
+    fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
+
+    fun relabel_assm depth (l, t) (subst, next) =
+      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
+        ((l, t), (subst, next))
+      end
+
+    fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
+
+    fun relabel_steps _ _ _ [] = []
+      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
+        let
+          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
+          val sub = relabel_proofs subst depth sub
+          val by = apfst (relabel_facts subst) by
+        in
+          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+        end
+      | relabel_steps subst depth next (step :: steps) =
+        step :: relabel_steps subst depth next steps
+    and relabel_proof subst depth (Proof (fix, assms, steps)) =
+      let val (assms, subst) = relabel_assms subst depth assms in
+        Proof (fix, assms, relabel_steps subst depth 1 steps)
+      end
+    and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
+  in
+    relabel_proof [] 0
+  end
+
 val indent_size = 2
 
-fun string_of_isar_proof ctxt type_enc lam_trans i n proof =
+fun string_of_isar_proof ctxt type_enc lam_trans i n comment_of proof =
   let
     (* Make sure only type constraints inserted by the type annotation code are printed. *)
     val ctxt =
@@ -160,7 +256,7 @@
 
     val register_fixes = map Free #> fold Variable.auto_fixes
 
-    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+    fun add_str s' = apfst (suffix s')
 
     fun of_indent ind = replicate_string (ind * indent_size) " "
     fun of_moreover ind = of_indent ind ^ "moreover\n"
@@ -188,18 +284,6 @@
             |> maybe_quote),
        ctxt |> Variable.auto_fixes term)
 
-    fun by_method meth = "by " ^
-      (case meth of
-        Simp_Method => "simp"
-      | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
-      | Auto_Method => "auto"
-      | Fastforce_Method => "fastforce"
-      | Force_Method => "force"
-      | Arith_Method => "arith"
-      | Blast_Method => "blast"
-      | Meson_Method => "meson"
-      | _ => raise Fail "Sledgehammer_Isar_Print: by_method")
-
     fun with_facts none _ [] [] = none
       | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
 
@@ -213,15 +297,7 @@
     fun of_method ls ss Metis_Method =
         using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
       | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
-      | of_method ls ss meth = using_facts ls ss ^ by_method 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) ^ of_method ls ss meth
-      end
+      | of_method ls ss meth = using_facts ls ss ^ "by " ^ string_of_proof_method meth
 
     fun of_free (s, T) =
       maybe_quote s ^ " :: " ^
@@ -232,22 +308,17 @@
 
     fun add_fix _ [] = I
       | add_fix ind xs =
-        add_suffix (of_indent ind ^ "fix ")
+        add_str (of_indent ind ^ "fix ")
         #> add_frees xs
-        #> add_suffix "\n"
+        #> add_str "\n"
 
     fun add_assm ind (l, t) =
-      add_suffix (of_indent ind ^ "assume " ^ of_label l)
+      add_str (of_indent ind ^ "assume " ^ of_label l)
       #> add_term t
-      #> add_suffix "\n"
+      #> add_str "\n"
 
     fun add_assms ind assms = fold (add_assm ind) assms
 
-    fun add_step_post ind l t facts meth =
-      add_suffix (of_label l)
-      #> add_term t
-      #> add_suffix (of_byline ind facts meth ^ "\n")
-
     fun of_subproof ind ctxt proof =
       let
         val ind = ind + 1
@@ -266,20 +337,22 @@
     and add_step_pre ind qs subproofs (s, ctxt) =
       (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
     and add_step ind (Let (t1, t2)) =
-        add_suffix (of_indent ind ^ "let ")
-        #> add_term t1
-        #> add_suffix " = "
-        #> add_term t2
-        #> add_suffix "\n"
-      | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
+        add_str (of_indent ind ^ "let ")
+        #> add_term t1 #> add_str " = " #> add_term t2
+        #> add_str "\n"
+      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (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
+             [] => add_str (of_have qs (length subproofs) ^ " ")
+           | _ =>
+             add_str (of_obtain qs (length subproofs) ^ " ") #> add_frees xs #> add_str " where ")
+        #> add_str (of_label l)
+        #> add_term t
+        #> add_str (" " ^
+             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
+             (case comment_of l methss of
+               "" => ""
+             | comment => " (* " ^ comment ^ " *)") ^ "\n")
     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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -30,11 +30,11 @@
 
 fun try0_step _ _ (step as Let _) = step
   | try0_step preplay_timeout
-      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
-      (step as Prove (_, _, l, _, _, _)) =
+      ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
+      (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
     let
       val timeout =
-        (case get_preplay_outcome l of
+        (case Lazy.force (preplay_outcome l meth) of
           Played time => Time.+ (time, slack)
         | _ => preplay_timeout)
 
@@ -44,7 +44,8 @@
         | _ => NONE)
     in
       (case Par_List.get_some try_variant (variants_of_step step) of
-        SOME (step', result) => (set_preplay_outcome l result; step')
+        SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
+        (set_preplay_outcome l meth' result; step')
       | NONE => step)
     end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 18:58:50 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 19:32:13 2014 +0100
@@ -8,6 +8,7 @@
 sig
   val sledgehammerN : string
   val log2 : real -> real
+  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val app_hd : ('a -> 'a) -> 'a list -> 'a list
   val n_fold_cartesian_product : 'a list list -> 'a list list
   val plural_s : int -> string
@@ -38,6 +39,8 @@
 val log10_2 = Math.log10 2.0
 fun log2 n = Math.log10 n / log10_2
 
+fun map3 xs = Ctr_Sugar_Util.map3 xs
+
 fun app_hd f (x :: xs) = f x :: xs
 
 fun cartesian_product [] _ = []