6 Transfer of proofs from external provers. |
6 Transfer of proofs from external provers. |
7 *) |
7 *) |
8 |
8 |
9 signature SLEDGEHAMMER_PROOF_RECONSTRUCT = |
9 signature SLEDGEHAMMER_PROOF_RECONSTRUCT = |
10 sig |
10 sig |
|
11 type locality = Sledgehammer_Fact_Filter.locality |
11 type minimize_command = string list -> string |
12 type minimize_command = string list -> string |
12 |
13 |
13 val metis_proof_text: |
14 val metis_proof_text: |
14 bool * minimize_command * string * (string * bool) vector * thm * int |
15 bool * minimize_command * string * (string * locality) vector * thm * int |
15 -> string * (string * bool) list |
16 -> string * (string * locality) list |
16 val isar_proof_text: |
17 val isar_proof_text: |
17 string Symtab.table * bool * int * Proof.context * int list list |
18 string Symtab.table * bool * int * Proof.context * int list list |
18 -> bool * minimize_command * string * (string * bool) vector * thm * int |
19 -> bool * minimize_command * string * (string * locality) vector * thm * int |
19 -> string * (string * bool) list |
20 -> string * (string * locality) list |
20 val proof_text: |
21 val proof_text: |
21 bool -> string Symtab.table * bool * int * Proof.context * int list list |
22 bool -> string Symtab.table * bool * int * Proof.context * int list list |
22 -> bool * minimize_command * string * (string * bool) vector * thm * int |
23 -> bool * minimize_command * string * (string * locality) vector * thm * int |
23 -> string * (string * bool) list |
24 -> string * (string * locality) list |
24 end; |
25 end; |
25 |
26 |
26 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = |
27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = |
27 struct |
28 struct |
28 |
29 |
576 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = |
577 fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = |
577 if tag = "cnf" orelse tag = "fof" then |
578 if tag = "cnf" orelse tag = "fof" then |
578 (case strip_prefix_and_unascii axiom_prefix (List.last rest) of |
579 (case strip_prefix_and_unascii axiom_prefix (List.last rest) of |
579 SOME name => |
580 SOME name => |
580 if member (op =) rest "file" then |
581 if member (op =) rest "file" then |
581 SOME (name, is_true_for axiom_names name) |
582 SOME (name, find_first_in_vector axiom_names name General) |
582 else |
583 else |
583 axiom_name_at_index num |
584 axiom_name_at_index num |
584 | NONE => axiom_name_at_index num) |
585 | NONE => axiom_name_at_index num) |
585 else |
586 else |
586 NONE |
587 NONE |
622 "\nTo minimize the number of lemmas, try this: " ^ |
623 "\nTo minimize the number of lemmas, try this: " ^ |
623 Markup.markup Markup.sendback command ^ "." |
624 Markup.markup Markup.sendback command ^ "." |
624 |
625 |
625 fun used_facts axiom_names = |
626 fun used_facts axiom_names = |
626 used_facts_in_atp_proof axiom_names |
627 used_facts_in_atp_proof axiom_names |
627 #> List.partition snd |
628 #> List.partition (curry (op =) Chained o snd) |
628 #> pairself (sort_distinct (string_ord) o map fst) |
629 #> pairself (sort_distinct (string_ord o pairself fst)) |
629 |
630 |
630 fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, |
631 fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, |
631 goal, i) = |
632 goal, i) = |
632 let |
633 let |
633 val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof |
634 val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof |
634 val n = Logic.count_prems (prop_of goal) |
635 val n = Logic.count_prems (prop_of goal) |
635 in |
636 in |
636 (metis_line full_types i n other_lemmas ^ |
637 (metis_line full_types i n (map fst other_lemmas) ^ |
637 minimize_line minimize_command (other_lemmas @ chained_lemmas), |
638 minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), |
638 map (rpair false) other_lemmas @ map (rpair true) chained_lemmas) |
639 other_lemmas @ chained_lemmas) |
639 end |
640 end |
640 |
641 |
641 (** Isar proof construction and manipulation **) |
642 (** Isar proof construction and manipulation **) |
642 |
643 |
643 fun merge_fact_sets (ls1, ss1) (ls2, ss2) = |
644 fun merge_fact_sets (ls1, ss1) (ls2, ss2) = |