1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 15:33:18 2010 +0100
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 19 16:04:15 2010 +0100
1.3 @@ -184,7 +184,7 @@
1.4 emit_structured_proof = full};
1.5
1.6 val vampire = tptp_prover ("vampire", vampire_prover_config false);
1.7 -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
1.8 +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
1.9
1.10
1.11 (* E prover *)
1.12 @@ -206,7 +206,7 @@
1.13 emit_structured_proof = full};
1.14
1.15 val eprover = tptp_prover ("e", eprover_config false);
1.16 -val eprover_full = tptp_prover ("e_full", eprover_config true);
1.17 +val eprover_isar = tptp_prover ("e_isar", eprover_config true);
1.18
1.19
1.20 (* SPASS *)
1.21 @@ -290,7 +290,7 @@
1.22 "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
1.23
1.24 val provers =
1.25 - [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
1.26 + [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
1.27 remote_vampire, remote_spass, remote_eprover]
1.28 val prover_setup = fold add_prover provers
1.29
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 15:33:18 2010 +0100
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Mar 19 16:04:15 2010 +0100
2.3 @@ -428,26 +428,33 @@
2.4 fun isar_header [] = proofstart
2.5 | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
2.6
2.7 -fun decode_tstp_file cnfs ctxt th sgno thm_names =
2.8 - let val _ = trace_proof_msg (K "\ndecode_tstp_file: start\n")
2.9 - val tuples = map (dest_tstp o tstp_line o explode) cnfs
2.10 - val _ = trace_proof_msg (fn () => Int.toString (length tuples) ^ " tuples extracted\n")
2.11 - val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
2.12 - val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
2.13 - val _ = trace_proof_msg (fn () => Int.toString (length raw_lines) ^ " raw_lines extracted\n")
2.14 - val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
2.15 - val _ = trace_proof_msg (fn () => Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
2.16 - val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
2.17 - val _ = trace_proof_msg (fn () => Int.toString (length lines) ^ " lines extracted\n")
2.18 - val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
2.19 - val _ = trace_proof_msg (fn () => Int.toString (length ccls) ^ " conjecture clauses\n")
2.20 - val ccls = map forall_intr_vars ccls
2.21 - val _ = app (fn th => trace_proof_msg (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
2.22 - val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
2.23 - val _ = trace_proof_msg (K "\ndecode_tstp_file: finishing\n")
2.24 - in
2.25 - isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
2.26 - end handle STREE _ => error "Could not extract proof (ATP output malformed?)";
2.27 +fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
2.28 + let
2.29 + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
2.30 + val tuples = map (dest_tstp o tstp_line o explode) cnfs
2.31 + val _ = trace_proof_msg (fn () =>
2.32 + Int.toString (length tuples) ^ " tuples extracted\n")
2.33 + val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
2.34 + val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
2.35 + val _ = trace_proof_msg (fn () =>
2.36 + Int.toString (length raw_lines) ^ " raw_lines extracted\n")
2.37 + val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
2.38 + val _ = trace_proof_msg (fn () =>
2.39 + Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
2.40 + val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
2.41 + val _ = trace_proof_msg (fn () =>
2.42 + Int.toString (length lines) ^ " lines extracted\n")
2.43 + val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
2.44 + val _ = trace_proof_msg (fn () =>
2.45 + Int.toString (length ccls) ^ " conjecture clauses\n")
2.46 + val ccls = map forall_intr_vars ccls
2.47 + val _ = app (fn th => trace_proof_msg
2.48 + (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
2.49 + val isar_lines = isar_lines ctxt (map prop_of ccls)
2.50 + (stringify_deps thm_names [] lines)
2.51 + val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
2.52 + in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end
2.53 + handle STREE _ => error "Could not extract proof (ATP output malformed?)";
2.54
2.55
2.56 (*=== EXTRACTING PROOF-TEXT === *)
2.57 @@ -530,19 +537,17 @@
2.58 (* atp_minimize [atp=<prover>] <lemmas> *)
2.59 fun minimize_line _ [] = ""
2.60 | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
2.61 - (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
2.62 - space_implode " " (kill_chained lemmas))
2.63 -
2.64 -val sendback_metis_no_chained =
2.65 - Markup.markup Markup.sendback o metis_line o kill_chained
2.66 + Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
2.67 + space_implode " " (kill_chained lemmas))
2.68
2.69 fun metis_lemma_list dfg name result =
2.70 - let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
2.71 - in (sendback_metis_no_chained lemmas ^ "\n" ^ minimize_line name lemmas ^
2.72 - (if used_conj then
2.73 - ""
2.74 - else
2.75 - "\nWarning: The goal is provable because the context is inconsistent."),
2.76 + let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
2.77 + (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
2.78 + minimize_line name lemmas ^
2.79 + (if used_conj then
2.80 + ""
2.81 + else
2.82 + "\nWarning: The goal is provable because the context is inconsistent."),
2.83 kill_chained lemmas)
2.84 end;
2.85
2.86 @@ -551,15 +556,17 @@
2.87 let
2.88 (* Could use "split_lines", but it can return blank lines *)
2.89 val lines = String.tokens (equal #"\n");
2.90 - val kill_spaces = String.translate (fn c => if Char.isSpace c then "" else str c)
2.91 + val kill_spaces =
2.92 + String.translate (fn c => if Char.isSpace c then "" else str c)
2.93 val extract = get_proof_extract proof
2.94 val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
2.95 val (one_line_proof, lemma_names) = metis_lemma_list false name result
2.96 - val structured =
2.97 - if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
2.98 - else decode_tstp_file cnfs ctxt goal subgoalno thm_names
2.99 + val tokens = String.tokens (fn c => c = #" ") one_line_proof
2.100 + val isar_proof =
2.101 + if member (op =) tokens chained_hint then ""
2.102 + else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
2.103 in
2.104 - (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback structured,
2.105 + (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
2.106 lemma_names)
2.107 end
2.108