# HG changeset patch
# User boehmes
# Date 1290601872 -3600
# Node ID dcb27631cb45be854fb76197a41481567ec96172
# Parent  1e761b5cd09713024004dfefca507aab7302b487
instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)

diff -r 1e761b5cd097 -r dcb27631cb45 src/HOL/Tools/SMT/smt_normalize.ML
--- 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