--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200
@@ -66,7 +66,7 @@
val type_decl_prefix : string
val sym_decl_prefix : string
val preds_sym_formula_prefix : string
- val tags_sym_formula_prefix : string
+ val lightweight_tags_sym_formula_prefix : string
val fact_prefix : string
val conjecture_prefix : string
val helper_prefix : string
@@ -172,7 +172,7 @@
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val preds_sym_formula_prefix = "psy_"
-val tags_sym_formula_prefix = "tsy_"
+val lightweight_tags_sym_formula_prefix = "tsy_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
@@ -1665,11 +1665,11 @@
intro_info, NONE)
end
-fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind nonmono_Ts
- type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
+ nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
let
val ident_base =
- tags_sym_formula_prefix ^ s ^
+ lightweight_tags_sym_formula_prefix ^ s ^
(if n > 1 then "_" ^ string_of_int j else "")
val (kind, maybe_negate) =
if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
@@ -1749,8 +1749,8 @@
| Lightweight =>
let val n = length decls in
(0 upto n - 1 ~~ decls)
- |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind
- nonmono_Ts type_sys n s)
+ |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
+ conj_sym_kind nonmono_Ts type_sys n s)
end)
fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
--- a/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200
@@ -55,6 +55,28 @@
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
| used_axioms _ _ = NONE
+fun cterm_from_metis ctxt sym_tab tm =
+ let val thy = Proof_Context.theory_of ctxt in
+ tm |> hol_term_from_metis MX sym_tab ctxt
+ |> Syntax.check_term
+ (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
+ |> cterm_of thy
+ end
+
+(* Lightweight predicate type information comes in two flavors, "t = t'" and
+ "t => t'", where "t" and "t'" are the same term modulo type tags.
+ In Isabelle, type tags are stripped away, so we are left with "t = t" or
+ "t => t". *)
+fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth =
+ (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of
+ [(true, (_, [_, tm]))] =>
+ tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive
+ RS @{thm meta_eq_to_obj_eq}
+ | [_, (_, tm)] =>
+ tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume
+ | _ => raise Fail "unexpected tags sym clause")
+ |> Meson.make_meta_clause
+
val clause_params =
{ordering = Metis_KnuthBendixOrder.default,
orderLiterals = Metis_Clause.UnsignedLiteralOrder,
@@ -88,6 +110,11 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
val (mode, sym_tab, {axioms, old_skolems, ...}) =
prepare_metis_problem ctxt mode type_sys cls ths
+ val axioms =
+ axioms |> map
+ (fn (mth, SOME th) => (mth, th)
+ | (mth, NONE) =>
+ (mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth))
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200
@@ -15,7 +15,7 @@
datatype mode = FO | HO | FT | MX
type metis_problem =
- {axioms : (Metis_Thm.thm * thm) list,
+ {axioms : (Metis_Thm.thm * thm option) list,
tfrees : type_literal list,
old_skolems : (string * term) list}
@@ -236,7 +236,7 @@
(* ------------------------------------------------------------------------- *)
type metis_problem =
- {axioms : (Metis_Thm.thm * thm) list,
+ {axioms : (Metis_Thm.thm * thm option) list,
tfrees : type_literal list,
old_skolems : (string * term) list}
@@ -309,14 +309,17 @@
(phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
|> Metis_Thm.axiom,
case try (unprefix conjecture_prefix) ident of
- SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s)))
+ SOME s =>
+ SOME (Meson.make_meta_clause (nth clauses (the (Int.fromString s))))
| NONE =>
+ if String.isPrefix lightweight_tags_sym_formula_prefix ident then
+ NONE
(* FIXME: missing:
- if String.isPrefix helper_prefix then
+ else if String.isPrefix helper_prefix then
...
+*)
else
-*)
- TrueI)
+ SOME TrueI)
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
@@ -363,15 +366,15 @@
hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
metis_ith
in
- {axioms = (mth, isa_ith) :: axioms,
+ {axioms = (mth, SOME isa_ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
end;
fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
- {axioms = (mth, ith) :: axioms, tfrees = tfrees,
+ {axioms = (mth, SOME ith) :: axioms, tfrees = tfrees,
old_skolems = old_skolems}
fun add_tfrees {axioms, tfrees, old_skolems} =
- {axioms =
- map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ axioms,
+ {axioms = map (rpair (SOME TrueI) o metis_of_tfree)
+ (distinct (op =) tfrees) @ axioms,
tfrees = tfrees, old_skolems = old_skolems}
val problem =
{axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}