re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
authorboehmes
Wed Dec 15 10:12:44 2010 +0100 (2010-12-15)
changeset 411272ea84c8535c6
parent 41126 e0bd443c0fdd
child 41128 bb2fa5c13d1a
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
abolished SMT interface concept in favor of solver classes (now also the translation configuration is stored in the context);
proof reconstruction is now expected to return a theorem stating False (and hence needs to discharge all hypothetical definitions);
built-in functions carry additionally their arity and their most general type;
slightly generalized the definition of fun_app
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Word/Tools/smt_word.ML
     1.1 --- a/src/HOL/SMT.thy	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 10:12:44 2010 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4  following constant.
     1.5  *}
     1.6  
     1.7 -definition fun_app where "fun_app f x = f x"
     1.8 +definition fun_app where "fun_app f = f"
     1.9  
    1.10  text {*
    1.11  Some solvers support a theory of arrays which can be used to encode
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Dec 15 08:39:24 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Dec 15 10:12:44 2010 +0100
     2.3 @@ -17,15 +17,15 @@
     2.4    val is_builtin_typ_ext: Proof.context -> typ -> bool
     2.5  
     2.6    (*built-in numbers*)
     2.7 -  val builtin_num: Proof.context -> term -> string option
     2.8 +  val builtin_num: Proof.context -> term -> (string * typ) option
     2.9    val is_builtin_num: Proof.context -> term -> bool
    2.10    val is_builtin_num_ext: Proof.context -> term -> bool
    2.11  
    2.12    (*built-in functions*)
    2.13    type 'a bfun = Proof.context -> typ -> term list -> 'a
    2.14    val add_builtin_fun: SMT_Utils.class ->
    2.15 -    (string * typ) * (string * term list) option bfun -> Context.generic ->
    2.16 -    Context.generic
    2.17 +    (string * typ) * (((string * int) * typ) * term list * typ) option bfun ->
    2.18 +    Context.generic -> Context.generic
    2.19    val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic ->
    2.20      Context.generic
    2.21    val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
    2.22 @@ -33,10 +33,8 @@
    2.23    val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
    2.24    val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
    2.25    val builtin_fun: Proof.context -> string * typ -> term list ->
    2.26 -    (string * term list) option
    2.27 +    (((string * int) * typ) * term list * typ) option
    2.28    val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    2.29 -  val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
    2.30 -  val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
    2.31    val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
    2.32    val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
    2.33  end
    2.34 @@ -131,7 +129,7 @@
    2.35      NONE => NONE
    2.36    | SOME (T, i) =>
    2.37        (case lookup_builtin_typ ctxt T of
    2.38 -        SOME (_, Int (_, g)) => g T i
    2.39 +        SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
    2.40        | _ => NONE))
    2.41  
    2.42  val is_builtin_num = is_some oo builtin_num
    2.43 @@ -148,7 +146,8 @@
    2.44  
    2.45  structure Builtin_Funcs = Generic_Data
    2.46  (
    2.47 -  type T = (bool bfun, (string * term list) option bfun) btab
    2.48 +  type T =
    2.49 +    (bool bfun, (((string * int) * typ) * term list * typ) option bfun) btab
    2.50    val empty = Symtab.empty
    2.51    val extend = I
    2.52    val merge = merge_btab
    2.53 @@ -158,7 +157,10 @@
    2.54    Builtin_Funcs.map (insert_btab cs n T (Int f))
    2.55  
    2.56  fun add_builtin_fun' cs (t, n) =
    2.57 -  add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
    2.58 +  let
    2.59 +    val T = Term.fastype_of t
    2.60 +    fun bfun _ U ts = SOME (((n, length (Term.binder_types T)), U), ts, T)
    2.61 +  in add_builtin_fun cs (Term.dest_Const t, bfun) end
    2.62  
    2.63  fun add_builtin_fun_ext ((n, T), f) =
    2.64    Builtin_Funcs.map (insert_btab U.basicC n T (Ext f))
    2.65 @@ -180,18 +182,6 @@
    2.66  
    2.67  fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
    2.68  
    2.69 -fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
    2.70 -  (case lookup_builtin_fun ctxt c of
    2.71 -    SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
    2.72 -  | _ => false)
    2.73 -
    2.74 -fun is_pred_type T = Term.body_type T = @{typ bool}
    2.75 -fun is_conn_type T =
    2.76 -  forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
    2.77 -
    2.78 -fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
    2.79 -fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
    2.80 -
    2.81  fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
    2.82    (case lookup_builtin_fun ctxt c of
    2.83      SOME (_, Int f) => is_some (f ctxt T ts)
     3.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 08:39:24 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Dec 15 10:12:44 2010 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4    options = (fn ctxt => [
     3.5      "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
     3.6      "-lang", "smtlib", "-output-lang", "presentation"]),
     3.7 -  interface = SMTLIB_Interface.interface,
     3.8 +  class = SMTLIB_Interface.smtlibC,
     3.9    outcome =
    3.10      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    3.11    cex_parser = NONE,
    3.12 @@ -55,7 +55,7 @@
    3.13    options = (fn ctxt => [
    3.14      "--rand-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
    3.15      "--smtlib"]),
    3.16 -  interface = SMTLIB_Interface.interface,
    3.17 +  class = SMTLIB_Interface.smtlibC,
    3.18    outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    3.19    cex_parser = NONE,
    3.20    reconstruct = NONE,
    3.21 @@ -89,7 +89,7 @@
    3.22    env_var = "Z3_SOLVER",
    3.23    is_remote = true,
    3.24    options = z3_options,
    3.25 -  interface = Z3_Interface.interface,
    3.26 +  class = Z3_Interface.smtlib_z3C,
    3.27    outcome = z3_on_last_line,
    3.28    cex_parser = SOME Z3_Model.parse_counterex,
    3.29    reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
     4.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 08:39:24 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 10:12:44 2010 +0100
     4.3 @@ -7,21 +7,18 @@
     4.4  signature SMT_SOLVER =
     4.5  sig
     4.6    (*configuration*)
     4.7 -  type interface = {
     4.8 -    class: SMT_Utils.class,
     4.9 -    translate: SMT_Translate.config }
    4.10    datatype outcome = Unsat | Sat | Unknown
    4.11    type solver_config = {
    4.12      name: string,
    4.13      env_var: string,
    4.14      is_remote: bool,
    4.15      options: Proof.context -> string list,
    4.16 -    interface: interface,
    4.17 +    class: SMT_Utils.class,
    4.18      outcome: string -> string list -> outcome * string list,
    4.19      cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    4.20        term list * term list) option,
    4.21      reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    4.22 -      (int list * thm) * Proof.context) option,
    4.23 +      int list * thm) option,
    4.24      default_max_relevant: int }
    4.25  
    4.26    (*registry*)
    4.27 @@ -57,10 +54,6 @@
    4.28  
    4.29  (* configuration *)
    4.30  
    4.31 -type interface = {
    4.32 -  class: SMT_Utils.class,
    4.33 -  translate: SMT_Translate.config }
    4.34 -
    4.35  datatype outcome = Unsat | Sat | Unknown
    4.36  
    4.37  type solver_config = {
    4.38 @@ -68,12 +61,12 @@
    4.39    env_var: string,
    4.40    is_remote: bool,
    4.41    options: Proof.context -> string list,
    4.42 -  interface: interface,
    4.43 +  class: SMT_Utils.class,
    4.44    outcome: string -> string list -> outcome * string list,
    4.45    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    4.46      term list * term list) option,
    4.47    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    4.48 -    (int list * thm) * Proof.context) option,
    4.49 +    int list * thm) option,
    4.50    default_max_relevant: int }
    4.51  
    4.52  
    4.53 @@ -163,7 +156,7 @@
    4.54  fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o
    4.55    Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
    4.56  
    4.57 -fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
    4.58 +fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) =
    4.59    let
    4.60      fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
    4.61      fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
    4.62 @@ -175,32 +168,20 @@
    4.63          Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
    4.64    end
    4.65  
    4.66 -fun invoke translate_config name cmd options ithms ctxt =
    4.67 +fun invoke name cmd options ithms ctxt =
    4.68    let
    4.69      val args = C.solver_options_of ctxt @ options ctxt
    4.70      val comments = ("solver: " ^ name) ::
    4.71        ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) ::
    4.72        ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) ::
    4.73        "arguments:" :: args
    4.74 -  in
    4.75 -    ithms
    4.76 -    |> tap (trace_assms ctxt)
    4.77 -    |> SMT_Translate.translate translate_config ctxt comments
    4.78 -    ||> tap (trace_recon_data ctxt)
    4.79 -    |>> run_solver ctxt cmd args
    4.80 -    |> rpair ctxt
    4.81 -  end
    4.82  
    4.83 -fun discharge_definitions thm =
    4.84 -  if Thm.nprems_of thm = 0 then thm
    4.85 -  else discharge_definitions (@{thm reflexive} RS thm)
    4.86 -
    4.87 -fun set_has_datatypes with_datatypes translate =
    4.88 -  let val {prefixes, header, is_fol, has_datatypes, serialize} = translate
    4.89 -  in
    4.90 -   {prefixes=prefixes, header=header, is_fol=is_fol,
    4.91 -    has_datatypes=has_datatypes andalso with_datatypes, serialize=serialize}
    4.92 -  end
    4.93 +    val (str, recon as {context=ctxt', ...}) =
    4.94 +      ithms
    4.95 +      |> tap (trace_assms ctxt)
    4.96 +      |> SMT_Translate.translate ctxt comments
    4.97 +      ||> tap trace_recon_data
    4.98 +  in (run_solver ctxt' cmd args str, recon) end
    4.99  
   4.100  fun trace_assumptions ctxt iwthms idxs =
   4.101    let
   4.102 @@ -227,26 +208,21 @@
   4.103    env_var: string,
   4.104    is_remote: bool,
   4.105    options: Proof.context -> string list,
   4.106 -  interface: interface,
   4.107 -  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
   4.108 -    (int list * thm) * Proof.context,
   4.109 +  reconstruct: Proof.context -> string list * SMT_Translate.recon ->
   4.110 +    int list * thm,
   4.111    default_max_relevant: int }
   4.112  
   4.113  fun gen_solver name (info : solver_info) rm ctxt iwthms =
   4.114    let
   4.115 -    val {env_var, is_remote, options, interface, reconstruct, ...} = info
   4.116 -    val {translate, ...} = interface
   4.117 -    val translate' = set_has_datatypes (Config.get ctxt C.datatypes) translate
   4.118 +    val {env_var, is_remote, options, reconstruct, ...} = info
   4.119      val cmd = (rm, env_var, is_remote, name)
   4.120    in
   4.121      SMT_Normalize.normalize ctxt iwthms
   4.122      |> rpair ctxt
   4.123      |-> SMT_Monomorph.monomorph
   4.124 -    |-> invoke translate' name cmd options
   4.125 -    |-> reconstruct
   4.126 -    |-> (fn (idxs, thm) => fn ctxt' => thm
   4.127 -    |> singleton (ProofContext.export ctxt' ctxt)
   4.128 -    |> discharge_definitions
   4.129 +    |-> invoke name cmd options
   4.130 +    |> reconstruct ctxt
   4.131 +    |> (fn (idxs, thm) => thm
   4.132      |> tap (fn _ => trace_assumptions ctxt iwthms idxs)
   4.133      |> pair idxs)
   4.134    end
   4.135 @@ -261,12 +237,13 @@
   4.136  )
   4.137  
   4.138  local
   4.139 -  fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
   4.140 +  fun finish outcome cex_parser reconstruct ocl outer_ctxt
   4.141 +      (output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) =
   4.142      (case outcome output of
   4.143        (Unsat, ls) =>
   4.144          if not (Config.get ctxt C.oracle) andalso is_some reconstruct
   4.145 -        then the reconstruct ctxt recon ls
   4.146 -        else (([], ocl ()), ctxt)
   4.147 +        then the reconstruct outer_ctxt recon ls
   4.148 +        else ([], ocl ())
   4.149      | (result, ls) =>
   4.150          let
   4.151            val (ts, us) =
   4.152 @@ -283,14 +260,12 @@
   4.153  
   4.154  fun add_solver cfg =
   4.155    let
   4.156 -    val {name, env_var, is_remote, options, interface, outcome, cex_parser,
   4.157 +    val {name, env_var, is_remote, options, class, outcome, cex_parser,
   4.158        reconstruct, default_max_relevant} = cfg
   4.159 -    val {class, ...} = interface
   4.160  
   4.161      fun core_oracle () = cfalse
   4.162  
   4.163      fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
   4.164 -      interface=interface,
   4.165        reconstruct=finish (outcome name) cex_parser reconstruct ocl,
   4.166        default_max_relevant=default_max_relevant }
   4.167    in
     5.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 08:39:24 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 10:12:44 2010 +0100
     5.3 @@ -15,7 +15,7 @@
     5.4      SLet of string * sterm * sterm |
     5.5      SQua of squant * string list * sterm spattern list * int option * sterm
     5.6  
     5.7 -  (*configuration options*)
     5.8 +  (*translation configuration*)
     5.9    type prefixes = {sort_prefix: string, func_prefix: string}
    5.10    type sign = {
    5.11      header: string list,
    5.12 @@ -24,17 +24,21 @@
    5.13      funcs: (string * (string list * string)) list }
    5.14    type config = {
    5.15      prefixes: prefixes,
    5.16 -    header: Proof.context -> term list -> string list,
    5.17 +    header: term list -> string list,
    5.18      is_fol: bool,
    5.19      has_datatypes: bool,
    5.20      serialize: string list -> sign -> sterm list -> string }
    5.21    type recon = {
    5.22 +    context: Proof.context,
    5.23      typs: typ Symtab.table,
    5.24      terms: term Symtab.table,
    5.25 -    unfolds: thm list,
    5.26 +    rewrite_rules: thm list,
    5.27      assms: (int * thm) list }
    5.28  
    5.29 -  val translate: config -> Proof.context -> string list -> (int * thm) list ->
    5.30 +  (*translation*)
    5.31 +  val add_config: SMT_Utils.class * (Proof.context -> config) ->
    5.32 +    Context.generic -> Context.generic 
    5.33 +  val translate: Proof.context -> string list -> (int * thm) list ->
    5.34      string * recon
    5.35  end
    5.36  
    5.37 @@ -59,7 +63,7 @@
    5.38  
    5.39  
    5.40  
    5.41 -(* configuration options *)
    5.42 +(* translation configuration *)
    5.43  
    5.44  type prefixes = {sort_prefix: string, func_prefix: string}
    5.45  
    5.46 @@ -71,20 +75,416 @@
    5.47  
    5.48  type config = {
    5.49    prefixes: prefixes,
    5.50 -  header: Proof.context -> term list -> string list,
    5.51 +  header: term list -> string list,
    5.52    is_fol: bool,
    5.53    has_datatypes: bool,
    5.54    serialize: string list -> sign -> sterm list -> string }
    5.55  
    5.56  type recon = {
    5.57 +  context: Proof.context,
    5.58    typs: typ Symtab.table,
    5.59    terms: term Symtab.table,
    5.60 -  unfolds: thm list,
    5.61 +  rewrite_rules: thm list,
    5.62    assms: (int * thm) list }
    5.63  
    5.64  
    5.65  
    5.66 -(* utility functions *)
    5.67 +(* translation context *)
    5.68 +
    5.69 +fun make_tr_context {sort_prefix, func_prefix} =
    5.70 +  (sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty)
    5.71 +
    5.72 +fun string_of_index pre i = pre ^ string_of_int i
    5.73 +
    5.74 +fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) =
    5.75 +  (case Typtab.lookup typs T of
    5.76 +    SOME (n, _) => (n, cx)
    5.77 +  | NONE =>
    5.78 +      let
    5.79 +        val n = string_of_index sp Tidx
    5.80 +        val typs' = Typtab.update (T, (n, proper)) typs
    5.81 +      in (n, (sp, Tidx+1, typs', fp, idx, terms)) end)
    5.82 +
    5.83 +fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) =
    5.84 +  (case Termtab.lookup terms t of
    5.85 +    SOME (n, _) => (n, cx)
    5.86 +  | NONE => 
    5.87 +      let
    5.88 +        val n = string_of_index fp idx
    5.89 +        val terms' = Termtab.update (t, (n, sort)) terms
    5.90 +      in (n, (sp, Tidx, typs, fp, idx+1, terms')) end)
    5.91 +
    5.92 +fun sign_of header dtyps (_, _, typs, _, _, terms) = {
    5.93 +  header = header,
    5.94 +  sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
    5.95 +  dtyps = dtyps,
    5.96 +  funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []}
    5.97 +
    5.98 +fun recon_of ctxt rules thms ithms revertT revert (_, _, typs, _, _, terms) =
    5.99 +  let
   5.100 +    fun add_typ (T, (n, _)) = Symtab.update (n, revertT T)
   5.101 +    val typs' = Typtab.fold add_typ typs Symtab.empty
   5.102 +
   5.103 +    fun add_fun (t, (n, _)) = Symtab.update (n, revert t)
   5.104 +    val terms' = Termtab.fold add_fun terms Symtab.empty
   5.105 +
   5.106 +    val assms = map (pair ~1) thms @ ithms
   5.107 +  in
   5.108 +    {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms}
   5.109 +  end
   5.110 +
   5.111 +
   5.112 +
   5.113 +(* preprocessing *)
   5.114 +
   5.115 +(** mark built-in constants as Var **)
   5.116 +
   5.117 +fun mark_builtins ctxt =
   5.118 +  let
   5.119 +    (*
   5.120 +      Note: schematic terms cannot occur anymore in terms at this stage.
   5.121 +    *)
   5.122 +    fun mark t =
   5.123 +      (case Term.strip_comb t of
   5.124 +        (u as Const (@{const_name If}, _), ts) => marks u ts
   5.125 +      | (u as Const c, ts) =>
   5.126 +          (case B.builtin_num ctxt t of
   5.127 +            SOME (n, T) =>
   5.128 +              let val v = ((n, 0), T)
   5.129 +              in Vartab.update v #> pair (Var v) end
   5.130 +          | NONE =>
   5.131 +              (case B.builtin_fun ctxt c ts of
   5.132 +                SOME ((ni, T), us, U) =>
   5.133 +                  Vartab.update (ni, U) #> marks (Var (ni, T)) us
   5.134 +              | NONE => marks u ts))
   5.135 +      | (Abs (n, T, u), ts) => mark u #-> (fn u' => marks (Abs (n, T, u')) ts)
   5.136 +      | (u, ts) => marks u ts)
   5.137 + 
   5.138 +    and marks t ts = fold_map mark ts #>> Term.list_comb o pair t
   5.139 +
   5.140 +  in (fn ts => swap (fold_map mark ts Vartab.empty)) end
   5.141 +
   5.142 +fun mark_builtins' ctxt t = hd (snd (mark_builtins ctxt [t]))
   5.143 +
   5.144 +
   5.145 +(** FIXME **)
   5.146 +
   5.147 +local
   5.148 +  (*
   5.149 +    mark constructors and selectors as Vars (forcing eta-expansion),
   5.150 +    add missing datatype selectors via hypothetical definitions,
   5.151 +    also return necessary datatype and record theorems
   5.152 +  *)
   5.153 +in
   5.154 +
   5.155 +fun collect_datatypes_and_records (tr_context, ctxt) ts =
   5.156 +  (([], tr_context, ctxt), ts)
   5.157 +
   5.158 +end
   5.159 +
   5.160 +
   5.161 +(** eta-expand quantifiers, let expressions and built-ins *)
   5.162 +
   5.163 +local
   5.164 +  fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t $ Bound 0)
   5.165 +
   5.166 +  fun exp T = eta (Term.domain_type (Term.domain_type T))
   5.167 +
   5.168 +  fun exp2 T q =
   5.169 +    let val U = Term.domain_type T
   5.170 +    in Abs (Name.uu, U, q $ eta (Term.domain_type U) (Bound 0)) end
   5.171 +
   5.172 +  fun exp2' T l =
   5.173 +    let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
   5.174 +    in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
   5.175 +
   5.176 +  fun expf t i T ts =
   5.177 +    let val Ts = U.dest_funT i T |> fst |> drop (length ts)
   5.178 +    in Term.list_comb (t, ts) |> fold_rev eta Ts end
   5.179 +
   5.180 +  fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
   5.181 +    | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
   5.182 +    | expand (q as Const (@{const_name All}, T)) = exp2 T q
   5.183 +    | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
   5.184 +    | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
   5.185 +    | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
   5.186 +    | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
   5.187 +        l $ expand t $ abs_expand a
   5.188 +    | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
   5.189 +        l $ expand t $ exp (Term.range_type T) u
   5.190 +    | expand ((l as Const (@{const_name Let}, T)) $ t) = exp2 T (l $ expand t)
   5.191 +    | expand (l as Const (@{const_name Let}, T)) = exp2' T l
   5.192 +    | expand (Abs a) = abs_expand a
   5.193 +    | expand t =
   5.194 +        (case Term.strip_comb t of
   5.195 +          (u as Const (@{const_name If}, T), ts) => expf u 3 T (map expand ts)
   5.196 +        | (u as Var ((_, i), T), ts) => expf u i T (map expand ts)
   5.197 +        | (u, ts) => Term.list_comb (u, map expand ts))
   5.198 +
   5.199 +  and abs_expand (n, T, t) = Abs (n, T, expand t)
   5.200 +in
   5.201 +
   5.202 +val eta_expand = map expand
   5.203 +
   5.204 +end
   5.205 +
   5.206 +
   5.207 +(** lambda-lifting **)
   5.208 +
   5.209 +local
   5.210 +  fun mk_def Ts T lhs rhs =
   5.211 +    let
   5.212 +      val eq = HOLogic.eq_const T $ lhs $ rhs
   5.213 +      val trigger =
   5.214 +        [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
   5.215 +        |> map (HOLogic.mk_list @{typ SMT.pattern})
   5.216 +        |> HOLogic.mk_list @{typ "SMT.pattern list"}
   5.217 +      fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
   5.218 +    in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end
   5.219 +
   5.220 +  fun replace_lambda Us Ts t (cx as (defs, ctxt)) =
   5.221 +    let
   5.222 +      val T = Term.fastype_of1 (Us @ Ts, t)
   5.223 +      val lev = length Us
   5.224 +      val bs = sort int_ord (Term.add_loose_bnos (t, lev, []))
   5.225 +      val bss = map_index (fn (i, j) => (j, Integer.add lev i)) bs
   5.226 +      val norm = perhaps (AList.lookup (op =) bss)
   5.227 +      val t' = Term.map_aterms (fn Bound i => Bound (norm i) | t => t) t
   5.228 +      val Ts' = map (nth Ts) bs
   5.229 +
   5.230 +      fun mk_abs U u = Abs (Name.uu, U, u)
   5.231 +      val abs_rhs = fold mk_abs Ts' (fold mk_abs Us t')
   5.232 +    in
   5.233 +      (case Termtab.lookup defs abs_rhs of
   5.234 +        SOME (f, _) => (Term.list_comb (f, map Bound bs), cx)
   5.235 +      | NONE =>
   5.236 +          let
   5.237 +            val (n, ctxt') =
   5.238 +              yield_singleton Variable.variant_fixes Name.uu ctxt
   5.239 +            val f = Free (n, rev Ts' ---> (rev Us ---> T))
   5.240 +            fun mk_bapp i t = t $ Bound i
   5.241 +            val lhs =
   5.242 +              f
   5.243 +              |> fold_rev (mk_bapp o snd) bss
   5.244 +              |> fold_rev mk_bapp (0 upto (length Us - 1))
   5.245 +            val def = mk_def (Us @ Ts') T lhs t'
   5.246 +          in (f, (Termtab.update (abs_rhs, (f, def)) defs, ctxt')) end)
   5.247 +    end
   5.248 +
   5.249 +  fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
   5.250 +    | dest_abs Ts t = (Ts, t)
   5.251 +
   5.252 +  fun traverse Ts t =
   5.253 +    (case t of
   5.254 +      (q as Const (@{const_name All}, _)) $ Abs a =>
   5.255 +        abs_traverse Ts a #>> (fn a' => q $ Abs a')
   5.256 +    | (q as Const (@{const_name Ex}, _)) $ Abs a =>
   5.257 +        abs_traverse Ts a #>> (fn a' => q $ Abs a')
   5.258 +    | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
   5.259 +        traverse Ts u ##>> abs_traverse Ts a #>>
   5.260 +        (fn (u', a') => l $ u' $ Abs a')
   5.261 +    | Abs _ =>
   5.262 +        let val (Us, u) = dest_abs [] t
   5.263 +        in traverse (Us @ Ts) u #-> replace_lambda Us Ts end
   5.264 +    | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $)
   5.265 +    | _ => pair t)
   5.266 +
   5.267 +  and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t'))
   5.268 +in
   5.269 +
   5.270 +fun lift_lambdas ctxt ts =
   5.271 +  (Termtab.empty, ctxt)
   5.272 +  |> fold_map (traverse []) ts
   5.273 +  |> (fn (us, (defs, ctxt')) =>
   5.274 +       (ctxt', Termtab.fold (cons o snd o snd) defs us))
   5.275 +
   5.276 +end
   5.277 +
   5.278 +
   5.279 +(** introduce explicit applications **)
   5.280 +
   5.281 +local
   5.282 +  (*
   5.283 +    Make application explicit for functions with varying number of arguments.
   5.284 +  *)
   5.285 +
   5.286 +  fun add t ts =
   5.287 +    Termtab.map_default (t, []) (Ord_List.insert int_ord (length ts))
   5.288 +
   5.289 +  fun collect t =
   5.290 +    (case Term.strip_comb t of
   5.291 +      (u as Const _, ts) => add u ts #> fold collect ts
   5.292 +    | (u as Free _, ts) => add u ts #> fold collect ts
   5.293 +    | (Abs (_, _, u), ts) => collect u #> fold collect ts
   5.294 +    | (_, ts) => fold collect ts)
   5.295 +
   5.296 +  fun app ts (t, T) =
   5.297 +    let val f = Const (@{const_name SMT.fun_app}, T --> T)
   5.298 +    in (Term.list_comb (f $ t, ts), snd (U.dest_funT (length ts) T)) end 
   5.299 +
   5.300 +  fun appl _ _ [] = fst
   5.301 +    | appl _ [] ts = fst o app ts
   5.302 +    | appl i (k :: ks) ts =
   5.303 +        let val (ts1, ts2) = chop (k - i) ts
   5.304 +        in appl k ks ts2 o app ts1 end
   5.305 +
   5.306 +  fun appl0 [_] ts (t, _) = Term.list_comb (t, ts)
   5.307 +    | appl0 (0 :: ks) ts tT = appl 0 ks ts tT
   5.308 +    | appl0 ks ts tT = appl 0 ks ts tT
   5.309 +
   5.310 +  fun apply terms T t ts = appl0 (Termtab.lookup_list terms t) ts (t, T)
   5.311 +
   5.312 +  fun get_arities i t =
   5.313 +    (case Term.strip_comb t of
   5.314 +      (Bound j, ts) =>
   5.315 +        (if i = j then Ord_List.insert int_ord (length ts) else I) #>
   5.316 +        fold (get_arities i) ts
   5.317 +    | (Abs (_, _, u), ts) => get_arities (i+1) u #> fold (get_arities i) ts
   5.318 +    | (_, ts) => fold (get_arities i) ts)
   5.319 +in
   5.320 +
   5.321 +fun intro_explicit_application ts =
   5.322 +  let
   5.323 +    val terms = fold collect ts Termtab.empty
   5.324 +
   5.325 +    fun traverse (env as (arities, Ts)) t =
   5.326 +      (case Term.strip_comb t of
   5.327 +        (u as Const (_, T), ts) => apply terms T u (map (traverse env) ts)
   5.328 +      | (u as Free (_, T), ts) => apply terms T u (map (traverse env) ts)
   5.329 +      | (u as Bound i, ts) =>
   5.330 +          appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i)
   5.331 +      | (Abs (n, T, u), ts) =>
   5.332 +          let val env' = (get_arities 0 u [] :: arities, T :: Ts)
   5.333 +          in traverses env (Abs (n, T, traverse env' u)) ts end
   5.334 +      | (u, ts) => traverses env u ts)
   5.335 +    and traverses env t ts = Term.list_comb (t, map (traverse env) ts)
   5.336 +  in map (traverse ([], [])) ts end
   5.337 +
   5.338 +val fun_app_eq = mk_meta_eq @{thm SMT.fun_app_def}
   5.339 +
   5.340 +end
   5.341 +
   5.342 +
   5.343 +(** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **)
   5.344 +
   5.345 +val tboolT = @{typ SMT.term_bool}
   5.346 +val term_true = Const (@{const_name True}, tboolT)
   5.347 +val term_false = Const (@{const_name False}, tboolT)
   5.348 +
   5.349 +val term_bool = @{lemma "True ~= False" by simp}
   5.350 +val term_bool_prop =
   5.351 +  let
   5.352 +    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
   5.353 +      | replace @{const True} = term_true
   5.354 +      | replace @{const False} = term_false
   5.355 +      | replace t = t
   5.356 +  in
   5.357 +    Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool))
   5.358 +  end
   5.359 +
   5.360 +val fol_rules = [
   5.361 +  Let_def,
   5.362 +  @{lemma "P = True == P" by (rule eq_reflection) simp},
   5.363 +  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   5.364 +
   5.365 +fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
   5.366 +      reduce_let (Term.betapply (u, t))
   5.367 +  | reduce_let (t $ u) = reduce_let t $ reduce_let u
   5.368 +  | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
   5.369 +  | reduce_let t = t
   5.370 +
   5.371 +fun is_pred_type NONE = false
   5.372 +  | is_pred_type (SOME T) = (Term.body_type T = @{typ bool})
   5.373 +
   5.374 +fun is_conn_type NONE = false
   5.375 +  | is_conn_type (SOME T) =
   5.376 +      forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
   5.377 +
   5.378 +fun revert_typ @{typ SMT.term_bool} = @{typ bool}
   5.379 +  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
   5.380 +  | revert_typ T = T
   5.381 +
   5.382 +val revert_types = Term.map_types revert_typ
   5.383 +
   5.384 +fun folify ctxt builtins =
   5.385 +  let
   5.386 +    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
   5.387 +
   5.388 +    fun as_tbool @{typ bool} = tboolT
   5.389 +      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
   5.390 +      | as_tbool T = T
   5.391 +    fun mapTs f g i = U.dest_funT i #> (fn (Ts, T) => map f Ts ---> g T)
   5.392 +    fun predT i = mapTs as_tbool I i
   5.393 +    fun funcT i = mapTs as_tbool as_tbool i
   5.394 +    fun func i (n, T) = (n, funcT i T)
   5.395 +
   5.396 +    fun map_ifT T = T |> Term.dest_funT ||> funcT 2 |> (op -->)
   5.397 +    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
   5.398 +    fun wrap_in_if t = if_term $ t $ term_true $ term_false
   5.399 +
   5.400 +    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
   5.401 +
   5.402 +    fun in_term t =
   5.403 +      (case Term.strip_comb t of
   5.404 +        (Const (n as @{const_name If}, T), [t1, t2, t3]) =>
   5.405 +          Const (n, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
   5.406 +      | (Const (@{const_name HOL.eq}, _), _) => wrap_in_if (in_form t)
   5.407 +      | (Var (ni as (_, i), T), ts) =>
   5.408 +          let val U = Vartab.lookup builtins ni
   5.409 +          in
   5.410 +            if is_conn_type U orelse is_pred_type U then wrap_in_if (in_form t)
   5.411 +            else Term.list_comb (Var (ni, funcT i T), map in_term ts)
   5.412 +          end
   5.413 +      | (Const c, ts) =>
   5.414 +          Term.list_comb (Const (func (length ts) c), map in_term ts)
   5.415 +      | (Free c, ts) =>
   5.416 +          Term.list_comb (Free (func (length ts) c), map in_term ts)
   5.417 +      | _ => t)
   5.418 +
   5.419 +    and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
   5.420 +      | in_weight t = in_form t 
   5.421 +
   5.422 +    and in_pat (Const (c as (@{const_name pat}, _)) $ t) =
   5.423 +          Const (func 1 c) $ in_term t
   5.424 +      | in_pat (Const (c as (@{const_name nopat}, _)) $ t) =
   5.425 +          Const (func 1 c) $ in_term t
   5.426 +      | in_pat t = raise TERM ("bad pattern", [t])
   5.427 +
   5.428 +    and in_pats ps =
   5.429 +      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
   5.430 +
   5.431 +    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
   5.432 +      | in_trig t = in_weight t
   5.433 +
   5.434 +    and in_form t =
   5.435 +      (case Term.strip_comb t of
   5.436 +        (q as Const (qn, _), [Abs (n, T, u)]) =>
   5.437 +          if member (op =) [@{const_name All}, @{const_name Ex}] qn then
   5.438 +            q $ Abs (n, as_tbool T, in_trig u)
   5.439 +          else as_term (in_term t)
   5.440 +      | (u as Const (@{const_name If}, _), ts) =>
   5.441 +          Term.list_comb (u, map in_form ts)
   5.442 +      | (b as @{const HOL.eq (bool)}, ts) => Term.list_comb (b, map in_form ts)
   5.443 +      | (Const (n as @{const_name HOL.eq}, T), ts) =>
   5.444 +          Term.list_comb (Const (n, predT 2 T), map in_term ts)
   5.445 +      | (b as Var (ni as (_, i), T), ts) =>
   5.446 +          if is_conn_type (Vartab.lookup builtins ni) then
   5.447 +            Term.list_comb (b, map in_form ts)
   5.448 +          else if is_pred_type (Vartab.lookup builtins ni) then
   5.449 +            Term.list_comb (Var (ni, predT i T), map in_term ts)
   5.450 +          else as_term (in_term t)
   5.451 +      | _ => as_term (in_term t))
   5.452 +  in
   5.453 +    map (reduce_let #> in_form) #>
   5.454 +    cons (mark_builtins' ctxt term_bool_prop) #>
   5.455 +    pair (fol_rules, [term_bool])
   5.456 +  end
   5.457 +
   5.458 +
   5.459 +
   5.460 +(* translation into intermediate format *)
   5.461 +
   5.462 +(** utility functions **)
   5.463  
   5.464  val quantifier = (fn
   5.465      @{const_name All} => SOME SForall
   5.466 @@ -101,14 +501,14 @@
   5.467  
   5.468  fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
   5.469    | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
   5.470 -  | dest_pat t = raise TERM ("dest_pat", [t])
   5.471 +  | dest_pat t = raise TERM ("bad pattern", [t])
   5.472  
   5.473  fun dest_pats [] = I
   5.474    | dest_pats ts =
   5.475        (case map dest_pat ts |> split_list ||> distinct (op =) of
   5.476          (ps, [true]) => cons (SPat ps)
   5.477        | (ps, [false]) => cons (SNoPat ps)
   5.478 -      | _ => raise TERM ("dest_pats", ts))
   5.479 +      | _ => raise TERM ("bad multi-pattern", ts))
   5.480  
   5.481  fun dest_trigger (@{const trigger} $ tl $ t) =
   5.482        (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
   5.483 @@ -124,233 +524,19 @@
   5.484  fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
   5.485    | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
   5.486  
   5.487 -fun prop_of thm = HOLogic.dest_Trueprop (Thm.prop_of thm)
   5.488  
   5.489 -
   5.490 -
   5.491 -(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
   5.492 -
   5.493 -val tboolT = @{typ SMT.term_bool}
   5.494 -val term_true = Const (@{const_name True}, tboolT)
   5.495 -val term_false = Const (@{const_name False}, tboolT)
   5.496 -
   5.497 -val term_bool = @{lemma "True ~= False" by simp}
   5.498 -val term_bool_prop =
   5.499 -  let
   5.500 -    fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
   5.501 -      | replace @{const True} = term_true
   5.502 -      | replace @{const False} = term_false
   5.503 -      | replace t = t
   5.504 -  in Term.map_aterms replace (prop_of term_bool) end
   5.505 -
   5.506 -val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
   5.507 -    Const (@{const_name Let}, _) => true
   5.508 -  | @{const HOL.eq (bool)} $ _ $ @{const True} => true
   5.509 -  | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
   5.510 -  | _ => false)
   5.511 -
   5.512 -val rewrite_rules = [
   5.513 -  Let_def,
   5.514 -  @{lemma "P = True == P" by (rule eq_reflection) simp},
   5.515 -  @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
   5.516 -
   5.517 -fun rewrite ctxt ct =
   5.518 -  Conv.top_sweep_conv (fn ctxt' =>
   5.519 -    Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
   5.520 -
   5.521 -fun normalize ctxt thm =
   5.522 -  if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
   5.523 -
   5.524 -fun revert_typ @{typ SMT.term_bool} = @{typ bool}
   5.525 -  | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
   5.526 -  | revert_typ T = T
   5.527 -
   5.528 -val revert_types = Term.map_types revert_typ
   5.529 -
   5.530 -fun folify ctxt =
   5.531 -  let
   5.532 -    fun is_builtin_conn (@{const_name True}, _) _ = false
   5.533 -      | is_builtin_conn (@{const_name False}, _) _ = false
   5.534 -      | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
   5.535 -
   5.536 -    fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
   5.537 -
   5.538 -    fun as_tbool @{typ bool} = tboolT
   5.539 -      | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
   5.540 -      | as_tbool T = T
   5.541 -    fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
   5.542 -    fun predT T = mapTs as_tbool I T
   5.543 -    fun funcT T = mapTs as_tbool as_tbool T
   5.544 -    fun func (n, T) = Const (n, funcT T)
   5.545 -
   5.546 -    fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
   5.547 -    val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
   5.548 -    fun wrap_in_if t = if_term $ t $ term_true $ term_false
   5.549 -
   5.550 -    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
   5.551 -
   5.552 -    fun in_term t =
   5.553 -      (case Term.strip_comb t of
   5.554 -        (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
   5.555 -          Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
   5.556 -      | (Const c, ts) =>
   5.557 -          if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
   5.558 -          then wrap_in_if (in_form t)
   5.559 -          else Term.list_comb (func c, map in_term ts)
   5.560 -      | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
   5.561 -      | _ => t)
   5.562 -
   5.563 -    and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
   5.564 -      | in_weight t = in_form t 
   5.565 -
   5.566 -    and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
   5.567 -      | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
   5.568 -      | in_pat t = raise TERM ("in_pat", [t])
   5.569 -
   5.570 -    and in_pats ps =
   5.571 -      in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
   5.572 -
   5.573 -    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
   5.574 -      | in_trig t = in_weight t
   5.575 +(** translation from Isabelle terms into SMT intermediate terms **)
   5.576  
   5.577 -    and in_form t =
   5.578 -      (case Term.strip_comb t of
   5.579 -        (q as Const (qn, _), [Abs (n, T, t')]) =>
   5.580 -          if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
   5.581 -          else as_term (in_term t)
   5.582 -      | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
   5.583 -          if B.is_builtin_fun ctxt c [t'] then
   5.584 -            Const (n, predT T) $ in_list T in_term t'
   5.585 -          else as_term (in_term t)
   5.586 -      | (Const (c as (n, T)), ts) =>
   5.587 -          if B.is_builtin_conn ctxt c ts
   5.588 -          then Term.list_comb (Const c, map in_form ts)
   5.589 -          else if B.is_builtin_pred ctxt c ts
   5.590 -          then Term.list_comb (Const (n, predT T), map in_term ts)
   5.591 -          else as_term (in_term t)
   5.592 -      | _ => as_term (in_term t))
   5.593 -  in
   5.594 -    map (apsnd (normalize ctxt)) #> (fn irules =>
   5.595 -    ((rewrite_rules, (~1, term_bool) :: irules),
   5.596 -     term_bool_prop :: map (in_form o prop_of o snd) irules))
   5.597 -  end
   5.598 -
   5.599 -
   5.600 -
   5.601 -(* translation from Isabelle terms into SMT intermediate terms *)
   5.602 -
   5.603 -val empty_context = (1, Typtab.empty, [], 1, Termtab.empty)
   5.604 -
   5.605 -fun make_sign header (_, typs, dtyps, _, terms) = {
   5.606 -  header = header,
   5.607 -  sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [],
   5.608 -  funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms [],
   5.609 -  dtyps = rev dtyps }
   5.610 -
   5.611 -fun make_recon (unfolds, assms) (_, typs, _, _, terms) = {
   5.612 -  typs = Symtab.make (map (apfst fst o swap) (Typtab.dest typs)),
   5.613 -    (*FIXME: don't drop the datatype information! *)
   5.614 -  terms = Symtab.make (map (fn (t, (n, _)) => (n, t)) (Termtab.dest terms)),
   5.615 -  unfolds = unfolds,
   5.616 -  assms = assms }
   5.617 -
   5.618 -fun string_of_index pre i = pre ^ string_of_int i
   5.619 -
   5.620 -fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
   5.621 +fun intermediate header dtyps ctxt ts trx =
   5.622    let
   5.623 -    val s = string_of_index sort_prefix Tidx
   5.624 -    val U = revert_typ T
   5.625 -  in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
   5.626 -
   5.627 -fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
   5.628 -
   5.629 -fun fresh_typ T f cx =
   5.630 -  (case lookup_typ cx T of
   5.631 -    SOME (s, _) => (s, cx)
   5.632 -  | NONE => f T cx)
   5.633 -
   5.634 -fun new_fun func_prefix t ss (Tidx, typs, dtyps, idx, terms) =
   5.635 -  let
   5.636 -    val f = string_of_index func_prefix idx
   5.637 -    val terms' = Termtab.update (revert_types t, (f, ss)) terms
   5.638 -  in (f, (Tidx, typs, dtyps, idx+1, terms')) end
   5.639 -
   5.640 -fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
   5.641 -  (case Termtab.lookup terms (revert_types t) of
   5.642 -    SOME (f, _) => (f, cx)
   5.643 -  | NONE => new_fun func_prefix t ss cx)
   5.644 -
   5.645 -fun mk_type (_, Tfs) (d as Datatype.DtTFree _) = the (AList.lookup (op =) Tfs d)
   5.646 -  | mk_type Ts (Datatype.DtType (n, ds)) = Type (n, map (mk_type Ts) ds)
   5.647 -  | mk_type (Tds, _) (Datatype.DtRec i) = nth Tds i
   5.648 -
   5.649 -fun mk_selector ctxt Ts T n (i, d) =
   5.650 -  (case Datatype_Selectors.lookup_selector ctxt (n, i+1) of
   5.651 -    NONE => raise Fail ("missing selector for datatype constructor " ^ quote n)
   5.652 -  | SOME m => mk_type Ts d |> (fn U => (Const (m, T --> U), U)))
   5.653 -
   5.654 -fun mk_constructor ctxt Ts T (n, args) =
   5.655 -  let val (sels, Us) = split_list (map_index (mk_selector ctxt Ts T n) args)
   5.656 -  in (Const (n, Us ---> T), sels) end
   5.657 -
   5.658 -fun lookup_datatype ctxt n Ts =
   5.659 -  if member (op =) [@{type_name bool}, @{type_name nat}] n then NONE
   5.660 -  else
   5.661 -    Datatype.get_info (ProofContext.theory_of ctxt) n
   5.662 -    |> Option.map (fn {descr, ...} =>
   5.663 -         let
   5.664 -           val Tds = map (fn (_, (tn, _, _)) => Type (tn, Ts))
   5.665 -             (sort (int_ord o pairself fst) descr)
   5.666 -           val Tfs = (case hd descr of (_, (_, tfs, _)) => tfs ~~ Ts)
   5.667 -         in
   5.668 -           descr |> map (fn (i, (_, _, cs)) =>
   5.669 -             (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs))
   5.670 -         end)
   5.671 -
   5.672 -fun relaxed irules = (([], irules), map (prop_of o snd) irules)
   5.673 -
   5.674 -fun with_context header f (ths, ts) =
   5.675 -  let val (us, context) = fold_map f ts empty_context
   5.676 -  in ((make_sign (header ts) context, us), make_recon ths context) end
   5.677 -
   5.678 -
   5.679 -fun translate config ctxt comments =
   5.680 -  let
   5.681 -    val {prefixes, is_fol, header, has_datatypes, serialize} = config
   5.682 -    val {sort_prefix, func_prefix} = prefixes
   5.683 -
   5.684 -    fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
   5.685 -      | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
   5.686 -      | transT (T as Type (n, Ts)) =
   5.687 +    fun transT (T as TFree _) = add_typ T true
   5.688 +      | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
   5.689 +      | transT (T as Type _) =
   5.690            (case B.builtin_typ ctxt T of
   5.691              SOME n => pair n
   5.692 -          | NONE => fresh_typ T (fn _ => fn cx =>
   5.693 -              if not has_datatypes then new_typ sort_prefix true T cx
   5.694 -              else
   5.695 -                (case lookup_datatype ctxt n Ts of
   5.696 -                  NONE => new_typ sort_prefix true T cx
   5.697 -                | SOME dts =>
   5.698 -                    let val cx' = new_dtyps dts cx 
   5.699 -                    in (fst (the (lookup_typ cx' T)), cx') end)))
   5.700 +          | NONE => add_typ T true)
   5.701  
   5.702 -    and new_dtyps dts cx =
   5.703 -      let
   5.704 -        fun new_decl i t =
   5.705 -          let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
   5.706 -          in
   5.707 -            fold_map transT Ts ##>> transT T ##>>
   5.708 -            new_fun func_prefix t NONE #>> swap
   5.709 -          end
   5.710 -        fun new_dtyp_decl (con, sels) =
   5.711 -          new_decl (length sels) con ##>> fold_map (new_decl 1) sels #>>
   5.712 -          (fn ((con', _), sels') => (con', map (apsnd snd) sels'))
   5.713 -      in
   5.714 -        cx
   5.715 -        |> fold_map (new_typ sort_prefix false o fst) dts
   5.716 -        ||>> fold_map (fold_map new_dtyp_decl o snd) dts
   5.717 -        |-> (fn (ss, decls) => fn (Tidx, typs, dtyps, idx, terms) =>
   5.718 -              (Tidx, typs, (ss ~~ decls) :: dtyps, idx, terms))
   5.719 -      end
   5.720 +    val unmarked_builtins = [@{const_name If}, @{const_name HOL.eq}]
   5.721  
   5.722      fun app n ts = SApp (n, ts)
   5.723  
   5.724 @@ -361,37 +547,84 @@
   5.725              SOME (q, Ts, ps, w, b) =>
   5.726                fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
   5.727                trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
   5.728 -          | NONE => raise TERM ("intermediate", [t]))
   5.729 +          | NONE => raise TERM ("unsupported quantifier", [t]))
   5.730        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
   5.731            transT T ##>> trans t1 ##>> trans t2 #>>
   5.732            (fn ((U, u1), u2) => SLet (U, u1, u2))
   5.733 -      | (h as Const (c as (@{const_name distinct}, T)), ts) =>
   5.734 -          (case B.builtin_fun ctxt c ts of
   5.735 -            SOME (n, ts) => fold_map trans ts #>> app n
   5.736 -          | NONE => transs h T ts)
   5.737 -      | (h as Const (c as (_, T)), ts) =>
   5.738 -          (case B.builtin_num ctxt t of
   5.739 -            SOME n => pair (SApp (n, []))
   5.740 -          | NONE =>
   5.741 -              (case B.builtin_fun ctxt c ts of
   5.742 -                SOME (n, ts') => fold_map trans ts' #>> app n
   5.743 -              | NONE => transs h T ts))
   5.744 -      | (h as Free (_, T), ts) => transs h T ts
   5.745 +      | (Var ((n, _), _), ts) => fold_map trans ts #>> app n
   5.746 +      | (u as Const (c as (n, T)), ts) =>
   5.747 +          if member (op =) unmarked_builtins n then
   5.748 +            (case B.builtin_fun ctxt c ts of
   5.749 +              SOME (((m, _), _), us, _) => fold_map trans us #>> app m
   5.750 +            | NONE => raise TERM ("not a built-in symbol", [t]))
   5.751 +          else transs u T ts
   5.752 +      | (u as Free (_, T), ts) => transs u T ts
   5.753        | (Bound i, []) => pair (SVar i)
   5.754 -      | (Abs (_, _, t1 $ Bound 0), []) =>
   5.755 -        if not (loose_bvar1 (t1, 0)) then trans t1 (* eta-reduce on the fly *)
   5.756 -        else raise TERM ("smt_translate", [t])
   5.757 -      | _ => raise TERM ("smt_translate", [t]))
   5.758 -
   5.759 +      | _ => raise TERM ("bad SMT term", [t]))
   5.760 + 
   5.761      and transs t T ts =
   5.762        let val (Us, U) = U.dest_funT (length ts) T
   5.763        in
   5.764          fold_map transT Us ##>> transT U #-> (fn Up =>
   5.765 -        fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
   5.766 +        add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
   5.767        end
   5.768 +
   5.769 +    val (us, trx') = fold_map trans ts trx
   5.770 +  in ((sign_of (header ts) dtyps trx', us), trx') end
   5.771 +
   5.772 +
   5.773 +
   5.774 +(* translation *)
   5.775 +
   5.776 +structure Configs = Generic_Data
   5.777 +(
   5.778 +  type T = (Proof.context -> config) U.dict
   5.779 +  val empty = []
   5.780 +  val extend = I
   5.781 +  val merge = U.dict_merge fst
   5.782 +)
   5.783 +
   5.784 +fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))
   5.785 +
   5.786 +fun translate ctxt comments ithms =
   5.787 +  let
   5.788 +    val cs = SMT_Config.solver_class_of ctxt
   5.789 +    val {prefixes, is_fol, header, has_datatypes, serialize} =
   5.790 +      (case U.dict_get (Configs.get (Context.Proof ctxt)) cs of
   5.791 +        SOME cfg => cfg ctxt
   5.792 +      | NONE => error ("SMT: no translation configuration found " ^
   5.793 +          "for solver class " ^ quote (U.string_of_class cs)))
   5.794 +      
   5.795 +    val with_datatypes =
   5.796 +      has_datatypes andalso Config.get ctxt SMT_Config.datatypes
   5.797 +
   5.798 +    fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts)
   5.799 +
   5.800 +    val (builtins, ts1) =
   5.801 +      ithms
   5.802 +      |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd)
   5.803 +      |> map (Envir.eta_contract o Envir.beta_norm)
   5.804 +      |> mark_builtins ctxt
   5.805 +
   5.806 +    val ((dtyps, tr_context, ctxt1), ts2) =
   5.807 +      ((make_tr_context prefixes, ctxt), ts1)
   5.808 +      |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps)
   5.809 +
   5.810 +    val (ctxt2, ts3) =
   5.811 +      ts2
   5.812 +      |> eta_expand
   5.813 +      |> lift_lambdas ctxt1
   5.814 +      ||> intro_explicit_application
   5.815 +
   5.816 +    val ((rewrite_rules, extra_thms), ts4) =
   5.817 +      (if is_fol then folify ctxt2 builtins else pair ([], [])) ts3
   5.818 +
   5.819 +    val rewrite_rules' = fun_app_eq :: rewrite_rules
   5.820    in
   5.821 -    (if is_fol then folify ctxt else relaxed) #>
   5.822 -    with_context (header ctxt) trans #>> uncurry (serialize comments)
   5.823 +    (ts4, tr_context)
   5.824 +    |-> intermediate header dtyps ctxt2
   5.825 +    |>> uncurry (serialize comments)
   5.826 +    ||> recon_of ctxt2 rewrite_rules' extra_thms ithms revert_typ revert_types
   5.827    end
   5.828  
   5.829  end
     6.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 08:39:24 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 10:12:44 2010 +0100
     6.3 @@ -13,11 +13,13 @@
     6.4    (*class dictionaries*)
     6.5    type class = string list
     6.6    val basicC: class
     6.7 +  val string_of_class: class -> string
     6.8    type 'a dict = (class * 'a) Ord_List.T
     6.9    val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict
    6.10    val dict_update: class * 'a -> 'a dict -> 'a dict
    6.11    val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict
    6.12    val dict_lookup: 'a dict -> class -> 'a list
    6.13 +  val dict_get: 'a dict -> class -> 'a option
    6.14  
    6.15    (*types*)
    6.16    val dest_funT: int -> typ -> typ list * typ
    6.17 @@ -76,6 +78,9 @@
    6.18  
    6.19  val basicC = []
    6.20  
    6.21 +fun string_of_class [] = "basic"
    6.22 +  | string_of_class cs = "basic." ^ space_implode "." cs
    6.23 +
    6.24  type 'a dict = (class * 'a) Ord_List.T
    6.25  
    6.26  fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2)
    6.27 @@ -95,6 +100,11 @@
    6.28    let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE
    6.29    in map_filter match d end
    6.30  
    6.31 +fun dict_get d cs =
    6.32 +  (case AList.lookup (op =) d cs of
    6.33 +    NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs))
    6.34 +  | SOME x => SOME x)
    6.35 +
    6.36  
    6.37  (* types *)
    6.38  
     7.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Dec 15 08:39:24 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Dec 15 10:12:44 2010 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4    val smtlibC: SMT_Utils.class
     7.5    val add_logic: int * (term list -> string option) -> Context.generic ->
     7.6      Context.generic
     7.7 -  val interface: SMT_Solver.interface
     7.8 +  val translate_config: Proof.context -> SMT_Translate.config
     7.9    val setup: theory -> theory
    7.10  end
    7.11  
    7.12 @@ -28,9 +28,13 @@
    7.13  local
    7.14    fun int_num _ i = SOME (string_of_int i)
    7.15  
    7.16 -  fun distinct _ _ [t] =
    7.17 +  fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
    7.18          (case try HOLogic.dest_list t of
    7.19 -          SOME (ts as _ :: _) => SOME ("distinct", ts)
    7.20 +          SOME (ts as _ :: _) =>
    7.21 +            let
    7.22 +              fun mkT U = replicate (length ts) U ---> @{typ bool}
    7.23 +              val U = mkT T and U' = mkT (TVar (("'a", 0), @{sort type}))
    7.24 +            in SOME ((("distinct", length ts), U), ts, U') end
    7.25          | _ => NONE)
    7.26      | distinct _ _ _ = NONE
    7.27  in
    7.28 @@ -40,7 +44,6 @@
    7.29    fold (B.add_builtin_fun' smtlibC) [
    7.30      (@{const True}, "true"),
    7.31      (@{const False}, "false"),
    7.32 - (* FIXME: we do not test if these constants are fully applied! *)
    7.33      (@{const Not}, "not"),
    7.34      (@{const HOL.conj}, "and"),
    7.35      (@{const HOL.disj}, "or"),
    7.36 @@ -145,17 +148,17 @@
    7.37  
    7.38  (* interface *)
    7.39  
    7.40 -val interface = {
    7.41 -  class = smtlibC,
    7.42 -  translate = {
    7.43 -    prefixes = {
    7.44 -      sort_prefix = "S",
    7.45 -      func_prefix = "f"},
    7.46 -    header = choose_logic,
    7.47 -    is_fol = true,
    7.48 -    has_datatypes = false,
    7.49 -    serialize = serialize}}
    7.50 +fun translate_config ctxt = {
    7.51 +  prefixes = {
    7.52 +    sort_prefix = "S",
    7.53 +    func_prefix = "f"},
    7.54 +  header = choose_logic ctxt,
    7.55 +  is_fol = true,
    7.56 +  has_datatypes = false,
    7.57 +  serialize = serialize}
    7.58  
    7.59 -val setup = Context.theory_map setup_builtins
    7.60 +val setup = Context.theory_map (
    7.61 +  setup_builtins #>
    7.62 +  T.add_config (smtlibC, translate_config))
    7.63  
    7.64  end
     8.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 15 08:39:24 2010 +0100
     8.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 15 10:12:44 2010 +0100
     8.3 @@ -7,7 +7,6 @@
     8.4  signature Z3_INTERFACE =
     8.5  sig
     8.6    val smtlib_z3C: SMT_Utils.class
     8.7 -  val interface: SMT_Solver.interface
     8.8    val setup: theory -> theory
     8.9  
    8.10    datatype sym = Sym of string * sym list
    8.11 @@ -36,8 +35,14 @@
    8.12  (* interface *)
    8.13  
    8.14  local
    8.15 -  val {translate, extra_norm, ...} = SMTLIB_Interface.interface
    8.16 -  val {prefixes, is_fol, header, serialize, ...} = translate
    8.17 +  fun translate_config ctxt =
    8.18 +    let
    8.19 +      val {prefixes, header, is_fol, serialize, ...} =
    8.20 +        SMTLIB_Interface.translate_config ctxt
    8.21 +    in
    8.22 +      {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize,
    8.23 +        has_datatypes=true}
    8.24 +    end
    8.25  
    8.26    fun is_int_div_mod @{const div (int)} = true
    8.27      | is_int_div_mod @{const mod (int)} = true
    8.28 @@ -56,18 +61,10 @@
    8.29      B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    8.30  in
    8.31  
    8.32 -val interface = {
    8.33 -  class = smtlib_z3C,
    8.34 -  translate = {
    8.35 -    prefixes = prefixes,
    8.36 -    is_fol = is_fol,
    8.37 -    header = header,
    8.38 -    has_datatypes = true,
    8.39 -    serialize = serialize}}
    8.40 -
    8.41  val setup = Context.theory_map (
    8.42    setup_builtins #>
    8.43 -  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod))
    8.44 +  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
    8.45 +  SMT_Translate.add_config (smtlib_z3C, translate_config))
    8.46  
    8.47  end
    8.48  
    8.49 @@ -154,11 +151,8 @@
    8.50    | mk_distinct (cts as (ct :: _)) =
    8.51        Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
    8.52  
    8.53 -val access = U.mk_const_pat @{theory} @{const_name fun_app}
    8.54 -  (Thm.dest_ctyp o U.destT1)
    8.55 -fun mk_access array index =
    8.56 -  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
    8.57 -  in Thm.mk_binop (U.instTs cTs access) array index end
    8.58 +val access = U.mk_const_pat @{theory} @{const_name fun_app} U.destT1
    8.59 +fun mk_access array = Thm.capply (U.instT' array access) array
    8.60  
    8.61  val update = U.mk_const_pat @{theory} @{const_name fun_upd}
    8.62    (Thm.dest_ctyp o U.destT1)
    8.63 @@ -189,7 +183,7 @@
    8.64    | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3)
    8.65    | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
    8.66    | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
    8.67 -  | (Sym ("select", _), [ca, ck]) => SOME (mk_access ca ck)
    8.68 +  | (Sym ("select", _), [ca, ck]) => SOME (Thm.capply (mk_access ca) ck)
    8.69    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
    8.70    | _ =>
    8.71      (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
     9.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 08:39:24 2010 +0100
     9.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 10:12:44 2010 +0100
     9.3 @@ -8,7 +8,7 @@
     9.4  sig
     9.5    val add_z3_rule: thm -> Context.generic -> Context.generic
     9.6    val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
     9.7 -    (int list * thm) * Proof.context
     9.8 +    int list * thm
     9.9    val setup: theory -> theory
    9.10  end
    9.11  
    9.12 @@ -160,15 +160,17 @@
    9.13      | _ => z3_exn ("not asserted: " ^
    9.14          quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
    9.15  in
    9.16 -fun prepare_assms ctxt unfolds assms =
    9.17 +fun prepare_assms ctxt rewrite_rules assms =
    9.18    let
    9.19 -    val unfolds' = rewrites I ctxt [L.rewrite_true] unfolds
    9.20 +    val eqs = rewrites I ctxt [L.rewrite_true] rewrite_rules
    9.21      val assms' =
    9.22 -      rewrites apsnd ctxt (union Thm.eq_thm unfolds' prep_rules) assms
    9.23 -  in (unfolds', T.thm_net_of snd assms') end
    9.24 +      assms
    9.25 +      |> rewrites apsnd ctxt (union Thm.eq_thm eqs prep_rules)
    9.26 +      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
    9.27 +  in (eqs, T.thm_net_of snd assms') end
    9.28  
    9.29 -fun asserted ctxt (unfolds, assms) ct =
    9.30 -  let val revert_conv = rewrite_conv ctxt unfolds
    9.31 +fun asserted ctxt (eqs, assms) ct =
    9.32 +  let val revert_conv = rewrite_conv ctxt eqs then_conv Thm.eta_conversion
    9.33    in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end
    9.34  
    9.35  fun find_assm ctxt (unfolds, assms) ct =
    9.36 @@ -835,6 +837,22 @@
    9.37        (fn idx => result o lookup idx o pair ctxt o Inttab.map (K Unproved))
    9.38      end
    9.39  
    9.40 +  val disch_rules = map (pair false)
    9.41 +    [@{thm allI}, @{thm refl}, @{thm reflexive}]
    9.42 +
    9.43 +  fun disch_assm thm =
    9.44 +    if Thm.nprems_of thm = 0 then Drule.flexflex_unique thm
    9.45 +    else
    9.46 +      (case Seq.pull (Thm.biresolution false disch_rules 1 thm) of
    9.47 +        SOME (thm', _) => disch_assm thm'
    9.48 +      | NONE => raise THM ("failed to discharge premise", 1, [thm]))
    9.49 +
    9.50 +  fun discharge outer_ctxt (thm, inner_ctxt) =
    9.51 +    thm
    9.52 +    |> singleton (ProofContext.export inner_ctxt outer_ctxt)
    9.53 +    |> tap (tracing o prefix "final goal: " o PolyML.makestring)
    9.54 +    |> disch_assm    
    9.55 +
    9.56    fun filter_assms ctxt assms ptab =
    9.57      let
    9.58        fun step r ct =
    9.59 @@ -851,14 +869,18 @@
    9.60      in lookup end
    9.61  in
    9.62  
    9.63 -fun reconstruct ctxt {typs, terms, unfolds, assms} output =
    9.64 +fun reconstruct outer_ctxt recon output =
    9.65    let
    9.66 -    val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
    9.67 -    val assms' = prepare_assms cx unfolds assms
    9.68 +    val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
    9.69 +    val (idx, (ptab, vars, ctxt')) = P.parse ctxt typs terms output
    9.70 +    val assms' = prepare_assms ctxt' rewrite_rules assms
    9.71    in
    9.72 -    if Config.get cx SMT_Config.filter_only_facts
    9.73 -    then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
    9.74 -    else apfst (pair []) (prove cx assms' vars idx ptab)
    9.75 +    if Config.get ctxt' SMT_Config.filter_only_facts then
    9.76 +      (filter_assms ctxt' assms' ptab idx [], @{thm TrueI})
    9.77 +    else
    9.78 +      prove ctxt' assms' vars idx ptab
    9.79 +      |> discharge outer_ctxt
    9.80 +      |> pair []
    9.81    end
    9.82  
    9.83  end
    10.1 --- a/src/HOL/Word/Tools/smt_word.ML	Wed Dec 15 08:39:24 2010 +0100
    10.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Wed Dec 15 10:12:44 2010 +0100
    10.3 @@ -59,12 +59,19 @@
    10.4      | word_num _ _ = NONE
    10.5  
    10.6    fun if_fixed n T ts =
    10.7 -    let val (Ts, T) = Term.strip_type T
    10.8 -    in if forall (can dest_wordT) (T :: Ts) then SOME (n, ts) else NONE end
    10.9 +    let val (Us, U) = Term.strip_type T
   10.10 +    in
   10.11 +      if forall (can dest_wordT) (U :: Us) then
   10.12 +        SOME (((n, length Us), T), ts, T)
   10.13 +      else NONE
   10.14 +    end
   10.15  
   10.16    fun if_fixed' n T ts =
   10.17 -    if forall (can dest_wordT) (Term.binder_types T) then SOME (n, ts)
   10.18 -    else NONE
   10.19 +    let val Ts = Term.binder_types T
   10.20 +    in
   10.21 +      if forall (can dest_wordT) Ts then SOME (((n, length Ts), T), ts, T)
   10.22 +      else NONE
   10.23 +    end
   10.24  
   10.25    fun add_word_fun f (t, n) =
   10.26      B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n))
   10.27 @@ -79,28 +86,37 @@
   10.28      (dest_word_funT (Term.range_type T), dest_nat ts)
   10.29  
   10.30    fun shift n T ts =
   10.31 -    let val U = Term.domain_type T
   10.32 +    let
   10.33 +      val U = Term.domain_type T
   10.34 +      val T' = [U, U] ---> U
   10.35      in
   10.36 -      (case (can dest_wordT U, ts) of
   10.37 +      (case (can dest_wordT T', ts) of
   10.38          (true, [t, u]) =>
   10.39            (case try HOLogic.dest_number u of
   10.40 -            SOME (_,i) => SOME (n, [t, HOLogic.mk_number U i])
   10.41 +            SOME (_, i) => SOME (((n, 2), T'), [t, HOLogic.mk_number T' i], T')
   10.42            | NONE => NONE)  (* FIXME: also support non-numerical shifts *)
   10.43        | _ => NONE)
   10.44      end
   10.45  
   10.46    fun extract n T ts =
   10.47      try dest_nat_word_funT (T, ts)
   10.48 -    |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
   10.49 +    |> Option.map (fn ((_, i), (lb, ts')) =>
   10.50 +         let val T' = Term.range_type T
   10.51 +         in (((index2 n (i + lb - 1) lb, 1), T'), ts', T') end)
   10.52  
   10.53    fun extend n T ts =
   10.54      (case try dest_word_funT T of
   10.55 -      SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
   10.56 +      SOME (i, j) =>
   10.57 +        if j-i >= 0 then SOME (((index1 n (j-i), 1), T), ts, T)
   10.58 +        else NONE
   10.59      | _ => NONE)
   10.60  
   10.61    fun rotate n T ts =
   10.62 -    try dest_nat ts
   10.63 -    |> Option.map (fn (i, ts') => (index1 n i, ts'))
   10.64 +    let val T' = Term.range_type T
   10.65 +    in
   10.66 +      try dest_nat ts
   10.67 +      |> Option.map (fn (i, ts') => (((index1 n i, 1), T'), ts', T'))
   10.68 +    end
   10.69  in
   10.70  
   10.71  val setup_builtins =