merged

--- a/src/HOL/Predicate.thy	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Predicate.thy	Fri Jun 25 12:15:49 2010 +0200
@@ -645,7 +645,7 @@
 lemma "f () = False \<or> f () = True"
 by simp
 
-lemma closure_of_bool_cases:
+lemma closure_of_bool_cases [no_atp]:
 assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f"
 assumes "f = (%u. True) \<Longrightarrow> P f"
 shows "P f"

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 25 12:15:49 2010 +0200
@@ -223,7 +223,7 @@
           val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
           val result =
             do_run false
-            |> (fn (_, msecs0, _, SOME IncompleteUnprovable) =>
+            |> (fn (_, msecs0, _, SOME _) =>
                    do_run true
                    |> (fn (output, msecs, proof, outcome) =>
                           (output, msecs0 + msecs, proof, outcome))
@@ -298,9 +298,11 @@
 val spass_config : prover_config =
   {home_var = "SPASS_HOME",
    executable = "SPASS",
+   (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
      ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
-      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
+      \-VarWeight=3 -TimeLimit=" ^
+      string_of_int (to_generous_secs timeout div 2))
      |> not complete ? prefix "-SOS=1 ",
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 12:15:49 2010 +0200
@@ -446,13 +446,15 @@
   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   could then fail. See comment on mk_var.*)
 fun resolve_inc_tyvars(tha,i,thb) =
-  let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+  let
+      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
       val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   in
       case distinct Thm.eq_thm ths of
         [th] => th
       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
-  end;
+  end
+  handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg)
 
 fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 12:15:49 2010 +0200
@@ -88,10 +88,11 @@
   Symtab.map_default (c, [ctyps])
                      (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
 
-val fresh_sko_prefix = "Sledgehammer.Skox."
+val fresh_prefix = "Sledgehammer.Fresh."
 
 val flip = Option.map not
 
+val boring_natural_consts = [@{const_name If}]
 (* Including equality in this list might be expected to stop rules like
    subset_antisym from being chosen, but for some reason filtering works better
    with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
@@ -113,12 +114,15 @@
       | Free x => add_const_type_to_table (const_with_typ thy x)
       | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
       | t1 $ t2 => do_term t1 #> do_term t2
-      | Abs (_, _, t) => do_term t
+      | Abs (_, _, t) =>
+        (* Abstractions lead to combinators, so we add a penalty for them. *)
+        add_const_type_to_table (gensym fresh_prefix, [])
+        #> do_term t
       | _ => I
     fun do_quantifier sweet_pos pos body_t =
       do_formula pos body_t
       #> (if pos = SOME sweet_pos then I
-          else add_const_type_to_table (gensym fresh_sko_prefix, []))
+          else add_const_type_to_table (gensym fresh_prefix, []))
     and do_equality T t1 t2 =
       fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
             else do_term) [t1, t2]
@@ -148,7 +152,8 @@
   in
     Symtab.empty
     |> (if !use_natural_form then
-          fold (do_formula pos) ts
+          fold (Symtab.update o rpair []) boring_natural_consts
+          #> fold (do_formula pos) ts
         else
           fold (Symtab.update o rpair []) boring_cnf_consts
           #> fold do_term ts)
@@ -361,9 +366,15 @@
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
       val goal_const_tab = get_consts_typs thy (SOME true) goals
+      val relevance_threshold =
+        if !use_natural_form then 0.9 * relevance_threshold (* experimental *)
+        else relevance_threshold
       val _ =
         trace_msg (fn () => "Initial constants: " ^
-                            commas (Symtab.keys goal_const_tab))
+                            commas (goal_const_tab
+                                    |> Symtab.dest
+                                    |> filter (curry (op <>) [] o snd)
+                                    |> map fst))
       val relevant =
         relevant_clauses ctxt relevance_convergence defs_relevant max_new
                          relevance_override const_tab relevance_threshold
@@ -609,7 +620,7 @@
 fun count_literal (Literal (_, t)) = count_combterm t
 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
 
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
+fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
   #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)