# HG changeset patch
# User blanchet
# Date 1280167651 -7200
# Node ID a9b47b85ca24aca90f2bcc6977f5c089b18541b9
# Parent  c0b9efa8bfcaa972dc1504e67677957f88800dd1
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting

diff -r c0b9efa8bfca -r a9b47b85ca24 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:56:10 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 20:07:31 2010 +0200
@@ -137,8 +137,7 @@
       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
     and do_formula bs t =
       case t of
-        @{const Trueprop} $ t1 => do_formula bs t1
-      | @{const Not} $ t1 =>
+        @{const Not} $ t1 =>
         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
         do_quant bs AForall s T t'
@@ -153,15 +152,25 @@
                        |>> APred ||> union (op =) ts)
   in do_formula [] end
 
-(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
-   "extensionalize_theorem" in "Clausifier"). *)
+(* Converts an elim-rule into an equivalent theorem that does not have the
+   predicate variable. Leaves other theorems unchanged. We simply instantiate
+   the conclusion variable to False. (Cf. "transform_elim_term" in
+   "ATP_Systems".) *)
+(* FIXME: test! *)
+fun transform_elim_term t =
+  case Logic.strip_imp_concl t of
+    @{const Trueprop} $ Var (z, @{typ bool}) =>
+    subst_Vars [(z, @{const True})] t
+  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop True})] t
+  | _ => t
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+   (Cf. "extensionalize_theorem" in "Clausifier".) *)
 fun extensionalize_term t =
   let
-    fun aux j (Const (@{const_name "op ="}, _) $ t2 $ Abs (s, var_T, t')) =
-        let
-          val T' = fastype_of t'
-          val var_t = Var (("x", j), var_T)
-        in
+    fun aux j (Const (@{const_name "op ="}, Type (_, [Type (_, [_, T']), _]))
+               $ t2 $ Abs (s, var_T, t')) =
+        let val var_t = Var (("x", j), var_T) in
           Const (@{const_name "op ="}, T' --> T' --> HOLogic.boolT)
             $ betapply (t2, var_t) $ subst_bound (var_t, t')
           |> aux (j + 1)
@@ -169,13 +178,54 @@
       | aux _ t = t
   in aux (maxidx_of_term t + 1) t end
 
+(* FIXME: Guarantee freshness *)
+fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+fun conceal_bounds Ts t =
+  subst_bounds (map (Free o apfst concealed_bound_name)
+                    (length Ts - 1 downto 0 ~~ rev Ts), t)
+fun reveal_bounds Ts =
+  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+                    (0 upto length Ts - 1 ~~ Ts))
+
+fun introduce_combinators_in_term thy t =
+  let
+    fun aux Ts t =
+      case t of
+        @{const Not} $ t1 => @{const Not} $ aux Ts t1
+      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+        t0 $ Abs (s, T, aux (T :: Ts) t')
+      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+        t0 $ Abs (s, T, aux (T :: Ts) t')
+      | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+      | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+          $ t1 $ t2 =>
+        t0 $ aux Ts t1 $ aux Ts t2
+      | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+               t
+             else
+               t |> conceal_bounds Ts
+                 |> Envir.eta_contract
+                 |> cterm_of thy
+                 |> Clausifier.introduce_combinators_in_cterm
+                 |> prop_of |> Logic.dest_equals |> snd
+                 |> reveal_bounds Ts
+               handle THM (msg, _, _) =>
+                      (* A type variable of sort "{}" will make abstraction
+                         fail. *)
+                      t
+  in t |> not (Meson.is_fol_term thy t) ? aux [] end
+
 (* making axiom and conjecture clauses *)
 fun make_clause thy (formula_id, formula_name, kind, t) =
   let
     (* ### FIXME: introduce combinators and perform other transformations
        previously done by Clausifier.to_nnf *)
-    val t = t |> Object_Logic.atomize_term thy
+    val t = t |> transform_elim_term
+              |> Object_Logic.atomize_term thy
               |> extensionalize_term
+              |> introduce_combinators_in_term thy
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     FOLFormula {formula_name = formula_name, formula_id = formula_id,
@@ -236,9 +286,8 @@
       @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   in map snd (make_axiom_clauses thy cnfs) end
 
-fun negate_prop (@{const Trueprop} $ t) = negate_prop t
-  | negate_prop (@{const Not} $ t) = t
-  | negate_prop t = @{const Not} $ t
+fun negate_term (@{const Not} $ t) = t
+  | negate_term t = @{const Not} $ t
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
@@ -253,7 +302,7 @@
     val tycons = type_consts_of_terms thy (goal_t :: axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
     val conjectures =
-      make_conjecture_clauses thy (map negate_prop hyp_ts @ [concl_t])
+      make_conjecture_clauses thy (map negate_term hyp_ts @ [concl_t])
     val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls)
     val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls)
     val helper_clauses =
diff -r c0b9efa8bfca -r a9b47b85ca24 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 17:56:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 20:07:31 2010 +0200
@@ -7,6 +7,7 @@
 
 signature CLAUSIFIER =
 sig
+  val introduce_combinators_in_cterm : cterm -> thm
   val cnf_axiom: theory -> bool -> thm -> thm list
   val cnf_rules_pairs :
     theory -> bool -> (string * thm) list -> ((string * int) * thm) list
@@ -21,16 +22,17 @@
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
 
-(*Converts an elim-rule into an equivalent theorem that does not have the
-  predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
-  conclusion variable to False.*)
-fun transform_elim th =
+(* Converts an elim-rule into an equivalent theorem that does not have the
+   predicate variable. Leaves other theorems unchanged. We simply instantiate
+   the conclusion variable to False. (Cf. "transform_elim_term" in
+   "ATP_Systems".) *)
+fun transform_elim_theorem th =
   case concl_of th of    (*conclusion variable*)
        @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
     | v as Var(_, @{typ prop}) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
-    | _ => th;
+    | _ => th
 
 (*To enforce single-threading*)
 exception Clausify_failure of theory;
@@ -83,8 +85,8 @@
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
 (* ### FIXME: removes only one lambda? *)
-(* Removes the lambdas from an equation of the form "t = (%x. u)" (cf.
-   "extensionalize_term" in "ATP_Systems"). *)
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+   (Cf. "extensionalize_term" in "ATP_Systems".) *)
 fun extensionalize_theorem th =
   case prop_of th of
     _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
@@ -145,7 +147,7 @@
   end;
 
 (* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
-fun do_introduce_combinators ct =
+fun introduce_combinators_in_cterm ct =
   if is_quasi_lambda_free (term_of ct) then
     Thm.reflexive ct
   else case term_of ct of
@@ -153,23 +155,23 @@
     let
       val (cv, cta) = Thm.dest_abs NONE ct
       val (v, _) = dest_Free (term_of cv)
-      val u_th = do_introduce_combinators cta
+      val u_th = introduce_combinators_in_cterm cta
       val cu = Thm.rhs_of u_th
       val comb_eq = abstract (Thm.cabs cv cu)
     in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   | _ $ _ =>
     let val (ct1, ct2) = Thm.dest_comb ct in
-        Thm.combination (do_introduce_combinators ct1)
-                        (do_introduce_combinators ct2)
+        Thm.combination (introduce_combinators_in_cterm ct1)
+                        (introduce_combinators_in_cterm ct2)
     end
 
-fun introduce_combinators th =
+fun introduce_combinators_in_theorem th =
   if is_quasi_lambda_free (prop_of th) then
     th
   else
     let
       val th = Drule.eta_contraction_rule th
-      val eqth = do_introduce_combinators (cprop_of th)
+      val eqth = introduce_combinators_in_cterm (cprop_of th)
     in Thm.equal_elim eqth th end
     handle THM (msg, _, _) =>
            (warning ("Error in the combinator translation of " ^
@@ -225,7 +227,7 @@
 (* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
    into NNF. *)
 fun to_nnf th ctxt0 =
-  let val th1 = th |> transform_elim |> zero_var_indexes
+  let val th1 = th |> transform_elim_theorem |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
       val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
                     |> extensionalize_theorem
@@ -241,7 +243,7 @@
                       (assume_skolem_funs nnfth)
     val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   in
-    cnfs |> map introduce_combinators
+    cnfs |> map introduce_combinators_in_theorem
          |> Variable.export ctxt ctxt0
          |> Meson.finish_cnf
          |> map Thm.close_derivation
@@ -279,7 +281,7 @@
 val neg_clausify =
   single
   #> Meson.make_clauses_unsorted
-  #> map introduce_combinators
+  #> map introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
 end;