src/HOL/Tools/SMT/smt_translate.ML
changeset 43928 24d6e759753f
parent 43829 fba9754b827e
child 43929 61d432e51aff
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 09:23:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 09:23:12 2011 +0200
     1.3 @@ -38,8 +38,6 @@
     1.4    (*translation*)
     1.5    val add_config: SMT_Utils.class * (Proof.context -> config) ->
     1.6      Context.generic -> Context.generic 
     1.7 -  val lift_lambdas: Proof.context -> bool -> term list ->
     1.8 -    Proof.context * (term list * term list)
     1.9    val translate: Proof.context -> string list -> (int * thm) list ->
    1.10      string * recon
    1.11  end
    1.12 @@ -243,82 +241,6 @@
    1.13  end
    1.14  
    1.15  
    1.16 -(** lambda-lifting **)
    1.17 -
    1.18 -local
    1.19 -  fun mk_def triggers Ts T lhs rhs =
    1.20 -    let
    1.21 -      val eq = HOLogic.eq_const T $ lhs $ rhs
    1.22 -      fun trigger () =
    1.23 -        [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
    1.24 -        |> map (HOLogic.mk_list @{typ SMT.pattern})
    1.25 -        |> HOLogic.mk_list @{typ "SMT.pattern list"}
    1.26 -      fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
    1.27 -    in
    1.28 -      fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq
    1.29 -        else eq)
    1.30 -    end
    1.31 -
    1.32 -  fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts
    1.33 -
    1.34 -  fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
    1.35 -    | dest_abs Ts t = (Ts, t)
    1.36 -
    1.37 -  fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
    1.38 -    let
    1.39 -      val t1 = mk_abs Us t
    1.40 -      val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
    1.41 -      fun rep i k = if member (op =) bs i then (Bound k, k+1) else (Bound i, k)
    1.42 -      val (rs, _) = fold_map rep (0 upto length Ts - 1) 0
    1.43 -      val t2 = Term.subst_bounds (rs, t1)
    1.44 -      val Ts' = map (nth Ts) bs 
    1.45 -      val (_, t3) = dest_abs [] t2
    1.46 -      val t4 = mk_abs Ts' t2
    1.47 -
    1.48 -      val T = Term.fastype_of1 (Us @ Ts, t)
    1.49 -      fun app f = Term.list_comb (f, map Bound (rev bs))
    1.50 -    in
    1.51 -      (case Termtab.lookup defs t4 of
    1.52 -        SOME (f, _) => (app f, cx)
    1.53 -      | NONE =>
    1.54 -          let
    1.55 -            val (n, ctxt') =
    1.56 -              yield_singleton Variable.variant_fixes Name.uu ctxt
    1.57 -            val (is, UTs) = split_list (map_index I (Us @ Ts'))
    1.58 -            val f = Free (n, rev UTs ---> T)
    1.59 -            val lhs = Term.list_comb (f, map Bound (rev is))
    1.60 -            val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
    1.61 -          in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
    1.62 -    end
    1.63 -
    1.64 -  fun traverse triggers Ts t =
    1.65 -    (case t of
    1.66 -      (q as Const (@{const_name All}, _)) $ Abs a =>
    1.67 -        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    1.68 -    | (q as Const (@{const_name Ex}, _)) $ Abs a =>
    1.69 -        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    1.70 -    | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
    1.71 -        traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
    1.72 -        (fn (u', a') => l $ u' $ Abs a')
    1.73 -    | Abs _ =>
    1.74 -        let val (Us, u) = dest_abs [] t
    1.75 -        in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
    1.76 -    | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
    1.77 -    | _ => pair t)
    1.78 -
    1.79 -  and abs_traverse triggers Ts (n, T, t) =
    1.80 -    traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
    1.81 -in
    1.82 -
    1.83 -fun lift_lambdas ctxt triggers ts =
    1.84 -  (Termtab.empty, ctxt)
    1.85 -  |> fold_map (traverse triggers []) ts
    1.86 -  |> (fn (us, (defs, ctxt')) =>
    1.87 -       (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
    1.88 -
    1.89 -end
    1.90 -
    1.91 -
    1.92  (** introduce explicit applications **)
    1.93  
    1.94  local
    1.95 @@ -618,7 +540,7 @@
    1.96      val (ctxt2, ts3) =
    1.97        ts2
    1.98        |> eta_expand ctxt1 is_fol funcs
    1.99 -      |> lift_lambdas ctxt1 true
   1.100 +      |> Lambda_Lifting.lift_lambdas ctxt1 true
   1.101        ||> (op @)
   1.102        |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
   1.103