# HG changeset patch # User blanchet # Date 1307385394 -7200 # Node ID 29b55f292e0bc12df8cf82b3a2ef2aba4fdcfa36 # Parent 686fa0a0696e9975d562ed8d4266f24e81bd4135 added support for helpers in new Metis, so far only for polymorphic type encodings diff -r 686fa0a0696e -r 29b55f292e0b src/HOL/Tools/ATP/atp_translate.ML --- 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), diff -r 686fa0a0696e -r 29b55f292e0b src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 16:29:38 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:34 2011 +0200 @@ -17,8 +17,8 @@ val trace_msg : Proof.context -> (unit -> string) -> unit val verbose : bool Config.T val verbose_warning : Proof.context -> string -> unit - val hol_clause_from_metis_MX : - Proof.context -> int Symtab.table -> Metis_Literal.literal list -> term + val hol_clause_from_metis : + Proof.context -> int Symtab.table -> Metis_Thm.thm -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term * term -> bool val replay_one_inference : @@ -236,8 +236,11 @@ | atp_clause_from_metis lits = lits |> map atp_literal_from_metis |> mk_aconns AOr -fun hol_clause_from_metis_MX ctxt sym_tab = - atp_clause_from_metis #> prop_from_atp ctxt false sym_tab +fun hol_clause_from_metis ctxt sym_tab = + Metis_Thm.clause + #> Metis_LiteralSet.toList + #> atp_clause_from_metis + #> prop_from_atp ctxt false sym_tab fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms = let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms diff -r 686fa0a0696e -r 29b55f292e0b src/HOL/Tools/Metis/metis_tactics.ML --- 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 diff -r 686fa0a0696e -r 29b55f292e0b src/HOL/Tools/Metis/metis_translate.ML --- 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