# HG changeset patch # User boehmes # Date 1292433536 -3600 # Node ID 10eb369f8c01d1f3e783cf1f5570d5ab86faa344 # Parent 7c6178d45cc803a7674c348ff045b5dcc39fba27 fixed trigger inference: testing if a theorem already has a trigger was too strict; fixed monomorphization with respect to triggers (which might occur schematically) diff -r 7c6178d45cc8 -r 10eb369f8c01 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Wed Dec 15 16:32:45 2010 +0100 +++ b/src/HOL/SMT.thy Wed Dec 15 18:18:56 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 7c6178d45cc8 -r 10eb369f8c01 src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 16:32:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Wed Dec 15 18:18:56 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 7c6178d45cc8 -r 10eb369f8c01 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 16:32:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 18:18:56 2010 +0100 @@ -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 =