--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Mon Mar 22 10:25:07 2010 +0100
@@ -174,14 +174,14 @@
val vampire_max_new_clauses = 60;
val vampire_insert_theory_const = false;
-fun vampire_prover_config full : prover_config =
+fun vampire_prover_config isar : prover_config =
{command = Path.explode "$VAMPIRE_HOME/vampire",
arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
" -t " ^ string_of_int timeout),
failure_strs = vampire_failure_strs,
max_new_clauses = vampire_max_new_clauses,
insert_theory_const = vampire_insert_theory_const,
- emit_structured_proof = full};
+ emit_structured_proof = isar};
val vampire = tptp_prover ("vampire", vampire_prover_config false);
val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
@@ -196,14 +196,14 @@
val eprover_max_new_clauses = 100;
val eprover_insert_theory_const = false;
-fun eprover_config full : prover_config =
+fun eprover_config isar : prover_config =
{command = Path.explode "$E_HOME/eproof",
arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
" --silent --cpu-limit=" ^ string_of_int timeout),
failure_strs = eprover_failure_strs,
max_new_clauses = eprover_max_new_clauses,
insert_theory_const = eprover_insert_theory_const,
- emit_structured_proof = full};
+ emit_structured_proof = isar};
val eprover = tptp_prover ("e", eprover_config false);
val eprover_isar = tptp_prover ("e_isar", eprover_config true);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Mar 22 10:25:07 2010 +0100
@@ -463,7 +463,8 @@
fun neg_skolemize_tac ctxt =
EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
-val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
+val neg_clausify =
+ Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf;
fun neg_conjecture_clauses ctxt st0 n =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Mar 22 10:25:07 2010 +0100
@@ -333,26 +333,30 @@
then SOME ctm else perm ctms
in perm end;
-fun have_or_show "show " _ = "show \""
- | have_or_show have lname = have ^ lname ^ ": \""
-
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
ATP may have their literals reordered.*)
-fun isar_lines ctxt ctms =
- let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term)
- val _ = trace_proof_msg (K "\n\nisar_lines: start\n")
- fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
- (case permuted_clause t ctms of
- SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
- | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*)
- | doline have (lname, t, deps) =
- have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^
- "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
- fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
- | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
- in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
+fun isar_proof_body ctxt ctms =
+ let
+ val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
+ val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
+ fun have_or_show "show" _ = "show \""
+ | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+ fun do_line _ (lname, t, []) =
+ (* No deps: it's a conjecture clause, with no proof. *)
+ (case permuted_clause t ctms of
+ SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
+ [t]))
+ | do_line have (lname, t, deps) =
+ have_or_show have lname ^
+ string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
+ "\"\n by (metis " ^ space_implode " " deps ^ ")\n"
+ fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
+ | do_lines ((lname, t, deps) :: lines) =
+ do_line "have" (lname, t, deps) :: do_lines lines
+ in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) do_lines end;
-fun notequal t (_,t',_) = not (t aconv t');
+fun unequal t (_, t', _) = not (t aconv t');
(*No "real" literals means only type information*)
fun eq_types t = t aconv HOLogic.true_const;
@@ -368,7 +372,7 @@
if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
then map (replace_deps (lno, [])) lines
else
- (case take_prefix (notequal t) lines of
+ (case take_prefix (unequal t) lines of
(_,[]) => lines (*no repetition of proof line*)
| (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
pre @ map (replace_deps (lno', [lno])) post)
@@ -378,7 +382,7 @@
if eq_types t then (lno, t, deps) :: lines
(*Type information will be deleted later; skip repetition test.*)
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
- case take_prefix (notequal t) lines of
+ case take_prefix (unequal t) lines of
(_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*)
| (pre, (lno', t', _) :: post) =>
(lno, t', deps) :: (*repetition: replace later line by earlier one*)
@@ -450,10 +454,10 @@
val ccls = map forall_intr_vars ccls
val _ = app (fn th => trace_proof_msg
(fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
- val isar_lines = isar_lines ctxt (map prop_of ccls)
- (stringify_deps thm_names [] lines)
+ val body = isar_proof_body ctxt (map prop_of ccls)
+ (stringify_deps thm_names [] lines)
val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
- in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end
+ in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
handle STREE _ => error "Could not extract proof (ATP output malformed?)";
--- a/src/HOL/Tools/meson.ML Fri Mar 19 16:04:15 2010 +0100
+++ b/src/HOL/Tools/meson.ML Mon Mar 22 10:25:07 2010 +0100
@@ -18,6 +18,7 @@
val make_nnf: Proof.context -> thm -> thm
val skolemize: Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
+ val make_clauses_unsorted: thm list -> thm list
val make_clauses: thm list -> thm list
val make_horns: thm list -> thm list
val best_prolog_tac: (thm -> int) -> thm list -> tactic
@@ -560,7 +561,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
+fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =