instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 24 10:42:28 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 24 13:31:12 2010 +0100
@@ -35,6 +35,26 @@
+(* instantiate elimination rules *)
+
+local
+ val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
+
+ fun inst f ct thm =
+ let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
+ in Thm.instantiate ([], [(cv, ct)]) thm end
+in
+
+fun instantiate_elim thm =
+ (case Thm.concl_of thm of
+ @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
+ | Var _ => inst I cpfalse thm
+ | _ => thm)
+
+end
+
+
+
(* simplification of trivial distincts (distinct should have at least
three elements in the argument list) *)
@@ -520,6 +540,7 @@
else SOME (i, f ctxt' thm)
in
irules
+ |> map (apsnd instantiate_elim)
|> trivial_distinct ctxt
|> rewrite_bool_cases ctxt
|> normalize_numerals ctxt