--- a/NEWS Thu Jan 30 14:28:04 2014 +0100
+++ b/NEWS Thu Jan 30 14:37:53 2014 +0100
@@ -114,6 +114,14 @@
* Theory reorganizations:
* Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
+* Sledgehammer:
+ - Renamed options:
+ isar_compress ~> compress_isar
+ isar_try0 ~> try0_isar
+ INCOMPATIBILITY.
+
+* Try0: Added 'algebra' and 'meson' to the set of proof methods.
+
* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
--- a/src/Doc/Sledgehammer/document/root.tex Thu Jan 30 14:28:04 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jan 30 14:37:53 2014 +0100
@@ -359,7 +359,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, in addition to one-liner \textit{metis} or
\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
-\textit{isar\_compress} (\S\ref{output-format}).
+\textit{compress\_isar} (\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
@@ -1303,15 +1303,15 @@
(the default), Isar proofs are only generated when no working one-liner
\textit{metis} proof is available.
-\opdefault{isar\_compress}{int}{\upshape 10}
+\opdefault{compress\_isar}{int}{\upshape 10}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
is explicitly 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.
\optrueonly{dont\_compress\_isar}
-Alias for ``\textit{isar\_compress} = 0''.
+Alias for ``\textit{compress\_isar} = 0''.
-\optrue{isar\_try0}{dont\_try0\_isar}
+\optrue{try0\_isar}{dont\_try0\_isar}
Specifies whether standard proof methods such as \textit{auto} and
\textit{blast} should be tried as alternatives to \textit{metis} and
\textit{smt} in Isar proofs. The collection of methods is roughly the same as
--- a/src/HOL/Metis_Examples/Big_O.thy Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Jan 30 14:37:53 2014 +0100
@@ -29,7 +29,7 @@
(*** Now various verions with an increasing shrink factor ***)
-sledgehammer_params [isar_proofs, isar_compress = 1]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 2]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 3]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 4]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 1]
+sledgehammer_params [isar_proofs, compress_isar = 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 Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy Thu Jan 30 14:37:53 2014 +0100
@@ -21,7 +21,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-sledgehammer_params [isar_proofs, isar_compress = 1]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 2]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 3]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 4]
+sledgehammer_params [isar_proofs, compress_isar = 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_compress = 1]
+sledgehammer_params [isar_proofs, compress_isar = 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 Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 30 14:37:53 2014 +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_compress = 2] *)
+(* sledgehammer [isar_proofs, compress_isar = 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_compress.ML Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Thu Jan 30 14:37:53 2014 +0100
@@ -93,16 +93,16 @@
(* Precondition: The proof must be labeled canonically
(cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
-fun compress_proof isar_compress
+fun compress_proof compress_isar
({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
- if isar_compress <= 1.0 then
+ if compress_isar <= 1.0 then
proof
else
let
val (compress_further, decrement_step_count) =
let
val number_of_steps = add_proof_steps (steps_of_proof proof) 0
- val target_number_of_steps = Real.round (Real.fromInt number_of_steps / isar_compress)
+ val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
in
(fn () => !delta > 0, fn () => delta := !delta - 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jan 30 14:37:53 2014 +0100
@@ -94,8 +94,8 @@
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
- ("isar_compress", "10"),
- ("isar_try0", "true"),
+ ("compress_isar", "10"),
+ ("try0_isar", "true"),
("slice", "true"),
("minimize", "smart"),
("preplay_timeout", "3")]
@@ -103,7 +103,7 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
("dont_preplay", ("preplay_timeout", ["0"])),
- ("dont_compress_isar", ("isar_compress", ["0"])),
+ ("dont_compress_isar", ("compress_isar", ["0"])),
("isar_proof", ("isar_proofs", [])) (* legacy *)]
val negated_alias_params =
[("no_debug", "debug"),
@@ -117,7 +117,7 @@
("no_isar_proofs", "isar_proofs"),
("dont_slice", "slice"),
("dont_minimize", "minimize"),
- ("dont_try0_isar", "isar_try0")]
+ ("dont_try0_isar", "try0_isar")]
val params_not_for_minimize =
["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -286,8 +286,8 @@
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
- val isar_compress = Real.max (1.0, lookup_real "isar_compress")
- val isar_try0 = lookup_bool "isar_try0"
+ val compress_isar = Real.max (1.0, lookup_real "compress_isar")
+ val try0_isar = lookup_bool "try0_isar"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
val timeout = lookup_time "timeout"
@@ -299,7 +299,7 @@
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_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize,
+ compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Jan 30 14:37:53 2014 +0100
@@ -55,7 +55,7 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
- type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, isar_try0,
+ type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state goal facts =
let
@@ -70,7 +70,7 @@
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_proofs = isar_proofs, isar_compress = isar_compress, isar_try0 = isar_try0,
+ isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
expect = ""}
val problem =
@@ -226,7 +226,7 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, spy, 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_compress, isar_try0, slice, minimize, timeout,
+ max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
preplay_timeout, expect} : params) =
let
fun lookup_override name default_value =
@@ -243,7 +243,7 @@
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_proofs = isar_proofs,
- isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize,
+ compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 30 14:37:53 2014 +0100
@@ -36,8 +36,8 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- isar_compress : real,
- isar_try0 : bool,
+ compress_isar : real,
+ try0_isar : bool,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -277,8 +277,8 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- isar_compress : real,
- isar_try0 : bool,
+ compress_isar : real,
+ try0_isar : bool,
slice : bool,
minimize : bool option,
timeout : Time.time,
@@ -546,8 +546,8 @@
({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
best_max_new_mono_instances, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
- fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress,
- isar_try0, slice, timeout, preplay_timeout, ...})
+ fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
+ try0_isar, slice, timeout, preplay_timeout, ...})
minimize_command
({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -797,8 +797,8 @@
|> introduce_spass_skolem
|> factify_atp_proof fact_names hyp_ts concl_t
in
- (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
- isar_try0, atp_proof, goal)
+ (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
+ try0_isar, atp_proof, goal)
end
val one_line_params =
(preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 14:28:04 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 14:37:53 2014 +0100
@@ -209,8 +209,8 @@
let
fun isar_proof_of () =
let
- val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
- isar_try0, atp_proof, goal) = try isar_params ()
+ val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
+ try0_isar, atp_proof, goal) = try isar_params ()
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
val (_, ctxt) =
@@ -219,7 +219,7 @@
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
val do_preplay = preplay_timeout <> Time.zeroTime
- val isar_try0 = isar_try0 andalso do_preplay
+ val try0_isar = try0_isar andalso do_preplay
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
@@ -364,10 +364,10 @@
val (play_outcome, isar_proof) =
isar_proof
- |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
+ |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
preplay_interface
- |> isar_try0 ? try0 preplay_timeout preplay_interface
- |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
+ |> try0_isar ? try0 preplay_timeout preplay_interface
+ |> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface)
|> `overall_preplay_outcome
||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)