# HG changeset patch
# User blanchet
# Date 1282458369 -7200
# Node ID 3387432c18af5ab2a53e98d395aff16c385053c2
# Parent  baf9f06601e4d30766b862094a03cd5ad9523322
more work on finite axiom detection

diff -r baf9f06601e4 -r 3387432c18af src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Aug 22 08:12:00 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Sun Aug 22 08:26:09 2010 +0200
@@ -443,15 +443,13 @@
 
 (* Unwanted equalities are those between a (bound or schematic) variable that
    does not properly occur in the second operand. *)
-fun too_general_eqterms (Var z) t =
-    not (exists_subterm (fn Var z' => z = z' | _ => false) t)
-  | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j))
-  | too_general_eqterms _ _ = false
-
 val is_exhaustive_finite =
   let
-    fun do_equals t1 t2 =
-      too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
+    fun is_bad_equal (Var z) t =
+        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
+      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
+      | is_bad_equal _ _ = false
+    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
     fun do_formula pos t =
       case (pos, t) of
         (_, @{const Trueprop} $ t1) => do_formula pos t1
@@ -462,16 +460,16 @@
       | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
         do_formula pos t'
       | (_, @{const "==>"} $ t1 $ t2) =>
-        do_formula (not pos) t1 andalso do_formula pos t2
+        do_formula (not pos) t1 andalso
+        (t2 = @{prop False} orelse do_formula pos t2)
       | (_, @{const "op -->"} $ t1 $ t2) =>
-        do_formula (not pos) t1 andalso do_formula pos t2
+        do_formula (not pos) t1 andalso
+        (t2 = @{const False} orelse do_formula pos t2)
       | (_, @{const Not} $ t1) => do_formula (not pos) t1
       | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
       | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
       | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
       | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
-      | (_, @{const False}) => true
-      | (_, @{const True}) => true
       | _ => false
   in do_formula true end