fixed trigger inference: testing if a theorem already has a trigger was too strict;
authorboehmes
Wed Dec 15 18:18:56 2010 +0100 (2010-12-15)
changeset 4117410eb369f8c01
parent 41173 7c6178d45cc8
child 41175 5a9543f95cc6
fixed trigger inference: testing if a theorem already has a trigger was too strict;
fixed monomorphization with respect to triggers (which might occur schematically)
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_monomorph.ML
src/HOL/Tools/SMT/smt_normalize.ML
     1.1 --- a/src/HOL/SMT.thy	Wed Dec 15 16:32:45 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Dec 15 18:18:56 2010 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    "Tools/SMT/smt_utils.ML"
     1.5    "Tools/SMT/smt_failure.ML"
     1.6    "Tools/SMT/smt_config.ML"
     1.7 -  "Tools/SMT/smt_monomorph.ML"
     1.8 +  ("Tools/SMT/smt_monomorph.ML")
     1.9    ("Tools/SMT/smt_builtin.ML")
    1.10    ("Tools/SMT/smt_normalize.ML")
    1.11    ("Tools/SMT/smt_translate.ML")
    1.12 @@ -149,6 +149,7 @@
    1.13  
    1.14  subsection {* Setup *}
    1.15  
    1.16 +use "Tools/SMT/smt_monomorph.ML"
    1.17  use "Tools/SMT/smt_builtin.ML"
    1.18  use "Tools/SMT/smt_normalize.ML"
    1.19  use "Tools/SMT/smt_translate.ML"
     2.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Dec 15 16:32:45 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Dec 15 18:18:56 2010 +0100
     2.3 @@ -45,8 +45,19 @@
     2.4  fun is_const pred (n, T) = not (ignored n) andalso pred T
     2.5  
     2.6  fun collect_consts_if pred f =
     2.7 -  Thm.prop_of #>
     2.8 -  Term.fold_aterms (fn Const c => if is_const pred c then f c else I | _ => I)
     2.9 +  let
    2.10 +    fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
    2.11 +      | collect (t $ u) = collect t #> collect u
    2.12 +      | collect (Abs (_, _, t)) = collect t
    2.13 +      | collect (Const c) = if is_const pred c then f c else I
    2.14 +      | collect _ = I
    2.15 +    and collect_trigger t =
    2.16 +      let val dest = these o try HOLogic.dest_list 
    2.17 +      in fold (fold collect_pat o dest) (dest t) end
    2.18 +    and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
    2.19 +      | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
    2.20 +      | collect_pat _ = I
    2.21 +  in collect o Thm.prop_of end
    2.22  
    2.23  val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
    2.24  
     3.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:32:45 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 18:18:56 2010 +0100
     3.3 @@ -183,7 +183,7 @@
     3.4            (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
     3.5              ([], []) => [[ct]]
     3.6            | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
     3.7 -      | _ => [[ct]])
     3.8 +      | _ => [])
     3.9      else []
    3.10  
    3.11    fun proper_mpat _ _ _ [] = false
    3.12 @@ -227,8 +227,11 @@
    3.13  
    3.14      in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
    3.15  
    3.16 +  fun has_trigger (@{const SMT.trigger} $ _ $ _) = true
    3.17 +    | has_trigger _ = false
    3.18 +
    3.19    fun try_trigger_conv cv ct =
    3.20 -    if proper_quant false (K false) (Thm.term_of ct) then Conv.all_conv ct
    3.21 +    if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
    3.22      else Conv.try_conv cv ct
    3.23  
    3.24    fun infer_trigger_conv ctxt =