1.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jun 29 09:26:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jun 29 10:25:53 2010 +0200
     1.3 @@ -8,9 +8,6 @@
     1.4  signature CLAUSIFIER =
     1.5  sig
     1.6    val cnf_axiom: theory -> thm -> thm list
     1.7 -  val multi_base_blacklist: string list
     1.8 -  val is_theorem_bad_for_atps: thm -> bool
     1.9 -  val type_has_topsort: typ -> bool
    1.10    val cnf_rules_pairs :
    1.11      theory -> (string * thm) list -> ((string * int) * thm) list
    1.12    val neg_clausify: thm -> thm list
    1.13 @@ -21,12 +18,6 @@
    1.14  structure Clausifier : CLAUSIFIER =
    1.15  struct
    1.16  
    1.17 -val type_has_topsort = Term.exists_subtype
    1.18 -  (fn TFree (_, []) => true
    1.19 -    | TVar (_, []) => true
    1.20 -    | _ => false);
    1.21 -
    1.22 -
    1.23  (**** Transformation of Elimination Rules into First-Order Formulas****)
    1.24  
    1.25  val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    1.26 @@ -237,77 +228,20 @@
    1.27                      |> Meson.make_nnf ctxt
    1.28    in  (th3, ctxt)  end;
    1.29  
    1.30 -(*** Blacklisting (more in "Sledgehammer_Fact_Filter") ***)
    1.31 -
    1.32 -val max_lambda_nesting = 3
    1.33 -
    1.34 -fun term_has_too_many_lambdas max (t1 $ t2) =
    1.35 -    exists (term_has_too_many_lambdas max) [t1, t2]
    1.36 -  | term_has_too_many_lambdas max (Abs (_, _, t)) =
    1.37 -    max = 0 orelse term_has_too_many_lambdas (max - 1) t
    1.38 -  | term_has_too_many_lambdas _ _ = false
    1.39 -
    1.40 -fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    1.41 -
    1.42 -(* Don't count nested lambdas at the level of formulas, since they are
    1.43 -   quantifiers. *)
    1.44 -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    1.45 -    formula_has_too_many_lambdas (T :: Ts) t
    1.46 -  | formula_has_too_many_lambdas Ts t =
    1.47 -    if is_formula_type (fastype_of1 (Ts, t)) then
    1.48 -      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    1.49 -    else
    1.50 -      term_has_too_many_lambdas max_lambda_nesting t
    1.51 -
    1.52 -(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
    1.53 -   was 11. *)
    1.54 -val max_apply_depth = 15
    1.55 -
    1.56 -fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
    1.57 -  | apply_depth (Abs (_, _, t)) = apply_depth t
    1.58 -  | apply_depth _ = 0
    1.59 -
    1.60 -fun is_formula_too_complex t =
    1.61 -  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
    1.62 -  formula_has_too_many_lambdas [] t
    1.63 -
    1.64 -fun is_strange_thm th =
    1.65 -  case head_of (concl_of th) of
    1.66 -      Const (a, _) => (a <> @{const_name Trueprop} andalso
    1.67 -                       a <> @{const_name "=="})
    1.68 -    | _ => false;
    1.69 -
    1.70 -fun is_theorem_bad_for_atps thm =
    1.71 -  let val t = prop_of thm in
    1.72 -    is_formula_too_complex t orelse exists_type type_has_topsort t orelse
    1.73 -    is_strange_thm thm
    1.74 -  end
    1.75 -
    1.76 -(* FIXME: put other record thms here, or declare as "no_atp" *)
    1.77 -(* FIXME: move to "Sledgehammer_Fact_Filter" *)
    1.78 -val multi_base_blacklist =
    1.79 -  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
    1.80 -   "split_asm", "cases", "ext_cases"];
    1.81 -
    1.82  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    1.83  fun skolemize_theorem thy th =
    1.84 -  if member (op =) multi_base_blacklist
    1.85 -            (Long_Name.base_name (Thm.get_name_hint th)) orelse
    1.86 -     is_theorem_bad_for_atps th then
    1.87 -    []
    1.88 -  else
    1.89 -    let
    1.90 -      val ctxt0 = Variable.global_thm_context th
    1.91 -      val (nnfth, ctxt) = to_nnf th ctxt0
    1.92 -      val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
    1.93 -      val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
    1.94 -    in
    1.95 -      cnfs |> map introduce_combinators
    1.96 -           |> Variable.export ctxt ctxt0
    1.97 -           |> Meson.finish_cnf
    1.98 -           |> map Thm.close_derivation
    1.99 -    end
   1.100 -    handle THM _ => []
   1.101 +  let
   1.102 +    val ctxt0 = Variable.global_thm_context th
   1.103 +    val (nnfth, ctxt) = to_nnf th ctxt0
   1.104 +    val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
   1.105 +    val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   1.106 +  in
   1.107 +    cnfs |> map introduce_combinators
   1.108 +         |> Variable.export ctxt ctxt0
   1.109 +         |> Meson.finish_cnf
   1.110 +         |> map Thm.close_derivation
   1.111 +  end
   1.112 +  handle THM _ => []
   1.113  
   1.114  (* Convert Isabelle theorems into axiom clauses. *)
   1.115  (* FIXME: is transfer necessary? *)

     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 29 09:26:56 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jun 29 10:25:53 2010 +0200
     2.3 @@ -779,11 +779,14 @@
     2.4               raise METIS ("FOL_SOLVE", ""))
     2.5    end;
     2.6  
     2.7 +val type_has_top_sort =
     2.8 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
     2.9 +
    2.10  fun generic_metis_tac mode ctxt ths i st0 =
    2.11    let val _ = trace_msg (fn () =>
    2.12          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    2.13    in
    2.14 -    if exists_type type_has_topsort (prop_of st0) then
    2.15 +    if exists_type type_has_top_sort (prop_of st0) then
    2.16        (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
    2.17      else
    2.18        (Meson.MESON (maps neg_clausify)

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 29 09:26:56 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 29 10:25:53 2010 +0200
     3.3 @@ -393,8 +393,60 @@
     3.4  fun make_unique xs =
     3.5    Termtab.fold (cons o snd) (make_clause_table xs) []
     3.6  
     3.7 +(* FIXME: put other record thms here, or declare as "no_atp" *)
     3.8 +val multi_base_blacklist =
     3.9 +  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
    3.10 +   "split_asm", "cases", "ext_cases"]
    3.11 +
    3.12 +val max_lambda_nesting = 3
    3.13 +
    3.14 +fun term_has_too_many_lambdas max (t1 $ t2) =
    3.15 +    exists (term_has_too_many_lambdas max) [t1, t2]
    3.16 +  | term_has_too_many_lambdas max (Abs (_, _, t)) =
    3.17 +    max = 0 orelse term_has_too_many_lambdas (max - 1) t
    3.18 +  | term_has_too_many_lambdas _ _ = false
    3.19 +
    3.20 +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    3.21 +
    3.22 +(* Don't count nested lambdas at the level of formulas, since they are
    3.23 +   quantifiers. *)
    3.24 +fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
    3.25 +    formula_has_too_many_lambdas (T :: Ts) t
    3.26 +  | formula_has_too_many_lambdas Ts t =
    3.27 +    if is_formula_type (fastype_of1 (Ts, t)) then
    3.28 +      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
    3.29 +    else
    3.30 +      term_has_too_many_lambdas max_lambda_nesting t
    3.31 +
    3.32 +(* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
    3.33 +   was 11. *)
    3.34 +val max_apply_depth = 15
    3.35 +
    3.36 +fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
    3.37 +  | apply_depth (Abs (_, _, t)) = apply_depth t
    3.38 +  | apply_depth _ = 0
    3.39 +
    3.40 +fun is_formula_too_complex t =
    3.41 +  apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
    3.42 +  formula_has_too_many_lambdas [] t
    3.43 +
    3.44  val exists_sledgehammer_const =
    3.45 -  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
    3.46 +  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
    3.47 +
    3.48 +fun is_strange_thm th =
    3.49 +  case head_of (concl_of th) of
    3.50 +      Const (a, _) => (a <> @{const_name Trueprop} andalso
    3.51 +                       a <> @{const_name "=="})
    3.52 +    | _ => false
    3.53 +
    3.54 +val type_has_top_sort =
    3.55 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
    3.56 +
    3.57 +fun is_theorem_bad_for_atps thm =
    3.58 +  let val t = prop_of thm in
    3.59 +    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
    3.60 +    exists_sledgehammer_const t orelse is_strange_thm thm
    3.61 +  end
    3.62  
    3.63  fun all_name_thms_pairs ctxt chained_ths =
    3.64    let
    3.65 @@ -407,8 +459,7 @@
    3.66        (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
    3.67          if Facts.is_concealed facts name orelse
    3.68             (respect_no_atp andalso is_package_def name) orelse
    3.69 -           member (op =) Clausifier.multi_base_blacklist
    3.70 -                  (Long_Name.base_name name) then
    3.71 +           member (op =) multi_base_blacklist (Long_Name.base_name name) then
    3.72            I
    3.73          else
    3.74            let
    3.75 @@ -419,8 +470,7 @@
    3.76  
    3.77              val name1 = Facts.extern facts name;
    3.78              val name2 = Name_Space.extern full_space name;
    3.79 -            val ths = filter_out (Clausifier.is_theorem_bad_for_atps orf
    3.80 -                                  exists_sledgehammer_const) ths0
    3.81 +            val ths = filter_out is_theorem_bad_for_atps ths0
    3.82            in
    3.83              case find_first check_thms [name1, name2, name] of
    3.84                NONE => I