# HG changeset patch
# User blanchet
# Date 1282306142 -7200
# Node ID 5266689abbc1d90e561a89728a113c3088c54324
# Parent  6220e5ab32f77572497aacdbb4c5dea123463949
transform elim theorems before filtering "bool" and "prop" variables out;
another consequence of the transition to FOF

diff -r 6220e5ab32f7 -r 5266689abbc1 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 20 13:39:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Aug 20 14:09:02 2010 +0200
@@ -7,6 +7,7 @@
 
 signature CLAUSIFIER =
 sig
+  val transform_elim_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val cnf_axiom: theory -> thm -> thm list
diff -r 6220e5ab32f7 -r 5266689abbc1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 13:39:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 20 14:09:02 2010 +0200
@@ -442,18 +442,18 @@
             (respect_no_atp andalso is_package_def name) orelse
             member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
             String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
-          forall (not o member Thm.eq_thm add_thms) ths0 then
+           forall (not o member Thm.eq_thm add_thms) ths0 then
           I
         else
           let
             fun check_thms a =
               (case try (ProofContext.get_thms ctxt) a of
                 NONE => false
-              | SOME ths1 => Thm.eq_thms (ths0, ths1));
-
+              | SOME ths1 => Thm.eq_thms (ths0, ths1))
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
-            val ths = filter_out is_theorem_bad_for_atps ths0
+            val ths = filter (fn th => not (is_theorem_bad_for_atps th) orelse
+                                       member Thm.eq_thm add_thms th) ths0
           in
             case find_first check_thms [name1, name2, name] of
               NONE => I
@@ -565,6 +565,7 @@
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
           (if only then [] else all_name_thms_pairs ctxt add_thms chained_ths)
       |> make_unique
+      |> map (apsnd Clausifier.transform_elim_theorem)
       |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse
                                not (is_dangerous_term full_types (prop_of th)))
   in
diff -r 6220e5ab32f7 -r 5266689abbc1 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 13:39:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 14:09:02 2010 +0200
@@ -79,17 +79,6 @@
                        |>> AAtom ||> union (op =) ts)
   in do_formula [] end
 
-(* Converts an elim-rule into an equivalent theorem that does not have the
-   predicate variable. Leaves other theorems unchanged. We simply instantiate
-   the conclusion variable to False. (Cf. "transform_elim_term" in
-   "ATP_Systems".) *)
-fun transform_elim_term t =
-  case Logic.strip_imp_concl t of
-    @{const Trueprop} $ Var (z, @{typ bool}) =>
-    subst_Vars [(z, @{const False})] t
-  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
-  | _ => t
-
 fun presimplify_term thy =
   Skip_Proof.make_thm thy
   #> Meson.presimplify
@@ -190,7 +179,6 @@
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
-              |> transform_elim_term
               |> atomize_term
     val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
               |> extensionalize_term