# HG changeset patch
# User boehmes
# Date 1292781269 -3600
# Node ID 679118e35378f95c5c66f3bb675e85339b4367c2
# Parent  a7de9d36f4f2bc7637098f503aeb736c7bf6f548
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
removed odd retyping during folify (instead, keep all terms well-typed)

diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/SMT.thy	Sun Dec 19 18:54:29 2010 +0100
@@ -113,12 +113,14 @@
 uninterpreted constants (those not built-in in the target solver)
 are treated as function symbols in the first-order sense.  Their
 occurrences as head symbols in atoms (i.e., as predicate symbols) are
-turned into terms by equating such atoms with @{term True}.
-Whenever the boolean type occurs in first-order terms, it is replaced
-by the following type.
+turned into terms by logically equating such atoms with @{term True}.
+For technical reasons, @{term True} and @{term False} occurring inside
+terms are replaced by the following constants.
 *}
 
-typedecl term_bool
+definition term_true where "term_true = True"
+definition term_false where "term_false = False"
+
 
 
 
@@ -374,9 +376,8 @@
 
 
 
-hide_type term_bool
 hide_type (open) pattern
-hide_const Pattern fun_app z3div z3mod
+hide_const Pattern fun_app term_true term_false z3div z3mod
 hide_const (open) trigger pat nopat weight
 
 
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -12,28 +12,33 @@
     Context.generic -> Context.generic
   val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
     Context.generic
-  val builtin_typ: Proof.context -> typ -> string option
-  val is_builtin_typ: Proof.context -> typ -> bool
+  val dest_builtin_typ: Proof.context -> typ -> string option
   val is_builtin_typ_ext: Proof.context -> typ -> bool
 
   (*built-in numbers*)
-  val builtin_num: Proof.context -> term -> (string * typ) option
+  val dest_builtin_num: Proof.context -> term -> (string * typ) option
   val is_builtin_num: Proof.context -> term -> bool
   val is_builtin_num_ext: Proof.context -> term -> bool
 
   (*built-in functions*)
   type 'a bfun = Proof.context -> typ -> term list -> 'a
+  type bfunr = string * int * term list * (term list -> term)
   val add_builtin_fun: SMT_Utils.class ->
-    (string * typ) * (((string * int) * typ) * term list * typ) option bfun ->
-    Context.generic -> Context.generic
+    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
   val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
     Context.generic
   val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
     Context.generic
   val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
   val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
-  val builtin_fun: Proof.context -> string * typ -> term list ->
-    (((string * int) * typ) * term list * typ) option
+  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
+  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
+    bfunr option
+  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
   val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
   val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
@@ -108,13 +113,11 @@
 fun lookup_builtin_typ ctxt =
   lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
 
-fun builtin_typ ctxt T =
+fun dest_builtin_typ ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => f T
   | _ => NONE) 
 
-fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
-
 fun is_builtin_typ_ext ctxt T =
   (case lookup_builtin_typ ctxt T of
     SOME (_, Int (f, _)) => is_some (f T)
@@ -124,7 +127,7 @@
 
 (* built-in numbers *)
 
-fun builtin_num ctxt t =
+fun dest_builtin_num ctxt t =
   (case try HOLogic.dest_number t of
     NONE => NONE
   | SOME (T, i) =>
@@ -132,7 +135,7 @@
         SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
       | _ => NONE))
 
-val is_builtin_num = is_some oo builtin_num
+val is_builtin_num = is_some oo dest_builtin_num
 
 fun is_builtin_num_ext ctxt t =
   (case try HOLogic.dest_number t of
@@ -144,10 +147,11 @@
 
 type 'a bfun = Proof.context -> typ -> term list -> 'a
 
+type bfunr = string * int * term list * (term list -> term)
+
 structure Builtin_Funcs = Generic_Data
 (
-  type T =
-    (bool bfun, (((string * int) * typ) * term list * typ) option bfun) btab
+  type T = (bool bfun, bfunr option bfun) btab
   val empty = Symtab.empty
   val extend = I
   val merge = merge_btab
@@ -158,9 +162,10 @@
 
 fun add_builtin_fun' cs (t, n) =
   let
-    val T = Term.fastype_of t
-    fun bfun _ U ts = SOME (((n, length (Term.binder_types T)), U), ts, T)
-  in add_builtin_fun cs (Term.dest_Const t, bfun) end
+    val c as (m, T) = Term.dest_Const t
+    fun app U ts = Term.list_comb (Const (m, U), ts)
+    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
+  in add_builtin_fun cs (c, bfun) end
 
 fun add_builtin_fun_ext ((n, T), f) =
   Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
@@ -175,12 +180,40 @@
 fun lookup_builtin_fun ctxt =
   lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
 
-fun builtin_fun ctxt (c as (_, T)) ts =
+fun dest_builtin_fun ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
     SOME (_, Int f) => f ctxt T ts
   | _ => NONE)
 
-fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
+fun dest_builtin_eq ctxt t u =
+  let
+    val aT = TFree (Name.aT, @{sort type})
+    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
+    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
+  in
+    dest_builtin_fun ctxt c []
+    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
+  end
+
+fun special_builtin_fun pred ctxt (c as (_, T)) ts =
+  if pred (Term.body_type T, Term.binder_types T) then
+    dest_builtin_fun ctxt c ts
+  else NONE
+
+fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
+
+fun dest_builtin_conn ctxt =
+  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
+
+fun dest_builtin ctxt c ts =
+  let val t =Term.list_comb (Const c, ts)
+  in
+    (case dest_builtin_num ctxt t of
+      SOME (n, _) => SOME (n, 0, [], K t)
+    | NONE => dest_builtin_fun ctxt c ts)
+  end
+
+fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
 
 fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -35,11 +35,15 @@
     | is_linear [t, u] = U.is_number t orelse U.is_number u
     | is_linear _ = false
 
-  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
+  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
+
+  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
     | times _ _ _  = NONE
 
+  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
+
   fun divide _ T (ts as [_, t]) =
-        if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE
+        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
     | divide _ _ _ = NONE
 in
 
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -120,12 +120,12 @@
   dtyps = dtyps,
   funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
 
-fun recon_of ctxt rules thms ithms revertT revert (_, _, typs, _, _, terms) =
+fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) =
   let
-    fun add_typ (T, (n, _)) = Symtab.update (n, revertT T)
+    fun add_typ (T, (n, _)) = Symtab.update (n, T)
     val typs' = Typtab.fold add_typ typs Symtab.empty
 
-    fun add_fun (t, (n, _)) = Symtab.update (n, revert t)
+    fun add_fun (t, (n, _)) = Symtab.update (n, t)
     val terms' = Termtab.fold add_fun terms Symtab.empty
 
     val assms = map (pair ~1) thms @ ithms
@@ -137,43 +137,11 @@
 
 (* preprocessing *)
 
-(** mark built-in constants as Var **)
-
-fun mark_builtins ctxt =
-  let
-    (*
-      Note: schematic terms cannot occur anymore in terms at this stage.
-    *)
-    fun mark t =
-      (case Term.strip_comb t of
-        (u as Const (@{const_name If}, _), ts) => marks u ts
-      | (u as @{const SMT.weight}, [t1, t2]) =>
-          mark t2 #>> (fn t2' => u $ t1 $ t2')
-      | (u as Const c, ts) =>
-          (case B.builtin_num ctxt t of
-            SOME (n, T) =>
-              let val v = ((n, 0), T)
-              in Vartab.update v #> pair (Var v) end
-          | NONE =>
-              (case B.builtin_fun ctxt c ts of
-                SOME ((ni, T), us, U) =>
-                  Vartab.update (ni, U) #> marks (Var (ni, T)) us
-              | NONE => marks u ts))
-      | (Abs (n, T, u), ts) => mark u #-> (fn u' => marks (Abs (n, T, u')) ts)
-      | (u, ts) => marks u ts)
- 
-    and marks t ts = fold_map mark ts #>> Term.list_comb o pair t
-
-  in (fn ts => swap (fold_map mark ts Vartab.empty)) end
-
-fun mark_builtins' ctxt t = hd (snd (mark_builtins ctxt [t]))
-
-
 (** FIXME **)
 
 local
   (*
-    mark constructors and selectors as Vars (forcing eta-expansion),
+    force eta-expansion for constructors and selectors,
     add missing datatype selectors via hypothetical definitions,
     also return necessary datatype and record theorems
   *)
@@ -200,38 +168,44 @@
     let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
     in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
 
-  fun expf t i T ts =
-    let val Ts = U.dest_funT i T |> fst |> drop (length ts)
+  fun expf k i T t =
+    let val Ts = drop i (fst (U.dest_funT k T))
     in
-      Term.list_comb (t, ts)
-      |> Term.incr_boundvars (length Ts)
+      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
-
-  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)) = 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)) = exp2 T q
-    | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
-        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
-    | 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
-    | expand (Abs a) = abs_expand a
-    | expand t =
-        (case Term.strip_comb t of
-          (u as Const (@{const_name If}, T), ts) => expf u 3 T (map expand ts)
-        | (u as Var ((_, i), T), ts) => expf u i T (map expand ts)
-        | (u, ts) => Term.list_comb (u, map expand ts))
-
-  and abs_expand (n, T, t) = Abs (n, T, expand t)
 in
 
-val eta_expand = map expand
+fun eta_expand ctxt =
+  let
+    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)) = 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)) = exp2 T q
+      | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
+          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
+      | 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
+      | expand t =
+          (case Term.strip_comb t of
+            (u as Const (c as (_, T)), ts) =>
+              (case B.dest_builtin ctxt c ts of
+                SOME (_, k, us, mk) =>
+                  if k = length us then mk (map expand us)
+                  else expf k (length ts) T (mk (map expand us))
+              | NONE => Term.list_comb (u, map expand ts))
+          | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts)
+          | (u, ts) => Term.list_comb (u, map expand ts))
+
+    and abs_expand (n, T, t) = Abs (n, T, expand t)
+  
+  in map expand end
 
 end
 
@@ -354,118 +328,92 @@
 
 (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **)
 
-val tboolT = @{typ SMT.term_bool}
-val term_true = Const (@{const_name True}, tboolT)
-val term_false = Const (@{const_name False}, tboolT)
-
-val term_bool = @{lemma "True ~= False" by simp}
-val term_bool_prop =
-  let
-    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
-      | replace @{const True} = term_true
-      | replace @{const False} = term_false
-      | replace t = t
-  in Term.map_aterms replace (U.prop_of term_bool) end
+local
+  val term_bool = @{lemma "SMT.term_true ~= SMT.term_false"
+    by (simp add: SMT.term_true_def SMT.term_false_def)}
 
-val fol_rules = [
-  Let_def,
-  @{lemma "P = True == P" by (rule eq_reflection) simp},
-  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
+  val fol_rules = [
+    Let_def,
+    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 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 is_pred_type NONE = false
-  | is_pred_type (SOME T) = (Term.body_type T = @{typ bool})
+  fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
 
-fun is_conn_type NONE = false
-  | is_conn_type (SOME T) =
-      forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
+  fun wrap_in_if t =
+    @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
+
+  fun is_builtin_conn_or_pred ctxt c ts =
+    is_some (B.dest_builtin_conn ctxt c ts) orelse
+    is_some (B.dest_builtin_pred ctxt c ts)
 
-fun revert_typ @{typ SMT.term_bool} = @{typ bool}
-  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
-  | revert_typ T = T
+  fun builtin b ctxt c ts =
+    (case (Const c, ts) of
+      (@{const HOL.eq (bool)}, [t, u]) =>
+        if t = @{const SMT.term_true} orelse u = @{const SMT.term_true} then
+          B.dest_builtin_eq ctxt t u
+        else b ctxt c ts
+    | _ => b ctxt c ts)
+in
 
-val revert_types = Term.map_types revert_typ
-
-fun folify ctxt builtins =
+fun folify ctxt =
   let
-    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
-
-    fun as_tbool @{typ bool} = tboolT
-      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
-      | as_tbool T = T
-    fun mapTs f g i = U.dest_funT i #> (fn (Ts, T) => map f Ts ---> g T)
-    fun predT i = mapTs as_tbool I i
-    fun funcT i = mapTs as_tbool as_tbool i
-    fun func i (n, T) = (n, funcT i T)
-
-    fun map_ifT T = T |> Term.dest_funT ||> funcT 2 |> (op -->)
-    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
-    fun wrap_in_if t = if_term $ t $ term_true $ term_false
-
     fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
 
     fun in_term t =
       (case Term.strip_comb t of
-        (Const (n as @{const_name If}, T), [t1, t2, t3]) =>
-          Const (n, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
-      | (Const (@{const_name HOL.eq}, _), _) => wrap_in_if (in_form t)
-      | (Var (ni as (_, i), T), ts) =>
-          let val U = Vartab.lookup builtins ni
-          in
-            if is_conn_type U orelse is_pred_type U then wrap_in_if (in_form t)
-            else Term.list_comb (Var (ni, funcT i T), map in_term ts)
-          end
+        (@{const True}, []) => @{const SMT.term_true}
+      | (@{const False}, []) => @{const SMT.term_false}
+      | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
+          u $ in_form t1 $ in_term t2 $ in_term t3
       | (Const c, ts) =>
-          Term.list_comb (Const (func (length ts) c), map in_term ts)
-      | (Free c, ts) =>
-          Term.list_comb (Free (func (length ts) c), map in_term ts)
+          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if (in_form t)
+          else Term.list_comb (Const c, map in_term ts)
+      | (Free c, ts) => Term.list_comb (Free c, map in_term ts)
       | _ => t)
 
     and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
       | in_weight t = in_form t 
 
-    and in_pat (Const (c as (@{const_name SMT.pat}, _)) $ t) =
-          Const (func 1 c) $ in_term t
-      | in_pat (Const (c as (@{const_name SMT.nopat}, _)) $ t) =
-          Const (func 1 c) $ in_term t
+    and in_pat ((p as Const (@{const_name SMT.pat}, _)) $ t) = p $ in_term t
+      | in_pat ((p as Const (@{const_name SMT.nopat}, _)) $ t) = p $ in_term t
       | in_pat t = raise TERM ("bad pattern", [t])
 
     and in_pats ps =
       in_list @{typ "SMT.pattern list"} (in_list @{typ SMT.pattern} in_pat) ps
 
-    and in_trig ((c as @{const SMT.trigger}) $ p $ t) =
+    and in_trigger ((c as @{const SMT.trigger}) $ p $ t) =
           c $ in_pats p $ in_weight t
-      | in_trig t = in_weight t
+      | in_trigger t = in_weight t
 
     and in_form t =
       (case Term.strip_comb t of
         (q as Const (qn, _), [Abs (n, T, u)]) =>
           if member (op =) [@{const_name All}, @{const_name Ex}] qn then
-            q $ Abs (n, as_tbool T, in_trig u)
+            q $ Abs (n, T, in_trigger u)
           else as_term (in_term t)
-      | (u as Const (@{const_name If}, _), ts) =>
-          Term.list_comb (u, map in_form ts)
-      | (b as @{const HOL.eq (bool)}, ts) => Term.list_comb (b, map in_form ts)
-      | (Const (n as @{const_name HOL.eq}, T), ts) =>
-          Term.list_comb (Const (n, predT 2 T), map in_term ts)
-      | (b as Var (ni as (_, i), T), ts) =>
-          if is_conn_type (Vartab.lookup builtins ni) then
-            Term.list_comb (b, map in_form ts)
-          else if is_pred_type (Vartab.lookup builtins ni) then
-            Term.list_comb (Var (ni, predT i T), map in_term ts)
-          else as_term (in_term t)
+      | (Const c, ts) =>
+          (case B.dest_builtin_conn ctxt c ts of
+            SOME (_, _, us, mk) => mk (map in_form us)
+          | NONE =>
+              (case B.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) #>
-    cons (mark_builtins' ctxt term_bool_prop) #>
-    pair (fol_rules, [term_bool])
+    cons (U.prop_of term_bool) #>
+    pair (fol_rules, [term_bool], builtin)
   end
 
+end
 
 
 (* translation into intermediate format *)
@@ -513,17 +461,15 @@
 
 (** translation from Isabelle terms into SMT intermediate terms **)
 
-fun intermediate header dtyps ctxt ts trx =
+fun intermediate header dtyps builtin ctxt ts trx =
   let
     fun transT (T as TFree _) = add_typ T true
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
       | transT (T as Type _) =
-          (case B.builtin_typ ctxt T of
+          (case B.dest_builtin_typ ctxt T of
             SOME n => pair n
           | NONE => add_typ T true)
 
-    val unmarked_builtins = [@{const_name If}, @{const_name HOL.eq}]
-
     fun app n ts = SApp (n, ts)
 
     fun trans t =
@@ -537,13 +483,10 @@
       | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
           transT T ##>> trans t1 ##>> trans t2 #>>
           (fn ((U, u1), u2) => SLet (U, u1, u2))
-      | (Var ((n, _), _), ts) => fold_map trans ts #>> app n
-      | (u as Const (c as (n, T)), ts) =>
-          if member (op =) unmarked_builtins n then
-            (case B.builtin_fun ctxt c ts of
-              SOME (((m, _), _), us, _) => fold_map trans us #>> app m
-            | NONE => raise TERM ("not a built-in symbol", [t]))
-          else transs u T ts
+      | (u as Const (c as (_, T)), ts) =>
+          (case builtin ctxt c ts of
+            SOME (n, _, us, _) => fold_map trans us #>> app n
+          | NONE => transs u T ts)
       | (u as Free (_, T), ts) => transs u T ts
       | (Bound i, []) => pair (SVar i)
       | _ => raise TERM ("bad SMT term", [t]))
@@ -590,10 +533,7 @@
 
     fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
 
-    val (builtins, ts1) =
-      ithms
-      |> map (Envir.beta_eta_contract o U.prop_of o snd)
-      |> mark_builtins ctxt
+    val ts1 = map (Envir.beta_eta_contract o U.prop_of o snd) ithms
 
     val ((dtyps, tr_context, ctxt1), ts2) =
       ((make_tr_context prefixes, ctxt), ts1)
@@ -601,19 +541,19 @@
 
     val (ctxt2, ts3) =
       ts2
-      |> eta_expand
+      |> eta_expand ctxt1
       |> lift_lambdas ctxt1
       ||> intro_explicit_application
 
-    val ((rewrite_rules, extra_thms), ts4) =
-      (if is_fol then folify ctxt2 builtins else pair ([], [])) ts3
+    val ((rewrite_rules, extra_thms, builtin), ts4) =
+      (if is_fol then folify ctxt2 else pair ([], [], I)) ts3
 
     val rewrite_rules' = fun_app_eq :: rewrite_rules
   in
     (ts4, tr_context)
-    |-> intermediate header dtyps ctxt2
+    |-> intermediate header dtyps (builtin B.dest_builtin) ctxt2
     |>> uncurry (serialize comments)
-    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms revert_typ revert_types
+    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms
   end
 
 end
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -33,15 +33,17 @@
     | is_linear [t, u] = U.is_number t orelse U.is_number u
     | is_linear _ = false
 
-  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
+  fun times _ _ ts =
+    let val mk = Term.list_comb o pair @{const times (int)}
+    in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
 
-  fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
+  fun distinct _ T [t] =
         (case try HOLogic.dest_list t of
           SOME (ts as _ :: _) =>
             let
-              fun mkT U = replicate (length ts) U ---> @{typ bool}
-              val U = mkT T and U' = mkT (TVar (("'a", 0), @{sort type}))
-            in SOME ((("distinct", length ts), U), ts, U') end
+              val c = Const (@{const_name distinct}, T)
+              fun mk us = c $ HOLogic.mk_list T us
+            in SOME ("distinct", length ts, ts, mk) end
         | _ => NONE)
     | distinct _ _ _ = NONE
 in
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -322,6 +322,7 @@
     addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
     addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
     addsimps @{thms array_rules}
+    addsimps @{thms term_true_def} addsimps @{thms term_false_def}
     addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
     addsimprocs [
       Simplifier.simproc_global @{theory} "fast_int_arith" [
diff -r a7de9d36f4f2 -r 679118e35378 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Sun Dec 19 17:55:56 2010 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML	Sun Dec 19 18:54:29 2010 +0100
@@ -58,70 +58,77 @@
         Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
     | word_num _ _ = NONE
 
-  fun if_fixed n T ts =
+  fun if_fixed pred m n T ts =
     let val (Us, U) = Term.strip_type T
     in
-      if forall (can dest_wordT) (U :: Us) then
-        SOME (((n, length Us), T), ts, T)
-      else NONE
-    end
-
-  fun if_fixed' n T ts =
-    let val Ts = Term.binder_types T
-    in
-      if forall (can dest_wordT) Ts then SOME (((n, length Ts), T), ts, T)
+      if pred (U, Us) then
+        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
       else NONE
     end
 
+  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
+  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
+
   fun add_word_fun f (t, n) =
-    B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n))
+    let val c as (m, _) = Term.dest_Const t
+    in B.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
+
+  fun hd2 xs = hd (tl xs)
 
-  fun add_word_fun' f (t, n) = add_word_fun f (t, n)
+  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
+
+  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
+    | dest_nat t = raise TERM ("not a natural number", [t])
+
+  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
+    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
 
-  fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
-    | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
-  fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
-    | dest_nat ts = raise TERM ("dest_nat", ts)
-  fun dest_nat_word_funT (T, ts) =
-    (dest_word_funT (Term.range_type T), dest_nat ts)
+  fun shift m n T ts =
+    let val U = Term.domain_type T
+    in
+      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
+        (true, SOME i) =>
+          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
+      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
+    end
 
-  fun shift n T ts =
-    let
-      val U = Term.domain_type T
-      val T' = [U, U] ---> U
+  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
+
+  fun extract m n T ts =
+    let val U = Term.range_type (Term.range_type T)
     in
-      (case (can dest_wordT T', ts) of
-        (true, [t, u]) =>
-          (case try HOLogic.dest_number u of
-            SOME (_, i) => SOME (((n, 2), T'), [t, HOLogic.mk_number T' i], T')
-          | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
+      (case (try (dest_nat o hd) ts, try dest_wordT U) of
+        (SOME lb, SOME i) =>
+          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
       | _ => NONE)
     end
 
-  fun extract n T ts =
-    try dest_nat_word_funT (T, ts)
-    |> Option.map (fn ((_, i), (lb, ts')) =>
-         let val T' = Term.range_type T
-         in (((index2 n (i + lb - 1) lb, 1), T'), ts', T') end)
+  fun mk_extend c ts = Term.list_comb (Const c, ts)
 
-  fun extend n T ts =
-    (case try dest_word_funT T of
-      SOME (i, j) =>
-        if j-i >= 0 then SOME (((index1 n (j-i), 1), T), ts, T)
-        else NONE
-    | _ => NONE)
+  fun extend m n T ts =
+    let val (U1, U2) = Term.dest_funT T
+    in
+      (case (try dest_wordT U1, try dest_wordT U2) of
+        (SOME i, SOME j) =>
+          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
+          else NONE
+      | _ => NONE)
+    end
 
-  fun rotate n T ts =
-    let val T' = Term.range_type T
+  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
+
+  fun rotate m n T ts =
+    let val U = Term.domain_type (Term.range_type T)
     in
-      try dest_nat ts
-      |> Option.map (fn (i, ts') => (((index1 n i, 1), T'), ts', T'))
+      (case (can dest_wordT U, try (dest_nat o hd) ts) of
+        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
+      | _ => NONE)
     end
 in
 
 val setup_builtins =
   B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
-  fold (add_word_fun' if_fixed) [
+  fold (add_word_fun if_fixed_all) [
     (@{term "uminus :: 'a::len word => _"}, "bvneg"),
     (@{term "plus :: 'a::len word => _"}, "bvadd"),
     (@{term "minus :: 'a::len word => _"}, "bvsub"),
@@ -143,7 +150,7 @@
   fold (add_word_fun rotate) [
     (@{term word_rotl}, "rotate_left"),
     (@{term word_rotr}, "rotate_right") ] #>
-  fold (add_word_fun' if_fixed') [
+  fold (add_word_fun if_fixed_args) [
     (@{term "less :: 'a::len word => _"}, "bvult"),
     (@{term "less_eq :: 'a::len word => _"}, "bvule"),
     (@{term word_sless}, "bvslt"),