# HG changeset patch
# User blanchet
# Date 1305904573 -7200
# Node ID ce269ee43800e0e5878c254110f9428147b1b1d8
# Parent  fd4babefe3f2619a8ede220e25f17c9ba89f0e39
further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged

diff -r fd4babefe3f2 -r ce269ee43800 src/HOL/Tools/Metis/metis_translate.ML
--- 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
diff -r fd4babefe3f2 -r ce269ee43800 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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