--- a/src/HOL/SMT.thy Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/SMT.thy Wed Dec 15 18:20:44 2010 +0100
@@ -11,7 +11,7 @@
"Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_failure.ML"
"Tools/SMT/smt_config.ML"
- "Tools/SMT/smt_monomorph.ML"
+ ("Tools/SMT/smt_monomorph.ML")
("Tools/SMT/smt_builtin.ML")
("Tools/SMT/smt_normalize.ML")
("Tools/SMT/smt_translate.ML")
@@ -149,6 +149,7 @@
subsection {* Setup *}
+use "Tools/SMT/smt_monomorph.ML"
use "Tools/SMT/smt_builtin.ML"
use "Tools/SMT/smt_normalize.ML"
use "Tools/SMT/smt_translate.ML"
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 18:20:44 2010 +0100
@@ -45,8 +45,19 @@
fun is_const pred (n, T) = not (ignored n) andalso pred T
fun collect_consts_if pred f =
- Thm.prop_of #>
- Term.fold_aterms (fn Const c => if is_const pred c then f c else I | _ => I)
+ let
+ fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
+ | collect (t $ u) = collect t #> collect u
+ | collect (Abs (_, _, t)) = collect t
+ | collect (Const c) = if is_const pred c then f c else I
+ | collect _ = I
+ and collect_trigger t =
+ let val dest = these o try HOLogic.dest_list
+ in fold (fold collect_pat o dest) (dest t) end
+ and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
+ | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
+ | collect_pat _ = I
+ in collect o Thm.prop_of end
val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 18:20:44 2010 +0100
@@ -141,7 +141,7 @@
"must have the same kind: " ^ Syntax.string_of_term ctxt t)
fun check_trigger_conv ctxt ct =
- if proper_quant false proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+ if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
else check_trigger_error ctxt (Thm.term_of ct)
@@ -183,7 +183,7 @@
(case pairself (minimal_pats vs) (Thm.dest_comb ct) of
([], []) => [[ct]]
| (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
- | _ => [[ct]])
+ | _ => [])
else []
fun proper_mpat _ _ _ [] = false
@@ -227,8 +227,11 @@
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
+ fun has_trigger (@{const SMT.trigger} $ _ $ _) = true
+ | has_trigger _ = false
+
fun try_trigger_conv cv ct =
- if proper_quant false (K false) (Thm.term_of ct) then Conv.all_conv ct
+ if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
else Conv.try_conv cv ct
fun infer_trigger_conv ctxt =
@@ -256,20 +259,20 @@
fun is_weight (@{const SMT.weight} $ w $ t) =
(case try HOLogic.dest_number w of
- SOME (_, i) => i > 0 andalso has_no_weight t
+ SOME (_, i) => i >= 0 andalso has_no_weight t
| _ => false)
| is_weight t = has_no_weight t
fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
- | proper_trigger t = has_no_weight t
+ | proper_trigger t = is_weight t
fun check_weight_error ctxt t =
- error ("SMT weight must be a positive number and must only occur " ^
+ error ("SMT weight must be a non-negative number and must only occur " ^
"under the top-most quantifier and an optional trigger: " ^
Syntax.string_of_term ctxt t)
fun check_weight_conv ctxt ct =
- if U.under_quant proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+ if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
else check_weight_error ctxt (Thm.term_of ct)
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 18:20:44 2010 +0100
@@ -147,6 +147,8 @@
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) =>
@@ -378,9 +380,7 @@
| replace @{const True} = term_true
| replace @{const False} = term_false
| replace t = t
- in
- Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool))
- end
+ in Term.map_aterms replace (U.prop_of term_bool) end
val fol_rules = [
Let_def,
@@ -496,14 +496,7 @@
| group_quant _ Ts t = (Ts, t)
fun dest_weight (@{const SMT.weight} $ w $ t) =
- ((SOME (snd (HOLogic.dest_number w)), t)
- handle TERM _ =>
- (case w of
- Var ((s, _), _) => (* FIXME: temporary workaround *)
- (case Int.fromString s of
- SOME n => (SOME n, t)
- | NONE => raise TERM ("bad weight", [w]))
- | _ => raise TERM ("bad weight", [w])))
+ (SOME (snd (HOLogic.dest_number w)), t)
| dest_weight t = (NONE, t)
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
@@ -609,8 +602,7 @@
val (builtins, ts1) =
ithms
- |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd)
- |> map (Envir.eta_contract o Envir.beta_norm)
+ |> map (Envir.beta_eta_contract o U.prop_of o snd)
|> mark_builtins ctxt
val ((dtyps, tr_context, ctxt1), ts2) =
--- a/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 18:20:44 2010 +0100
@@ -47,6 +47,8 @@
val mk_cprop: cterm -> cterm
val dest_cprop: cterm -> cterm
val mk_cequals: cterm -> cterm -> cterm
+ val term_of: cterm -> term
+ val prop_of: thm -> term
(*conversions*)
val if_conv: (term -> bool) -> conv -> conv -> conv
@@ -177,6 +179,10 @@
val equals = mk_const_pat @{theory} @{const_name "=="} destT1
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
+fun term_of ct = dest_prop (Thm.term_of ct)
+fun prop_of thm = dest_prop (Thm.prop_of thm)
+
(* conversions *)
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 18:20:44 2010 +0100
@@ -33,6 +33,7 @@
structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
struct
+structure U = SMT_Utils
structure T = Z3_Proof_Tools
@@ -41,10 +42,10 @@
type littab = thm Termtab.table
-fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
+fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
-fun insert_lit thm = Termtab.update (`T.prop_of thm)
-fun delete_lit thm = Termtab.delete (T.prop_of thm)
+fun insert_lit thm = Termtab.update (`U.prop_of thm)
+fun delete_lit thm = Termtab.delete (U.prop_of thm)
fun lookup_lit lits = Termtab.lookup lits
fun get_first_lit f =
Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
@@ -161,9 +162,9 @@
val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
fun explode1 thm =
- if Termtab.defined tab (T.prop_of thm) then cons thm
+ if Termtab.defined tab (U.prop_of thm) then cons thm
else
- (case dest_rules (T.prop_of thm) of
+ (case dest_rules (U.prop_of thm) of
SOME (rule1, rule2) =>
explode2 rule1 thm #>
explode2 rule2 thm #>
@@ -171,12 +172,12 @@
| NONE => cons thm)
and explode2 dest_rule thm =
- if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
+ if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm)
then explode1 (T.compose dest_rule thm)
else cons (T.compose dest_rule thm)
fun explode0 thm =
- if not is_conj andalso is_dneg (T.prop_of thm)
+ if not is_conj andalso is_dneg (U.prop_of thm)
then [T.compose dneg_rule thm]
else explode1 thm []
@@ -284,7 +285,7 @@
val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
fun contra_left conj thm =
let
- val rules = explode_term conj (T.prop_of thm)
+ val rules = explode_term conj (U.prop_of thm)
fun contra_lits (t, rs) =
(case t of
@{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 18:20:44 2010 +0100
@@ -15,6 +15,7 @@
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
struct
+structure U = SMT_Utils
structure P = Z3_Proof_Parser
structure T = Z3_Proof_Tools
structure L = Z3_Proof_Literals
@@ -233,9 +234,9 @@
fun lit_elim conj (p, idx) ct ptab =
let val lits = literals_of p
in
- (case L.lookup_lit lits (T.term_of ct) of
+ (case L.lookup_lit lits (U.term_of ct) of
SOME lit => (Thm lit, ptab)
- | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
+ | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
end
in
val and_elim = lit_elim true
@@ -266,7 +267,7 @@
val explode_disj = L.explode false true false
val join_disj = L.join false
fun unit thm thms th =
- let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
+ let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -403,7 +404,7 @@
named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
in
fun nnf ctxt vars ps ct =
- (case T.term_of ct of
+ (case U.term_of ct of
_ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
if l aconv r
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 18:10:32 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 18:20:44 2010 +0100
@@ -6,9 +6,7 @@
signature Z3_PROOF_TOOLS =
sig
- (*accessing and modifying terms*)
- val term_of: cterm -> term
- val prop_of: thm -> term
+ (*modifying terms*)
val as_meta_eq: cterm -> cterm
(*theorem nets*)
@@ -51,12 +49,7 @@
-(* accessing terms *)
-
-val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
-
-fun term_of ct = dest_prop (Thm.term_of ct)
-fun prop_of thm = dest_prop (Thm.prop_of thm)
+(* modifying terms *)
fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))