--- 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
@@ -117,11 +117,12 @@
val skolem_methods = basic_systematic_methods
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
- (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
+ (one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal,
+ subgoal_count)) =
let
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
- fun isar_proof_of () =
+ fun generate_proof_text () =
let
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
isar_params ()
@@ -329,32 +330,42 @@
#> 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
- "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
- Active.sendback_markup [Markup.padding_command] isar_text
+ (case add_isar_steps (steps_of_isar_proof isar_proof) 0 of
+ 1 =>
+ one_line_proof_text ctxt 0
+ (if play_outcome_ord (play_outcome, one_line_play) = LESS then
+ (case isar_proof of
+ Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
+ let val used_facts' = filter (member (op =) gfs o fst) used_facts in
+ ((meth, play_outcome), banner, used_facts', minimize_command, subgoal,
+ subgoal_count)
+ end)
+ else
+ one_line_params) ^
+ (if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)"
+ else "")
+ | num_steps =>
+ let
+ val msg =
+ (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @
+ (if do_preplay then [string_of_play_outcome play_outcome] else [])
+ in
+ one_line_proof_text ctxt 0 one_line_params ^
+ "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+ Active.sendback_markup [Markup.padding_command]
+ (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
+ end)
end
-
- val one_line_proof = one_line_proof_text ctxt 0 one_line_params
- val isar_proof =
- if debug then
- isar_proof_of ()
- else
- (case try isar_proof_of () of
- SOME s => s
- | NONE =>
- if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
in
- one_line_proof ^ isar_proof
+ if debug then
+ generate_proof_text ()
+ else
+ (case try generate_proof_text () of
+ SOME s => s
+ | NONE =>
+ one_line_proof_text ctxt 0 one_line_params ^
+ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else ""))
end
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
--- 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
@@ -251,20 +251,14 @@
fun using_facts [] [] = ""
| using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
- fun is_direct_method (Metis_Method _) = true
- | is_direct_method Meson_Method = true
- | is_direct_method SMT2_Method = true
- | is_direct_method Simp_Method = true
- | is_direct_method _ = false
-
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
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 command ls ss meth =
- let val direct = is_direct_method meth in
+ fun of_method ls ss meth =
+ let val direct = is_proof_method_direct meth in
using_facts ls (if direct then [] else ss) ^
- command ^ " " ^ string_of_proof_method ctxt (if direct then ss else []) meth
+ "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
end
fun of_free (s, T) =
@@ -308,7 +302,7 @@
#> add_str (of_label l)
#> add_term t
#> add_str (" " ^
- of_method "by" (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
+ of_method (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)) =
@@ -319,12 +313,8 @@
|> fst
in
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- (case proof of
- Proof (_, _, [Prove (_, _, _, _, [], (_, gfs), meth :: _, _)]) =>
- of_method (if n = 1 then "by" else "apply") [] gfs meth
- | _ =>
- of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
- of_indent 0 ^ (if n = 1 then "qed" else "next"))
+ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
+ of_indent 0 ^ (if n = 1 then "qed" else "next")
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:22 2014 +0200
@@ -33,6 +33,7 @@
type one_line_params =
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+ val is_proof_method_direct : proof_method -> bool
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
@@ -71,6 +72,12 @@
type one_line_params =
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+fun is_proof_method_direct (Metis_Method _) = true
+ | is_proof_method_direct Meson_Method = true
+ | is_proof_method_direct SMT2_Method = true
+ | is_proof_method_direct Simp_Method = true
+ | is_proof_method_direct _ = false
+
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
fun string_of_proof_method ctxt ss meth =
@@ -136,12 +143,14 @@
fun apply_on_subgoal _ 1 = "by "
| apply_on_subgoal 1 _ = "apply "
- | apply_on_subgoal i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+ | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
(* FIXME *)
fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
- apply_on_subgoal i n ^ string_of_proof_method ctxt ss meth
+ let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in
+ (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
+ apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth
+ end
fun try_command_line banner play command =
let val s = string_of_play_outcome play in