src/HOL/Tools/SMT/smt_translate.ML
changeset 42319 9a8ba59aed06
parent 41785 77dcc197df9a
child 42321 ce83c1654b86
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     1.3 @@ -168,17 +168,17 @@
     1.4  (** eta-expand quantifiers, let expressions and built-ins *)
     1.5  
     1.6  local
     1.7 -  fun eta T t = Abs (Name.uu, T, Term.incr_boundvars 1 t $ Bound 0)
     1.8 +  fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0))
     1.9  
    1.10 -  fun exp T = eta (Term.domain_type (Term.domain_type T))
    1.11 +  fun exp f T = eta f (Term.domain_type (Term.domain_type T))
    1.12  
    1.13    fun exp2 T q =
    1.14      let val U = Term.domain_type T
    1.15 -    in Abs (Name.uu, U, q $ eta (Term.domain_type U) (Bound 0)) end
    1.16 +    in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
    1.17  
    1.18    fun exp2' T l =
    1.19      let val (U1, U2) = Term.dest_funT T ||> Term.domain_type
    1.20 -    in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end
    1.21 +    in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end
    1.22  
    1.23    fun expf k i T t =
    1.24      let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
    1.25 @@ -189,7 +189,7 @@
    1.26      end
    1.27  in
    1.28  
    1.29 -fun eta_expand ctxt funcs =
    1.30 +fun eta_expand ctxt is_fol funcs =
    1.31    let
    1.32      fun exp_func t T ts =
    1.33        (case Termtab.lookup funcs t of
    1.34 @@ -199,18 +199,30 @@
    1.35        | NONE => Term.list_comb (t, ts))
    1.36  
    1.37      fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a
    1.38 -      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp T t
    1.39 +      | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t
    1.40        | expand (q as Const (@{const_name All}, T)) = exp2 T q
    1.41        | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
    1.42 -      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp T t
    1.43 +      | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
    1.44        | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
    1.45        | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) =
    1.46 -          l $ expand t $ abs_expand a
    1.47 +          if is_fol then expand (Term.betapply (Abs a, t))
    1.48 +          else l $ expand t $ abs_expand a
    1.49        | expand ((l as Const (@{const_name Let}, T)) $ t $ u) =
    1.50 -          l $ expand t $ exp (Term.range_type T) u
    1.51 +          if is_fol then expand (u $ t)
    1.52 +          else l $ expand t $ exp expand (Term.range_type T) u
    1.53        | expand ((l as Const (@{const_name Let}, T)) $ t) =
    1.54 -          exp2 T (l $ expand t)
    1.55 -      | expand (l as Const (@{const_name Let}, T)) = exp2' T l
    1.56 +          if is_fol then
    1.57 +            let val U = Term.domain_type (Term.range_type T)
    1.58 +            in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
    1.59 +          else exp2 T (l $ expand t)
    1.60 +      | expand (l as Const (@{const_name Let}, T)) =
    1.61 +          if is_fol then 
    1.62 +            let val U = Term.domain_type (Term.range_type T)
    1.63 +            in
    1.64 +              Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U,
    1.65 +                Bound 0 $ Bound 1))
    1.66 +            end
    1.67 +          else exp2' T l
    1.68        | expand t =
    1.69            (case Term.strip_comb t of
    1.70              (u as Const (c as (_, T)), ts) =>
    1.71 @@ -363,12 +375,6 @@
    1.72      @{lemma "P = True == P" by (rule eq_reflection) simp},
    1.73      @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
    1.74  
    1.75 -  fun reduce_let (Const (@{const_name Let}, _) $ t $ u) =
    1.76 -        reduce_let (Term.betapply (u, t))
    1.77 -    | reduce_let (t $ u) = reduce_let t $ reduce_let u
    1.78 -    | reduce_let (Abs (n, T, t)) = Abs (n, T, reduce_let t)
    1.79 -    | reduce_let t = t
    1.80 -
    1.81    fun as_term t = @{const HOL.eq (bool)} $ t $ @{const SMT.term_true}
    1.82  
    1.83    fun wrap_in_if t =
    1.84 @@ -432,7 +438,7 @@
    1.85                | NONE => as_term (in_term t)))
    1.86        | _ => as_term (in_term t))
    1.87    in
    1.88 -    map (reduce_let #> in_form) #>
    1.89 +    map in_form #>
    1.90      cons (SMT_Utils.prop_of term_bool) #>
    1.91      pair (fol_rules, [term_bool], builtin)
    1.92    end
    1.93 @@ -566,7 +572,7 @@
    1.94  
    1.95      val (ctxt2, ts3) =
    1.96        ts2
    1.97 -      |> eta_expand ctxt1 funcs
    1.98 +      |> eta_expand ctxt1 is_fol funcs
    1.99        |> lift_lambdas ctxt1
   1.100        ||> intro_explicit_application
   1.101