# 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