# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID ef3ff88562451f606f3256c360b2399cbd5c4854 # Parent e11bd628f1a5a5870173545fd7c84f044461f08c fixed type helper indices in new Metis diff -r e11bd628f1a5 -r ef3ff8856245 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200 @@ -127,7 +127,7 @@ val translate_atp_fact : Proof.context -> format -> type_sys -> bool -> (string * locality) * thm -> translated_formula option * ((string * locality) * thm) - val helper_table : (string * (bool * thm list)) list + 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 @@ -1253,42 +1253,38 @@ (** Helper facts **) -(* The Boolean indicates that a fairly sound type encoding is needed. - "false" must precede "true" to ensure consistent numbering and a correct - mapping in Metis. *) +(* The Boolean indicates that a fairly sound type encoding is needed. *) val helper_table = - [("COMBI", (false, @{thms Meson.COMBI_def})), - ("COMBK", (false, @{thms Meson.COMBK_def})), - ("COMBB", (false, @{thms Meson.COMBB_def})), - ("COMBC", (false, @{thms Meson.COMBC_def})), - ("COMBS", (false, @{thms Meson.COMBS_def})), - ("fequal", + [(("COMBI", false), @{thms Meson.COMBI_def}), + (("COMBK", false), @{thms Meson.COMBK_def}), + (("COMBB", false), @{thms Meson.COMBB_def}), + (("COMBC", false), @{thms Meson.COMBC_def}), + (("COMBS", false), @{thms Meson.COMBS_def}), + (("fequal", true), (* This is a lie: Higher-order equality doesn't need a sound type encoding. However, this is done so for backward compatibility: Including the equality helpers by default in Metis breaks a few existing proofs. *) - (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] - fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), - ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), - ("fFalse", (true, @{thms True_or_False})), - ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), - ("fTrue", (true, @{thms True_or_False})), - ("fNot", - (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] - fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), - ("fconj", - (false, - @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" - by (unfold fconj_def) fast+})), - ("fdisj", - (false, - @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" - by (unfold fdisj_def) fast+})), - ("fimplies", - (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" - "~ 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))) + @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), + (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]), + (("fFalse", true), @{thms True_or_False}), + (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]), + (("fTrue", true), @{thms True_or_False}), + (("fNot", false), + @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}), + (("fconj", false), + @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q" + by (unfold fconj_def) fast+}), + (("fdisj", false), + @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q" + by (unfold fdisj_def) fast+}), + (("fimplies", false), + @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" + "~ fimplies P Q | ~ P | Q" + by (unfold fimplies_def) fast+}), + (("If", true), @{thms if_True if_False True_or_False})] + |> map (apsnd (map zero_var_indexes)) val type_tag = `make_fixed_const type_tag_name @@ -1331,7 +1327,7 @@ val fairly_sound = is_type_sys_fairly_sound type_sys in helper_table - |> maps (fn (helper_s, (needs_fairly_sound, ths)) => + |> maps (fn ((helper_s, needs_fairly_sound), ths) => if helper_s <> unmangled_s orelse (needs_fairly_sound andalso not fairly_sound) then [] diff -r e11bd628f1a5 -r ef3ff8856245 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:35 2011 +0200 @@ -195,7 +195,7 @@ fun generic_metis_tac modes type_sys ctxt ths i st0 = let val _ = trace_msg ctxt (fn () => - "Metis called with theorems " ^ + "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1 in diff -r e11bd628f1a5 -r ef3ff8856245 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 @@ -327,12 +327,14 @@ String.isPrefix lightweight_tags_sym_formula_prefix ident then Isa_Reflexive_or_Trivial |> some else if String.isPrefix helper_prefix ident then - case space_explode "_" ident of - _ :: const :: j :: _ => - nth (helper_table |> filter (curry (op =) const o fst) - |> maps (snd o snd)) + case (String.isSuffix typed_helper_suffix ident, + space_explode "_" ident) of + (needs_fairly_sound, _ :: const :: j :: _) => + nth ((const, needs_fairly_sound) + |> AList.lookup (op =) helper_table |> the) (the (Int.fromString j) - 1) - |> prepare_helper |> Isa_Raw |> some + |> prepare_helper + |> Isa_Raw |> some | _ => raise Fail ("malformed helper identifier " ^ quote ident) else case try (unprefix conjecture_prefix) ident of SOME s => @@ -424,8 +426,8 @@ let val helper_ths = helper_table - |> filter (is_used o prefix const_prefix o fst) - |> maps (fn (_, (needs_full_types, thms)) => + |> filter (is_used o prefix const_prefix o fst o fst) + |> maps (fn ((_, needs_full_types), thms) => if needs_full_types andalso mode <> FT then [] else map (`prepare_helper) thms) in problem |> fold (add_thm false) helper_ths end