author boehmes Fri Apr 08 19:04:08 2011 +0200 (2011-04-08) changeset 42319 9a8ba59aed06 parent 42318 0fd33b6b22cf child 42320 1f09e4c680fc
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
```     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
1.3 @@ -469,6 +469,7 @@
1.4    "f (\<forall>x. g x) \<Longrightarrow> True"
1.5    by smt+
1.6
1.7 +lemma True using let_rsp by smt
1.8
1.9  lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps)
1.10
```
```     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
2.3 @@ -168,17 +168,17 @@
2.4  (** eta-expand quantifiers, let expressions and built-ins *)
2.5
2.6  local
2.7 -  fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t \$ Bound 0)
2.8 +  fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t \$ Bound 0))
2.9
2.10 -  fun exp T = eta (Term.domain_type (Term.domain_type T))
2.11 +  fun exp f T = eta f (Term.domain_type (Term.domain_type T))
2.12
2.13    fun exp2 T q =
2.14      let val U = Term.domain_type T
2.15 -    in Abs (Name.uu, U, q \$ eta (Term.domain_type U) (Bound 0)) end
2.16 +    in Abs (Name.uu, U, q \$ eta I (Term.domain_type U) (Bound 0)) end
2.17
2.18    fun exp2' T l =
2.19      let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
2.20 -    in Abs (Name.uu, U1, eta U2 (l \$ Bound 0)) end
2.21 +    in Abs (Name.uu, U1, eta I U2 (l \$ Bound 0)) end
2.22
2.23    fun expf k i T t =
2.24      let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
2.25 @@ -189,7 +189,7 @@
2.26      end
2.27  in
2.28
2.29 -fun eta_expand ctxt funcs =
2.30 +fun eta_expand ctxt is_fol funcs =
2.31    let
2.32      fun exp_func t T ts =
2.33        (case Termtab.lookup funcs t of
2.34 @@ -199,18 +199,30 @@
2.35        | NONE => Term.list_comb (t, ts))
2.36
2.37      fun expand ((q as Const (@{const_name All}, _)) \$ Abs a) = q \$ abs_expand a
2.38 -      | expand ((q as Const (@{const_name All}, T)) \$ t) = q \$ exp T t
2.39 +      | expand ((q as Const (@{const_name All}, T)) \$ t) = q \$ exp expand T t
2.40        | expand (q as Const (@{const_name All}, T)) = exp2 T q
2.41        | expand ((q as Const (@{const_name Ex}, _)) \$ Abs a) = q \$ abs_expand a
2.42 -      | expand ((q as Const (@{const_name Ex}, T)) \$ t) = q \$ exp T t
2.43 +      | expand ((q as Const (@{const_name Ex}, T)) \$ t) = q \$ exp expand T t
2.44        | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
2.45        | expand ((l as Const (@{const_name Let}, _)) \$ t \$ Abs a) =
2.46 -          l \$ expand t \$ abs_expand a
2.47 +          if is_fol then expand (Term.betapply (Abs a, t))
2.48 +          else l \$ expand t \$ abs_expand a
2.49        | expand ((l as Const (@{const_name Let}, T)) \$ t \$ u) =
2.50 -          l \$ expand t \$ exp (Term.range_type T) u
2.51 +          if is_fol then expand (u \$ t)
2.52 +          else l \$ expand t \$ exp expand (Term.range_type T) u
2.53        | expand ((l as Const (@{const_name Let}, T)) \$ t) =
2.54 -          exp2 T (l \$ expand t)
2.55 -      | expand (l as Const (@{const_name Let}, T)) = exp2' T l
2.56 +          if is_fol then
2.57 +            let val U = Term.domain_type (Term.range_type T)
2.58 +            in Abs (Name.uu, U, Bound 0 \$ Term.incr_boundvars 1 t) end
2.59 +          else exp2 T (l \$ expand t)
2.60 +      | expand (l as Const (@{const_name Let}, T)) =
2.61 +          if is_fol then
2.62 +            let val U = Term.domain_type (Term.range_type T)
2.63 +            in
2.64 +              Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U,
2.65 +                Bound 0 \$ Bound 1))
2.66 +            end
2.67 +          else exp2' T l
2.68        | expand t =
2.69            (case Term.strip_comb t of
2.70              (u as Const (c as (_, T)), ts) =>
2.71 @@ -363,12 +375,6 @@
2.72      @{lemma "P = True == P" by (rule eq_reflection) simp},
2.73      @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
2.74
2.75 -  fun reduce_let (Const (@{const_name Let}, _) \$ t \$ u) =
2.76 -        reduce_let (Term.betapply (u, t))
2.77 -    | reduce_let (t \$ u) = reduce_let t \$ reduce_let u
2.78 -    | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
2.79 -    | reduce_let t = t
2.80 -
2.81    fun as_term t = @{const HOL.eq (bool)} \$ t \$ @{const SMT.term_true}
2.82
2.83    fun wrap_in_if t =
2.84 @@ -432,7 +438,7 @@
2.85                | NONE => as_term (in_term t)))
2.86        | _ => as_term (in_term t))
2.87    in
2.88 -    map (reduce_let #> in_form) #>
2.89 +    map in_form #>
2.90      cons (SMT_Utils.prop_of term_bool) #>
2.91      pair (fol_rules, [term_bool], builtin)
2.92    end
2.93 @@ -566,7 +572,7 @@
2.94
2.95      val (ctxt2, ts3) =
2.96        ts2
2.97 -      |> eta_expand ctxt1 funcs
2.98 +      |> eta_expand ctxt1 is_fol funcs
2.99        |> lift_lambdas ctxt1
2.100        ||> intro_explicit_application
2.101
```