1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 16:23:03 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri May 20 17:16:13 2011 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4    val tvar_classes_of_terms : term list -> string list
     1.5    val type_consts_of_terms : theory -> term list -> string list
     1.6    val string_of_mode : mode -> string
     1.7 -  val metis_helpers : (string * (bool * thm list)) list
     1.8 +  val metis_helpers : (string * (bool * bool * thm list)) list
     1.9    val prepare_metis_problem :
    1.10      mode -> Proof.context -> bool -> thm list -> thm list list
    1.11      -> mode * metis_problem
    1.12 @@ -258,7 +258,7 @@
    1.13    | sorts_on_typs_aux ((x,i),  s::ss) =
    1.14        let val sorts = sorts_on_typs_aux ((x,i), ss)
    1.15        in
    1.16 -          if s = "HOL.type" then sorts
    1.17 +          if s = the_single @{sort HOL.type} then sorts
    1.18            else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
    1.19            else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
    1.20        end;
    1.21 @@ -641,37 +641,42 @@
    1.22        end
    1.23    end;
    1.24  
    1.25 -(* "true" indicates that a sound type encoding is needed *)
    1.26 +(* The first Boolean indicates that a fairly sound type encoding is needed.
    1.27 +   The second Boolean indicates whether the helper should be kept in
    1.28 +   polymorphic encodings that erase most of the types. (The K combinator is
    1.29 +   then omitted to prevent finding a contradiction with "Suc n ~= n".) *)
    1.30  val metis_helpers =
    1.31 -  [("COMBI", (false, @{thms Meson.COMBI_def})),
    1.32 -   ("COMBK", (false, @{thms Meson.COMBK_def})),
    1.33 -   ("COMBB", (false, @{thms Meson.COMBB_def})),
    1.34 -   ("COMBC", (false, @{thms Meson.COMBC_def})),
    1.35 -   ("COMBS", (false, @{thms Meson.COMBS_def})),
    1.36 +  [("COMBI", (false, true, @{thms Meson.COMBI_def})),
    1.37 +   ("COMBK", (false, false, @{thms Meson.COMBK_def})),
    1.38 +   ("COMBB", (false, true, @{thms Meson.COMBB_def})),
    1.39 +   ("COMBC", (false, true, @{thms Meson.COMBC_def})),
    1.40 +   ("COMBS", (false, true, @{thms Meson.COMBS_def})),
    1.41     ("fequal",
    1.42      (* This is a lie: Higher-order equality doesn't need a sound type encoding.
    1.43         However, this is done so for backward compatibility: Including the
    1.44         equality helpers by default in Metis breaks a few existing proofs. *)
    1.45 -    (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.46 -                  fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.47 -   ("fFalse", (true, @{thms True_or_False})),
    1.48 -   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    1.49 -   ("fTrue", (true, @{thms True_or_False})),
    1.50 -   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    1.51 +    (true, true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.52 +                        fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.53 +   ("fFalse", (true, true, @{thms True_or_False})),
    1.54 +   ("fFalse", (false, true, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    1.55 +   ("fTrue", (true, true, @{thms True_or_False})),
    1.56 +   ("fTrue", (false, true, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    1.57     ("fNot",
    1.58 -    (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.59 -                   fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.60 +    (false, true, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.61 +                         fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.62     ("fconj",
    1.63 -    (false, @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
    1.64 -              by (unfold fconj_def) fast+})),
    1.65 +    (false, true,
    1.66 +     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
    1.67 +         by (unfold fconj_def) fast+})),
    1.68     ("fdisj",
    1.69 -    (false, @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
    1.70 -              by (unfold fdisj_def) fast+})),
    1.71 +    (false, true,
    1.72 +     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
    1.73 +         by (unfold fdisj_def) fast+})),
    1.74     ("fimplies",
    1.75 -    (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
    1.76 -                    "~ fimplies P Q | ~ P | Q"
    1.77 -              by (unfold fimplies_def) fast+})),
    1.78 -   ("If", (true, @{thms if_True if_False True_or_False}))]
    1.79 +    (false, true, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
    1.80 +                          "~ fimplies P Q | ~ P | Q"
    1.81 +                      by (unfold fimplies_def) fast+})),
    1.82 +   ("If", (true, true, @{thms if_True if_False True_or_False}))]
    1.83  
    1.84  (* ------------------------------------------------------------------------- *)
    1.85  (* Logic maps manage the interface between HOL and first-order logic.        *)
    1.86 @@ -778,7 +783,7 @@
    1.87              val helper_ths =
    1.88                metis_helpers
    1.89                |> filter (is_used o prefix const_prefix o fst)
    1.90 -              |> maps (fn (_, (needs_full_types, thms)) =>
    1.91 +              |> maps (fn (_, (needs_full_types, _, thms)) =>
    1.92                            if needs_full_types andalso mode <> FT then []
    1.93                            else map prepare_helper thms)
    1.94            in lmap |> fold (add_thm false) helper_ths end

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 16:23:03 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 17:16:13 2011 +0200
     2.3 @@ -740,9 +740,9 @@
     2.4      let
     2.5        val thy = Proof_Context.theory_of ctxt
     2.6        val unmangled_s = mangled_s |> unmangled_const_name
     2.7 -      fun dub_and_inst c needs_some_types (th, j) =
     2.8 +      fun dub_and_inst c needs_fairly_sound (th, j) =
     2.9          ((c ^ "_" ^ string_of_int j ^
    2.10 -          (if needs_some_types then typed_helper_suffix
    2.11 +          (if needs_fairly_sound then typed_helper_suffix
    2.12             else untyped_helper_suffix),
    2.13            General),
    2.14           let val t = th |> prop_of in
    2.15 @@ -756,17 +756,20 @@
    2.16           end)
    2.17        fun make_facts eq_as_iff =
    2.18          map_filter (make_fact ctxt false eq_as_iff false)
    2.19 -      val has_some_types = is_type_sys_fairly_sound type_sys
    2.20 +      val fairly_sound = is_type_sys_fairly_sound type_sys
    2.21      in
    2.22        metis_helpers
    2.23 -      |> maps (fn (metis_s, (needs_some_types, ths)) =>
    2.24 +      |> maps (fn (metis_s, (needs_fairly_sound, mono, ths)) =>
    2.25                    if metis_s <> unmangled_s orelse
    2.26 -                     (needs_some_types andalso not has_some_types) then
    2.27 +                     (needs_fairly_sound andalso not fairly_sound) orelse
    2.28 +                     (not mono andalso
    2.29 +                      polymorphism_of_type_sys type_sys = Polymorphic andalso
    2.30 +                      level_of_type_sys type_sys <> All_Types) then
    2.31                      []
    2.32                    else
    2.33                      ths ~~ (1 upto length ths)
    2.34 -                    |> map (dub_and_inst mangled_s needs_some_types)
    2.35 -                    |> make_facts (not needs_some_types))
    2.36 +                    |> map (dub_and_inst mangled_s needs_fairly_sound)
    2.37 +                    |> make_facts (not needs_fairly_sound))
    2.38      end
    2.39    | NONE => []
    2.40  fun helper_facts_for_sym_table ctxt type_sys sym_tab =