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