# HG changeset patch # User boehmes # Date 1292433644 -3600 # Node ID 5a9543f95cc62734e756a34fcf4ba16a0df96c0f # Parent 10eb369f8c01d1f3e783cf1f5570d5ab86faa344# Parent 043f8dc3b51f41232cbe29fcad361421208b6a14 merged diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/SMT.thy --- 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" diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/smt_monomorph.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) diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/smt_normalize.ML --- 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) diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/smt_translate.ML --- 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) = diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/smt_utils.ML --- 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 *) diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/z3_proof_literals.ML --- 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) diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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))) diff -r 043f8dc3b51f -r 5a9543f95cc6 src/HOL/Tools/SMT/z3_proof_tools.ML --- 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))