try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -611,7 +611,8 @@
 (* Translation of HO Clauses                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-fun cnf_th thy th = hd (cnf_axiom thy th);
+fun cnf_helper_theorem thy raw th =
+  if raw then th else the_single (cnf_axiom thy th)
 
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
@@ -661,6 +662,17 @@
   | string_of_mode HO = "HO"
   | string_of_mode FT = "FT"
 
+val helpers =
+  [("c_COMBI", (false, @{thms COMBI_def})),
+   ("c_COMBK", (false, @{thms COMBK_def})),
+   ("c_COMBB", (false, @{thms COMBB_def})),
+   ("c_COMBC", (false, @{thms COMBC_def})),
+   ("c_COMBS", (false, @{thms COMBS_def})),
+   ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
+   ("c_True", (true, @{thms True_or_False})),
+   ("c_False", (true, @{thms True_or_False})),
+   ("c_If", (true, @{thms if_True if_False True_or_False}))]
+
 (* Function to generate metis clauses, including comb and type clauses *)
 fun build_map mode0 ctxt cls ths =
   let val thy = ProofContext.theory_of ctxt
@@ -688,17 +700,21 @@
         |> add_tfrees
         |> fold (add_thm false) ths
       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
-      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
-      (*Now check for the existence of certain combinators*)
-      val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
-      val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
-      val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
-      val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
-      val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
-      val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
+      fun is_used c =
+        exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
       val lmap =
-        lmap |> mode <> FO
-                ? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
+        if mode = FO then
+          lmap
+        else
+          let
+            val helper_ths =
+              helpers |> filter (is_used o fst)
+                      |> maps (fn (_, (raw, thms)) =>
+                                  if mode = FT orelse not raw then
+                                    map (cnf_helper_theorem @{theory} raw) thms
+                                  else
+                                    [])
+          in lmap |> fold (add_thm false) helper_ths end
   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
 
 fun refute cls =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -27,7 +27,8 @@
     -> Proof.context * (thm list * 'a) -> thm list
     -> (thm * (string * int)) list
   val prepare_clauses :
-    bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list
+    bool -> bool -> thm list -> thm list
+    -> (thm * (axiom_name * hol_clause_id)) list
     -> (thm * (axiom_name * hol_clause_id)) list -> theory
     -> axiom_name vector
        * (hol_clause list * hol_clause list * hol_clause list *
@@ -565,7 +566,7 @@
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chained_ths axcls extra_cls thy =
+fun prepare_clauses dfg full_types goal_cls chained_ths axcls extra_cls thy =
   let
     val is_FO = is_fol_goal thy goal_cls
     val ccls = subtract_cls extra_cls goal_cls
@@ -579,7 +580,8 @@
     val conjectures = make_conjecture_clauses dfg thy ccls
     val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses dfg thy extra_cls)
     val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses dfg thy axcls)
-    val helper_clauses = get_helper_clauses dfg thy is_FO conjectures extra_cls
+    val helper_clauses =
+      get_helper_clauses dfg thy is_FO full_types conjectures extra_cls
     val (supers', arity_clauses) = make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = make_classrel_clauses thy subs supers'
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -111,9 +111,8 @@
         in
           (SOME min_thms,
            proof_text isar_proof
-               (pool, debug, full_types, isar_shrink_factor, ctxt,
-                conjecture_shape)
-               (K "", proof, internal_thm_names, goal, i) |> fst)
+               (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+               (full_types, K "", proof, internal_thm_names, goal, i) |> fst)
         end
     | {outcome = SOME TimedOut, ...} =>
         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
@@ -126,7 +125,8 @@
                \option (e.g., \"timeout = " ^
                string_of_int (10 + msecs div 1000) ^ " s\").")
     | {message, ...} => (NONE, "ATP error: " ^ message))
-    handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n [])
+    handle Sledgehammer_HOL_Clause.TRIVIAL =>
+           (SOME [], metis_line full_types i n [])
          | ERROR msg => (NONE, "Error: " ^ msg)
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -111,7 +111,7 @@
 fun union_all xss = fold (union (op =)) xss []
 
 (* Readable names for the more common symbolic functions. Do not mess with the
-   last six entries of the table unless you know what you are doing. *)
+   last nine entries of the table unless you know what you are doing. *)
 val const_trans_table =
   Symtab.make [(@{const_name "op ="}, "equal"),
                (@{const_name "op &"}, "and"),
@@ -123,7 +123,10 @@
                (@{const_name COMBK}, "COMBK"),
                (@{const_name COMBB}, "COMBB"),
                (@{const_name COMBC}, "COMBC"),
-               (@{const_name COMBS}, "COMBS")]
+               (@{const_name COMBS}, "COMBS"),
+               (@{const_name True}, "True"),
+               (@{const_name False}, "False"),
+               (@{const_name If}, "If")]
 
 val type_const_trans_table =
   Symtab.make [(@{type_name "*"}, "prod"),

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -37,7 +37,7 @@
        (thm * (axiom_name * hol_clause_id)) list -> (axiom_name * hol_clause) list
   val type_wrapper_name : string
   val get_helper_clauses :
-    bool -> theory -> bool -> hol_clause list
+    bool -> theory -> bool -> bool -> hol_clause list
       -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
   val write_tptp_file : bool -> bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
@@ -54,13 +54,13 @@
 open Sledgehammer_FOL_Clause
 open Sledgehammer_Fact_Preprocessor
 
-fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
+fun min_arity_of const_min_arity c =
+  the_default 0 (Symtab.lookup const_min_arity c)
 
 (*True if the constant ever appears outside of the top-level position in literals.
   If false, the constant always receives all of its arguments and is used as a predicate.*)
 fun needs_hBOOL explicit_apply const_needs_hBOOL c =
-  explicit_apply orelse
-    the_default false (Symtab.lookup const_needs_hBOOL c);
+  explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
 
 
 (******************************************************)
@@ -452,10 +452,6 @@
 (* write clauses to files                                             *)
 (**********************************************************************)
 
-val init_counters =
-  Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0),
-               ("c_COMBS", 0)];
-
 fun count_combterm (CombConst ((c, _), _, _)) =
     Symtab.map_entry c (Integer.add 1)
   | count_combterm (CombVar _) = I
@@ -465,28 +461,37 @@
 
 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
 
-fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint)
+val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0)))
+fun cnf_helper_thms thy raw =
+  map (`Thm.get_name_hint)
+  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+
+val optional_helpers =
+  [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
+   (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})),
+   (["c_COMBS"], (false, @{thms COMBS_def}))]
+val optional_typed_helpers =
+  [(["c_True", "c_False"], (true, @{thms True_or_False})),
+   (["c_If"], (true, @{thms if_True if_False True_or_False}))]
+val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
 
-fun get_helper_clauses dfg thy isFO conjectures axcls =
-  if isFO then
-    []
-  else
-    let
-        val axclauses = map snd (make_axiom_clauses dfg thy axcls)
-        val ct = init_counters
-                 |> fold (fold count_clause) [conjectures, axclauses]
-        fun needed c = the (Symtab.lookup ct c) > 0
-        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
-                 then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}]
-                 else []
-        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
-                 then cnf_helper_thms thy [@{thm COMBB_def}, @{thm COMBC_def}]
-                 else []
-        val S = if needed "c_COMBS" then cnf_helper_thms thy [@{thm COMBS_def}]
-                else []
-        val other = cnf_helper_thms thy [@{thm fequal_imp_equal},
-                                         @{thm equal_imp_fequal}]
-    in map snd (make_axiom_clauses dfg thy (other @ IK @ BC @ S)) end
+val init_counters =
+  Symtab.make (maps (maps (map (rpair 0) o fst))
+                    [optional_helpers, optional_typed_helpers])
+
+fun get_helper_clauses dfg thy is_FO full_types conjectures axcls =
+  let
+    val axclauses = map snd (make_axiom_clauses dfg thy axcls)
+    val ct = fold (fold count_clause) [conjectures, axclauses] init_counters
+    fun is_needed c = the (Symtab.lookup ct c) > 0
+    val cnfs =
+      (optional_helpers
+       |> full_types ? append optional_typed_helpers
+       |> maps (fn (ss, (raw, ths)) =>
+                   if exists is_needed ss then cnf_helper_thms thy raw ths
+                   else []))
+      @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
+  in map snd (make_axiom_clauses dfg thy cnfs) end
 
 (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   are not at top level, to see if hBOOL is needed.*)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jun 21 12:28:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jun 21 12:31:41 2010 +0200
@@ -14,17 +14,17 @@
   val invert_type_const: string -> string
   val num_type_args: theory -> string -> int
   val strip_prefix: string -> string -> string option
-  val metis_line: int -> int -> string list -> string
+  val metis_line: bool -> int -> int -> string list -> string
   val metis_proof_text:
-    minimize_command * string * string vector * thm * int
+    bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    name_pool option * bool * bool * int * Proof.context * int list list
-    -> minimize_command * string * string vector * thm * int
+    name_pool option * bool * int * Proof.context * int list list
+    -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val proof_text:
-    bool -> name_pool option * bool * bool * int * Proof.context * int list list
-    -> minimize_command * string * string vector * thm * int
+    bool -> name_pool option * bool * int * Proof.context * int list list
+    -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
 end;
 
@@ -600,13 +600,15 @@
 fun metis_apply _ 1 = "by "
   | metis_apply 1 _ = "apply "
   | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_itself [] = "metis"
-  | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
-fun metis_command i n (ls, ss) =
-  metis_using ls ^ metis_apply i n ^ metis_itself ss
-fun metis_line i n ss =
+fun metis_name full_types = if full_types then "metisFT" else "metis"
+fun metis_call full_types [] = metis_name full_types
+  | metis_call full_types ss =
+    "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
+fun metis_command full_types i n (ls, ss) =
+  metis_using ls ^ metis_apply i n ^ metis_call full_types ss
+fun metis_line full_types i n ss =
   "Try this command: " ^
-  Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
+  Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
 fun minimize_line _ [] = ""
   | minimize_line minimize_command facts =
     case minimize_command facts of
@@ -617,7 +619,8 @@
 
 val unprefix_chained = perhaps (try (unprefix chained_prefix))
 
-fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
+fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
+                      i) =
   let
     val raw_lemmas =
       atp_proof |> extract_clause_numbers_in_atp_proof
@@ -630,8 +633,8 @@
     val lemmas = other_lemmas @ chained_lemmas
     val n = Logic.count_prems (prop_of goal)
   in
-    (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas,
-     lemmas)
+    (metis_line full_types i n other_lemmas ^
+     minimize_line minimize_command lemmas, lemmas)
   end
 
 (** Isar proof construction and manipulation **)
@@ -932,7 +935,7 @@
         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt i n =
+fun string_for_proof ctxt full_types i n =
   let
     fun fix_print_mode f x =
       setmp_CRITICAL show_no_free_types true
@@ -956,7 +959,7 @@
       let
         val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
         val ss = ss |> map unprefix_chained |> sort_distinct string_ord
-      in metis_command 1 1 (ls, ss) end
+      in metis_command full_types 1 1 (ls, ss) end
     and do_step ind (Fix xs) =
         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
       | do_step ind (Let (t1, t2)) =
@@ -989,17 +992,16 @@
         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   in do_proof end
 
-fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
-                     conjecture_shape)
-                    (minimize_command, atp_proof, thm_names, goal, i) =
+fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+                    (other_params as (full_types, _, atp_proof, thm_names, goal,
+                                      i)) =
   let
     val thy = ProofContext.theory_of ctxt
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
     val n = Logic.count_prems (prop_of goal)
-    val (one_line_proof, lemma_names) =
-      metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
+    val (one_line_proof, lemma_names) = metis_proof_text other_params
     fun isar_proof_for () =
       case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
                                 atp_proof conjecture_shape thm_names params
@@ -1009,7 +1011,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt i n of
+           |> string_for_proof ctxt full_types i n of
         "" => ""
       | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =