generate full first-order formulas (FOF) in Sledgehammer

--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -115,13 +115,6 @@
   | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
   | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
 
-fun shape_of_clauses _ [] = []
-  | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
-  | shape_of_clauses j ((_ :: lits) :: clauses) =
-    let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
-      (j :: hd shape) :: tl shape
-    end
-
 
 (* Clause preparation *)
 
@@ -133,24 +126,42 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
 
-(* FIXME: kill *)
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun combformula_for_prop thy =
+  let
+    val do_term = combterm_from_term thy
+    fun do_quant bs q s T t' =
+      do_formula ((s, T) :: bs) t'
+      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+    and do_conn bs c t1 t2 =
+      do_formula bs t1 ##>> do_formula bs t2
+      #>> (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 =>
+        do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+        do_quant bs AForall s T t'
+      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+        do_quant bs AExists s T t'
+      | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
+      | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
+      | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
+      | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+        do_conn bs AIff t1 t2
+      | _ => (fn ts => do_term bs (Envir.eta_contract t)
+                       |>> APred ||> union (op =) ts)
+  in do_formula [] end
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (formula_id, formula_name, kind, th) skolems =
+fun make_clause thy (formula_id, formula_name, kind, t) skolems =
   let
-    val (skolems, t) = th |> prop_of |> conceal_skolem_terms formula_id skolems
-    val (lits, ctypes_sorts) = literals_of_term thy t
-    (* FIXME: avoid "literals_of_term *)
-    val combformula =
-      case lits of
-        [] => APred (CombConst (("c_False", "False"), CombType (("bool", "bool"), []), []))
-      | _ =>
-        let val phis = lits |> map (fn FOLLiteral (pos, tm) => APred tm |> not pos ? mk_anot) in
-          fold (mk_aconn AOr) (tl phis) (hd phis)
-          |> kind = Conjecture ? mk_anot
-        end
+    (* ### FIXME: introduce combinators and perform other transformations
+       previously done by Clausifier.to_nnf *)
+    val (skolems, t) =
+      t |> Object_Logic.atomize_term thy
+        |> conceal_skolem_terms formula_id skolems
+    val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     (skolems,
      FOLFormula {formula_name = formula_name, formula_id = formula_id,
@@ -160,7 +171,7 @@
 
 fun add_axiom_clause thy ((name, k), th) (skolems, clss) =
   let
-    val (skolems, cls) = make_clause thy (k, name, Axiom, th) skolems
+    val (skolems, cls) = make_clause thy (k, name, Axiom, prop_of th) skolems
   in (skolems, (name, cls) :: clss) end
 
 fun make_axiom_clauses thy clauses =
@@ -169,11 +180,11 @@
 fun make_conjecture_clauses thy =
   let
     fun aux _ _ [] = []
-      | aux n skolems (th :: ths) =
+      | aux n skolems (t :: ts) =
         let
           val (skolems, cls) =
-            make_clause thy (n, "conjecture", Conjecture, th) skolems
-        in cls :: aux (n + 1) skolems ths end
+            make_clause thy (n, "conjecture", Conjecture, t) skolems
+        in cls :: aux (n + 1) skolems ts end
   in aux 0 [] end
 
 (** Helper clauses **)
@@ -220,20 +231,24 @@
       @ (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
+
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses full_types goal_cls axcls extra_cls thy =
+fun prepare_clauses full_types hyp_ts concl_t axcls extra_cls thy =
   let
-    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
-    val ccls = subtract_cls extra_cls goal_cls
-    val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
-    val ccltms = map prop_of ccls
-    and axtms = map (prop_of o snd) extra_cls
-    val subs = tfree_classes_of_terms ccltms
-    and supers = tvar_classes_of_terms axtms
-    and tycons = type_consts_of_terms thy (ccltms @ axtms)
+    val goal_t = Logic.list_implies (hyp_ts, concl_t)
+    val is_FO = Meson.is_fol_term thy goal_t
+    val _ = trace_msg (fn _ => Syntax.string_of_term_global thy goal_t)
+    val axtms = map (prop_of o snd) extra_cls
+    val subs = tfree_classes_of_terms [goal_t]
+    val supers = tvar_classes_of_terms axtms
+    val tycons = type_consts_of_terms thy (goal_t :: axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
-    val conjectures = make_conjecture_clauses thy ccls
+    val conjectures =
+      make_conjecture_clauses thy (map negate_prop 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 =
@@ -307,20 +322,20 @@
     (* get clauses and prepare them for writing *)
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt;
-    val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
-    val goal_cls = List.concat goal_clss
+    (* ### FIXME: (1) preprocessing for "if" etc. *)
+    val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
     val the_filtered_clauses =
       case filtered_clauses of
         SOME fcls => fcls
       | NONE => relevant_facts full_types relevance_threshold
                     relevance_convergence defs_relevant max_axiom_clauses
                     (the_default prefers_theory_relevant theory_relevant)
-                    relevance_override goal goal_cls
+                    relevance_override goal hyp_ts concl_t
                 |> Clausifier.cnf_rules_pairs thy true
     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
     val (internal_thm_names, clauses) =
-      prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
-                      thy
+      prepare_clauses full_types hyp_ts concl_t the_axiom_clauses
+                      the_filtered_clauses thy
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -387,7 +402,9 @@
           val (pool, conjecture_offset) =
             write_tptp_file thy readable_names explicit_forall full_types
                             explicit_apply probfile clauses
-          val conjecture_shape = shape_of_clauses (conjecture_offset + 1) goal_clss
+          val conjecture_shape =
+            conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
+            |> map single (* ### FIXME: get rid of "map single" *)
           val result =
             do_run false
             |> (fn (_, msecs0, _, SOME _) =>
@@ -448,8 +465,8 @@
      string_of_int (to_generous_secs timeout),
    proof_delims = [tstp_proof_delims],
    known_failures =
-     [(Unprovable, "SZS status: Satisfiable"),
-      (Unprovable, "SZS status Satisfiable"),
+     [(Unprovable, "SZS status: CounterSatisfiable"),
+      (Unprovable, "SZS status CounterSatisfiable"),
       (TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
       (OutOfResources,

--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -11,8 +11,6 @@
   val cnf_rules_pairs :
     theory -> bool -> (string * thm) list -> ((string * int) * thm) list
   val neg_clausify: thm -> thm list
-  val neg_conjecture_clauses:
-    Proof.context -> thm -> int -> thm list list * (string * typ) list
 end;
 
 structure Clausifier : CLAUSIFIER =
@@ -222,7 +220,8 @@
     |> Thm.varifyT_global
   end
 
-(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
+(* 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
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
@@ -231,7 +230,7 @@
                     |> Meson.make_nnf ctxt
   in  (th3, ctxt)  end;
 
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+(* Skolemize a named theorem, with Skolem functions as additional premises. *)
 fun skolemize_theorem thy cheat th =
   let
     val ctxt0 = Variable.global_thm_context th
@@ -255,6 +254,7 @@
 (**** Translate a set of theorems into CNF ****)
 
 (*The combination of rev and tail recursion preserves the original order*)
+(* ### FIXME: kill "cheat" *)
 fun cnf_rules_pairs thy cheat =
   let
     fun do_one _ [] = []
@@ -280,13 +280,4 @@
   #> map introduce_combinators
   #> Meson.finish_cnf
 
-fun neg_conjecture_clauses ctxt st0 n =
-  let
-    (* "Option" is thrown if the assumptions contain schematic variables. *)
-    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
-    val ({params, prems, ...}, _) =
-      Subgoal.focus (Variable.set_body false ctxt) n st
-  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
-
-
 end;

--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -34,6 +34,7 @@
                   literals: fol_literal list, ctypes_sorts: typ list}
 
   val type_wrapper_name : string
+  val bound_var_prefix : string
   val schematic_var_prefix: string
   val fixed_var_prefix: string
   val tvar_prefix: string
@@ -46,6 +47,7 @@
   val ascii_of: string -> string
   val undo_ascii_of: string -> string
   val strip_prefix_and_undo_ascii: string -> string -> string option
+  val make_bound_var : string -> string
   val make_schematic_var : string * int -> string
   val make_fixed_var : string -> string
   val make_schematic_type_var : string * int -> string
@@ -63,6 +65,8 @@
   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   val combtyp_of : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
+  val combterm_from_term :
+    theory -> (string * typ) list -> term -> combterm * typ list
   val literals_of_term : theory -> term -> fol_literal list * typ list
   val conceal_skolem_terms :
     int -> (string * term) list -> term -> (string * term) list * term
@@ -77,8 +81,9 @@
 
 val type_wrapper_name = "ti"
 
-val schematic_var_prefix = "V_";
-val fixed_var_prefix = "v_";
+val bound_var_prefix = "B_"
+val schematic_var_prefix = "V_"
+val fixed_var_prefix = "v_"
 
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
@@ -177,8 +182,9 @@
 fun ascii_of_indexname (v,0) = ascii_of v
   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
 
-fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
-fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
+fun make_bound_var x = bound_var_prefix ^ ascii_of x
+fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
+fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
 
 fun make_schematic_type_var (x,i) =
       tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
@@ -402,8 +408,13 @@
   | simp_type_of (TVar (x, _)) =
     CombTVar (make_schematic_type_var x, string_of_indexname x)
 
-(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
-fun combterm_of thy (Const (c, T)) =
+(* Converts a term (with combinators) into a combterm. Also accummulates sort
+   infomation. *)
+fun combterm_from_term thy bs (P $ Q) =
+      let val (P', tsP) = combterm_from_term thy bs P
+          val (Q', tsQ) = combterm_from_term thy bs Q
+      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
+  | combterm_from_term thy _ (Const (c, T)) =
       let
         val (tp, ts) = type_of T
         val tvar_list =
@@ -414,22 +425,25 @@
           |> map simp_type_of
         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
       in  (c',ts)  end
-  | combterm_of _ (Free(v, T)) =
+  | combterm_from_term _ _ (Free (v, T)) =
       let val (tp,ts) = type_of T
           val v' = CombConst (`make_fixed_var v, tp, [])
       in  (v',ts)  end
-  | combterm_of _ (Var(v, T)) =
+  | combterm_from_term _ _ (Var (v, T)) =
       let val (tp,ts) = type_of T
           val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
       in  (v',ts)  end
-  | combterm_of thy (P $ Q) =
-      let val (P', tsP) = combterm_of thy P
-          val (Q', tsQ) = combterm_of thy Q
-      in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
-  | combterm_of _ (Abs _) = raise Fail "HOL clause: Abs"
+  | combterm_from_term _ bs (Bound j) =
+      let
+        val (s, T) = nth bs j
+        val (tp, ts) = type_of T
+        val v' = CombConst (`make_bound_var s, tp, [])
+      in (v', ts) end
+  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
-  | predicate_of thy (t, pos) = (combterm_of thy (Envir.eta_contract t), pos)
+  | predicate_of thy (t, pos) =
+    (combterm_from_term thy [] (Envir.eta_contract t), pos)
 
 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
     literals_of_term1 args thy P

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -16,7 +16,8 @@
     Proof.context -> thm list -> Facts.ref -> string * thm list
   val relevant_facts :
     bool -> real -> real -> bool -> int -> bool -> relevance_override
-    -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list
+    -> Proof.context * (thm list * 'a) -> term list -> term
+    -> (string * thm) list
 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -148,9 +149,8 @@
         do_term t0 #> do_formula pos t1  (* theory constant *)
       | _ => do_term t
   in
-    Symtab.empty
-    |> fold (Symtab.update o rpair []) boring_natural_consts
-    |> fold (do_formula pos) ts
+    Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
+                 |> fold (do_formula pos) ts
   end
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
@@ -343,7 +343,7 @@
 
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
-                     thy axioms goals =
+                     thy axioms goal_ts =
   if relevance_threshold > 1.0 then
     []
   else if relevance_threshold < 0.0 then
@@ -352,7 +352,7 @@
     let
       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
                            Symtab.empty
-      val goal_const_tab = get_consts_typs thy (SOME true) goals
+      val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
       val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
       val _ =
         trace_msg (fn () => "Initial constants: " ^
@@ -563,12 +563,14 @@
 fun relevant_facts full_types relevance_threshold relevance_convergence
                    defs_relevant max_new theory_relevant
                    (relevance_override as {add, del, only})
-                   (ctxt, (chained_ths, _)) goal_cls =
+                   (ctxt, (chained_ths, _)) hyp_ts concl_t =
   let
     val thy = ProofContext.theory_of ctxt
     val add_thms = maps (ProofContext.get_fact ctxt) add
     val has_override = not (null add) orelse not (null del)
-    val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
+(*###
+    val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
+*)
     val axioms =
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
           (map (name_thms_pair_from_ref ctxt chained_ths) add @
@@ -581,7 +583,7 @@
   in
     relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
-                     thy axioms (map prop_of goal_cls)
+                     thy axioms (concl_t :: hyp_ts)
     |> has_override ? make_unique
     |> sort_wrt fst
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -954,17 +954,12 @@
         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   in do_proof end
 
-fun strip_subgoal goal i =
-  let
-    val (t, frees) = Logic.goal_params (prop_of goal) i
-    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
-    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
-  in (rev (map dest_Free frees), hyp_ts, concl_t) end
-
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
                     (other_params as (full_types, _, atp_proof, thm_names, goal,
                                       i)) =
   let
+    (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal
+       to ATP_Systems *)
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -76,7 +76,7 @@
   | string_for_connective AIff = "<=>"
   | string_for_connective ANotIff = "<~>"
 fun string_for_formula (AQuant (q, xs, phi)) =
-    string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
+    string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
     string_for_formula phi
   | string_for_formula (AConn (c, [phi])) =
     string_for_connective c ^ " " ^ string_for_formula phi

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 14:14:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jul 26 17:03:21 2010 +0200
@@ -18,6 +18,7 @@
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
+  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -126,5 +127,11 @@
     | NONE => raise Type.TYPE_MATCH
   end
 
+fun strip_subgoal goal i =
+  let
+    val (t, frees) = Logic.goal_params (prop_of goal) i
+    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
+    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
+  in (rev (map dest_Free frees), hyp_ts, concl_t) end
 
 end;