# HG changeset patch
# User blanchet
# Date 1310657370 -7200
# Node ID fba9754b827e5050fefb25fe0e7b5ae686767b26
# Parent  e07a2c4cbad8909ce45c5d0827433a9f4d9833f1
allow lambda-lifting without triggers

diff -r e07a2c4cbad8 -r fba9754b827e src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 16:50:05 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 17:29:30 2011 +0200
@@ -38,7 +38,7 @@
   (*translation*)
   val add_config: SMT_Utils.class * (Proof.context -> config) ->
     Context.generic -> Context.generic 
-  val lift_lambdas: Proof.context -> term list ->
+  val lift_lambdas: Proof.context -> bool -> term list ->
     Proof.context * (term list * term list)
   val translate: Proof.context -> string list -> (int * thm) list ->
     string * recon
@@ -246,22 +246,25 @@
 (** lambda-lifting **)
 
 local
-  fun mk_def Ts T lhs rhs =
+  fun mk_def triggers Ts T lhs rhs =
     let
       val eq = HOLogic.eq_const T $ lhs $ rhs
-      val trigger =
+      fun trigger () =
         [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
         |> map (HOLogic.mk_list @{typ SMT.pattern})
         |> HOLogic.mk_list @{typ "SMT.pattern list"}
       fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
-    in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end
+    in
+      fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq
+        else eq)
+    end
 
   fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts
 
   fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
     | dest_abs Ts t = (Ts, t)
 
-  fun replace_lambda Us Ts t (cx as (defs, ctxt)) =
+  fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
     let
       val t1 = mk_abs Us t
       val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
@@ -284,31 +287,32 @@
             val (is, UTs) = split_list (map_index I (Us @ Ts'))
             val f = Free (n, rev UTs ---> T)
             val lhs = Term.list_comb (f, map Bound (rev is))
-            val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
+            val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
           in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
     end
 
-  fun traverse Ts t =
+  fun traverse triggers Ts t =
     (case t of
       (q as Const (@{const_name All}, _)) $ Abs a =>
-        abs_traverse Ts a #>> (fn a' => q $ Abs a')
+        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
     | (q as Const (@{const_name Ex}, _)) $ Abs a =>
-        abs_traverse Ts a #>> (fn a' => q $ Abs a')
+        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
     | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
-        traverse Ts u ##>> abs_traverse Ts a #>>
+        traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
         (fn (u', a') => l $ u' $ Abs a')
     | Abs _ =>
         let val (Us, u) = dest_abs [] t
-        in traverse (Us @ Ts) u #-> replace_lambda Us Ts end
-    | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $)
+        in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
+    | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
     | _ => pair t)
 
-  and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t'))
+  and abs_traverse triggers Ts (n, T, t) =
+    traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
 in
 
-fun lift_lambdas ctxt ts =
+fun lift_lambdas ctxt triggers ts =
   (Termtab.empty, ctxt)
-  |> fold_map (traverse []) ts
+  |> fold_map (traverse triggers []) ts
   |> (fn (us, (defs, ctxt')) =>
        (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
 
@@ -614,7 +618,7 @@
     val (ctxt2, ts3) =
       ts2
       |> eta_expand ctxt1 is_fol funcs
-      |> lift_lambdas ctxt1
+      |> lift_lambdas ctxt1 true
       ||> (op @)
       |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)