# HG changeset patch
# User boehmes
# Date 1309108202 -7200
# Node ID 9bece8cbb5be20b9601fa729dd066db4c2e251a1
# Parent  df80747342cb69bad780cf184a2401baad40c1e7
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
maintain extra-logical information when introducing explicit application;
handle let-expressions properly

diff -r df80747342cb -r 9bece8cbb5be src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Jun 25 20:03:07 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Jun 26 19:10:02 2011 +0200
@@ -333,7 +333,14 @@
     | (_, ts) => fold min_arities ts)
 
   fun minimize types t i =
-    if i = 0 orelse Typtab.defined types (Term.type_of t) then 0 else i
+    let
+      fun find_min j [] _ = j
+        | find_min j (U :: Us) T =
+            if Typtab.defined types T then j
+            else find_min (j + 1) Us (U --> T)
+
+      val (Ts, T) = Term.strip_type (Term.type_of t)
+    in find_min 0 (take i (rev Ts)) T end
 
   fun app u (t, T) =
     (Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T)
@@ -354,11 +361,15 @@
       if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
       else apply (the (Termtab.lookup arities' t)) t T ts
 
+    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
+
     fun traverse Ts t =
       (case Term.strip_comb t of
-        (q as Const (@{const_name All}, _), [u as Abs _]) => q $ traverse Ts u
-      | (q as Const (@{const_name Ex}, _), [u as Abs _]) => q $ traverse Ts u
-      | (q as Const (@{const_name Ex}, _), [u1 as Abs _, u2]) =>
+        (q as Const (@{const_name All}, _), [Abs (x, T, u)]) =>
+          q $ Abs (x, T, in_trigger (T :: Ts) u)
+      | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) =>
+          q $ Abs (x, T, in_trigger (T :: Ts) u)
+      | (q as Const (@{const_name Let}, _), [u1 as Abs _, u2]) =>
           q $ traverse Ts u1 $ traverse Ts u2
       | (u as Const (c as (_, T)), ts) =>
           (case SMT_Builtin.dest_builtin ctxt c ts of
@@ -368,6 +379,20 @@
       | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
       | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
       | (u, ts) => traverses Ts u ts)
+    and in_trigger Ts ((c as @{const SMT.trigger}) $ p $ t) =
+          c $ in_pats Ts p $ in_weight Ts t
+      | in_trigger Ts t = in_weight Ts t
+    and in_pats Ts ps =
+      in_list @{typ "SMT.pattern list"}
+        (in_list @{typ SMT.pattern} (in_pat Ts)) ps
+    and in_pat Ts ((p as Const (@{const_name SMT.pat}, _)) $ t) =
+          p $ traverse Ts t
+      | in_pat Ts ((p as Const (@{const_name SMT.nopat}, _)) $ t) =
+          p $ traverse Ts t
+      | in_pat _ t = raise TERM ("bad pattern", [t])
+    and in_weight Ts ((c as @{const SMT.weight}) $ w $ t) =
+          c $ w $ traverse Ts t
+      | in_weight Ts t = traverse Ts t 
     and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
   in map (traverse []) ts end