equal
deleted
inserted
replaced
7 Translation of HOL to FOL for Metis. |
7 Translation of HOL to FOL for Metis. |
8 *) |
8 *) |
9 |
9 |
10 signature METIS_TRANSLATE = |
10 signature METIS_TRANSLATE = |
11 sig |
11 sig |
|
12 type type_enc = ATP_Translate.type_enc |
|
13 |
12 datatype isa_thm = |
14 datatype isa_thm = |
13 Isa_Reflexive_or_Trivial | |
15 Isa_Reflexive_or_Trivial | |
14 Isa_Raw of thm |
16 Isa_Raw of thm |
15 |
17 |
16 val metis_equal : string |
18 val metis_equal : string |
23 val trace_msg : Proof.context -> (unit -> string) -> unit |
25 val trace_msg : Proof.context -> (unit -> string) -> unit |
24 val verbose_warning : Proof.context -> string -> unit |
26 val verbose_warning : Proof.context -> string -> unit |
25 val metis_name_table : ((string * int) * (string * bool)) list |
27 val metis_name_table : ((string * int) * (string * bool)) list |
26 val reveal_old_skolem_terms : (string * term) list -> term -> term |
28 val reveal_old_skolem_terms : (string * term) list -> term -> term |
27 val prepare_metis_problem : |
29 val prepare_metis_problem : |
28 Proof.context -> string -> thm list -> thm list |
30 Proof.context -> type_enc -> thm list -> thm list |
29 -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list |
31 -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list |
30 end |
32 end |
31 |
33 |
32 structure Metis_Translate : METIS_TRANSLATE = |
34 structure Metis_Translate : METIS_TRANSLATE = |
33 struct |
35 struct |
165 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
167 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
166 |
168 |
167 (* Function to generate metis clauses, including comb and type clauses *) |
169 (* Function to generate metis clauses, including comb and type clauses *) |
168 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses = |
170 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses = |
169 let |
171 let |
170 val type_enc = type_enc_from_string Unsound type_enc |
|
171 val (conj_clauses, fact_clauses) = |
172 val (conj_clauses, fact_clauses) = |
172 if polymorphism_of_type_enc type_enc = Polymorphic then |
173 if polymorphism_of_type_enc type_enc = Polymorphic then |
173 (conj_clauses, fact_clauses) |
174 (conj_clauses, fact_clauses) |
174 else |
175 else |
175 conj_clauses @ fact_clauses |
176 conj_clauses @ fact_clauses |