# HG changeset patch
# User blanchet
# Date 1311595812 -7200
# Node ID e1d29c3ca9334be3e2bfa75d66692ffbf540748e
# Parent  91294d386539ca368f4caa19a02f677c0c4bae1f
introduced hybrid lambda translation

diff -r 91294d386539 -r e1d29c3ca933 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 14:10:12 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jul 25 14:10:12 2011 +0200
@@ -63,6 +63,7 @@
   val concealedN : string
   val liftingN : string
   val combinatorsN : string
+  val hybridN : string
   val lambdasN : string
   val smartN : string
   val dest_dir : string Config.T
@@ -337,6 +338,7 @@
 val concealedN = "concealed"
 val liftingN = "lifting"
 val combinatorsN = "combinators"
+val hybridN = "hybrid"
 val lambdasN = "lambdas"
 val smartN = "smart"
 
@@ -535,6 +537,19 @@
           Lambda_Lifting.is_quantifier
   #> fst
 
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+    intentionalize_def t
+  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    let
+      fun lam T t = Abs (Name.uu, T, t)
+      val (head, args) = strip_comb t ||> rev
+      val head_T = fastype_of head
+      val n = length args
+      val arg_Ts = head_T |> binder_types |> take n |> rev
+      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+  | intentionalize_def t = t
+
 fun translate_atp_lambdas ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>
@@ -553,6 +568,10 @@
            lift_lambdas ctxt type_enc
          else if trans = combinatorsN then
            map (introduce_combinators ctxt) #> rpair []
+         else if trans = hybridN then
+           lift_lambdas ctxt type_enc
+           ##> maps (fn t => [t, introduce_combinators ctxt
+                                     (intentionalize_def t)])
          else if trans = lambdasN then
            map (Envir.eta_contract) #> rpair []
          else