--- a/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 17:16:13 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Fri May 20 17:16:13 2011 +0200
@@ -75,7 +75,7 @@
val tvar_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
val string_of_mode : mode -> string
- val metis_helpers : (string * (bool * bool * thm list)) list
+ val metis_helpers : (string * (bool * thm list)) list
val prepare_metis_problem :
mode -> Proof.context -> bool -> thm list -> thm list list
-> mode * metis_problem
@@ -641,42 +641,39 @@
end
end;
-(* The first Boolean indicates that a fairly sound type encoding is needed.
- The second Boolean indicates whether the helper should be kept in
- polymorphic encodings that erase most of the types. (The K combinator is
- then omitted to prevent finding a contradiction with "Suc n ~= n".) *)
+(* The Boolean indicates that a fairly sound type encoding is needed. *)
val metis_helpers =
- [("COMBI", (false, true, @{thms Meson.COMBI_def})),
- ("COMBK", (false, false, @{thms Meson.COMBK_def})),
- ("COMBB", (false, true, @{thms Meson.COMBB_def})),
- ("COMBC", (false, true, @{thms Meson.COMBC_def})),
- ("COMBS", (false, true, @{thms Meson.COMBS_def})),
+ [("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",
(* 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, true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
- ("fFalse", (true, true, @{thms True_or_False})),
- ("fFalse", (false, true, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
- ("fTrue", (true, true, @{thms True_or_False})),
- ("fTrue", (false, true, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
+ (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ ("fFalse", (true, @{thms True_or_False})),
+ ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
+ ("fTrue", (true, @{thms True_or_False})),
+ ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
("fNot",
- (false, true, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
- fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+ (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
+ fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
("fconj",
- (false, true,
+ (false,
@{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
by (unfold fconj_def) fast+})),
("fdisj",
- (false, true,
+ (false,
@{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
by (unfold fdisj_def) fast+})),
("fimplies",
- (false, true, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
- "~ fimplies P Q | ~ P | Q"
- by (unfold fimplies_def) fast+})),
- ("If", (true, true, @{thms if_True if_False True_or_False}))]
+ (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}))]
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
@@ -783,7 +780,7 @@
val helper_ths =
metis_helpers
|> filter (is_used o prefix const_prefix o fst)
- |> maps (fn (_, (needs_full_types, _, thms)) =>
+ |> maps (fn (_, (needs_full_types, thms)) =>
if needs_full_types andalso mode <> FT then []
else map prepare_helper thms)
in lmap |> fold (add_thm false) helper_ths end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 17:16:13 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri May 20 17:16:13 2011 +0200
@@ -759,12 +759,9 @@
val fairly_sound = is_type_sys_fairly_sound type_sys
in
metis_helpers
- |> maps (fn (metis_s, (needs_fairly_sound, mono, ths)) =>
+ |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
if metis_s <> unmangled_s orelse
- (needs_fairly_sound andalso not fairly_sound) orelse
- (not mono andalso
- polymorphism_of_type_sys type_sys = Polymorphic andalso
- level_of_type_sys type_sys <> All_Types) then
+ (needs_fairly_sound andalso not fairly_sound) then
[]
else
ths ~~ (1 upto length ths)
@@ -966,10 +963,10 @@
fun should_declare_sym type_sys pred_sym s =
not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
not (String.isPrefix tptp_special_prefix s) andalso
- ((case type_sys of
- Simple_Types _ => true
- | Tags (_, _, Light) => true
- | _ => false) orelse not pred_sym)
+ (case type_sys of
+ Simple_Types _ => true
+ | Tags (_, _, Light) => true
+ | _ => not pred_sym)
fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
let
@@ -1212,12 +1209,19 @@
val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
val helpers =
repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
+ val lavish_nonmono_Ts =
+ if null nonmono_Ts orelse
+ polymorphism_of_type_sys type_sys <> Polymorphic then
+ nonmono_Ts
+ else
+ [TVar (("'a", 0), HOLogic.typeS)]
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
- |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
+ |> problem_lines_for_sym_decl_table ctxt conj_sym_kind lavish_nonmono_Ts
+ type_sys
val helper_lines =
- map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys)
+ map (formula_line_for_fact ctxt helper_prefix lavish_nonmono_Ts type_sys)
(0 upto length helpers - 1 ~~ helpers)
|> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ())
(* Reordering these might confuse the proof reconstruction code or the SPASS