--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 16:29:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:34 2011 +0200
@@ -77,6 +77,7 @@
val tfree_clause_prefix : string
val typed_helper_suffix : string
val untyped_helper_suffix : string
+ val type_tag_idempotence_helper_name : string
val predicator_name : string
val app_op_name : string
val type_tag_name : string
@@ -87,7 +88,8 @@
val ascii_of: string -> string
val unascii_of: string -> string
val strip_prefix_and_unascii : string -> string -> string option
- val proxify_const : string -> (int * (string * string)) option
+ val proxy_table : (string * (string * (thm * (string * string)))) list
+ val proxify_const : string -> (string * string) option
val invert_const: string -> string
val unproxify_const: string -> string
val make_bound_var : string -> string
@@ -125,6 +127,7 @@
Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
-> translated_formula option * ((string * locality) * thm)
val helper_table : (string * (bool * thm list)) list
+ val should_specialize_helper : type_sys -> term -> bool
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
@@ -183,12 +186,13 @@
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
-val class_rel_clause_prefix = "crel_"
+val class_rel_clause_prefix = "clar_"
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
+val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
val predicator_name = "hBOOL"
val app_op_name = "hAPP"
@@ -257,19 +261,23 @@
else
NONE
-val proxies =
- [("c_False",
- (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),
- ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),
- ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),
- ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),
- ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),
- ("c_implies",
- (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),
- ("equal",
- (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]
+val proxy_table =
+ [("c_False", (@{const_name False}, (@{thm fFalse_def},
+ ("fFalse", @{const_name ATP.fFalse})))),
+ ("c_True", (@{const_name True}, (@{thm fTrue_def},
+ ("fTrue", @{const_name ATP.fTrue})))),
+ ("c_Not", (@{const_name Not}, (@{thm fNot_def},
+ ("fNot", @{const_name ATP.fNot})))),
+ ("c_conj", (@{const_name conj}, (@{thm fconj_def},
+ ("fconj", @{const_name ATP.fconj})))),
+ ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
+ ("fdisj", @{const_name ATP.fdisj})))),
+ ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
+ ("fimplies", @{const_name ATP.fimplies})))),
+ ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
+ ("fequal", @{const_name ATP.fequal}))))]
-val proxify_const = AList.lookup (op =) proxies #> Option.map snd
+val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
(* Readable names for the more common symbolic functions. Do not mess with the
table unless you know what you are doing. *)
@@ -291,14 +299,14 @@
(@{const_name Meson.COMBC}, "COMBC"),
(@{const_name Meson.COMBS}, "COMBS")]
|> Symtab.make
- |> fold (Symtab.update o swap o snd o snd o snd) proxies
+ |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
const_trans_table |> Symtab.dest |> map swap |> Symtab.make
val const_trans_table_unprox =
Symtab.empty
- |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies
+ |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
@@ -793,7 +801,7 @@
CombApp (intro top_level tm1, intro false tm2)
| intro top_level (CombConst (name as (s, _), T, T_args)) =
(case proxify_const s of
- SOME (_, proxy_base) =>
+ SOME proxy_base =>
if top_level orelse is_setting_higher_order format type_sys then
case (top_level, s) of
(_, "c_False") => (`I tptp_false, [])
@@ -1284,52 +1292,57 @@
"~ fimplies P Q | ~ P | Q"
by (unfold fimplies_def) fast+})),
("If", (true, @{thms if_True if_False True_or_False}))]
+ |> map (apsnd (apsnd (map zero_var_indexes)))
val type_tag = `make_fixed_const type_tag_name
-fun ti_ti_helper_fact () =
+fun type_tag_idempotence_fact () =
let
fun var s = ATerm (`I s, [])
- fun tag tm = ATerm (type_tag, [var "X", tm])
+ fun tag tm = ATerm (type_tag, [var "T", tm])
+ val tagged_x = tag (var "X")
in
- Formula (helper_prefix ^ "ti_ti", Axiom,
- AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
+ Formula (type_tag_idempotence_helper_name, Axiom,
+ AAtom (ATerm (`I tptp_equal, [tag tagged_x, tagged_x]))
|> close_formula_universally, simp_info, NONE)
end
+fun should_specialize_helper type_sys t =
+ case general_type_arg_policy type_sys of
+ Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
+ | _ => false
+
fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
case strip_prefix_and_unascii const_prefix s of
SOME mangled_s =>
let
val thy = Proof_Context.theory_of ctxt
val unmangled_s = mangled_s |> unmangled_const_name
- fun dub_and_inst c needs_fairly_sound (th, j) =
- ((c ^ "_" ^ string_of_int j ^
+ fun dub_and_inst needs_fairly_sound (th, j) =
+ ((unmangled_s ^ "_" ^ string_of_int j ^
+ (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
(if needs_fairly_sound then typed_helper_suffix
else untyped_helper_suffix),
General),
let val t = th |> prop_of in
- t |> ((case general_type_arg_policy type_sys of
- Mangled_Type_Args _ => true
- | _ => false) andalso
- not (null (Term.hidden_polymorphism t)))
+ t |> should_specialize_helper type_sys t
? (case types of
[T] => specialize_type thy (invert_const unmangled_s, T)
| _ => I)
end)
- fun make_facts eq_as_iff =
- map_filter (make_fact ctxt format type_sys true false eq_as_iff false)
+ val make_facts =
+ map_filter (make_fact ctxt format type_sys false false false false)
val fairly_sound = is_type_sys_fairly_sound type_sys
in
helper_table
- |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
- if metis_s <> unmangled_s orelse
+ |> maps (fn (helper_s, (needs_fairly_sound, ths)) =>
+ if helper_s <> unmangled_s orelse
(needs_fairly_sound andalso not fairly_sound) then
[]
else
ths ~~ (1 upto length ths)
- |> map (dub_and_inst mangled_s needs_fairly_sound)
- |> make_facts (not needs_fairly_sound))
+ |> map (dub_and_inst needs_fairly_sound)
+ |> make_facts)
end
| NONE => []
fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
@@ -1509,11 +1522,14 @@
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
-fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
+fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
(j, formula as {name, locality, kind, ...}) =
- Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
- else string_of_int j ^ "_") ^
- ascii_of name,
+ Formula (prefix ^
+ (if freshen andalso
+ polymorphism_of_type_sys type_sys <> Polymorphic then
+ string_of_int j ^ "_"
+ else
+ "") ^ encode name,
kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
case locality of
Intro => intro_info
@@ -1774,9 +1790,9 @@
|-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
nonmono_Ts type_sys)
-fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavyweight)) =
+fun needs_type_tag_idempotence (Tags (Polymorphic, level, Heavyweight)) =
level = Nonmonotonic_Types orelse level = Finite_Types
- | should_add_ti_ti_helper _ = false
+ | needs_type_tag_idempotence _ = false
fun offset_of_heading_in_problem _ [] j = j
| offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
@@ -1822,16 +1838,19 @@
lavish_nonmono_Ts type_sys
val helper_lines =
0 upto length helpers - 1 ~~ helpers
- |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
- type_sys)
- |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
- else I)
+ |> map (formula_line_for_fact ctxt format helper_prefix I false
+ lavish_nonmono_Ts type_sys)
+ |> (if needs_type_tag_idempotence type_sys then
+ cons (type_tag_idempotence_fact ())
+ else
+ I)
(* Reordering these might confuse the proof reconstruction code or the SPASS
FLOTTER hack. *)
val problem =
[(explicit_declsN, sym_decl_lines),
(factsN,
- map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
+ map (formula_line_for_fact ctxt format fact_prefix ascii_of true
+ nonmono_Ts type_sys)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
(aritiesN, map formula_line_for_arity_clause arity_clauses),
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 16:29:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:34 2011 +0200
@@ -46,8 +46,6 @@
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
-fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
-
(* Designed to work also with monomorphic instances of polymorphic theorems. *)
fun have_common_thm ths1 ths2 =
exists (member (untyped_aconv o pairself prop_of) ths1)
@@ -60,11 +58,10 @@
(* 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 =
+ "t => t". Type tag idempotence is also handled this way. *)
+fun reflexive_or_trivial_from_metis ctxt sym_tab mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis_MX ctxt sym_tab
- (Metis_LiteralSet.toList (Metis_Thm.clause mth)) of
+ case hol_clause_from_metis ctxt sym_tab mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
| Const (@{const_name disj}, _) $ t1 $ t2 =>
@@ -74,6 +71,9 @@
end
|> Meson.make_meta_clause
+(* FIXME: implement using "hol_clause_from_metis ctxt sym_tab mth" *)
+fun specialize_helper mth ith = ith
+
val clause_params =
{ordering = Metis_KnuthBendixOrder.default,
orderLiterals = Metis_Clause.UnsignedLiteralOrder,
@@ -107,19 +107,21 @@
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))
+ fun get_isa_thm mth Isa_Reflexive_or_Trivial =
+ reflexive_or_trivial_from_metis ctxt sym_tab mth
+ | get_isa_thm mth (Isa_Helper ith) =
+ ith |> should_specialize_helper (the type_sys) (prop_of ith)
+ ? specialize_helper mth
+ | get_isa_thm _ (Isa_Raw ith) = ith
+ val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
- val thms = map #1 axioms
+ val thms = axioms |> map fst
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
in
- case filter (is_false o prop_of) cls of
- false_th::_ => [false_th RS @{thm FalseE}]
+ case filter (fn t => prop_of t aconv @{prop False}) cls of
+ false_th :: _ => [false_th RS @{thm FalseE}]
| [] =>
case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
|> Metis_Resolution.loop of
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 16:29:38 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:34 2011 +0200
@@ -14,8 +14,13 @@
datatype mode = FO | HO | FT | MX
+ datatype isa_thm =
+ Isa_Reflexive_or_Trivial |
+ Isa_Helper of thm |
+ Isa_Raw of thm
+
type metis_problem =
- {axioms : (Metis_Thm.thm * thm option) list,
+ {axioms : (Metis_Thm.thm * isa_thm) list,
tfrees : type_literal list,
old_skolems : (string * term) list}
@@ -235,8 +240,13 @@
(* Logic maps manage the interface between HOL and first-order logic. *)
(* ------------------------------------------------------------------------- *)
+datatype isa_thm =
+ Isa_Reflexive_or_Trivial |
+ Isa_Helper of thm |
+ Isa_Raw of thm
+
type metis_problem =
- {axioms : (Metis_Thm.thm * thm option) list,
+ {axioms : (Metis_Thm.thm * isa_thm) list,
tfrees : type_literal list,
old_skolems : (string * term) list}
@@ -285,6 +295,10 @@
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
+val proxy_defs = map (fst o snd o snd) proxy_table
+val prepare_helper =
+ Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
+
fun metis_name_from_atp s ary =
AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false)
fun metis_term_from_atp (ATerm (s, tms)) =
@@ -308,18 +322,23 @@
fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
(phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
|> Metis_Thm.axiom,
- case try (unprefix conjecture_prefix) ident of
+ if ident = type_tag_idempotence_helper_name orelse
+ String.isPrefix lightweight_tags_sym_formula_prefix ident then
+ Isa_Reflexive_or_Trivial
+ else if String.isPrefix helper_prefix ident then
+ case space_explode "_" ident of
+ _ :: const :: j :: _ =>
+ Isa_Helper (nth (AList.lookup (op =) helper_table const |> the |> snd)
+ (the (Int.fromString j) - 1)
+ |> prepare_helper)
+ | _ => raise Fail ("malformed helper identifier " ^ quote ident)
+ else case try (unprefix conjecture_prefix) ident of
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:
- else if String.isPrefix helper_prefix then
- ...
-*)
- else
- SOME TrueI)
+ let val j = the (Int.fromString s) in
+ Isa_Raw (if j = length clauses then TrueI
+ else Meson.make_meta_clause (nth clauses j))
+ end
+ | NONE => Isa_Raw TrueI)
| metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
@@ -342,8 +361,7 @@
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
false false (map prop_of clauses) @{prop False} []
val axioms =
- atp_problem
- |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
+ atp_problem |> maps (map (metis_axiom_from_atp clauses) o snd)
in
(MX, sym_tab,
{axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
@@ -366,14 +384,14 @@
hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
metis_ith
in
- {axioms = (mth, SOME isa_ith) :: axioms,
+ {axioms = (mth, Isa_Raw 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, SOME ith) :: axioms, tfrees = tfrees,
+ {axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees,
old_skolems = old_skolems}
fun add_tfrees {axioms, tfrees, old_skolems} =
- {axioms = map (rpair (SOME TrueI) o metis_of_tfree)
+ {axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree)
(distinct (op =) tfrees) @ axioms,
tfrees = tfrees, old_skolems = old_skolems}
val problem =
@@ -389,18 +407,12 @@
problem
else
let
- val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def
- fimplies_def fequal_def}
- val prepare_helper =
- zero_var_indexes
- #> `(Meson.make_meta_clause
- #> rewrite_rule (map safe_mk_meta_eq fdefs))
val helper_ths =
helper_table
|> filter (is_used o prefix const_prefix o fst)
|> maps (fn (_, (needs_full_types, thms)) =>
if needs_full_types andalso mode <> FT then []
- else map prepare_helper thms)
+ else map (`prepare_helper) thms)
in problem |> fold (add_thm false) helper_ths end
val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
in (mode, Symtab.empty, fold add_type_thm type_ths problem) end