equal
deleted
inserted
replaced
7 Proof reconstruction for Metis. |
7 Proof reconstruction for Metis. |
8 *) |
8 *) |
9 |
9 |
10 signature METIS_RECONSTRUCT = |
10 signature METIS_RECONSTRUCT = |
11 sig |
11 sig |
12 type type_enc = ATP_Translate.type_enc |
12 type type_enc = ATP_Problem_Generate.type_enc |
13 |
13 |
14 exception METIS of string * string |
14 exception METIS of string * string |
15 |
15 |
16 val hol_clause_from_metis : |
16 val hol_clause_from_metis : |
17 Proof.context -> type_enc -> int Symtab.table |
17 Proof.context -> type_enc -> int Symtab.table |
28 |
28 |
29 structure Metis_Reconstruct : METIS_RECONSTRUCT = |
29 structure Metis_Reconstruct : METIS_RECONSTRUCT = |
30 struct |
30 struct |
31 |
31 |
32 open ATP_Problem |
32 open ATP_Problem |
33 open ATP_Translate |
33 open ATP_Problem_Generate |
34 open ATP_Reconstruct |
34 open ATP_Proof_Reconstruct |
35 open Metis_Translate |
35 open Metis_Generate |
36 |
36 |
37 exception METIS of string * string |
37 exception METIS of string * string |
38 |
38 |
39 fun atp_name_from_metis type_enc s = |
39 fun atp_name_from_metis type_enc s = |
40 case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of |
40 case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of |
99 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
99 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
100 |
100 |
101 (* INFERENCE RULE: AXIOM *) |
101 (* INFERENCE RULE: AXIOM *) |
102 |
102 |
103 (* This causes variables to have an index of 1 by default. See also |
103 (* This causes variables to have an index of 1 by default. See also |
104 "term_from_atp" in "ATP_Reconstruct". *) |
104 "term_from_atp" in "ATP_Proof_Reconstruct". *) |
105 val axiom_inference = Thm.incr_indexes 1 oo lookth |
105 val axiom_inference = Thm.incr_indexes 1 oo lookth |
106 |
106 |
107 (* INFERENCE RULE: ASSUME *) |
107 (* INFERENCE RULE: ASSUME *) |
108 |
108 |
109 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} |
109 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} |