src/HOL/Tools/SMT/smt_translate.ML
changeset 43829 fba9754b827e
parent 43554 9bece8cbb5be
child 43928 24d6e759753f
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 16:50:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Thu Jul 14 17:29:30 2011 +0200
     1.3 @@ -38,7 +38,7 @@
     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 -> term list ->
     1.8 +  val lift_lambdas: Proof.context -> bool -> term list ->
     1.9      Proof.context * (term list * term list)
    1.10    val translate: Proof.context -> string list -> (int * thm) list ->
    1.11      string * recon
    1.12 @@ -246,22 +246,25 @@
    1.13  (** lambda-lifting **)
    1.14  
    1.15  local
    1.16 -  fun mk_def Ts T lhs rhs =
    1.17 +  fun mk_def triggers Ts T lhs rhs =
    1.18      let
    1.19        val eq = HOLogic.eq_const T $ lhs $ rhs
    1.20 -      val trigger =
    1.21 +      fun trigger () =
    1.22          [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
    1.23          |> map (HOLogic.mk_list @{typ SMT.pattern})
    1.24          |> HOLogic.mk_list @{typ "SMT.pattern list"}
    1.25        fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
    1.26 -    in fold mk_all Ts (@{const SMT.trigger} $ trigger $ eq) end
    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 Us Ts t (cx as (defs, ctxt)) =
    1.38 +  fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
    1.39      let
    1.40        val t1 = mk_abs Us t
    1.41        val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
    1.42 @@ -284,31 +287,32 @@
    1.43              val (is, UTs) = split_list (map_index I (Us @ Ts'))
    1.44              val f = Free (n, rev UTs ---> T)
    1.45              val lhs = Term.list_comb (f, map Bound (rev is))
    1.46 -            val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
    1.47 +            val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
    1.48            in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
    1.49      end
    1.50  
    1.51 -  fun traverse Ts t =
    1.52 +  fun traverse triggers Ts t =
    1.53      (case t of
    1.54        (q as Const (@{const_name All}, _)) $ Abs a =>
    1.55 -        abs_traverse Ts a #>> (fn a' => q $ Abs a')
    1.56 +        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    1.57      | (q as Const (@{const_name Ex}, _)) $ Abs a =>
    1.58 -        abs_traverse Ts a #>> (fn a' => q $ Abs a')
    1.59 +        abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    1.60      | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
    1.61 -        traverse Ts u ##>> abs_traverse Ts a #>>
    1.62 +        traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
    1.63          (fn (u', a') => l $ u' $ Abs a')
    1.64      | Abs _ =>
    1.65          let val (Us, u) = dest_abs [] t
    1.66 -        in traverse (Us @ Ts) u #-> replace_lambda Us Ts end
    1.67 -    | u1 $ u2 => traverse Ts u1 ##>> traverse Ts u2 #>> (op $)
    1.68 +        in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
    1.69 +    | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
    1.70      | _ => pair t)
    1.71  
    1.72 -  and abs_traverse Ts (n, T, t) = traverse (T::Ts) t #>> (fn t' => (n, T, t'))
    1.73 +  and abs_traverse triggers Ts (n, T, t) =
    1.74 +    traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
    1.75  in
    1.76  
    1.77 -fun lift_lambdas ctxt ts =
    1.78 +fun lift_lambdas ctxt triggers ts =
    1.79    (Termtab.empty, ctxt)
    1.80 -  |> fold_map (traverse []) ts
    1.81 +  |> fold_map (traverse triggers []) ts
    1.82    |> (fn (us, (defs, ctxt')) =>
    1.83         (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
    1.84  
    1.85 @@ -614,7 +618,7 @@
    1.86      val (ctxt2, ts3) =
    1.87        ts2
    1.88        |> eta_expand ctxt1 is_fol funcs
    1.89 -      |> lift_lambdas ctxt1
    1.90 +      |> lift_lambdas ctxt1 true
    1.91        ||> (op @)
    1.92        |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
    1.93