# HG changeset patch # User wenzelm # Date 1350566929 -7200 # Node ID 12cece6d951da368db249841da93f35b06ba4e4b # Parent 54ec43352eb1c790a7c220b620186248329610ca# Parent 70a2694e924f45cbcc4dcb099fed6afe8fca4f08 merged diff -r 70a2694e924f -r 12cece6d951d NEWS --- a/NEWS Thu Oct 18 15:16:39 2012 +0200 +++ b/NEWS Thu Oct 18 15:28:49 2012 +0200 @@ -185,6 +185,8 @@ - Rationalized type encodings ("type_enc" option). - Renamed "kill_provers" subcommand to "kill" - Renamed options: + isar_proof ~> isar_proofs + isar_shrink_factor ~> isar_shrinkage max_relevant ~> max_facts relevance_thresholds ~> fact_thresholds diff -r 70a2694e924f -r 12cece6d951d src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Oct 18 15:16:39 2012 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Oct 18 15:28:49 2012 +0200 @@ -309,10 +309,10 @@ fast the call is. You can click the proof to insert it into the theory text. In addition, you can ask Sledgehammer for an Isar text proof by passing the -\textit{isar\_proof} option (\S\ref{output-format}): +\textit{isar\_proofs} option (\S\ref{output-format}): \prew -\textbf{sledgehammer} [\textit{isar\_proof}] +\textbf{sledgehammer} [\textit{isar\_proofs}] \postw When Isar proof construction is successful, it can yield proofs that are more @@ -366,10 +366,10 @@ the provers time out, you can try lowering this value to, say, 25 or 50 and see if that helps. -\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies +\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies that Isar proofs should be generated, instead of one-liner \textit{metis} or \textit{smt} proofs. The length of the Isar proofs can be controlled by setting -\textit{isar\_shrink\_factor} (\S\ref{output-format}). +\textit{isar\_shrinkage} (\S\ref{output-format}). \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the provers' time limit. It is set to 30 seconds, but since Sledgehammer runs @@ -470,7 +470,7 @@ solutions: \begin{enum} -\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to +\item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to obtain a step-by-step Isar proof where each step is justified by \textit{metis}. Since the steps are fairly small, \textit{metis} is more likely to be able to replay them. @@ -504,11 +504,11 @@ \point{Why are the generated Isar proofs so ugly/broken?} The current implementation of the Isar proof feature, -enabled by the \textit{isar\_proof} option (\S\ref{output-format}), +enabled by the \textit{isar\_proofs} option (\S\ref{output-format}), is highly experimental. Work on a new implementation has begun. There is a large body of research into transforming resolution proofs into natural deduction proofs (such as Isar proofs), which we hope to leverage. In the meantime, a workaround is to -set the \textit{isar\_shrink\_factor} option (\S\ref{output-format}) to a larger +set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger value or to try several provers and keep the nicest-looking proof. \point{How can I tell whether a suggested proof is sound?} @@ -723,7 +723,7 @@ example: \prew -\textbf{sledgehammer} [\textit{isar\_proof}, \,\textit{timeout} = 120] +\textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] \postw Default values can be set using \textbf{sledgehammer\_\allowbreak params}: @@ -1293,16 +1293,16 @@ \nopagebreak {\small See also \textit{overlord} (\S\ref{mode-of-operation}).} -\opfalse{isar\_proof}{no\_isar\_proof} +\opfalse{isar\_proofs}{no\_isar\_proofs} Specifies whether Isar proofs should be output in addition to one-liner \textit{metis} proofs. Isar proof construction is still experimental and often fails; however, they are usually faster and sometimes more robust than \textit{metis} proofs. -\opdefault{isar\_shrink\_factor}{int}{\upshape 1} -Specifies the granularity of the Isar proof. A value of $n$ indicates that each -Isar proof step should correspond to a group of up to $n$ consecutive proof -steps in the ATP proof. +\opdefault{isar\_shrinkage}{int}{\upshape 10} +Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs} +is enabled. A value of $n$ indicates that each Isar proof step should correspond +to a group of up to $n$ consecutive proof steps in the ATP proof. \end{enum} \subsection{Authentication} diff -r 70a2694e924f -r 12cece6d951d src/HOL/Metis_Examples/Big_O.thy --- a/src/HOL/Metis_Examples/Big_O.thy Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Metis_Examples/Big_O.thy Thu Oct 18 15:28:49 2012 +0200 @@ -29,7 +29,7 @@ (*** Now various verions with an increasing shrink factor ***) -sledgehammer_params [isar_proof, isar_shrink_factor = 1] +sledgehammer_params [isar_proofs, isar_shrinkage = 1] lemma "(\c\'a\linordered_idom. @@ -60,7 +60,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F4) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 2] +sledgehammer_params [isar_proofs, isar_shrinkage = 2] lemma "(\c\'a\linordered_idom. @@ -83,7 +83,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis F2) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 3] +sledgehammer_params [isar_proofs, isar_shrinkage = 3] lemma "(\c\'a\linordered_idom. @@ -103,7 +103,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis A1 abs_ge_zero) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 4] +sledgehammer_params [isar_proofs, isar_shrinkage = 4] lemma "(\c\'a\linordered_idom. @@ -123,7 +123,7 @@ thus "\h x\ \ \c\ * \f x\" by (metis abs_mult) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 1] +sledgehammer_params [isar_proofs, isar_shrinkage = 1] lemma bigo_alt_def: "O(f) = {h. \c. (0 < c \ (\x. abs (h x) <= c * abs (f x)))}" by (auto simp add: bigo_def bigo_pos_const) diff -r 70a2694e924f -r 12cece6d951d src/HOL/Metis_Examples/Sets.thy --- a/src/HOL/Metis_Examples/Sets.thy Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Metis_Examples/Sets.thy Thu Oct 18 15:28:49 2012 +0200 @@ -21,7 +21,7 @@ lemma "P(n::nat) ==> ~P(0) ==> n ~= 0" by metis -sledgehammer_params [isar_proof, isar_shrink_factor = 1] +sledgehammer_params [isar_proofs, isar_shrinkage = 1] (*multiple versions of this example*) lemma (*equal_union: *) @@ -70,7 +70,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proof, isar_shrink_factor = 2] +sledgehammer_params [isar_proofs, isar_shrinkage = 2] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -107,7 +107,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by metis qed -sledgehammer_params [isar_proof, isar_shrink_factor = 3] +sledgehammer_params [isar_proofs, isar_shrinkage = 3] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -124,7 +124,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_commute Un_upper2) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 4] +sledgehammer_params [isar_proofs, isar_shrinkage = 4] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" @@ -140,7 +140,7 @@ ultimately show "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V\'a set. Y \ V \ Z \ V \ X \ V))" by (metis Un_subset_iff Un_upper2) qed -sledgehammer_params [isar_proof, isar_shrink_factor = 1] +sledgehammer_params [isar_proofs, isar_shrinkage = 1] lemma (*equal_union: *) "(X = Y \ Z) = (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" diff -r 70a2694e924f -r 12cece6d951d src/HOL/Metis_Examples/Trans_Closure.thy --- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Oct 18 15:28:49 2012 +0200 @@ -44,7 +44,7 @@ lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\ \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" -(* sledgehammer [isar_proof, isar_shrink_factor = 2] *) +(* sledgehammer [isar_proofs, isar_shrinkage = 2] *) proof - assume A1: "f c = Intg x" assume A2: "\y. f b = Intg y \ y \ x" diff -r 70a2694e924f -r 12cece6d951d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 18 15:28:49 2012 +0200 @@ -486,19 +486,6 @@ end handle ERROR msg => ("error: " ^ msg, SH_ERROR) -fun thms_of_name ctxt name = - let - val lex = Keyword.get_lexicons - val get = maps (Proof_Context.get_fact ctxt o fst) - in - Source.of_string name - |> Symbol.source - |> Token.source {do_recover=SOME false} lex Position.start - |> Token.source_proper - |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE - |> Source.exhaust - end - in fun run_sledgehammer trivial args reconstructor named_thms id @@ -544,7 +531,8 @@ SH_OK (time_isa, time_prover, names) => let fun get_thms (name, stature) = - try (thms_of_name (Proof.context_of st)) name + try (Sledgehammer_Reconstruct.thms_of_name (Proof.context_of st)) + name |> Option.map (pair (name, stature)) in change_data id inc_sh_success; diff -r 70a2694e924f -r 12cece6d951d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 18 15:28:49 2012 +0200 @@ -94,8 +94,8 @@ ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), - ("isar_proof", "false"), - ("isar_shrink_factor", "1"), + ("isar_proofs", "false"), + ("isar_shrinkage", "10"), ("slice", "true"), ("minimize", "smart"), ("preplay_timeout", "3")] @@ -112,14 +112,14 @@ ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), - ("no_isar_proof", "isar_proof"), + ("no_isar_proofs", "isar_proofs"), ("dont_slice", "slice"), ("dont_minimize", "minimize")] val params_for_minimize = ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", "uncurried_aliases", "max_mono_iters", "max_new_mono_instances", - "isar_proof", "isar_shrink_factor", "timeout", "preplay_timeout"] + "isar_proofs", "isar_shrinkage", "timeout", "preplay_timeout"] val property_dependent_params = ["provers", "timeout"] @@ -272,6 +272,13 @@ SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value.") + fun lookup_real name = + case lookup name of + NONE => 0.0 + | SOME s => case Real.fromString s of + SOME n => n + | NONE => error ("Parameter " ^ quote name ^ + " must be assigned a real value.") fun lookup_real_pair name = case lookup name of NONE => (0.0, 0.0) @@ -308,8 +315,8 @@ val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" - val isar_proof = lookup_bool "isar_proof" - val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") + val isar_proofs = lookup_bool "isar_proofs" + val isar_shrinkage = Real.max (1.0, lookup_real "isar_shrinkage") val slice = mode <> Auto_Try andalso lookup_bool "slice" val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" @@ -325,10 +332,9 @@ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, + isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r 70a2694e924f -r 12cece6d951d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 18 15:28:49 2012 +0200 @@ -54,7 +54,7 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, - uncurried_aliases, isar_proof, isar_shrink_factor, + uncurried_aliases, isar_proofs, isar_shrinkage, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let @@ -72,9 +72,9 @@ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slice = false, - minimize = SOME false, timeout = timeout, + max_new_mono_instances = max_new_mono_instances, + isar_proofs = isar_proofs, isar_shrinkage = isar_shrinkage, + slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, @@ -236,8 +236,8 @@ fun adjust_reconstructor_params override_params ({debug, verbose, overlord, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, - fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof, - isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect} + fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, + isar_shrinkage, slice, minimize, timeout, preplay_timeout, expect} : params) = let fun lookup_override name default_value = @@ -254,14 +254,13 @@ lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, + isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun maybe_minimize ctxt mode do_learn name - (params as {verbose, isar_proof, minimize, ...}) + (params as {verbose, isar_proofs, minimize, ...}) ({state, subgoal, subgoal_count, facts, ...} : prover_problem) (result as {outcome, used_facts, run_time, preplay, message, message_tail} : prover_result) = @@ -282,7 +281,7 @@ <= Config.get ctxt auto_minimize_max_time fun prover_fast_enough () = can_min_fast_enough run_time in - if isar_proof then + if isar_proofs then ((prover_fast_enough (), (name, params)), preplay) else let val preplay = preplay () in diff -r 70a2694e924f -r 12cece6d951d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 15:28:49 2012 +0200 @@ -33,8 +33,8 @@ fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, - isar_proof : bool, - isar_shrink_factor : int, + isar_proofs : bool, + isar_shrinkage : real, slice : bool, minimize : bool option, timeout : Time.time, @@ -326,8 +326,8 @@ fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, - isar_proof : bool, - isar_shrink_factor : int, + isar_proofs : bool, + isar_shrinkage : real, slice : bool, minimize : bool option, timeout : Time.time, @@ -642,7 +642,7 @@ best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, max_mono_iters, - max_new_mono_instances, isar_proof, isar_shrink_factor, + max_new_mono_instances, isar_proofs, isar_shrinkage, slice, timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = @@ -777,7 +777,7 @@ fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name - val full_proof = debug orelse isar_proof + val full_proof = debug orelse isar_proofs val args = arguments ctxt full_proof extra slice_timeout (ord, ord_info, sel_weights) val command = @@ -883,7 +883,7 @@ fn preplay => let val isar_params = - (debug, isar_shrink_factor, pool, fact_names, sym_tab, + (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, atp_proof, goal) val one_line_params = (preplay, proof_banner mode name, used_facts, @@ -891,7 +891,7 @@ subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt isar_proof isar_params num_chained + proof_text ctxt isar_proofs isar_params num_chained one_line_params end, (if verbose then diff -r 70a2694e924f -r 12cece6d951d src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 15:16:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 15:28:49 2012 +0200 @@ -23,11 +23,12 @@ type one_line_params = play * string * (string * stature) list * minimize_command * int * int type isar_params = - bool * int * string Symtab.table * (string * stature) list vector + bool * bool * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm val smtN : string val string_for_reconstructor : reconstructor -> string + val thms_of_name : Proof.context -> string -> thm list val lam_trans_from_atp_proof : string proof -> string -> string val is_typed_helper_used_in_atp_proof : string proof -> bool val used_facts_in_atp_proof : @@ -51,6 +52,7 @@ open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct +open Sledgehammer_Util structure String_Redirect = ATP_Proof_Redirect( type key = step_name @@ -59,6 +61,7 @@ open String_Redirect + (** reconstructors **) datatype reconstructor = @@ -76,6 +79,19 @@ metis_call type_enc lam_trans | string_for_reconstructor SMT = smtN +fun thms_of_name ctxt name = + let + val lex = Keyword.get_lexicons + val get = maps (Proof_Context.get_fact ctxt o fst) + in + Source.of_string name + |> Symbol.source + |> Token.source {do_recover=SOME false} lex Position.start + |> Token.source_proper + |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE + |> Source.exhaust + end + (** fact extraction from ATP proofs **) @@ -433,9 +449,9 @@ fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false -fun add_desired_line _ _ _ (line as Definition_Step (name, _, _)) (j, lines) = +fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) - | add_desired_line isar_shrink_factor fact_names frees + | add_desired_line fact_names frees (Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) = (j + 1, if is_fact fact_names ss orelse @@ -445,7 +461,7 @@ (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso not (exists_subterm (is_bad_free frees) t) andalso - length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso + length deps >= 2 andalso (* kill next to last line, which usually results in a trivial step *) j <> 1) then Inference_Step (name, t, rule, deps) :: lines (* keep line *) @@ -734,7 +750,9 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end -fun minimize_locally ctxt type_enc lam_trans proof = +val merge_timeout_slack = 1.2 + +fun shrink_locally ctxt type_enc lam_trans isar_shrinkage proof = let (* Merging spots, greedy algorithm *) fun cost (Prove (_, _ , t, _)) = Term.size_of_term t @@ -747,11 +765,11 @@ fold_index (fn (i, s2) => fn (s1, pile) => (s2, pile |> can_merge s1 s2 ? cons (i, cost s1))) (tl proof) (hd proof, []) - |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst + |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst - (* Enrich context with facts *) + (* Enrich context with local facts *) val thy = Proof_Context.theory_of ctxt - fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) + fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = ctxt |> lbl <> no_label ? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) @@ -760,21 +778,18 @@ (* Timing *) fun take_time tac arg = - let - val t_start = Timing.start () - in - (tac arg ; Timing.result t_start |> #cpu) + let val timing = Timing.start () in + (tac arg; Timing.result timing |> #cpu) end fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 = let fun thmify (Prove (_, _, t, _)) = sorry t val facts = fact_names - |>> map string_for_label - |> op @ - |> map (Proof_Context.get_thm rich_ctxt) + |>> map string_for_label |> op @ + |> map (the_single o thms_of_name rich_ctxt) |> (if member (op =) qs Then then cons (the s0 |> thmify) else I) - val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *) + val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) fun tac {context = ctxt, prems = _} = Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 in @@ -802,32 +817,34 @@ val s12 = merge s1 s2 val t1 = try_metis s1 s0 () val t2 = try_metis s2 (SOME s1) () - val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal + val timeout = + t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack + |> Time.fromReal in - (TimeLimit.timeLimit tlimit (try_metis s12 s0) (); - SOME (front @ (case s0 of - NONE => s12 :: tail - | SOME s => s :: s12 :: tail))) + (TimeLimit.timeLimit timeout (try_metis s12 s0) (); + SOME (front @ (the_list s0 @ s12 :: tail))) handle _ => NONE end - fun merge_steps proof [] = proof - | merge_steps proof (i :: is) = - case try_merge proof i of - NONE => merge_steps proof is + fun spill_shrinkage shrinkage = isar_shrinkage + shrinkage - 1.0 + fun merge_steps _ proof [] = proof + | merge_steps shrinkage proof (i :: is) = + if shrinkage < 1.5 then + merge_steps (spill_shrinkage shrinkage) proof is + else case try_merge proof i of + NONE => merge_steps (spill_shrinkage shrinkage) proof is | SOME proof' => - merge_steps proof' (map (fn j => if j > i then j - 1 else j) is) - in merge_steps proof merge_spots end + merge_steps (shrinkage - 1.0) proof' + (map (fn j => if j > i then j - 1 else j) is) + in merge_steps isar_shrinkage proof merge_spots end type isar_params = - bool * int * string Symtab.table * (string * stature) list vector + bool * bool * real * string Symtab.table * (string * stature) list vector * int Symtab.table * string proof * thm -fun isar_proof_text ctxt isar_proof_requested - (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal) - (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = +fun isar_proof_text ctxt isar_proofs + (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, atp_proof, goal) + (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val isar_shrink_factor = - (if isar_proof_requested then 1 else 2) * isar_shrink_factor val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val one_line_proof = one_line_proof_text 0 one_line_params @@ -848,7 +865,7 @@ |> repair_waldmeister_endgame |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) - |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees) + |-> fold_rev (add_desired_line fact_names frees) |> snd val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) val conjs = @@ -894,42 +911,54 @@ map (do_inf outer) infs val isar_proof = (if null params then [] else [Fix params]) @ - (ref_graph + (ref_graph |> redirect_graph axioms tainted |> chain_direct_proof |> map (do_inf true) |> kill_duplicate_assumptions_in_proof |> kill_useless_labels_in_proof |> relabel_proof - |> minimize_locally ctxt type_enc lam_trans) - |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count + |> shrink_locally ctxt type_enc lam_trans + (if isar_proofs then isar_shrinkage else 1000.0)) + val num_steps = length isar_proof + val isar_text = + string_for_proof ctxt type_enc lam_trans subgoal subgoal_count + isar_proof in - case isar_proof of + case isar_text of "" => - if isar_proof_requested then + if isar_proofs then "\nNo structured proof available (proof too short)." else "" | _ => - "\n\n" ^ (if isar_proof_requested then "Structured proof" - else "Perhaps this will work") ^ - ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof + "\n\n" ^ + (if isar_proofs then + "Structured proof" ^ + (if verbose then + " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^ + ")" + else + "") + else + "Perhaps this will work") ^ + ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text end val isar_proof = if debug then isar_proof_of () else case try isar_proof_of () of SOME s => s - | NONE => if isar_proof_requested then + | NONE => if isar_proofs then "\nWarning: The Isar proof construction failed." else "" in one_line_proof ^ isar_proof end -fun proof_text ctxt isar_proof isar_params num_chained +fun proof_text ctxt isar_proofs isar_params num_chained (one_line_params as (preplay, _, _, _, _, _)) = - (if case preplay of Failed_to_Play _ => true | _ => isar_proof then - isar_proof_text ctxt isar_proof isar_params + (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then + isar_proof_text ctxt isar_proofs isar_params else one_line_proof_text num_chained) one_line_params