removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
authorboehmes
Sun Dec 19 18:54:29 2010 +0100 (2010-12-19)
changeset 41281679118e35378
parent 41280 a7de9d36f4f2
child 41282 a4d1b5eef12e
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)
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Word/Tools/smt_word.ML
     1.1 --- a/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Sun Dec 19 18:54:29 2010 +0100
     1.3 @@ -113,12 +113,14 @@
     1.4  uninterpreted constants (those not built-in in the target solver)
     1.5  are treated as function symbols in the first-order sense.  Their
     1.6  occurrences as head symbols in atoms (i.e., as predicate symbols) are
     1.7 -turned into terms by equating such atoms with @{term True}.
     1.8 -Whenever the boolean type occurs in first-order terms, it is replaced
     1.9 -by the following type.
    1.10 +turned into terms by logically equating such atoms with @{term True}.
    1.11 +For technical reasons, @{term True} and @{term False} occurring inside
    1.12 +terms are replaced by the following constants.
    1.13  *}
    1.14  
    1.15 -typedecl term_bool
    1.16 +definition term_true where "term_true = True"
    1.17 +definition term_false where "term_false = False"
    1.18 +
    1.19  
    1.20  
    1.21  
    1.22 @@ -374,9 +376,8 @@
    1.23  
    1.24  
    1.25  
    1.26 -hide_type term_bool
    1.27  hide_type (open) pattern
    1.28 -hide_const Pattern fun_app z3div z3mod
    1.29 +hide_const Pattern fun_app term_true term_false z3div z3mod
    1.30  hide_const (open) trigger pat nopat weight
    1.31  
    1.32  
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 17:55:56 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 18:54:29 2010 +0100
     2.3 @@ -12,28 +12,33 @@
     2.4      Context.generic -> Context.generic
     2.5    val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
     2.6      Context.generic
     2.7 -  val builtin_typ: Proof.context -> typ -> string option
     2.8 -  val is_builtin_typ: Proof.context -> typ -> bool
     2.9 +  val dest_builtin_typ: Proof.context -> typ -> string option
    2.10    val is_builtin_typ_ext: Proof.context -> typ -> bool
    2.11  
    2.12    (*built-in numbers*)
    2.13 -  val builtin_num: Proof.context -> term -> (string * typ) option
    2.14 +  val dest_builtin_num: Proof.context -> term -> (string * typ) option
    2.15    val is_builtin_num: Proof.context -> term -> bool
    2.16    val is_builtin_num_ext: Proof.context -> term -> bool
    2.17  
    2.18    (*built-in functions*)
    2.19    type 'a bfun = Proof.context -> typ -> term list -> 'a
    2.20 +  type bfunr = string * int * term list * (term list -> term)
    2.21    val add_builtin_fun: SMT_Utils.class ->
    2.22 -    (string * typ) * (((string * int) * typ) * term list * typ) option bfun ->
    2.23 -    Context.generic -> Context.generic
    2.24 +    (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
    2.25    val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
    2.26      Context.generic
    2.27    val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
    2.28      Context.generic
    2.29    val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
    2.30    val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
    2.31 -  val builtin_fun: Proof.context -> string * typ -> term list ->
    2.32 -    (((string * int) * typ) * term list * typ) option
    2.33 +  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
    2.34 +    bfunr option
    2.35 +  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
    2.36 +  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
    2.37 +    bfunr option
    2.38 +  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
    2.39 +    bfunr option
    2.40 +  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
    2.41    val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    2.42    val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
    2.43    val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
    2.44 @@ -108,13 +113,11 @@
    2.45  fun lookup_builtin_typ ctxt =
    2.46    lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
    2.47  
    2.48 -fun builtin_typ ctxt T =
    2.49 +fun dest_builtin_typ ctxt T =
    2.50    (case lookup_builtin_typ ctxt T of
    2.51      SOME (_, Int (f, _)) => f T
    2.52    | _ => NONE) 
    2.53  
    2.54 -fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
    2.55 -
    2.56  fun is_builtin_typ_ext ctxt T =
    2.57    (case lookup_builtin_typ ctxt T of
    2.58      SOME (_, Int (f, _)) => is_some (f T)
    2.59 @@ -124,7 +127,7 @@
    2.60  
    2.61  (* built-in numbers *)
    2.62  
    2.63 -fun builtin_num ctxt t =
    2.64 +fun dest_builtin_num ctxt t =
    2.65    (case try HOLogic.dest_number t of
    2.66      NONE => NONE
    2.67    | SOME (T, i) =>
    2.68 @@ -132,7 +135,7 @@
    2.69          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
    2.70        | _ => NONE))
    2.71  
    2.72 -val is_builtin_num = is_some oo builtin_num
    2.73 +val is_builtin_num = is_some oo dest_builtin_num
    2.74  
    2.75  fun is_builtin_num_ext ctxt t =
    2.76    (case try HOLogic.dest_number t of
    2.77 @@ -144,10 +147,11 @@
    2.78  
    2.79  type 'a bfun = Proof.context -> typ -> term list -> 'a
    2.80  
    2.81 +type bfunr = string * int * term list * (term list -> term)
    2.82 +
    2.83  structure Builtin_Funcs = Generic_Data
    2.84  (
    2.85 -  type T =
    2.86 -    (bool bfun, (((string * int) * typ) * term list * typ) option bfun) btab
    2.87 +  type T = (bool bfun, bfunr option bfun) btab
    2.88    val empty = Symtab.empty
    2.89    val extend = I
    2.90    val merge = merge_btab
    2.91 @@ -158,9 +162,10 @@
    2.92  
    2.93  fun add_builtin_fun' cs (t, n) =
    2.94    let
    2.95 -    val T = Term.fastype_of t
    2.96 -    fun bfun _ U ts = SOME (((n, length (Term.binder_types T)), U), ts, T)
    2.97 -  in add_builtin_fun cs (Term.dest_Const t, bfun) end
    2.98 +    val c as (m, T) = Term.dest_Const t
    2.99 +    fun app U ts = Term.list_comb (Const (m, U), ts)
   2.100 +    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
   2.101 +  in add_builtin_fun cs (c, bfun) end
   2.102  
   2.103  fun add_builtin_fun_ext ((n, T), f) =
   2.104    Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
   2.105 @@ -175,12 +180,40 @@
   2.106  fun lookup_builtin_fun ctxt =
   2.107    lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
   2.108  
   2.109 -fun builtin_fun ctxt (c as (_, T)) ts =
   2.110 +fun dest_builtin_fun ctxt (c as (_, T)) ts =
   2.111    (case lookup_builtin_fun ctxt c of
   2.112      SOME (_, Int f) => f ctxt T ts
   2.113    | _ => NONE)
   2.114  
   2.115 -fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
   2.116 +fun dest_builtin_eq ctxt t u =
   2.117 +  let
   2.118 +    val aT = TFree (Name.aT, @{sort type})
   2.119 +    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
   2.120 +    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
   2.121 +  in
   2.122 +    dest_builtin_fun ctxt c []
   2.123 +    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
   2.124 +  end
   2.125 +
   2.126 +fun special_builtin_fun pred ctxt (c as (_, T)) ts =
   2.127 +  if pred (Term.body_type T, Term.binder_types T) then
   2.128 +    dest_builtin_fun ctxt c ts
   2.129 +  else NONE
   2.130 +
   2.131 +fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
   2.132 +
   2.133 +fun dest_builtin_conn ctxt =
   2.134 +  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
   2.135 +
   2.136 +fun dest_builtin ctxt c ts =
   2.137 +  let val t =Term.list_comb (Const c, ts)
   2.138 +  in
   2.139 +    (case dest_builtin_num ctxt t of
   2.140 +      SOME (n, _) => SOME (n, 0, [], K t)
   2.141 +    | NONE => dest_builtin_fun ctxt c ts)
   2.142 +  end
   2.143 +
   2.144 +fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
   2.145  
   2.146  fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
   2.147    (case lookup_builtin_fun ctxt c of
     3.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 17:55:56 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 18:54:29 2010 +0100
     3.3 @@ -35,11 +35,15 @@
     3.4      | is_linear [t, u] = U.is_number t orelse U.is_number u
     3.5      | is_linear _ = false
     3.6  
     3.7 -  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
     3.8 +  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
     3.9 +
    3.10 +  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
    3.11      | times _ _ _  = NONE
    3.12  
    3.13 +  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
    3.14 +
    3.15    fun divide _ T (ts as [_, t]) =
    3.16 -        if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE
    3.17 +        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
    3.18      | divide _ _ _ = NONE
    3.19  in
    3.20  
     4.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Sun Dec 19 17:55:56 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Dec 19 18:54:29 2010 +0100
     4.3 @@ -120,12 +120,12 @@
     4.4    dtyps = dtyps,
     4.5    funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
     4.6  
     4.7 -fun recon_of ctxt rules thms ithms revertT revert (_, _, typs, _, _, terms) =
     4.8 +fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) =
     4.9    let
    4.10 -    fun add_typ (T, (n, _)) = Symtab.update (n, revertT T)
    4.11 +    fun add_typ (T, (n, _)) = Symtab.update (n, T)
    4.12      val typs' = Typtab.fold add_typ typs Symtab.empty
    4.13  
    4.14 -    fun add_fun (t, (n, _)) = Symtab.update (n, revert t)
    4.15 +    fun add_fun (t, (n, _)) = Symtab.update (n, t)
    4.16      val terms' = Termtab.fold add_fun terms Symtab.empty
    4.17  
    4.18      val assms = map (pair ~1) thms @ ithms
    4.19 @@ -137,43 +137,11 @@
    4.20  
    4.21  (* preprocessing *)
    4.22  
    4.23 -(** mark built-in constants as Var **)
    4.24 -
    4.25 -fun mark_builtins ctxt =
    4.26 -  let
    4.27 -    (*
    4.28 -      Note: schematic terms cannot occur anymore in terms at this stage.
    4.29 -    *)
    4.30 -    fun mark t =
    4.31 -      (case Term.strip_comb t of
    4.32 -        (u as Const (@{const_name If}, _), ts) => marks u ts
    4.33 -      | (u as @{const SMT.weight}, [t1, t2]) =>
    4.34 -          mark t2 #>> (fn t2' => u $ t1 $ t2')
    4.35 -      | (u as Const c, ts) =>
    4.36 -          (case B.builtin_num ctxt t of
    4.37 -            SOME (n, T) =>
    4.38 -              let val v = ((n, 0), T)
    4.39 -              in Vartab.update v #> pair (Var v) end
    4.40 -          | NONE =>
    4.41 -              (case B.builtin_fun ctxt c ts of
    4.42 -                SOME ((ni, T), us, U) =>
    4.43 -                  Vartab.update (ni, U) #> marks (Var (ni, T)) us
    4.44 -              | NONE => marks u ts))
    4.45 -      | (Abs (n, T, u), ts) => mark u #-> (fn u' => marks (Abs (n, T, u')) ts)
    4.46 -      | (u, ts) => marks u ts)
    4.47 - 
    4.48 -    and marks t ts = fold_map mark ts #>> Term.list_comb o pair t
    4.49 -
    4.50 -  in (fn ts => swap (fold_map mark ts Vartab.empty)) end
    4.51 -
    4.52 -fun mark_builtins' ctxt t = hd (snd (mark_builtins ctxt [t]))
    4.53 -
    4.54 -
    4.55  (** FIXME **)
    4.56  
    4.57  local
    4.58    (*
    4.59 -    mark constructors and selectors as Vars (forcing eta-expansion),
    4.60 +    force eta-expansion for constructors and selectors,
    4.61      add missing datatype selectors via hypothetical definitions,
    4.62      also return necessary datatype and record theorems
    4.63    *)
    4.64 @@ -200,38 +168,44 @@
    4.65      let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
    4.66      in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
    4.67  
    4.68 -  fun expf t i T ts =
    4.69 -    let val Ts = U.dest_funT i T |> fst |> drop (length ts)
    4.70 +  fun expf k i T t =
    4.71 +    let val Ts = drop i (fst (U.dest_funT k T))
    4.72      in
    4.73 -      Term.list_comb (t, ts)
    4.74 -      |> Term.incr_boundvars (length Ts)
    4.75 +      Term.incr_boundvars (length Ts) t
    4.76        |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
    4.77        |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
    4.78      end
    4.79 -
    4.80 -  fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
    4.81 -    | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
    4.82 -    | expand (q as Const (@{const_name All}, T)) = exp2 T q
    4.83 -    | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
    4.84 -    | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
    4.85 -    | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
    4.86 -    | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
    4.87 -        l $ expand t $ abs_expand a
    4.88 -    | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
    4.89 -        l $ expand t $ exp (Term.range_type T) u
    4.90 -    | expand ((l as Const (@{const_name Let}, T)) $ t) = exp2 T (l $ expand t)
    4.91 -    | expand (l as Const (@{const_name Let}, T)) = exp2' T l
    4.92 -    | expand (Abs a) = abs_expand a
    4.93 -    | expand t =
    4.94 -        (case Term.strip_comb t of
    4.95 -          (u as Const (@{const_name If}, T), ts) => expf u 3 T (map expand ts)
    4.96 -        | (u as Var ((_, i), T), ts) => expf u i T (map expand ts)
    4.97 -        | (u, ts) => Term.list_comb (u, map expand ts))
    4.98 -
    4.99 -  and abs_expand (n, T, t) = Abs (n, T, expand t)
   4.100  in
   4.101  
   4.102 -val eta_expand = map expand
   4.103 +fun eta_expand ctxt =
   4.104 +  let
   4.105 +    fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
   4.106 +      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
   4.107 +      | expand (q as Const (@{const_name All}, T)) = exp2 T q
   4.108 +      | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
   4.109 +      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
   4.110 +      | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
   4.111 +      | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
   4.112 +          l $ expand t $ abs_expand a
   4.113 +      | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
   4.114 +          l $ expand t $ exp (Term.range_type T) u
   4.115 +      | expand ((l as Const (@{const_name Let}, T)) $ t) =
   4.116 +          exp2 T (l $ expand t)
   4.117 +      | expand (l as Const (@{const_name Let}, T)) = exp2' T l
   4.118 +      | expand t =
   4.119 +          (case Term.strip_comb t of
   4.120 +            (u as Const (c as (_, T)), ts) =>
   4.121 +              (case B.dest_builtin ctxt c ts of
   4.122 +                SOME (_, k, us, mk) =>
   4.123 +                  if k = length us then mk (map expand us)
   4.124 +                  else expf k (length ts) T (mk (map expand us))
   4.125 +              | NONE => Term.list_comb (u, map expand ts))
   4.126 +          | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts)
   4.127 +          | (u, ts) => Term.list_comb (u, map expand ts))
   4.128 +
   4.129 +    and abs_expand (n, T, t) = Abs (n, T, expand t)
   4.130 +  
   4.131 +  in map expand end
   4.132  
   4.133  end
   4.134  
   4.135 @@ -354,118 +328,92 @@
   4.136  
   4.137  (** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **)
   4.138  
   4.139 -val tboolT = @{typ SMT.term_bool}
   4.140 -val term_true = Const (@{const_name True}, tboolT)
   4.141 -val term_false = Const (@{const_name False}, tboolT)
   4.142 -
   4.143 -val term_bool = @{lemma "True ~= False" by simp}
   4.144 -val term_bool_prop =
   4.145 -  let
   4.146 -    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
   4.147 -      | replace @{const True} = term_true
   4.148 -      | replace @{const False} = term_false
   4.149 -      | replace t = t
   4.150 -  in Term.map_aterms replace (U.prop_of term_bool) end
   4.151 +local
   4.152 +  val term_bool = @{lemma "SMT.term_true ~= SMT.term_false"
   4.153 +    by (simp add: SMT.term_true_def SMT.term_false_def)}
   4.154  
   4.155 -val fol_rules = [
   4.156 -  Let_def,
   4.157 -  @{lemma "P = True == P" by (rule eq_reflection) simp},
   4.158 -  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   4.159 +  val fol_rules = [
   4.160 +    Let_def,
   4.161 +    mk_meta_eq @{thm SMT.term_true_def},
   4.162 +    mk_meta_eq @{thm SMT.term_false_def},
   4.163 +    @{lemma "P = True == P" by (rule eq_reflection) simp},
   4.164 +    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   4.165  
   4.166 -fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
   4.167 -      reduce_let (Term.betapply (u, t))
   4.168 -  | reduce_let (t $ u) = reduce_let t $ reduce_let u
   4.169 -  | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
   4.170 -  | reduce_let t = t
   4.171 +  fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
   4.172 +        reduce_let (Term.betapply (u, t))
   4.173 +    | reduce_let (t $ u) = reduce_let t $ reduce_let u
   4.174 +    | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
   4.175 +    | reduce_let t = t
   4.176  
   4.177 -fun is_pred_type NONE = false
   4.178 -  | is_pred_type (SOME T) = (Term.body_type T = @{typ bool})
   4.179 +  fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
   4.180  
   4.181 -fun is_conn_type NONE = false
   4.182 -  | is_conn_type (SOME T) =
   4.183 -      forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
   4.184 +  fun wrap_in_if t =
   4.185 +    @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false}
   4.186 +
   4.187 +  fun is_builtin_conn_or_pred ctxt c ts =
   4.188 +    is_some (B.dest_builtin_conn ctxt c ts) orelse
   4.189 +    is_some (B.dest_builtin_pred ctxt c ts)
   4.190  
   4.191 -fun revert_typ @{typ SMT.term_bool} = @{typ bool}
   4.192 -  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
   4.193 -  | revert_typ T = T
   4.194 +  fun builtin b ctxt c ts =
   4.195 +    (case (Const c, ts) of
   4.196 +      (@{const HOL.eq (bool)}, [t, u]) =>
   4.197 +        if t = @{const SMT.term_true} orelse u = @{const SMT.term_true} then
   4.198 +          B.dest_builtin_eq ctxt t u
   4.199 +        else b ctxt c ts
   4.200 +    | _ => b ctxt c ts)
   4.201 +in
   4.202  
   4.203 -val revert_types = Term.map_types revert_typ
   4.204 -
   4.205 -fun folify ctxt builtins =
   4.206 +fun folify ctxt =
   4.207    let
   4.208 -    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
   4.209 -
   4.210 -    fun as_tbool @{typ bool} = tboolT
   4.211 -      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
   4.212 -      | as_tbool T = T
   4.213 -    fun mapTs f g i = U.dest_funT i #> (fn (Ts, T) => map f Ts ---> g T)
   4.214 -    fun predT i = mapTs as_tbool I i
   4.215 -    fun funcT i = mapTs as_tbool as_tbool i
   4.216 -    fun func i (n, T) = (n, funcT i T)
   4.217 -
   4.218 -    fun map_ifT T = T |> Term.dest_funT ||> funcT 2 |> (op -->)
   4.219 -    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
   4.220 -    fun wrap_in_if t = if_term $ t $ term_true $ term_false
   4.221 -
   4.222      fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
   4.223  
   4.224      fun in_term t =
   4.225        (case Term.strip_comb t of
   4.226 -        (Const (n as @{const_name If}, T), [t1, t2, t3]) =>
   4.227 -          Const (n, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
   4.228 -      | (Const (@{const_name HOL.eq}, _), _) => wrap_in_if (in_form t)
   4.229 -      | (Var (ni as (_, i), T), ts) =>
   4.230 -          let val U = Vartab.lookup builtins ni
   4.231 -          in
   4.232 -            if is_conn_type U orelse is_pred_type U then wrap_in_if (in_form t)
   4.233 -            else Term.list_comb (Var (ni, funcT i T), map in_term ts)
   4.234 -          end
   4.235 +        (@{const True}, []) => @{const SMT.term_true}
   4.236 +      | (@{const False}, []) => @{const SMT.term_false}
   4.237 +      | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
   4.238 +          u $ in_form t1 $ in_term t2 $ in_term t3
   4.239        | (Const c, ts) =>
   4.240 -          Term.list_comb (Const (func (length ts) c), map in_term ts)
   4.241 -      | (Free c, ts) =>
   4.242 -          Term.list_comb (Free (func (length ts) c), map in_term ts)
   4.243 +          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if (in_form t)
   4.244 +          else Term.list_comb (Const c, map in_term ts)
   4.245 +      | (Free c, ts) => Term.list_comb (Free c, map in_term ts)
   4.246        | _ => t)
   4.247  
   4.248      and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
   4.249        | in_weight t = in_form t 
   4.250  
   4.251 -    and in_pat (Const (c as (@{const_name SMT.pat}, _)) $ t) =
   4.252 -          Const (func 1 c) $ in_term t
   4.253 -      | in_pat (Const (c as (@{const_name SMT.nopat}, _)) $ t) =
   4.254 -          Const (func 1 c) $ in_term t
   4.255 +    and in_pat ((p as Const (@{const_name SMT.pat}, _)) $ t) = p $ in_term t
   4.256 +      | in_pat ((p as Const (@{const_name SMT.nopat}, _)) $ t) = p $ in_term t
   4.257        | in_pat t = raise TERM ("bad pattern", [t])
   4.258  
   4.259      and in_pats ps =
   4.260        in_list @{typ "SMT.pattern list"} (in_list @{typ SMT.pattern} in_pat) ps
   4.261  
   4.262 -    and in_trig ((c as @{const SMT.trigger}) $ p $ t) =
   4.263 +    and in_trigger ((c as @{const SMT.trigger}) $ p $ t) =
   4.264            c $ in_pats p $ in_weight t
   4.265 -      | in_trig t = in_weight t
   4.266 +      | in_trigger t = in_weight t
   4.267  
   4.268      and in_form t =
   4.269        (case Term.strip_comb t of
   4.270          (q as Const (qn, _), [Abs (n, T, u)]) =>
   4.271            if member (op =) [@{const_name All}, @{const_name Ex}] qn then
   4.272 -            q $ Abs (n, as_tbool T, in_trig u)
   4.273 +            q $ Abs (n, T, in_trigger u)
   4.274            else as_term (in_term t)
   4.275 -      | (u as Const (@{const_name If}, _), ts) =>
   4.276 -          Term.list_comb (u, map in_form ts)
   4.277 -      | (b as @{const HOL.eq (bool)}, ts) => Term.list_comb (b, map in_form ts)
   4.278 -      | (Const (n as @{const_name HOL.eq}, T), ts) =>
   4.279 -          Term.list_comb (Const (n, predT 2 T), map in_term ts)
   4.280 -      | (b as Var (ni as (_, i), T), ts) =>
   4.281 -          if is_conn_type (Vartab.lookup builtins ni) then
   4.282 -            Term.list_comb (b, map in_form ts)
   4.283 -          else if is_pred_type (Vartab.lookup builtins ni) then
   4.284 -            Term.list_comb (Var (ni, predT i T), map in_term ts)
   4.285 -          else as_term (in_term t)
   4.286 +      | (Const c, ts) =>
   4.287 +          (case B.dest_builtin_conn ctxt c ts of
   4.288 +            SOME (_, _, us, mk) => mk (map in_form us)
   4.289 +          | NONE =>
   4.290 +              (case B.dest_builtin_pred ctxt c ts of
   4.291 +                SOME (_, _, us, mk) => mk (map in_term us)
   4.292 +              | NONE => as_term (in_term t)))
   4.293        | _ => as_term (in_term t))
   4.294    in
   4.295      map (reduce_let #> in_form) #>
   4.296 -    cons (mark_builtins' ctxt term_bool_prop) #>
   4.297 -    pair (fol_rules, [term_bool])
   4.298 +    cons (U.prop_of term_bool) #>
   4.299 +    pair (fol_rules, [term_bool], builtin)
   4.300    end
   4.301  
   4.302 +end
   4.303  
   4.304  
   4.305  (* translation into intermediate format *)
   4.306 @@ -513,17 +461,15 @@
   4.307  
   4.308  (** translation from Isabelle terms into SMT intermediate terms **)
   4.309  
   4.310 -fun intermediate header dtyps ctxt ts trx =
   4.311 +fun intermediate header dtyps builtin ctxt ts trx =
   4.312    let
   4.313      fun transT (T as TFree _) = add_typ T true
   4.314        | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
   4.315        | transT (T as Type _) =
   4.316 -          (case B.builtin_typ ctxt T of
   4.317 +          (case B.dest_builtin_typ ctxt T of
   4.318              SOME n => pair n
   4.319            | NONE => add_typ T true)
   4.320  
   4.321 -    val unmarked_builtins = [@{const_name If}, @{const_name HOL.eq}]
   4.322 -
   4.323      fun app n ts = SApp (n, ts)
   4.324  
   4.325      fun trans t =
   4.326 @@ -537,13 +483,10 @@
   4.327        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
   4.328            transT T ##>> trans t1 ##>> trans t2 #>>
   4.329            (fn ((U, u1), u2) => SLet (U, u1, u2))
   4.330 -      | (Var ((n, _), _), ts) => fold_map trans ts #>> app n
   4.331 -      | (u as Const (c as (n, T)), ts) =>
   4.332 -          if member (op =) unmarked_builtins n then
   4.333 -            (case B.builtin_fun ctxt c ts of
   4.334 -              SOME (((m, _), _), us, _) => fold_map trans us #>> app m
   4.335 -            | NONE => raise TERM ("not a built-in symbol", [t]))
   4.336 -          else transs u T ts
   4.337 +      | (u as Const (c as (_, T)), ts) =>
   4.338 +          (case builtin ctxt c ts of
   4.339 +            SOME (n, _, us, _) => fold_map trans us #>> app n
   4.340 +          | NONE => transs u T ts)
   4.341        | (u as Free (_, T), ts) => transs u T ts
   4.342        | (Bound i, []) => pair (SVar i)
   4.343        | _ => raise TERM ("bad SMT term", [t]))
   4.344 @@ -590,10 +533,7 @@
   4.345  
   4.346      fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
   4.347  
   4.348 -    val (builtins, ts1) =
   4.349 -      ithms
   4.350 -      |> map (Envir.beta_eta_contract o U.prop_of o snd)
   4.351 -      |> mark_builtins ctxt
   4.352 +    val ts1 = map (Envir.beta_eta_contract o U.prop_of o snd) ithms
   4.353  
   4.354      val ((dtyps, tr_context, ctxt1), ts2) =
   4.355        ((make_tr_context prefixes, ctxt), ts1)
   4.356 @@ -601,19 +541,19 @@
   4.357  
   4.358      val (ctxt2, ts3) =
   4.359        ts2
   4.360 -      |> eta_expand
   4.361 +      |> eta_expand ctxt1
   4.362        |> lift_lambdas ctxt1
   4.363        ||> intro_explicit_application
   4.364  
   4.365 -    val ((rewrite_rules, extra_thms), ts4) =
   4.366 -      (if is_fol then folify ctxt2 builtins else pair ([], [])) ts3
   4.367 +    val ((rewrite_rules, extra_thms, builtin), ts4) =
   4.368 +      (if is_fol then folify ctxt2 else pair ([], [], I)) ts3
   4.369  
   4.370      val rewrite_rules' = fun_app_eq :: rewrite_rules
   4.371    in
   4.372      (ts4, tr_context)
   4.373 -    |-> intermediate header dtyps ctxt2
   4.374 +    |-> intermediate header dtyps (builtin B.dest_builtin) ctxt2
   4.375      |>> uncurry (serialize comments)
   4.376 -    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms revert_typ revert_types
   4.377 +    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms
   4.378    end
   4.379  
   4.380  end
     5.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 17:55:56 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 18:54:29 2010 +0100
     5.3 @@ -33,15 +33,17 @@
     5.4      | is_linear [t, u] = U.is_number t orelse U.is_number u
     5.5      | is_linear _ = false
     5.6  
     5.7 -  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
     5.8 +  fun times _ _ ts =
     5.9 +    let val mk = Term.list_comb o pair @{const times (int)}
    5.10 +    in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
    5.11  
    5.12 -  fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
    5.13 +  fun distinct _ T [t] =
    5.14          (case try HOLogic.dest_list t of
    5.15            SOME (ts as _ :: _) =>
    5.16              let
    5.17 -              fun mkT U = replicate (length ts) U ---> @{typ bool}
    5.18 -              val U = mkT T and U' = mkT (TVar (("'a", 0), @{sort type}))
    5.19 -            in SOME ((("distinct", length ts), U), ts, U') end
    5.20 +              val c = Const (@{const_name distinct}, T)
    5.21 +              fun mk us = c $ HOLogic.mk_list T us
    5.22 +            in SOME ("distinct", length ts, ts, mk) end
    5.23          | _ => NONE)
    5.24      | distinct _ _ _ = NONE
    5.25  in
     6.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sun Dec 19 17:55:56 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sun Dec 19 18:54:29 2010 +0100
     6.3 @@ -322,6 +322,7 @@
     6.4      addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
     6.5      addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
     6.6      addsimps @{thms array_rules}
     6.7 +    addsimps @{thms term_true_def} addsimps @{thms term_false_def}
     6.8      addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
     6.9      addsimprocs [
    6.10        Simplifier.simproc_global @{theory} "fast_int_arith" [
     7.1 --- a/src/HOL/Word/Tools/smt_word.ML	Sun Dec 19 17:55:56 2010 +0100
     7.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Sun Dec 19 18:54:29 2010 +0100
     7.3 @@ -58,70 +58,77 @@
     7.4          Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
     7.5      | word_num _ _ = NONE
     7.6  
     7.7 -  fun if_fixed n T ts =
     7.8 +  fun if_fixed pred m n T ts =
     7.9      let val (Us, U) = Term.strip_type T
    7.10      in
    7.11 -      if forall (can dest_wordT) (U :: Us) then
    7.12 -        SOME (((n, length Us), T), ts, T)
    7.13 -      else NONE
    7.14 -    end
    7.15 -
    7.16 -  fun if_fixed' n T ts =
    7.17 -    let val Ts = Term.binder_types T
    7.18 -    in
    7.19 -      if forall (can dest_wordT) Ts then SOME (((n, length Ts), T), ts, T)
    7.20 +      if pred (U, Us) then
    7.21 +        SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T)))
    7.22        else NONE
    7.23      end
    7.24  
    7.25 +  fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
    7.26 +  fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
    7.27 +
    7.28    fun add_word_fun f (t, n) =
    7.29 -    B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n))
    7.30 +    let val c as (m, _) = Term.dest_Const t
    7.31 +    in B.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
    7.32 +
    7.33 +  fun hd2 xs = hd (tl xs)
    7.34  
    7.35 -  fun add_word_fun' f (t, n) = add_word_fun f (t, n)
    7.36 +  fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i
    7.37 +
    7.38 +  fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n)
    7.39 +    | dest_nat t = raise TERM ("not a natural number", [t])
    7.40 +
    7.41 +  fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
    7.42 +    | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
    7.43  
    7.44 -  fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
    7.45 -    | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
    7.46 -  fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
    7.47 -    | dest_nat ts = raise TERM ("dest_nat", ts)
    7.48 -  fun dest_nat_word_funT (T, ts) =
    7.49 -    (dest_word_funT (Term.range_type T), dest_nat ts)
    7.50 +  fun shift m n T ts =
    7.51 +    let val U = Term.domain_type T
    7.52 +    in
    7.53 +      (case (can dest_wordT U, try (dest_nat o hd2) ts) of
    7.54 +        (true, SOME i) =>
    7.55 +          SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T))
    7.56 +      | _ => NONE)   (* FIXME: also support non-numerical shifts *)
    7.57 +    end
    7.58  
    7.59 -  fun shift n T ts =
    7.60 -    let
    7.61 -      val U = Term.domain_type T
    7.62 -      val T' = [U, U] ---> U
    7.63 +  fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
    7.64 +
    7.65 +  fun extract m n T ts =
    7.66 +    let val U = Term.range_type (Term.range_type T)
    7.67      in
    7.68 -      (case (can dest_wordT T', ts) of
    7.69 -        (true, [t, u]) =>
    7.70 -          (case try HOLogic.dest_number u of
    7.71 -            SOME (_, i) => SOME (((n, 2), T'), [t, HOLogic.mk_number T' i], T')
    7.72 -          | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
    7.73 +      (case (try (dest_nat o hd) ts, try dest_wordT U) of
    7.74 +        (SOME lb, SOME i) =>
    7.75 +          SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
    7.76        | _ => NONE)
    7.77      end
    7.78  
    7.79 -  fun extract n T ts =
    7.80 -    try dest_nat_word_funT (T, ts)
    7.81 -    |> Option.map (fn ((_, i), (lb, ts')) =>
    7.82 -         let val T' = Term.range_type T
    7.83 -         in (((index2 n (i + lb - 1) lb, 1), T'), ts', T') end)
    7.84 +  fun mk_extend c ts = Term.list_comb (Const c, ts)
    7.85  
    7.86 -  fun extend n T ts =
    7.87 -    (case try dest_word_funT T of
    7.88 -      SOME (i, j) =>
    7.89 -        if j-i >= 0 then SOME (((index1 n (j-i), 1), T), ts, T)
    7.90 -        else NONE
    7.91 -    | _ => NONE)
    7.92 +  fun extend m n T ts =
    7.93 +    let val (U1, U2) = Term.dest_funT T
    7.94 +    in
    7.95 +      (case (try dest_wordT U1, try dest_wordT U2) of
    7.96 +        (SOME i, SOME j) =>
    7.97 +          if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
    7.98 +          else NONE
    7.99 +      | _ => NONE)
   7.100 +    end
   7.101  
   7.102 -  fun rotate n T ts =
   7.103 -    let val T' = Term.range_type T
   7.104 +  fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
   7.105 +
   7.106 +  fun rotate m n T ts =
   7.107 +    let val U = Term.domain_type (Term.range_type T)
   7.108      in
   7.109 -      try dest_nat ts
   7.110 -      |> Option.map (fn (i, ts') => (((index1 n i, 1), T'), ts', T'))
   7.111 +      (case (can dest_wordT U, try (dest_nat o hd) ts) of
   7.112 +        (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
   7.113 +      | _ => NONE)
   7.114      end
   7.115  in
   7.116  
   7.117  val setup_builtins =
   7.118    B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   7.119 -  fold (add_word_fun' if_fixed) [
   7.120 +  fold (add_word_fun if_fixed_all) [
   7.121      (@{term "uminus :: 'a::len word => _"}, "bvneg"),
   7.122      (@{term "plus :: 'a::len word => _"}, "bvadd"),
   7.123      (@{term "minus :: 'a::len word => _"}, "bvsub"),
   7.124 @@ -143,7 +150,7 @@
   7.125    fold (add_word_fun rotate) [
   7.126      (@{term word_rotl}, "rotate_left"),
   7.127      (@{term word_rotr}, "rotate_right") ] #>
   7.128 -  fold (add_word_fun' if_fixed') [
   7.129 +  fold (add_word_fun if_fixed_args) [
   7.130      (@{term "less :: 'a::len word => _"}, "bvult"),
   7.131      (@{term "less_eq :: 'a::len word => _"}, "bvule"),
   7.132      (@{term word_sless}, "bvslt"),