# HG changeset patch
# User blanchet
# Date 1403590762 -7200
# Node ID 4868ec62f533baf1ac55ba11b300ce03f0c325a6
# Parent  a9c2272d01f630994a6ea2d27a3abb9bd9de45f7
don't generate Isar proof skeleton for what amounts to a one-line proof

diff -r a9c2272d01f6 -r 4868ec62f533 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 24 08:19:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 24 08:19:22 2014 +0200
@@ -329,25 +329,19 @@
                #> chain_isar_proof
                #> kill_useless_labels_in_isar_proof
                #> relabel_isar_proof_nicely)
+
+        val isar_text = string_of_isar_proof ctxt subgoal subgoal_count isar_proof
+        val msg =
+          (if verbose then
+             let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
+               [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+             end
+           else
+             []) @
+          (if do_preplay then [string_of_play_outcome play_outcome] else [])
       in
-        (case string_of_isar_proof ctxt subgoal subgoal_count isar_proof of
-          "" =>
-          if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
-          else ""
-        | isar_text =>
-          let
-            val msg =
-              (if verbose then
-                 let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
-                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
-                 end
-               else
-                 []) @
-              (if do_preplay then [string_of_play_outcome play_outcome] else [])
-          in
-            "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
-            Active.sendback_markup [Markup.padding_command] isar_text
-          end)
+        "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+        Active.sendback_markup [Markup.padding_command] isar_text
       end
 
     val one_line_proof = one_line_proof_text ctxt 0 one_line_params
diff -r a9c2272d01f6 -r 4868ec62f533 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Jun 24 08:19:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Jun 24 08:19:22 2014 +0200
@@ -122,7 +122,7 @@
 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 (x as Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
+fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
     let val (qs', lfs) = chain_qs_lfs lbl lfs in
       Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
     end
@@ -261,10 +261,10 @@
        arguably stylistically superior, because it emphasises the structure of the proof. It is also
        more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
        and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
-    fun of_method ls ss meth =
+    fun of_method command ls ss meth =
       let val direct = is_direct_method meth in
         using_facts ls (if direct then [] else ss) ^
-        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
+        command ^ " " ^ string_of_proof_method ctxt (if direct then ss else []) meth
       end
 
     fun of_free (s, T) =
@@ -308,7 +308,7 @@
         #> add_str (of_label l)
         #> add_term t
         #> add_str (" " ^
-             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
+             of_method "by" (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
              (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
     and add_steps ind = fold (add_step ind)
     and of_proof ind ctxt (Proof (xs, assms, steps)) =
@@ -318,14 +318,13 @@
       |> add_steps ind steps
       |> fst
   in
-    (* One-step Metis proofs are pointless; better use the one-liner directly. *)
+    (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
     (case proof of
-      Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
-    | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => ""
+      Proof (_, _, [Prove (_, _, _, _, [], (_, gfs), meth :: _, _)]) =>
+      of_method (if n = 1 then "by" else "apply") [] gfs meth
     | _ =>
-      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
       of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
-      of_indent 0 ^ (if n <> 1 then "next" else "qed"))
+      of_indent 0 ^ (if n = 1 then "qed" else "next"))
   end
 
 end;