# HG changeset patch
# User blanchet
# Date 1275748763 -7200
# Node ID 635425a442e80295666976ada1ffb2693f780892
# Parent  cdba266f038384e357be3ee7cdb35b05c2f88d60
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound

diff -r cdba266f0383 -r 635425a442e8 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:08:35 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Sat Jun 05 16:39:23 2010 +0200
@@ -239,14 +239,14 @@
 fun generic_tptp_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
-        (params as {debug, overlord, respect_no_atp, relevance_threshold,
-                    relevance_convergence, theory_relevant, defs_relevant,
-                    isar_proof, ...})
+        (params as {debug, overlord, full_types, respect_no_atp,
+                    relevance_threshold, relevance_convergence, theory_relevant,
+                    defs_relevant, isar_proof, ...})
         minimize_command timeout =
   generic_prover overlord
-      (get_relevant_facts respect_no_atp relevance_threshold
-                          relevance_convergence defs_relevant max_axiom_clauses
-                          (the_default prefers_theory_relevant theory_relevant))
+      (relevant_facts full_types respect_no_atp relevance_threshold
+                      relevance_convergence defs_relevant max_axiom_clauses
+                      (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses false)
       (write_tptp_file (debug andalso overlord)) home_var
       executable (arguments timeout) proof_delims known_failures name params
@@ -314,13 +314,13 @@
 fun generic_dfg_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
                 max_axiom_clauses, prefers_theory_relevant})
-        (params as {overlord, respect_no_atp, relevance_threshold,
+        (params as {overlord, full_types, respect_no_atp, relevance_threshold,
                     relevance_convergence, theory_relevant, defs_relevant, ...})
         minimize_command timeout =
   generic_prover overlord
-      (get_relevant_facts respect_no_atp relevance_threshold
-                          relevance_convergence defs_relevant max_axiom_clauses
-                          (the_default prefers_theory_relevant theory_relevant))
+      (relevant_facts full_types respect_no_atp relevance_threshold
+                      relevance_convergence defs_relevant max_axiom_clauses
+                      (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses true) write_dfg_file home_var executable
       (arguments timeout) proof_delims known_failures name params
       minimize_command
diff -r cdba266f0383 -r 635425a442e8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Jun 05 16:08:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sat Jun 05 16:39:23 2010 +0200
@@ -21,8 +21,8 @@
   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
-  val get_relevant_facts :
-    bool -> real -> real -> bool -> int -> bool -> relevance_override
+  val relevant_facts :
+    bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> thm list
     -> (thm * (string * int)) list
   val prepare_clauses :
@@ -255,13 +255,17 @@
       end
   end;
 
+fun cnf_for_facts ctxt =
+  let val thy = ProofContext.theory_of ctxt in
+    maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
+  end
+
 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
                      (relevance_override as {add, del, ...}) ctab =
   let
     val thy = ProofContext.theory_of ctxt
-    val cnf_for_facts = maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt)
-    val add_thms = cnf_for_facts add
-    val del_thms = cnf_for_facts del
+    val add_thms = cnf_for_facts ctxt add
+    val del_thms = cnf_for_facts ctxt del
     fun iter threshold rel_consts =
       let
         fun relevant ([], _) [] = []  (* Nothing added this iteration *)
@@ -372,7 +376,7 @@
 
           val name1 = Facts.extern facts name;
           val name2 = Name_Space.extern full_space name;
-          val ths = filter_out bad_for_atp ths0;
+          val ths = filter_out is_bad_for_atp ths0;
         in
           if Facts.is_concealed facts name orelse
              (respect_no_atp andalso is_package_def name) then
@@ -472,7 +476,8 @@
 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   | restrict_to_logic thy false cls = cls;
 
-(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
+(**** Predicates to detect unwanted clauses (prolific or likely to cause
+      unsoundness) ****)
 
 (** Too general means, positive equality literal with a variable X as one operand,
   when X does not occur properly in the other operand. This rules out clearly
@@ -501,31 +506,41 @@
 fun has_typed_var tycons = exists_subterm
   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
 
-(*Clauses are forbidden to contain variables of these types. The typical reason is that
-  they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
-  The resulting clause will have no type constraint, yielding false proofs. Even "bool"
-  leads to many unsound proofs, though (obviously) only for higher-order problems.*)
-val unwanted_types = [@{type_name unit}, @{type_name bool}];
+(* Clauses are forbidden to contain variables of these types. The typical reason
+   is that they lead to unsoundness. Note that "unit" satisfies numerous
+   equations like "?x = ()". The resulting clause will have no type constraint,
+   yielding false proofs. Even "bool" leads to many unsound proofs, though only
+   for higher-order problems. *)
+val dangerous_types = [@{type_name unit}, @{type_name bool}];
 
-fun unwanted t =
-  t = @{prop True} orelse has_typed_var unwanted_types t orelse
-  forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
+(* Clauses containing variables of type "unit" or "bool" or of the form
+   "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
+   omitted. *)
+fun is_dangerous_term _ @{prop True} = true
+  | is_dangerous_term full_types t =
+    not full_types andalso 
+    (has_typed_var dangerous_types t orelse
+     forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
 
-(*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
-  likely to lead to unsound proofs.*)
-fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
+fun is_dangerous_theorem full_types add_thms thm =
+  not (member Thm.eq_thm add_thms thm) andalso
+  is_dangerous_term full_types (prop_of thm)
+
+fun remove_dangerous_clauses full_types add_thms =
+  filter_out (is_dangerous_theorem full_types add_thms o fst)
 
 fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
 
-fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
-                       defs_relevant max_new theory_relevant
-                       (relevance_override as {add, del, only})
-                       (ctxt, (chained_ths, _)) goal_cls =
+fun relevant_facts full_types respect_no_atp relevance_threshold
+                   relevance_convergence defs_relevant max_new theory_relevant
+                   (relevance_override as {add, del, only})
+                   (ctxt, (chained_ths, _)) goal_cls =
   if (only andalso null add) orelse relevance_threshold > 1.0 then
     []
   else
     let
       val thy = ProofContext.theory_of ctxt
+      val add_thms = cnf_for_facts ctxt add
       val has_override = not (null add) orelse not (null del)
       val is_FO = is_first_order thy goal_cls
       val axioms =
@@ -535,7 +550,7 @@
         |> cnf_rules_pairs thy
         |> not has_override ? make_unique
         |> restrict_to_logic thy is_FO
-        |> remove_unwanted_clauses
+        |> not only ? remove_dangerous_clauses full_types add_thms
     in
       relevance_filter ctxt relevance_threshold relevance_convergence
                        defs_relevant max_new theory_relevant relevance_override
diff -r cdba266f0383 -r 635425a442e8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 05 16:08:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Jun 05 16:39:23 2010 +0200
@@ -14,7 +14,7 @@
   val skolem_infix: string
   val cnf_axiom: theory -> thm -> thm list
   val multi_base_blacklist: string list
-  val bad_for_atp: thm -> bool
+  val is_bad_for_atp: thm -> bool
   val type_has_topsort: typ -> bool
   val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
   val suppress_endtheory: bool Unsynchronized.ref
@@ -340,10 +340,9 @@
                        a <> @{const_name "=="})
     | _ => false;
 
-fun bad_for_atp th =
-  too_complex (prop_of th)
-  orelse exists_type type_has_topsort (prop_of th)
-  orelse is_strange_thm th;
+fun is_bad_for_atp th =
+  too_complex (prop_of th) orelse
+  exists_type type_has_topsort (prop_of th) orelse is_strange_thm th
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
@@ -357,7 +356,7 @@
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm (s, th) =
   if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse
-     bad_for_atp th then
+     is_bad_for_atp th then
     []
   else
     let
@@ -443,7 +442,7 @@
     val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
       if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
       else fold_index (fn (i, th) =>
-        if bad_for_atp th orelse is_some (lookup_cache thy th) then I
+        if is_bad_for_atp th orelse is_some (lookup_cache thy th) then I
         else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
   in
     if null new_facts then NONE