--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100
@@ -82,7 +82,7 @@
structure Metis_Translate : METIS_TRANSLATE =
struct
-val type_tag_name = "ty"
+val type_tag_name = "ti"
val bound_var_prefix = "B_"
val schematic_var_prefix = "V_"
@@ -102,23 +102,30 @@
fun union_all xss = fold (union (op =)) xss []
(* Readable names for the more common symbolic functions. Do not mess with the
- last nine entries of the table unless you know what you are doing. *)
+ table unless you know what you are doing. *)
val const_trans_table =
Symtab.make [(@{type_name Product_Type.prod}, "prod"),
(@{type_name Sum_Type.sum}, "sum"),
+ (@{const_name False}, "False"),
+ (@{const_name True}, "True"),
+ (@{const_name Not}, "Not"),
+ (@{const_name conj}, "conj"),
+ (@{const_name disj}, "disj"),
+ (@{const_name implies}, "implies"),
(@{const_name HOL.eq}, "equal"),
- (@{const_name HOL.conj}, "and"),
- (@{const_name HOL.disj}, "or"),
- (@{const_name HOL.implies}, "implies"),
(@{const_name Set.member}, "member"),
+ (@{const_name Metis.fFalse}, "fFalse"),
+ (@{const_name Metis.fTrue}, "fTrue"),
+ (@{const_name Metis.fNot}, "fNot"),
+ (@{const_name Metis.fconj}, "fconj"),
+ (@{const_name Metis.fdisj}, "fdisj"),
+ (@{const_name Metis.fimplies}, "fimplies"),
(@{const_name Metis.fequal}, "fequal"),
(@{const_name Meson.COMBI}, "COMBI"),
(@{const_name Meson.COMBK}, "COMBK"),
(@{const_name Meson.COMBB}, "COMBB"),
(@{const_name Meson.COMBC}, "COMBC"),
(@{const_name Meson.COMBS}, "COMBS"),
- (@{const_name True}, "True"),
- (@{const_name False}, "False"),
(@{const_name If}, "If")]
(* Invert the table of translations between Isabelle and ATPs. *)
@@ -550,6 +557,12 @@
| string_of_mode FT = "FT"
fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+ | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
+ | fn_isa_to_met_sublevel "c_True" = "c_fTrue"
+ | fn_isa_to_met_sublevel "c_Not" = "c_fNot"
+ | fn_isa_to_met_sublevel "c_conj" = "c_fconj"
+ | fn_isa_to_met_sublevel "c_disj" = "c_fdisj"
+ | fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
| fn_isa_to_met_sublevel x = x
fun fn_isa_to_met_toplevel "equal" = "="
| fn_isa_to_met_toplevel x = x
@@ -648,16 +661,41 @@
end;
val helpers =
- [("c_COMBI", (false, map (`I) @{thms Meson.COMBI_def})),
- ("c_COMBK", (false, map (`I) @{thms Meson.COMBK_def})),
- ("c_COMBB", (false, map (`I) @{thms Meson.COMBB_def})),
- ("c_COMBC", (false, map (`I) @{thms Meson.COMBC_def})),
- ("c_COMBS", (false, map (`I) @{thms Meson.COMBS_def})),
- ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
- @{thms fequal_imp_equal equal_imp_fequal})),
- ("c_True", (true, map (`I) @{thms True_or_False})),
- ("c_False", (true, map (`I) @{thms True_or_False})),
- ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
+ [("c_COMBI", (false, @{thms Meson.COMBI_def})),
+ ("c_COMBK", (false, @{thms Meson.COMBK_def})),
+ ("c_COMBB", (false, @{thms Meson.COMBB_def})),
+ ("c_COMBC", (false, @{thms Meson.COMBC_def})),
+ ("c_COMBS", (false, @{thms Meson.COMBS_def})),
+ ("c_fequal",
+ (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse"
+ by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])),
+ ("c_fFalse", (false, [@{lemma "~ fFalse"
+ by (unfold Metis.fFalse_def) fast}])),
+ ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse"
+ by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])),
+ ("c_fTrue", (false, [@{lemma "fTrue"
+ by (unfold Metis.fTrue_def) fast}])),
+ ("c_fNot",
+ (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ ("c_fconj",
+ (false, @{lemma "~ P | ~ Q | Metis.fconj P Q"
+ "~ Metis.fconj P Q | P"
+ "~ Metis.fconj P Q | Q"
+ by (unfold Metis.fconj_def) fast+})),
+ ("c_fdisj",
+ (false, @{lemma "~ P | Metis.fdisj P Q"
+ "~ Q | Metis.fdisj P Q"
+ "~ Metis.fdisj P Q | P | Q"
+ by (unfold Metis.fdisj_def) fast+})),
+ ("c_fimplies",
+ (false, @{lemma "P | Metis.fimplies P Q"
+ "~ Q | Metis.fimplies P Q"
+ "~ Metis.fimplies P Q | ~ P | Q"
+ by (unfold Metis.fimplies_def) fast+})),
+ ("c_If", (true, @{thms if_True if_False True_or_False})) (* FIXME *)]
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
@@ -733,20 +771,20 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture (metis_ith, isa_ith)
+ fun add_thm is_conjecture (isa_ith, metis_ith)
{axioms, tfrees, old_skolems} : metis_problem =
let
val (mth, tfree_lits, old_skolems) =
hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
old_skolems metis_ith
in
- {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
+ {axioms = (mth, isa_ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
end;
val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
- |> fold (add_thm true o `I) cls
+ |> fold (add_thm true o `Meson.make_meta_clause) cls
|> add_tfrees
- |> fold (fold (add_thm false o `I)) thss
+ |> fold (fold (add_thm false o `Meson.make_meta_clause)) thss
val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -755,14 +793,18 @@
lmap
else
let
+ val fdefs = @{thms Metis.fFalse_def Metis.fTrue_def Metis.fNot_def
+ Metis.fconj_def Metis.fdisj_def
+ Metis.fimplies_def Metis.fequal_def}
+ val prepare_helper =
+ zero_var_indexes
+ #> `(Meson.make_meta_clause
+ #> rewrite_rule (map safe_mk_meta_eq fdefs))
val helper_ths =
helpers |> filter (is_used o fst)
|> maps (fn (c, (needs_full_types, thms)) =>
- if not (is_used c) orelse
- needs_full_types andalso mode <> FT then
- []
- else
- thms)
+ if needs_full_types andalso mode <> FT then []
+ else map prepare_helper thms)
in lmap |> fold (add_thm false) helper_ths end
in
(mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)