unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
authorboehmes
Fri Apr 08 19:04:08 2011 +0200 (2011-04-08)
changeset 423199a8ba59aed06
parent 42318 0fd33b6b22cf
child 42320 1f09e4c680fc
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/Tools/SMT/smt_translate.ML
     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