src/HOL/Tools/SMT/smt_normalize.ML
changeset 40685 dcb27631cb45
parent 40681 872b08416fb4
child 40686 4725ed462387
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 10:42:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 13:31:12 2010 +0100
     1.3 @@ -35,6 +35,26 @@
     1.4  
     1.5  
     1.6  
     1.7 +(* instantiate elimination rules *)
     1.8 + 
     1.9 +local
    1.10 +  val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.11 +
    1.12 +  fun inst f ct thm =
    1.13 +    let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.14 +    in Thm.instantiate ([], [(cv, ct)]) thm end
    1.15 +in
    1.16 +
    1.17 +fun instantiate_elim thm =
    1.18 +  (case Thm.concl_of thm of
    1.19 +    @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
    1.20 +  | Var _ => inst I cpfalse thm
    1.21 +  | _ => thm)
    1.22 +
    1.23 +end
    1.24 +
    1.25 +
    1.26 +
    1.27  (* simplification of trivial distincts (distinct should have at least
    1.28     three elements in the argument list) *)
    1.29  
    1.30 @@ -520,6 +540,7 @@
    1.31        else SOME (i, f ctxt' thm)
    1.32    in
    1.33      irules
    1.34 +    |> map (apsnd instantiate_elim)
    1.35      |> trivial_distinct ctxt
    1.36      |> rewrite_bool_cases ctxt
    1.37      |> normalize_numerals ctxt