# HG changeset patch
# User blanchet
# Date 1328026148 -3600
# Node ID 0ccf458a3633bb73e18425c9dd18e87eedbf6d9f
# Parent  90be435411f0f2193b2e21edf6ffefbaafeec92d
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)

diff -r 90be435411f0 -r 0ccf458a3633 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 16:11:15 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 17:09:08 2012 +0100
@@ -692,12 +692,15 @@
 
 (* Requires bound variables not to clash with any schematic variables (as should
    be the case right after lambda-lifting). *)
-fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
-    let
-      val names = Name.make_context (map fst (Term.add_var_names t []))
-      val (s, _) = Name.variant s names
-    in open_form (subst_bound (Var ((s, 0), T), t)) end
-  | open_form t = t
+fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
+    (case try unprefix s of
+       SOME s =>
+       let
+         val names = Name.make_context (map fst (Term.add_var_names t' []))
+         val (s, _) = Name.variant s names
+       in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
+     | NONE => t)
+  | open_form _ t = t
 
 fun lift_lams_part_1 ctxt type_enc =
   map close_form #> rpair ctxt
@@ -708,7 +711,9 @@
                     lam_lifted_mono_prefix) ^ "_a"))
           Lambda_Lifting.is_quantifier
   #> fst
-val lift_lams_part_2 = pairself (map (open_form o constify_lifted))
+fun lift_lams_part_2 (facts, lifted) =
+  (map (open_form (unprefix close_form_prefix) o constify_lifted) facts,
+   map (open_form I o constify_lifted) lifted)
 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1
 
 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
@@ -1235,15 +1240,14 @@
     if s = tptp_true then NONE else SOME formula
   | formula => SOME formula
 
-fun not_trueprop (@{const Trueprop} $ t) =
-    @{const Trueprop} $ (@{const Not} $ t)
-  | not_trueprop t =
-    if fastype_of t = @{typ bool} then @{const Not} $ t
+fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+  | s_not_trueprop t =
+    if fastype_of t = @{typ bool} then s_not t
     else @{prop False} (* "t" is too meta *)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (kind, t)) =>
-          t |> kind = Conjecture ? not_trueprop
+          t |> kind = Conjecture ? s_not_trueprop
             |> make_formula ctxt format type_enc (format <> CNF) name stature
                             kind)
 
@@ -1730,7 +1734,7 @@
       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
-      map (pair prem_kind) hyp_ts @ [(Conjecture, not_trueprop concl_t)]
+      map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
       |> map (apsnd freeze_term)
       |> map2 (pair o rpair (Local, General) o string_of_int)
               (0 upto length hyp_ts)
diff -r 90be435411f0 -r 0ccf458a3633 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 16:11:15 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 31 17:09:08 2012 +0100
@@ -362,12 +362,11 @@
    prem_kind = #prem_kind spass_config,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
-                       ""))),
-      (0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
+     [(0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN,
                        spass_incompleteN))),
       (0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN,
-                       "")))]}
+                       ""))),
+      (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
 
 val spass_new = (spass_newN, spass_new_config)
 
diff -r 90be435411f0 -r 0ccf458a3633 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Jan 31 16:11:15 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Jan 31 17:09:08 2012 +0100
@@ -31,6 +31,7 @@
   val s_disj : term * term -> term
   val s_imp : term * term -> term
   val s_iff : term * term -> term
+  val close_form_prefix : string
   val close_form : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
@@ -264,10 +265,13 @@
   | s_iff (t1, @{const True}) = t1
   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
+val close_form_prefix = "ATP.close_form."
+
 fun close_form t =
   fold (fn ((s, i), T) => fn t' =>
            HOLogic.all_const T
-           $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
+           $ Abs (close_form_prefix ^ s, T,
+                  abstract_over (Var ((s, i), T), t')))
        (Term.add_vars t []) t
 
 fun monomorphic_term subst =