--- 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
--- 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}
--- 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
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
qed
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+sledgehammer_params [isar_proofs, isar_shrinkage = 2]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
qed
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+sledgehammer_params [isar_proofs, isar_shrinkage = 3]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
qed
-sledgehammer_params [isar_proof, isar_shrink_factor = 4]
+sledgehammer_params [isar_proofs, isar_shrinkage = 4]
lemma
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" 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. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
by (auto simp add: bigo_def bigo_pos_const)
--- 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 \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proof, isar_shrink_factor = 2]
+sledgehammer_params [isar_proofs, isar_shrinkage = 2]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -107,7 +107,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
qed
-sledgehammer_params [isar_proof, isar_shrink_factor = 3]
+sledgehammer_params [isar_proofs, isar_shrinkage = 3]
lemma (*equal_union: *)
"(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -124,7 +124,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> 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 \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
@@ -140,7 +140,7 @@
ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> 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 \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
--- 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 "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
\<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proof, isar_shrink_factor = 2] *)
+(* sledgehammer [isar_proofs, isar_shrinkage = 2] *)
proof -
assume A1: "f c = Intg x"
assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
--- 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;
--- 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
--- 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
--- 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
--- 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