# HG changeset patch
# User blanchet
# Date 1305904573 -7200
# Node ID fd4babefe3f2619a8ede220e25f17c9ba89f0e39
# Parent  a61e30bfd0bc83d6fec3c2bcd2dfbfd7ea80ac21
prevent unsound combinator proofs in partially typed polymorphic type systems

diff -r a61e30bfd0bc -r fd4babefe3f2 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 16:23:03 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 * thm list)) list
+  val metis_helpers : (string * (bool * bool * thm list)) list
   val prepare_metis_problem :
     mode -> Proof.context -> bool -> thm list -> thm list list
     -> mode * metis_problem
@@ -258,7 +258,7 @@
   | sorts_on_typs_aux ((x,i),  s::ss) =
       let val sorts = sorts_on_typs_aux ((x,i), ss)
       in
-          if s = "HOL.type" then sorts
+          if s = the_single @{sort HOL.type} then sorts
           else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
           else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
       end;
@@ -641,37 +641,42 @@
       end
   end;
 
-(* "true" indicates that a sound type encoding is needed *)
+(* 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".) *)
 val metis_helpers =
-  [("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})),
+  [("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})),
    ("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, @{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}])),
+    (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}])),
    ("fNot",
-    (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
-                   fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
+    (false, true, @{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+})),
+    (false, true,
+     @{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+})),
+    (false, true,
+     @{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}))]
+    (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}))]
 
 (* ------------------------------------------------------------------------- *)
 (* Logic maps manage the interface between HOL and first-order logic.        *)
@@ -778,7 +783,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 a61e30bfd0bc -r fd4babefe3f2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 16:23:03 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 17:16:13 2011 +0200
@@ -740,9 +740,9 @@
     let
       val thy = Proof_Context.theory_of ctxt
       val unmangled_s = mangled_s |> unmangled_const_name
-      fun dub_and_inst c needs_some_types (th, j) =
+      fun dub_and_inst c needs_fairly_sound (th, j) =
         ((c ^ "_" ^ string_of_int j ^
-          (if needs_some_types then typed_helper_suffix
+          (if needs_fairly_sound then typed_helper_suffix
            else untyped_helper_suffix),
           General),
          let val t = th |> prop_of in
@@ -756,17 +756,20 @@
          end)
       fun make_facts eq_as_iff =
         map_filter (make_fact ctxt false eq_as_iff false)
-      val has_some_types = is_type_sys_fairly_sound type_sys
+      val fairly_sound = is_type_sys_fairly_sound type_sys
     in
       metis_helpers
-      |> maps (fn (metis_s, (needs_some_types, ths)) =>
+      |> maps (fn (metis_s, (needs_fairly_sound, mono, ths)) =>
                   if metis_s <> unmangled_s orelse
-                     (needs_some_types andalso not has_some_types) then
+                     (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
                     []
                   else
                     ths ~~ (1 upto length ths)
-                    |> map (dub_and_inst mangled_s needs_some_types)
-                    |> make_facts (not needs_some_types))
+                    |> map (dub_and_inst mangled_s needs_fairly_sound)
+                    |> make_facts (not needs_fairly_sound))
     end
   | NONE => []
 fun helper_facts_for_sym_table ctxt type_sys sym_tab =