125 val unmangled_const_name : string -> string |
125 val unmangled_const_name : string -> string |
126 val unmangled_const : string -> string * string fo_term list |
126 val unmangled_const : string -> string * string fo_term list |
127 val translate_atp_fact : |
127 val translate_atp_fact : |
128 Proof.context -> format -> type_sys -> bool -> (string * locality) * thm |
128 Proof.context -> format -> type_sys -> bool -> (string * locality) * thm |
129 -> translated_formula option * ((string * locality) * thm) |
129 -> translated_formula option * ((string * locality) * thm) |
130 val helper_table : (string * (bool * thm list)) list |
130 val helper_table : ((string * bool) * thm list) list |
131 val should_specialize_helper : type_sys -> term -> bool |
131 val should_specialize_helper : type_sys -> term -> bool |
132 val tfree_classes_of_terms : term list -> string list |
132 val tfree_classes_of_terms : term list -> string list |
133 val tvar_classes_of_terms : term list -> string list |
133 val tvar_classes_of_terms : term list -> string list |
134 val type_constrs_of_terms : theory -> term list -> string list |
134 val type_constrs_of_terms : theory -> term list -> string list |
135 val prepare_atp_problem : |
135 val prepare_atp_problem : |
1251 update_combformula (formula_map |
1251 update_combformula (formula_map |
1252 (repair_combterm ctxt format type_sys sym_tab)) |
1252 (repair_combterm ctxt format type_sys sym_tab)) |
1253 |
1253 |
1254 (** Helper facts **) |
1254 (** Helper facts **) |
1255 |
1255 |
1256 (* The Boolean indicates that a fairly sound type encoding is needed. |
1256 (* The Boolean indicates that a fairly sound type encoding is needed. *) |
1257 "false" must precede "true" to ensure consistent numbering and a correct |
|
1258 mapping in Metis. *) |
|
1259 val helper_table = |
1257 val helper_table = |
1260 [("COMBI", (false, @{thms Meson.COMBI_def})), |
1258 [(("COMBI", false), @{thms Meson.COMBI_def}), |
1261 ("COMBK", (false, @{thms Meson.COMBK_def})), |
1259 (("COMBK", false), @{thms Meson.COMBK_def}), |
1262 ("COMBB", (false, @{thms Meson.COMBB_def})), |
1260 (("COMBB", false), @{thms Meson.COMBB_def}), |
1263 ("COMBC", (false, @{thms Meson.COMBC_def})), |
1261 (("COMBC", false), @{thms Meson.COMBC_def}), |
1264 ("COMBS", (false, @{thms Meson.COMBS_def})), |
1262 (("COMBS", false), @{thms Meson.COMBS_def}), |
1265 ("fequal", |
1263 (("fequal", true), |
1266 (* This is a lie: Higher-order equality doesn't need a sound type encoding. |
1264 (* This is a lie: Higher-order equality doesn't need a sound type encoding. |
1267 However, this is done so for backward compatibility: Including the |
1265 However, this is done so for backward compatibility: Including the |
1268 equality helpers by default in Metis breaks a few existing proofs. *) |
1266 equality helpers by default in Metis breaks a few existing proofs. *) |
1269 (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
1267 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
1270 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
1268 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), |
1271 ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), |
1269 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]), |
1272 ("fFalse", (true, @{thms True_or_False})), |
1270 (("fFalse", true), @{thms True_or_False}), |
1273 ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), |
1271 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]), |
1274 ("fTrue", (true, @{thms True_or_False})), |
1272 (("fTrue", true), @{thms True_or_False}), |
1275 ("fNot", |
1273 (("fNot", false), |
1276 (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
1274 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] |
1277 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), |
1275 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), |
1278 ("fconj", |
1276 (("fconj", false), |
1279 (false, |
1277 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" |
1280 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" |
1278 by (unfold fconj_def) fast+}), |
1281 by (unfold fconj_def) fast+})), |
1279 (("fdisj", false), |
1282 ("fdisj", |
1280 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" |
1283 (false, |
1281 by (unfold fdisj_def) fast+}), |
1284 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" |
1282 (("fimplies", false), |
1285 by (unfold fdisj_def) fast+})), |
1283 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" |
1286 ("fimplies", |
1284 "~ fimplies P Q | ~ P | Q" |
1287 (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" |
1285 by (unfold fimplies_def) fast+}), |
1288 "~ fimplies P Q | ~ P | Q" |
1286 (("If", true), @{thms if_True if_False True_or_False})] |
1289 by (unfold fimplies_def) fast+})), |
1287 |> map (apsnd (map zero_var_indexes)) |
1290 ("If", (true, @{thms if_True if_False True_or_False}))] |
|
1291 |> map (apsnd (apsnd (map zero_var_indexes))) |
|
1292 |
1288 |
1293 val type_tag = `make_fixed_const type_tag_name |
1289 val type_tag = `make_fixed_const type_tag_name |
1294 |
1290 |
1295 fun type_tag_idempotence_fact () = |
1291 fun type_tag_idempotence_fact () = |
1296 let |
1292 let |