--- a/NEWS Tue Nov 06 15:12:31 2012 +0100
+++ b/NEWS Tue Nov 06 15:15:33 2012 +0100
@@ -227,7 +227,7 @@
- Renamed "kill_provers" subcommand to "kill"
- Renamed options:
isar_proof ~> isar_proofs
- isar_shrink_factor ~> isar_shrinkage
+ isar_shrink_factor ~> isar_shrink
max_relevant ~> max_facts
relevance_thresholds ~> fact_thresholds
--- a/src/Doc/Sledgehammer/document/root.tex Tue Nov 06 15:12:31 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Tue Nov 06 15:15:33 2012 +0100
@@ -369,7 +369,7 @@
\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\_shrinkage} (\S\ref{output-format}).
+\textit{isar\_shrink} (\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
@@ -508,7 +508,7 @@
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\_shrinkage} option (\S\ref{output-format}) to a larger
+set the \textit{isar\_shrink} 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?}
@@ -1299,7 +1299,7 @@
fails; however, they are usually faster and sometimes more robust than
\textit{metis} proofs.
-\opdefault{isar\_shrinkage}{int}{\upshape 10}
+\opdefault{isar\_shrink}{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.
--- a/src/HOL/Metis_Examples/Big_O.thy Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Tue Nov 06 15:15:33 2012 +0100
@@ -29,7 +29,7 @@
(*** Now various verions with an increasing shrink factor ***)
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 2]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 3]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 4]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 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 Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Tue Nov 06 15:15:33 2012 +0100
@@ -21,7 +21,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 2]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 3]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 4]
+sledgehammer_params [isar_proofs, isar_shrink = 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_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 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 Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Tue Nov 06 15:15:33 2012 +0100
@@ -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_proofs, isar_shrinkage = 2] *)
+(* sledgehammer [isar_proofs, isar_shrink = 2] *)
proof -
assume A1: "f c = Intg x"
assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Nov 06 15:15:33 2012 +0100
@@ -95,7 +95,7 @@
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
("isar_proofs", "false"),
- ("isar_shrinkage", "10"),
+ ("isar_shrink", "10"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "3")]
@@ -119,7 +119,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
"uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
- "isar_proofs", "isar_shrinkage", "timeout", "preplay_timeout"]
+ "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "timeout"]
@@ -316,7 +316,7 @@
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_bool "isar_proofs"
- val isar_shrinkage = Real.max (1.0, lookup_real "isar_shrinkage")
+ val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize =
if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -333,7 +333,7 @@
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_proofs = isar_proofs,
- isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+ isar_shrink = isar_shrink, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Nov 06 15:15:33 2012 +0100
@@ -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_proofs, isar_shrinkage,
+ uncurried_aliases, isar_proofs, isar_shrink,
preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -73,7 +73,7 @@
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_proofs = isar_proofs, isar_shrinkage = isar_shrinkage,
+ isar_proofs = isar_proofs, isar_shrink = isar_shrink,
slice = false, minimize = SOME false, timeout = timeout,
preplay_timeout = preplay_timeout, expect = ""}
val problem =
@@ -237,7 +237,7 @@
({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_proofs,
- isar_shrinkage, slice, minimize, timeout, preplay_timeout, expect}
+ isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
: params) =
let
fun lookup_override name default_value =
@@ -255,7 +255,7 @@
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_proofs = isar_proofs,
- isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+ isar_shrink = isar_shrink, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 06 15:15:33 2012 +0100
@@ -34,7 +34,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool,
- isar_shrinkage : real,
+ isar_shrink : real,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -327,7 +327,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool,
- isar_shrinkage : real,
+ isar_shrink : 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_proofs, isar_shrinkage,
+ max_new_mono_instances, isar_proofs, isar_shrink,
slice, timeout, preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -888,7 +888,7 @@
else
()
val isar_params =
- (debug, verbose, preplay_timeout, isar_shrinkage,
+ (debug, verbose, preplay_timeout, isar_shrink,
pool, fact_names, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 06 15:15:33 2012 +0100
@@ -748,8 +748,8 @@
type key = label
val ord = label_ord)
-fun shrink_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout isar_shrinkage proof =
+fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
+ isar_shrink proof =
let
(* clean vector interface *)
fun get i v = Vector.sub (v, i)
@@ -770,7 +770,7 @@
(* proof vector *)
val proof_vect = proof |> map SOME |> Vector.fromList
val n = Vector.length proof_vect
- val n_target = Real.fromInt n / isar_shrinkage |> Real.round
+ val n_target = Real.fromInt n / isar_shrink |> Real.round
(* table for mapping from label to proof position *)
fun update_table (i, Prove (_, label, _, _)) =
@@ -932,8 +932,8 @@
* (string * stature) list vector * int Symtab.table * string proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_shrinkage,
- pool, fact_names, sym_tab, atp_proof, goal)
+ (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
+ atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
@@ -1030,8 +1030,7 @@
|> map (do_inf true)
|> append assms
|> shrink_proof debug ctxt type_enc lam_trans preplay
- preplay_timeout
- (if isar_proofs then isar_shrinkage else 1000.0)
+ preplay_timeout (if isar_proofs then isar_shrink else 1000.0)
(* ||> reorder_proof_to_minimize_jumps (* ? *) *)
||> chain_direct_proof
||> kill_useless_labels_in_proof