src/HOL/Tools/SMT/smt_translate.ML

 
 
 (** eta-expand quantifiers, let expressions and built-ins *)
 
 local
-  fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t $ Bound 0)
-
-  fun exp T = eta (Term.domain_type (Term.domain_type T))
+  fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0))
+
+  fun exp f T = eta f (Term.domain_type (Term.domain_type T))
 
   fun exp2 T q =
     let val U = Term.domain_type T
-    in Abs (Name.uu, U, q $ eta (Term.domain_type U) (Bound 0)) end
+    in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
 
   fun exp2' T l =
     let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
-    in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
+    in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end
 
   fun expf k i T t =
     let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
     in
       Term.incr_boundvars (length Ts) t
       |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
       |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
     end
 in
 
-fun eta_expand ctxt funcs =
+fun eta_expand ctxt is_fol funcs =
   let
     fun exp_func t T ts =
       (case Termtab.lookup funcs t of
         SOME k =>
           Term.list_comb (t, ts)
           |> k <> length ts ? expf k (length ts) T
       | NONE => Term.list_comb (t, ts))
 
     fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
-      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
+      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t
       | expand (q as Const (@{const_name All}, T)) = exp2 T q
       | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
-      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
+      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
       | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
       | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
-          l $ expand t $ abs_expand a
+          if is_fol then expand (Term.betapply (Abs a, t))
+          else l $ expand t $ abs_expand a
       | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
-          l $ expand t $ exp (Term.range_type T) u
+          if is_fol then expand (u $ t)
+          else l $ expand t $ exp expand (Term.range_type T) u
       | expand ((l as Const (@{const_name Let}, T)) $ t) =
-          exp2 T (l $ expand t)
-      | expand (l as Const (@{const_name Let}, T)) = exp2' T l
+          if is_fol then
+            let val U = Term.domain_type (Term.range_type T)
+            in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
+          else exp2 T (l $ expand t)
+      | expand (l as Const (@{const_name Let}, T)) =
+          if is_fol then 
+            let val U = Term.domain_type (Term.range_type T)
+            in
+              Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U,
+                Bound 0 $ Bound 1))
+            end
+          else exp2' T l
       | expand t =
           (case Term.strip_comb t of
             (u as Const (c as (_, T)), ts) =>
               (case SMT_Builtin.dest_builtin ctxt c ts of
                 SOME (_, k, us, mk) =>

     mk_meta_eq @{thm SMT.term_true_def},
     mk_meta_eq @{thm SMT.term_false_def},
     @{lemma "P = True == P" by (rule eq_reflection) simp},
     @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
 
-  fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
-        reduce_let (Term.betapply (u, t))
-    | reduce_let (t $ u) = reduce_let t $ reduce_let u
-    | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
-    | reduce_let t = t
-
   fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
 
   fun wrap_in_if t =
     @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
 

               (case SMT_Builtin.dest_builtin_pred ctxt c ts of
                 SOME (_, _, us, mk) => mk (map in_term us)
               | NONE => as_term (in_term t)))
       | _ => as_term (in_term t))
   in
-    map (reduce_let #> in_form) #>
+    map in_form #>
     cons (SMT_Utils.prop_of term_bool) #>
     pair (fol_rules, [term_bool], builtin)
   end
 
 end

       ((make_tr_context prefixes, ctxt), ts1)
       |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps)
 
     val (ctxt2, ts3) =
       ts2
-      |> eta_expand ctxt1 funcs
+      |> eta_expand ctxt1 is_fol funcs
       |> lift_lambdas ctxt1
       ||> intro_explicit_application
 
     val ((rewrite_rules, extra_thms, builtin), ts4) =
       (if is_fol then folify ctxt2 else pair ([], [], I)) ts3