--- a/NEWS Thu Oct 18 14:26:45 2012 +0200
+++ b/NEWS Thu Oct 18 15:05:17 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/HOL/Metis_Examples/Big_O.thy Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy Thu Oct 18 15:05:17 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 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Sets.thy Thu Oct 18 15:05:17 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 14:26:45 2012 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Oct 18 15:05:17 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/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 18 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 18 15:05:17 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 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 18 15:05:17 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 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 15:05:17 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 14:26:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 18 15:05:17 2012 +0200
@@ -23,7 +23,7 @@
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
@@ -52,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
@@ -448,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
@@ -460,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 *)
@@ -751,7 +752,7 @@
val merge_timeout_slack = 1.2
-fun minimize_locally ctxt type_enc lam_trans proof =
+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
@@ -824,24 +825,26 @@
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
@@ -862,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 =
@@ -908,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