added Sledgehammer support for higher-order propositional reasoning

--- a/src/HOL/Metis.thy	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Metis.thy	Wed Dec 15 11:26:28 2010 +0100
@@ -15,17 +15,26 @@
      ("Tools/try.ML")
 begin
 
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<longleftrightarrow> (X = Y)"
+definition fFalse :: bool where [no_atp]:
+"fFalse \<longleftrightarrow> False"
 
-lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
-by (simp add: fequal_def)
+definition fTrue :: bool where [no_atp]:
+"fTrue \<longleftrightarrow> True"
+
+definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
+"fNot P \<longleftrightarrow> \<not> P"
 
-lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
-by (simp add: fequal_def)
+definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fconj P Q \<longleftrightarrow> P \<and> Q"
+
+definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fdisj P Q \<longleftrightarrow> P \<or> Q"
 
-lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
-by auto
+definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal x y \<longleftrightarrow> (x = y)"
 
 use "Tools/Metis/metis_translate.ML"
 use "Tools/Metis/metis_reconstruct.ML"
@@ -36,8 +45,9 @@
   #> Metis_Tactics.setup
 *}
 
-hide_const (open) fequal
-hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
+hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal
+hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
+                 fequal_def
 
 subsection {* Try *}
 

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -81,22 +81,13 @@
 
 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
-fun smart_invert_const "fFalse" = @{const_name False}
-  | smart_invert_const "fTrue" = @{const_name True}
-  | smart_invert_const "fNot" = @{const_name Not}
-  | smart_invert_const "fconj" = @{const_name conj}
-  | smart_invert_const "fdisj" = @{const_name disj}
-  | smart_invert_const "fimplies" = @{const_name implies}
-  | smart_invert_const "fequal" = @{const_name HOL.eq}
-  | smart_invert_const s = invert_const s
-
 fun hol_type_from_metis_term _ (Metis_Term.Var v) =
      (case strip_prefix_and_unascii tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)
   | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
      (case strip_prefix_and_unascii type_const_prefix x of
-          SOME tc => Type (smart_invert_const tc,
+          SOME tc => Type (invert_const tc,
                            map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
       case strip_prefix_and_unascii tfree_prefix x of
@@ -132,7 +123,7 @@
             case strip_prefix_and_unascii const_prefix a of
                 SOME b =>
                   let
-                    val c = smart_invert_const b
+                    val c = invert_const b
                     val ntypes = num_type_args thy c
                     val nterms = length ts - ntypes
                     val tts = map tm_to_tt ts
@@ -158,7 +149,7 @@
               | NONE => (*Not a constant. Is it a type constructor?*)
             case strip_prefix_and_unascii type_const_prefix a of
                 SOME b =>
-                SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts)))
+                SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
             case strip_prefix_and_unascii tfree_prefix a of
                 SOME b => SomeType (mk_tfree ctxt b)
@@ -186,7 +177,7 @@
             Const (@{const_name HOL.eq}, HOLogic.typeT)
         | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
            (case strip_prefix_and_unascii const_prefix x of
-                SOME c => Const (smart_invert_const c, dummyT)
+                SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
@@ -200,7 +191,7 @@
             list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
         | cvt (t as Metis_Term.Fn (x, [])) =
            (case strip_prefix_and_unascii const_prefix x of
-                SOME c => Const (smart_invert_const c, dummyT)
+                SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix_and_unascii fixed_var_prefix x of
                 SOME v => Free (v, dummyT)

--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -74,6 +74,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 prepare_metis_problem :
     mode -> Proof.context -> bool -> thm list -> thm list list
     -> mode * metis_problem
@@ -130,8 +131,14 @@
 
 (* Invert the table of translations between Isabelle and ATPs. *)
 val const_trans_table_inv =
-  Symtab.update ("fequal", @{const_name HOL.eq})
-                (Symtab.make (map swap (Symtab.dest const_trans_table)))
+  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
+  |> fold Symtab.update [("fFalse", @{const_name False}),
+                         ("fTrue", @{const_name True}),
+                         ("fNot", @{const_name Not}),
+                         ("fconj", @{const_name conj}),
+                         ("fdisj", @{const_name disj}),
+                         ("fimplies", @{const_name implies}),
+                         ("fequal", @{const_name HOL.eq})]
 
 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
 
@@ -660,7 +667,7 @@
       end
   end;
 
-val helpers =
+val metis_helpers =
   [("c_COMBI", (false, @{thms Meson.COMBI_def})),
    ("c_COMBK", (false, @{thms Meson.COMBK_def})),
    ("c_COMBB", (false, @{thms Meson.COMBB_def})),
@@ -670,26 +677,20 @@
     (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
                    fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse"
-                          by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])),
-   ("c_fFalse", (false, [@{lemma "~ fFalse"
-                           by (unfold Metis.fFalse_def) fast}])),
+                          by (unfold fFalse_def fTrue_def) fast}])),
+   ("c_fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse"
-                         by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])),
-   ("c_fTrue", (false, [@{lemma "fTrue"
-                          by (unfold Metis.fTrue_def) fast}])),
+                         by (unfold fFalse_def fTrue_def) fast}])),
+   ("c_fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    ("c_fNot",
     (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
                    fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    ("c_fconj",
-    (false, @{lemma "~ P | ~ Q | Metis.fconj P Q"
-                    "~ Metis.fconj P Q | P"
-                    "~ Metis.fconj P Q | Q"
-              by (unfold Metis.fconj_def) fast+})),
+    (false, @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
+              by (unfold fconj_def) fast+})),
    ("c_fdisj",
-    (false, @{lemma "~ P | Metis.fdisj P Q"
-                    "~ Q | Metis.fdisj P Q"
-                    "~ Metis.fdisj P Q | P | Q"
-              by (unfold Metis.fdisj_def) fast+})),
+    (false, @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
+              by (unfold fdisj_def) fast+})),
    ("c_fimplies",
     (false, @{lemma "P | Metis.fimplies P Q"
                     "~ Q | Metis.fimplies P Q"
@@ -801,10 +802,11 @@
               #> `(Meson.make_meta_clause
                    #> rewrite_rule (map safe_mk_meta_eq fdefs))
             val helper_ths =
-              helpers |> filter (is_used o fst)
-                      |> maps (fn (c, (needs_full_types, thms)) =>
-                                  if needs_full_types andalso mode <> FT then []
-                                  else map prepare_helper thms)
+              metis_helpers
+              |> filter (is_used o fst)
+              |> maps (fn (c, (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
   in
     (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -126,7 +126,8 @@
 fun using_labels [] = ""
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name type_sys = if is_fully_typed type_sys then "metisFT" else "metis"
+fun metis_name type_sys =
+  if types_dangerous_types type_sys then "metisFT" else "metis"
 fun metis_call type_sys ss = command_call (metis_name type_sys) ss
 fun metis_command type_sys i n (ls, ss) =
   using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss
@@ -335,19 +336,14 @@
             val term_ts = map (aux NONE []) term_us
             val extra_ts = map (aux NONE []) extra_us
             val t =
-              Const (c, if is_fully_typed type_sys then
-                          case opt_T of
-                            SOME T => map fastype_of term_ts ---> T
-                          | NONE =>
-                            if num_type_args thy c = 0 then
-                              Sign.const_instance thy (c, [])
-                            else
-                              raise Fail ("no type information for " ^ quote c)
-                        else if num_type_args thy c = length type_us then
-                          Sign.const_instance thy (c,
-                              map (type_from_fo_term tfrees) type_us)
-                        else
-                          HOLogic.typeT)
+              Const (c, case opt_T of
+                          SOME T => map fastype_of term_ts ---> T
+                        | NONE =>
+                          if num_type_args thy c = length type_us then
+                            Sign.const_instance thy (c,
+                                map (type_from_fo_term tfrees) type_us)
+                          else
+                            HOLogic.typeT)
           in list_comb (t, term_ts @ extra_ts) end
         | NONE => (* a free or schematic variable *)
           let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -20,7 +20,6 @@
   val precise_overloaded_args : bool Unsynchronized.ref
   val fact_prefix : string
   val conjecture_prefix : string
-  val is_fully_typed : type_system -> bool
   val types_dangerous_types : type_system -> bool
   val num_atp_type_args : theory -> type_system -> string -> int
   val translate_atp_fact :
@@ -32,7 +31,7 @@
     -> string problem * string Symtab.table * int * (string * 'a) list vector
 end;
 
-structure Sledgehammer_ATP_Translate (*### : SLEDGEHAMMER_ATP_TRANSLATE *) =
+structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
 struct
 
 open ATP_Problem
@@ -65,10 +64,6 @@
   Const_Args |
   No_Types
 
-fun is_fully_typed (Tags full_types) = full_types
-  | is_fully_typed (Preds full_types) = full_types
-  | is_fully_typed _ = false
-
 fun types_dangerous_types (Tags _) = true
   | types_dangerous_types (Preds _) = true
   | types_dangerous_types _ = false
@@ -84,7 +79,7 @@
 fun needs_type_args thy type_sys s =
   case type_sys of
     Tags full_types => not full_types andalso is_overloaded thy s
-  | Preds full_types => is_overloaded thy s (* FIXME: could be more precise *)
+  | Preds _ => is_overloaded thy s (* FIXME: could be more precise *)
   | Const_Args => is_overloaded thy s
   | No_Types => false
 
@@ -100,9 +95,11 @@
   | mk_ahorn (phi :: phis) psi =
     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
 
-fun combformula_for_prop thy =
+fun combformula_for_prop thy eq_as_iff =
   let
-    val do_term = combterm_from_term thy
+    fun do_term bs t ts =
+      combterm_from_term thy bs (Envir.eta_contract t)
+      |>> AAtom ||> union (op =) ts
     fun do_quant bs q s T t' =
       let val s = Name.variant (map fst bs) s in
         do_formula ((s, T) :: bs) t'
@@ -123,9 +120,8 @@
       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
       | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
-        do_conn bs AIff t1 t2
-      | _ => (fn ts => do_term bs (Envir.eta_contract t)
-                       |>> AAtom ||> union (op =) ts)
+        if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
+      | _ => do_term bs t
   in do_formula [] end
 
 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
@@ -224,7 +220,7 @@
   in perhaps (try aux) end
 
 (* making fact and conjecture formulas *)
-fun make_formula ctxt presimp name kind t =
+fun make_formula ctxt eq_as_iff presimp name kind t =
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
@@ -237,66 +233,59 @@
               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
               |> kind <> Axiom ? freeze_term
-    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
+    val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t []
   in
     {name = name, combformula = combformula, kind = kind,
      ctypes_sorts = ctypes_sorts}
   end
 
-fun make_fact ctxt presimp ((name, _), th) =
-  case make_formula ctxt presimp name Axiom (prop_of th) of
+fun make_fact ctxt eq_as_iff presimp ((name, _), th) =
+  case make_formula ctxt eq_as_iff presimp name Axiom (prop_of th) of
     {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   | formula => SOME formula
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
-    map2 (fn j => make_formula ctxt true (Int.toString j)
+    map2 (fn j => make_formula ctxt true true (Int.toString j)
                                (if j = last then Conjecture else Hypothesis))
          (0 upto last) ts
   end
 
 (** Helper facts **)
 
-fun count_combterm (CombConst ((s, _), _, _)) =
-    Symtab.map_entry s (Integer.add 1)
-  | count_combterm (CombVar _) = I
-  | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
-fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
-  | count_combformula (AConn (_, phis)) = fold count_combformula phis
-  | count_combformula (AAtom tm) = count_combterm tm
-fun count_translated_formula ({combformula, ...} : translated_formula) =
-  count_combformula combformula
-
-val optional_helpers =
-  [(["c_COMBI"], @{thms Meson.COMBI_def}),
-   (["c_COMBK"], @{thms Meson.COMBK_def}),
-   (["c_COMBB"], @{thms Meson.COMBB_def}),
-   (["c_COMBC"], @{thms Meson.COMBC_def}),
-   (["c_COMBS"], @{thms Meson.COMBS_def})]
-val optional_fully_typed_helpers =
-  [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
-   (["c_If"], @{thms if_True if_False})]
-val mandatory_helpers = @{thms Metis.fequal_def}
+fun count_term (ATerm ((s, _), tms)) =
+  (if is_atp_variable s then I
+   else Symtab.map_entry s (Integer.add 1))
+  #> fold count_term tms
+fun count_formula (AQuant (_, _, phi)) = count_formula phi
+  | count_formula (AConn (_, phis)) = fold count_formula phis
+  | count_formula (AAtom tm) = count_term tm
 
 val init_counters =
-  [optional_helpers, optional_fully_typed_helpers] |> maps (maps fst)
-  |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
+  metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
+  |> Symtab.make
 
-fun get_helper_facts ctxt is_FO type_sys conjectures facts =
+fun get_helper_facts ctxt type_sys formulas =
   let
-    val ct =
-      fold (fold count_translated_formula) [conjectures, facts] init_counters
-    fun is_needed c = the (Symtab.lookup ct c) > 0
-    fun baptize th = ((Thm.get_name_hint th, false), th)
+    val no_dangerous_types = types_dangerous_types type_sys
+    val ct = init_counters |> fold count_formula formulas
+    fun is_used s = the (Symtab.lookup ct s) > 0
+    fun dub c needs_full_types (th, j) =
+      ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
+        false), th)
+    fun make_facts eq_as_iff = map_filter (make_fact ctxt eq_as_iff false)
   in
-    (optional_helpers
-     |> is_fully_typed type_sys ? append optional_fully_typed_helpers
-     |> maps (fn (ss, ths) =>
-                 if exists is_needed ss then map baptize ths else [])) @
-    (if is_FO then [] else map baptize mandatory_helpers)
-    |> map_filter (make_fact ctxt false)
+    metis_helpers
+    |> filter (is_used o fst)
+    |> maps (fn (c, (needs_full_types, ths)) =>
+                if needs_full_types andalso not no_dangerous_types then
+                  []
+                else
+                  ths ~~ (1 upto length ths)
+                  |> map (dub c needs_full_types)
+                  |> make_facts (not needs_full_types))
   end
 
-fun translate_atp_fact ctxt = `(make_fact ctxt true)
+fun translate_atp_fact ctxt = `(make_fact ctxt true true)
 
 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   let
@@ -311,20 +300,18 @@
        boost an ATP's performance (for some reason). *)
     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
     val goal_t = Logic.list_implies (hyp_ts, concl_t)
-    val is_FO = Meson.is_fol_term thy goal_t
     val subs = tfree_classes_of_terms [goal_t]
     val supers = tvar_classes_of_terms fact_ts
     val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
     (* TFrees in the conjecture; TVars in the facts *)
     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
-    val helper_facts = get_helper_facts ctxt is_FO type_sys conjectures facts
     val (supers', arity_clauses) =
       if type_sys = No_Types then ([], [])
       else make_arity_clauses thy tycons supers
     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
     (fact_names |> map single |> Vector.fromList,
-     (conjectures, facts, helper_facts, class_rel_clauses, arity_clauses))
+     (conjectures, facts, class_rel_clauses, arity_clauses))
   end
 
 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
@@ -352,7 +339,7 @@
   | is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false
 and is_type_dangerous ctxt (Type (s, Ts)) =
     is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts
-  | is_type_dangerous ctxt _ = false
+  | is_type_dangerous _ _ = false
 and is_type_constr_dangerous ctxt s =
   let val thy = ProofContext.theory_of ctxt in
     case Datatype_Data.get_info thy s of
@@ -376,6 +363,15 @@
     full_types orelse is_combtyp_dangerous ctxt ty
   | should_tag_with_type _ _ _ = false
 
+val fname_table =
+  [("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))),
+   ("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))),
+   ("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))),
+   ("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))),
+   ("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))),
+   ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
+   ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
+
 fun fo_term_for_combterm ctxt type_sys =
   let
     val thy = ProofContext.theory_of ctxt
@@ -385,27 +381,27 @@
         val (x, ty_args) =
           case head of
             CombConst (name as (s, s'), _, ty_args) =>
-            (case strip_prefix_and_unascii const_prefix s of
-               NONE =>
-               if s = "equal" then
-                 if top_level andalso length args = 2 then (name, [])
-                 else (("c_fequal", @{const_name Metis.fequal}), ty_args)
-               else
-                 (name, ty_args)
-             | SOME s'' =>
-               let
-                 val s'' = invert_const s''
-                 val ty_args =
-                   if needs_type_args thy type_sys s'' then ty_args else []
-                in
-                  if top_level then
-                    case s of
-                      "c_False" => (("$false", s'), [])
-                    | "c_True" => (("$true", s'), [])
-                    | _ => (name, ty_args)
-                  else
-                    (name, ty_args)
-                end)
+            (case AList.lookup (op =) fname_table s of
+               SOME (n, fname) =>
+               if top_level andalso length args = n then (name, [])
+               else (fname, ty_args)
+             | NONE =>
+               case strip_prefix_and_unascii const_prefix s of
+                 NONE => (name, ty_args)
+               | SOME s'' =>
+                 let
+                   val s'' = invert_const s''
+                   val ty_args =
+                     if needs_type_args thy type_sys s'' then ty_args else []
+                  in
+                    if top_level then
+                      case s of
+                        "c_False" => (("$false", s'), [])
+                      | "c_True" => (("$true", s'), [])
+                      | _ => (name, ty_args)
+                    else
+                      (name, ty_args)
+                  end)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t =
@@ -498,9 +494,14 @@
 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
 
+(* needed for helper facts if the problem otherwise does not involve equality *)
+val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false})
+
 fun const_table_for_problem explicit_apply problem =
-  if explicit_apply then NONE
-  else SOME (Symtab.empty |> consider_problem problem)
+  if explicit_apply then
+    NONE
+  else
+    SOME (Symtab.empty |> Symtab.update equal_entry |> consider_problem problem)
 
 fun min_arity_of thy type_sys NONE s =
     (if s = "equal" orelse s = type_tag_name orelse
@@ -561,14 +562,14 @@
       not sub_level andalso min_arity = max_arity
     | NONE => false
 
-fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) =
   if s = type_tag_name then
     case ts of
       [_, t' as ATerm ((s', _), _)] =>
-      if is_predicate const_tab s' then t' else boolify t
+      if is_predicate pred_const_tab s' then t' else boolify t
     | _ => raise Fail "malformed type tag"
   else
-    t |> not (is_predicate const_tab s) ? boolify
+    t |> not (is_predicate pred_const_tab s) ? boolify
 
 fun close_universally phi =
   let
@@ -586,33 +587,28 @@
 
 fun repair_formula thy explicit_forall type_sys const_tab =
   let
+    val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab
     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
       | aux (AConn (c, phis)) = AConn (c, map aux phis)
       | aux (AAtom tm) =
         AAtom (tm |> repair_applications_in_term thy type_sys const_tab
-                  |> repair_predicates_in_term const_tab)
+                  |> repair_predicates_in_term pred_const_tab)
   in aux #> explicit_forall ? close_universally end
 
 fun repair_problem_line thy explicit_forall type_sys const_tab
                         (Fof (ident, kind, phi)) =
   Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
-fun repair_problem_with_const_table thy =
-  map o apsnd o map ooo repair_problem_line thy
+fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
 
-fun repair_problem thy explicit_forall type_sys explicit_apply problem =
-  repair_problem_with_const_table thy explicit_forall type_sys
-      (const_table_for_problem explicit_apply problem) problem
+fun dest_Fof (Fof z) = z
 
 fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
                         explicit_apply hyp_ts concl_t facts =
   let
     val thy = ProofContext.theory_of ctxt
-    val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
-                      arity_clauses)) =
+    val (fact_names, (conjectures, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
     val fact_lines = map (problem_line_for_fact ctxt fact_prefix type_sys) facts
-    val helper_lines =
-      map (problem_line_for_fact ctxt helper_prefix type_sys) helper_facts
     val conjecture_lines =
       map (problem_line_for_conjecture ctxt type_sys) conjectures
     val tfree_lines = problem_lines_for_free_types type_sys conjectures
@@ -625,11 +621,21 @@
       [("Relevant facts", fact_lines),
        ("Class relationships", class_rel_lines),
        ("Arity declarations", arity_lines),
-       ("Helper facts", helper_lines),
+       ("Helper facts", []),
        ("Conjectures", conjecture_lines),
        ("Type variables", tfree_lines)]
-      |> repair_problem thy explicit_forall type_sys explicit_apply
-    val (problem, pool) = nice_atp_problem readable_names problem
+    val const_tab = const_table_for_problem explicit_apply problem
+    val problem =
+      problem |> repair_problem thy explicit_forall type_sys const_tab
+    val helper_facts =
+      get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
+    val helper_lines =
+      helper_facts
+      |> map (problem_line_for_fact ctxt helper_prefix type_sys
+              #> repair_problem_line thy explicit_forall type_sys const_tab)
+    val (problem, pool) =
+      problem |> AList.update (op =) ("Helper facts", helper_lines)
+              |> nice_atp_problem readable_names
     val conjecture_offset =
       length fact_lines + length class_rel_lines + length arity_lines
       + length helper_lines

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -233,6 +233,8 @@
       | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
         fold (do_term_or_formula T) [t1, t2]
       | @{const Trueprop} $ t1 => do_formula pos t1
+      | @{const False} => I
+      | @{const True} => I
       | @{const Not} $ t1 => do_formula (flip pos) t1
       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
         do_quantifier (pos = SOME false) T t'

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -127,11 +127,12 @@
       #default_max_relevant (get_atp thy name)
   end
 
-(* These are typically simplified away by "Meson.presimplify". Equality is
-   handled specially via "fequal". *)
+(* These are either simplified away by "Meson.presimplify" (most of the time) or
+   handled specially via "fFalse", "fTrue", ..., "fequal". *)
 val atp_irrelevant_consts =
-  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
-   @{const_name HOL.eq}]
+  [@{const_name False}, @{const_name True}, @{const_name Not},
+   @{const_name conj}, @{const_name disj}, @{const_name implies},
+   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
 
 fun is_built_in_const_for_prover ctxt name (s, T) args =
   if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) args