wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
authorboehmes
Mon Feb 21 09:14:48 2011 +0100 (2011-02-21)
changeset 4178577dcc197df9a
parent 41784 537013b8ba8e
child 41786 a5899d0ce1a1
wrap occurrences of quantifiers in first-order terms (i.e., outside first-order formulas) in If-expressions
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Feb 19 08:47:46 2011 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Feb 21 09:14:48 2011 +0100
     1.3 @@ -354,6 +354,8 @@
     1.4    val term_bool = @{lemma "SMT.term_true ~= SMT.term_false"
     1.5      by (simp add: SMT.term_true_def SMT.term_false_def)}
     1.6  
     1.7 +  val is_quant = member (op =) [@{const_name All}, @{const_name Ex}]
     1.8 +
     1.9    val fol_rules = [
    1.10      Let_def,
    1.11      mk_meta_eq @{thm SMT.term_true_def},
    1.12 @@ -395,8 +397,9 @@
    1.13        | (@{const False}, []) => @{const SMT.term_false}
    1.14        | (u as Const (@{const_name If}, _), [t1, t2, t3]) =>
    1.15            u $ in_form t1 $ in_term t2 $ in_term t3
    1.16 -      | (Const c, ts) =>
    1.17 +      | (Const (c as (n, _)), ts) =>
    1.18            if is_builtin_conn_or_pred ctxt c ts then wrap_in_if (in_form t)
    1.19 +          else  if is_quant n then wrap_in_if (in_form t)
    1.20            else Term.list_comb (Const c, map in_term ts)
    1.21        | (Free c, ts) => Term.list_comb (Free c, map in_term ts)
    1.22        | _ => t)
    1.23 @@ -418,8 +421,7 @@
    1.24      and in_form t =
    1.25        (case Term.strip_comb t of
    1.26          (q as Const (qn, _), [Abs (n, T, u)]) =>
    1.27 -          if member (op =) [@{const_name All}, @{const_name Ex}] qn then
    1.28 -            q $ Abs (n, T, in_trigger u)
    1.29 +          if is_quant qn then q $ Abs (n, T, in_trigger u)
    1.30            else as_term (in_term t)
    1.31        | (Const c, ts) =>
    1.32            (case SMT_Builtin.dest_builtin_conn ctxt c ts of