--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 22:29:50 2010 +0200
@@ -24,7 +24,7 @@
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
- shrink_factor: int,
+ isar_shrink_factor: int,
timeout: Time.time,
minimize_timeout: Time.time}
type problem =
@@ -83,7 +83,7 @@
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
- shrink_factor: int,
+ isar_shrink_factor: int,
timeout: Time.time,
minimize_timeout: Time.time}
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:29:50 2010 +0200
@@ -112,8 +112,8 @@
fun generic_prover overlord get_facts prepare write_file home_var executable
args proof_delims known_failures name
- ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...}
- : params) minimize_command
+ ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor,
+ ...} : params) minimize_command
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
let
@@ -218,7 +218,8 @@
case outcome of
NONE =>
proof_text isar_proof
- (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
+ (pool, debug, full_types, isar_shrink_factor, ctxt,
+ conjecture_shape)
(minimize_command, proof, internal_thm_names, th, subgoal)
| SOME failure => (string_for_failure failure ^ "\n", [])
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:29:50 2010 +0200
@@ -69,7 +69,7 @@
(* minimalization of thms *)
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
- isar_proof, shrink_factor, ...})
+ isar_proof, isar_shrink_factor, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
@@ -110,7 +110,8 @@
in
(SOME min_thms,
proof_text isar_proof
- (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
+ (pool, debug, full_types, isar_shrink_factor, ctxt,
+ conjecture_shape)
(K "", proof, internal_thm_names, goal, i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 22:29:50 2010 +0200
@@ -98,7 +98,7 @@
("theory_relevant", "smart"),
("defs_relevant", "false"),
("isar_proof", "false"),
- ("shrink_factor", "1"),
+ ("isar_shrink_factor", "1"),
("minimize_timeout", "5 s")]
val alias_params =
@@ -116,7 +116,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "full_types", "explicit_apply",
- "isar_proof", "shrink_factor", "minimize_timeout"]
+ "isar_proof", "isar_shrink_factor", "minimize_timeout"]
val property_dependent_params = ["atps", "full_types", "timeout"]
@@ -199,7 +199,7 @@
val theory_relevant = lookup_bool_option "theory_relevant"
val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
- val shrink_factor = Int.max (1, lookup_int "shrink_factor")
+ val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = lookup_time "timeout"
val minimize_timeout = lookup_time "minimize_timeout"
in
@@ -208,8 +208,8 @@
respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
- minimize_timeout = minimize_timeout}
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ timeout = timeout, minimize_timeout = minimize_timeout}
end
fun get_params thy = extract_params thy (default_raw_params thy)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 22:29:50 2010 +0200
@@ -569,7 +569,7 @@
fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
(j, line :: lines)
- | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees
+ | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
(Inference (num, t, deps)) (j, lines) =
(j + 1,
if is_axiom_clause_number thm_names num orelse
@@ -579,7 +579,7 @@
not (exists_subterm (is_bad_free frees) t) andalso
not (is_trivial_formula t) andalso
(null lines orelse (* last line must be kept *)
- (length deps >= 2 andalso j mod shrink_factor = 0))) then
+ (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
Inference (num, t, deps) :: lines (* keep line *)
else
map (replace_deps_in_line (num, deps)) lines) (* drop line *)
@@ -674,7 +674,7 @@
forall_vars t,
ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
-fun proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
+fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof
conjecture_shape thm_names params frees =
let
val lines =
@@ -683,7 +683,7 @@
|> decode_lines ctxt full_types
|> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
|> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
+ |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
conjecture_shape thm_names frees)
|> snd
in
@@ -981,7 +981,7 @@
do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
in do_proof end
-fun isar_proof_text (pool, debug, full_types, shrink_factor, ctxt,
+fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
conjecture_shape)
(minimize_command, atp_proof, thm_names, goal, i) =
let
@@ -992,8 +992,9 @@
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
fun isar_proof_for () =
- case proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof
- conjecture_shape thm_names params frees
+ case proof_from_atp_proof pool ctxt full_types isar_shrink_factor
+ atp_proof conjecture_shape thm_names params
+ frees
|> redirect_proof thy conjecture_shape hyp_ts concl_t
|> kill_duplicate_assumptions_in_proof
|> then_chain_proof