# HG changeset patch
# User blanchet
# Date 1310904695 -7200
# Node ID a875729380a4dd26091e0b0d521f554f0b57e987
# Parent  d636b053d4ff644bc045d3e0f1fe2454595a3c80
added lambda-lifting to Sledgehammer (rough)

diff -r d636b053d4ff -r a875729380a4 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
@@ -993,8 +993,8 @@
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts
-              ((name, loc), t) =
+fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc
+              presimp_consts ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
     case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
            |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
diff -r d636b053d4ff -r a875729380a4 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:35 2011 +0200
@@ -525,6 +525,11 @@
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
+fun lift_lambdas ctxt ts =
+  case SMT_Translate.lift_lambdas ctxt false ts |> snd of
+    (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
+  | (defs, ts) => ts @ defs
+
 fun translate_atp_lambdas ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>
@@ -537,16 +542,11 @@
          else
            trans)
   |> (fn trans =>
-         if trans = concealed_lambdasN then
-           map (conceal_lambdas ctxt)
-         else if trans = lambda_liftingN then
-           I (* TODO: implement *)
-         else if trans = combinatorsN then
-           map (introduce_combinators ctxt)
-         else if trans = lambdasN then
-           map Envir.eta_contract
-         else
-           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
+         if trans = concealed_lambdasN then map (conceal_lambdas ctxt)
+         else if trans = lambda_liftingN then lift_lambdas ctxt
+         else if trans = combinatorsN then map (introduce_combinators ctxt)
+         else if trans = lambdasN then map Envir.eta_contract
+         else error ("Unknown lambda translation method: " ^ quote trans ^ "."))
 
 val metis_minimize_max_time = seconds 2.0