# HG changeset patch
# User blanchet
# Date 1341956163 -7200
# Node ID 141ab3c13ac84ed08623f4cbf5be1a953a09481a
# Parent  82f88650874bd0001184e20208f3190b8f38c161
better tautology elimination

diff -r 82f88650874b -r 141ab3c13ac8 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Jul 10 23:36:03 2012 +0200
@@ -58,15 +58,6 @@
 
 fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
 
-fun facts_of thy =
-  let val ctxt = Proof_Context.init_global thy in
-    Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
-        (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
-    |> filter (curry (op =) @{typ bool} o fastype_of
-               o Object_Logic.atomize_term thy o prop_of o snd)
-    |> rev
-  end
-
 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    fixes that seem to be missing over there; or maybe the two code portions are
    not doing the same? *)
@@ -139,6 +130,26 @@
       end
   in [] |> add_patterns t |> sort string_ord end
 
+val known_tautologies =
+  [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def},
+   @{thm Bex_def}, @{thm If_def}]
+
+fun is_likely_tautology th =
+  (member Thm.eq_thm_prop known_tautologies th orelse
+   th |> prop_of |> interesting_terms_types_and_classes 0 ~1 |> null) andalso
+  not (Thm.eq_thm_prop (@{thm ext}, th))
+
+fun is_too_meta thy th =
+  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
+
+fun facts_of thy =
+  let val ctxt = Proof_Context.init_global thy in
+    Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] []
+        (Sledgehammer_Filter.clasimpset_rule_table_of ctxt)
+    |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
+    |> rev
+  end
+
 fun theory_ord p =
   if Theory.eq_thy p then EQUAL
   else if Theory.subthy p then LESS
@@ -259,15 +270,6 @@
 
 val dependencies_of = theorems_mentioned_in_proof_term o SOME
 
-val known_tautologies =
-  [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def},
-   @{thm Bex_def}, @{thm If_def}]
-
-fun is_likely_tautology th =
-  (member Thm.eq_thm_prop known_tautologies th orelse
-   th |> prop_of |> interesting_terms_types_and_classes 0 ~1 |> null) andalso
-  not (Thm.eq_thm_prop (@{thm ext}, th))
-
 fun generate_mash_dependency_file_for_theory thy include_thy file_name =
   let
     val path = file_name |> Path.explode
@@ -275,8 +277,7 @@
     val ths =
       facts_of thy |> not include_thy ? filter_out (has_thy thy o snd)
                    |> map snd
-    val all_names =
-      ths |> filter_out is_likely_tautology |> map Thm.get_name_hint
+    val all_names = ths |> map Thm.get_name_hint
     fun do_thm th =
       let
         val name = Thm.get_name_hint th
@@ -295,8 +296,7 @@
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
     val ths = facts |> map snd
-    val all_names =
-      ths |> filter_out is_likely_tautology |> map Thm.get_name_hint
+    val all_names = ths |> map Thm.get_name_hint
     fun do_fact ((_, (_, status)), th) prevs =
       let
         val name = Thm.get_name_hint th
@@ -415,8 +415,7 @@
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
     val ths = facts |> map snd
-    val all_names =
-      ths |> filter_out is_likely_tautology |> map Thm.get_name_hint
+    val all_names = ths |> map Thm.get_name_hint
     val infers =
       facts |> map (fn (_, th) =>
                        (fact_name_of (Thm.get_name_hint th),