removed needless complication for modern SMT solvers
authorblanchet
Fri Dec 04 14:15:16 2015 +0100 (2015-12-04)
changeset 617827d754aca6a75
parent 61781 e1e6bb36b27a
child 61783 7f36a8bfa822
removed needless complication for modern SMT solvers
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Dec 03 15:33:01 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 04 14:15:16 2015 +0100
     1.3 @@ -319,14 +319,10 @@
     1.4  
     1.5    val fol_rules = [
     1.6      Let_def,
     1.7 -    @{lemma "P = True == P" by (rule eq_reflection) simp},
     1.8 -    @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
     1.9 +    @{lemma "P = True == P" by (rule eq_reflection) simp}]
    1.10  
    1.11    exception BAD_PATTERN of unit
    1.12  
    1.13 -  fun wrap_in_if pat t =
    1.14 -    if pat then raise BAD_PATTERN () else @{const If (bool)} $ t $ @{const True} $ @{const False}
    1.15 -
    1.16    fun is_builtin_conn_or_pred ctxt c ts =
    1.17      is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse
    1.18      is_some (SMT_Builtin.dest_builtin_pred ctxt c ts)
    1.19 @@ -343,9 +339,10 @@
    1.20        | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
    1.21            if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
    1.22        | (Const (c as (n, _)), ts) =>
    1.23 -          if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t)
    1.24 -          else if is_quant n then wrap_in_if pat (in_form t)
    1.25 -          else Term.list_comb (Const c, map (in_term pat) ts)
    1.26 +          if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
    1.27 +            if pat then raise BAD_PATTERN () else in_form t
    1.28 +          else
    1.29 +            Term.list_comb (Const c, map (in_term pat) ts)
    1.30        | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
    1.31        | _ => t)
    1.32