10 signature METIS_TRANSLATE = |
10 signature METIS_TRANSLATE = |
11 sig |
11 sig |
12 type type_literal = ATP_Translate.type_literal |
12 type type_literal = ATP_Translate.type_literal |
13 type type_sys = ATP_Translate.type_sys |
13 type type_sys = ATP_Translate.type_sys |
14 |
14 |
15 datatype mode = FO | HO | FT | New |
15 datatype mode = FO | HO | FT | MX |
16 |
16 |
17 type metis_problem = |
17 type metis_problem = |
18 {axioms : (Metis_Thm.thm * thm) list, |
18 {axioms : (Metis_Thm.thm * thm) list, |
19 tfrees : type_literal list, |
19 tfrees : type_literal list, |
20 old_skolems : (string * term) list} |
20 old_skolems : (string * term) list} |
109 |
109 |
110 (* ------------------------------------------------------------------------- *) |
110 (* ------------------------------------------------------------------------- *) |
111 (* HOL to FOL (Isabelle to Metis) *) |
111 (* HOL to FOL (Isabelle to Metis) *) |
112 (* ------------------------------------------------------------------------- *) |
112 (* ------------------------------------------------------------------------- *) |
113 |
113 |
114 (* first-order, higher-order, fully-typed, new *) |
114 (* first-order, higher-order, fully-typed, mode X (fleXible) *) |
115 datatype mode = FO | HO | FT | New |
115 datatype mode = FO | HO | FT | MX |
116 |
116 |
117 fun string_of_mode FO = "FO" |
117 fun string_of_mode FO = "FO" |
118 | string_of_mode HO = "HO" |
118 | string_of_mode HO = "HO" |
119 | string_of_mode FT = "FT" |
119 | string_of_mode FT = "FT" |
120 | string_of_mode New = "New" |
120 | string_of_mode MX = "MX" |
121 |
121 |
122 fun fn_isa_to_met_sublevel "equal" = "c_fequal" |
122 fun fn_isa_to_met_sublevel "equal" = "c_fequal" |
123 | fn_isa_to_met_sublevel "c_False" = "c_fFalse" |
123 | fn_isa_to_met_sublevel "c_False" = "c_fFalse" |
124 | fn_isa_to_met_sublevel "c_True" = "c_fTrue" |
124 | fn_isa_to_met_sublevel "c_True" = "c_fTrue" |
125 | fn_isa_to_met_sublevel "c_Not" = "c_fNot" |
125 | fn_isa_to_met_sublevel "c_Not" = "c_fNot" |
308 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
308 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
309 |
309 |
310 val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light) |
310 val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light) |
311 |
311 |
312 (* Function to generate metis clauses, including comb and type clauses *) |
312 (* Function to generate metis clauses, including comb and type clauses *) |
313 fun prepare_metis_problem ctxt New type_sys conj_clauses fact_clauses = |
313 fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = |
314 let |
314 let |
315 val type_sys = type_sys |> the_default default_type_sys |
315 val type_sys = type_sys |> the_default default_type_sys |
316 val explicit_apply = NONE |
316 val explicit_apply = NONE |
317 val clauses = conj_clauses @ fact_clauses |
317 val clauses = conj_clauses @ fact_clauses |
318 val (atp_problem, _, _, _, _, _, sym_tab) = |
318 val (atp_problem, _, _, _, _, _, sym_tab) = |
320 false false (map prop_of clauses) @{prop False} [] |
320 false false (map prop_of clauses) @{prop False} [] |
321 val axioms = |
321 val axioms = |
322 atp_problem |
322 atp_problem |
323 |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) |
323 |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd) |
324 in |
324 in |
325 (New, sym_tab, |
325 (MX, sym_tab, |
326 {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) |
326 {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) |
327 end |
327 end |
328 | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = |
328 | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses = |
329 let |
329 let |
330 val thy = Proof_Context.theory_of ctxt |
330 val thy = Proof_Context.theory_of ctxt |