author blanchet Wed, 15 Dec 2010 11:26:28 +0100 changeset 41140 9c68004b8c9d parent 41139 cb1cbae54dbf child 41141 ad923cdd4a5d
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"
+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"
+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 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, _), _, _)) =
-  | 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) =
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)
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```