1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:08:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:39:23 2010 +0200
     1.3 @@ -239,14 +239,14 @@
     1.4  fun generic_tptp_prover
     1.5          (name, {home_var, executable, arguments, proof_delims, known_failures,
     1.6                  max_axiom_clauses, prefers_theory_relevant})
     1.7 -        (params as {debug, overlord, respect_no_atp, relevance_threshold,
     1.8 -                    relevance_convergence, theory_relevant, defs_relevant,
     1.9 -                    isar_proof, ...})
    1.10 +        (params as {debug, overlord, full_types, respect_no_atp,
    1.11 +                    relevance_threshold, relevance_convergence, theory_relevant,
    1.12 +                    defs_relevant, isar_proof, ...})
    1.13          minimize_command timeout =
    1.14    generic_prover overlord
    1.15 -      (get_relevant_facts respect_no_atp relevance_threshold
    1.16 -                          relevance_convergence defs_relevant max_axiom_clauses
    1.17 -                          (the_default prefers_theory_relevant theory_relevant))
    1.18 +      (relevant_facts full_types respect_no_atp relevance_threshold
    1.19 +                      relevance_convergence defs_relevant max_axiom_clauses
    1.20 +                      (the_default prefers_theory_relevant theory_relevant))
    1.21        (prepare_clauses false)
    1.22        (write_tptp_file (debug andalso overlord)) home_var
    1.23        executable (arguments timeout) proof_delims known_failures name params
    1.24 @@ -314,13 +314,13 @@
    1.25  fun generic_dfg_prover
    1.26          (name, {home_var, executable, arguments, proof_delims, known_failures,
    1.27                  max_axiom_clauses, prefers_theory_relevant})
    1.28 -        (params as {overlord, respect_no_atp, relevance_threshold,
    1.29 +        (params as {overlord, full_types, respect_no_atp, relevance_threshold,
    1.30                      relevance_convergence, theory_relevant, defs_relevant, ...})
    1.31          minimize_command timeout =
    1.32    generic_prover overlord
    1.33 -      (get_relevant_facts respect_no_atp relevance_threshold
    1.34 -                          relevance_convergence defs_relevant max_axiom_clauses
    1.35 -                          (the_default prefers_theory_relevant theory_relevant))
    1.36 +      (relevant_facts full_types respect_no_atp relevance_threshold
    1.37 +                      relevance_convergence defs_relevant max_axiom_clauses
    1.38 +                      (the_default prefers_theory_relevant theory_relevant))
    1.39        (prepare_clauses true) write_dfg_file home_var executable
    1.40        (arguments timeout) proof_delims known_failures name params
    1.41        minimize_command

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Jun 05 16:08:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Jun 05 16:39:23 2010 +0200
     2.3 @@ -21,8 +21,8 @@
     2.4    val tvar_classes_of_terms : term list -> string list
     2.5    val tfree_classes_of_terms : term list -> string list
     2.6    val type_consts_of_terms : theory -> term list -> string list
     2.7 -  val get_relevant_facts :
     2.8 -    bool -> real -> real -> bool -> int -> bool -> relevance_override
     2.9 +  val relevant_facts :
    2.10 +    bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
    2.11      -> Proof.context * (thm list * 'a) -> thm list
    2.12      -> (thm * (string * int)) list
    2.13    val prepare_clauses :
    2.14 @@ -255,13 +255,17 @@
    2.15        end
    2.16    end;
    2.17  
    2.18 +fun cnf_for_facts ctxt =
    2.19 +  let val thy = ProofContext.theory_of ctxt in
    2.20 +    maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
    2.21 +  end
    2.22 +
    2.23  fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
    2.24                       (relevance_override as {add, del, ...}) ctab =
    2.25    let
    2.26      val thy = ProofContext.theory_of ctxt
    2.27 -    val cnf_for_facts = maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
    2.28 -    val add_thms = cnf_for_facts add
    2.29 -    val del_thms = cnf_for_facts del
    2.30 +    val add_thms = cnf_for_facts ctxt add
    2.31 +    val del_thms = cnf_for_facts ctxt del
    2.32      fun iter threshold rel_consts =
    2.33        let
    2.34          fun relevant ([], _) [] = []  (* Nothing added this iteration *)
    2.35 @@ -372,7 +376,7 @@
    2.36  
    2.37            val name1 = Facts.extern facts name;
    2.38            val name2 = Name_Space.extern full_space name;
    2.39 -          val ths = filter_out bad_for_atp ths0;
    2.40 +          val ths = filter_out is_bad_for_atp ths0;
    2.41          in
    2.42            if Facts.is_concealed facts name orelse
    2.43               (respect_no_atp andalso is_package_def name) then
    2.44 @@ -472,7 +476,8 @@
    2.45  fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
    2.46    | restrict_to_logic thy false cls = cls;
    2.47  
    2.48 -(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
    2.49 +(**** Predicates to detect unwanted clauses (prolific or likely to cause
    2.50 +      unsoundness) ****)
    2.51  
    2.52  (** Too general means, positive equality literal with a variable X as one operand,
    2.53    when X does not occur properly in the other operand. This rules out clearly
    2.54 @@ -501,31 +506,41 @@
    2.55  fun has_typed_var tycons = exists_subterm
    2.56    (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
    2.57  
    2.58 -(*Clauses are forbidden to contain variables of these types. The typical reason is that
    2.59 -  they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
    2.60 -  The resulting clause will have no type constraint, yielding false proofs. Even "bool"
    2.61 -  leads to many unsound proofs, though (obviously) only for higher-order problems.*)
    2.62 -val unwanted_types = [@{type_name unit}, @{type_name bool}];
    2.63 +(* Clauses are forbidden to contain variables of these types. The typical reason
    2.64 +   is that they lead to unsoundness. Note that "unit" satisfies numerous
    2.65 +   equations like "?x = ()". The resulting clause will have no type constraint,
    2.66 +   yielding false proofs. Even "bool" leads to many unsound proofs, though only
    2.67 +   for higher-order problems. *)
    2.68 +val dangerous_types = [@{type_name unit}, @{type_name bool}];
    2.69  
    2.70 -fun unwanted t =
    2.71 -  t = @{prop True} orelse has_typed_var unwanted_types t orelse
    2.72 -  forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
    2.73 +(* Clauses containing variables of type "unit" or "bool" or of the form
    2.74 +   "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
    2.75 +   omitted. *)
    2.76 +fun is_dangerous_term _ @{prop True} = true
    2.77 +  | is_dangerous_term full_types t =
    2.78 +    not full_types andalso 
    2.79 +    (has_typed_var dangerous_types t orelse
    2.80 +     forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
    2.81  
    2.82 -(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
    2.83 -  likely to lead to unsound proofs.*)
    2.84 -fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
    2.85 +fun is_dangerous_theorem full_types add_thms thm =
    2.86 +  not (member Thm.eq_thm add_thms thm) andalso
    2.87 +  is_dangerous_term full_types (prop_of thm)
    2.88 +
    2.89 +fun remove_dangerous_clauses full_types add_thms =
    2.90 +  filter_out (is_dangerous_theorem full_types add_thms o fst)
    2.91  
    2.92  fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
    2.93  
    2.94 -fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
    2.95 -                       defs_relevant max_new theory_relevant
    2.96 -                       (relevance_override as {add, del, only})
    2.97 -                       (ctxt, (chained_ths, _)) goal_cls =
    2.98 +fun relevant_facts full_types respect_no_atp relevance_threshold
    2.99 +                   relevance_convergence defs_relevant max_new theory_relevant
   2.100 +                   (relevance_override as {add, del, only})
   2.101 +                   (ctxt, (chained_ths, _)) goal_cls =
   2.102    if (only andalso null add) orelse relevance_threshold > 1.0 then
   2.103      []
   2.104    else
   2.105      let
   2.106        val thy = ProofContext.theory_of ctxt
   2.107 +      val add_thms = cnf_for_facts ctxt add
   2.108        val has_override = not (null add) orelse not (null del)
   2.109        val is_FO = is_first_order thy goal_cls
   2.110        val axioms =
   2.111 @@ -535,7 +550,7 @@
   2.112          |> cnf_rules_pairs thy
   2.113          |> not has_override ? make_unique
   2.114          |> restrict_to_logic thy is_FO
   2.115 -        |> remove_unwanted_clauses
   2.116 +        |> not only ? remove_dangerous_clauses full_types add_thms
   2.117      in
   2.118        relevance_filter ctxt relevance_threshold relevance_convergence
   2.119                         defs_relevant max_new theory_relevant relevance_override

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 05 16:08:35 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 05 16:39:23 2010 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    val skolem_infix: string
     3.5    val cnf_axiom: theory -> thm -> thm list
     3.6    val multi_base_blacklist: string list
     3.7 -  val bad_for_atp: thm -> bool
     3.8 +  val is_bad_for_atp: thm -> bool
     3.9    val type_has_topsort: typ -> bool
    3.10    val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
    3.11    val suppress_endtheory: bool Unsynchronized.ref
    3.12 @@ -340,10 +340,9 @@
    3.13                         a <> @{const_name "=="})
    3.14      | _ => false;
    3.15  
    3.16 -fun bad_for_atp th =
    3.17 -  too_complex (prop_of th)
    3.18 -  orelse exists_type type_has_topsort (prop_of th)
    3.19 -  orelse is_strange_thm th;
    3.20 +fun is_bad_for_atp th =
    3.21 +  too_complex (prop_of th) orelse
    3.22 +  exists_type type_has_topsort (prop_of th) orelse is_strange_thm th
    3.23  
    3.24  (* FIXME: put other record thms here, or declare as "no_atp" *)
    3.25  val multi_base_blacklist =
    3.26 @@ -357,7 +356,7 @@
    3.27  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    3.28  fun skolem_thm (s, th) =
    3.29    if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
    3.30 -     bad_for_atp th then
    3.31 +     is_bad_for_atp th then
    3.32      []
    3.33    else
    3.34      let
    3.35 @@ -443,7 +442,7 @@
    3.36      val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
    3.37        if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
    3.38        else fold_index (fn (i, th) =>
    3.39 -        if bad_for_atp th orelse is_some (lookup_cache thy th) then I
    3.40 +        if is_bad_for_atp th orelse is_some (lookup_cache thy th) then I
    3.41          else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
    3.42    in
    3.43      if null new_facts then NONE