# HG changeset patch
# User blanchet
# Date 1282310187 -7200
# Node ID 4ca2cae2653f67b31c9c11c5f219c1684f1d5575
# Parent  fa7e19c6be747638fab30881ac6ced54c8f8271e
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
avoids relying on inconsistently implemented feature of TPTP format

diff -r fa7e19c6be74 -r 4ca2cae2653f src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Aug 20 14:18:55 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Aug 20 15:16:27 2010 +0200
@@ -15,7 +15,7 @@
     AConn of connective * ('a, 'b) formula list |
     AAtom of 'b
 
-  datatype kind = Axiom | Conjecture
+  datatype kind = Axiom | Hypothesis | Conjecture
   datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
   type 'a problem = (string * 'a problem_line list) list
 
@@ -42,7 +42,7 @@
   AConn of connective * ('a, 'b) formula list |
   AAtom of 'b
 
-datatype kind = Axiom | Conjecture
+datatype kind = Axiom | Hypothesis | Conjecture
 datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
 type 'a problem = (string * 'a problem_line list) list
 
@@ -76,8 +76,11 @@
 
 fun string_for_problem_line (Fof (ident, kind, phi)) =
   "fof(" ^ ident ^ ", " ^
-  (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
-  "    (" ^ string_for_formula phi ^ ")).\n"
+  (case kind of
+     Axiom => "axiom"
+   | Hypothesis => "hypothesis"
+   | Conjecture => "conjecture") ^
+  ",\n    (" ^ string_for_formula phi ^ ")).\n"
 fun strings_for_tptp_problem problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
diff -r fa7e19c6be74 -r 4ca2cae2653f src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 14:18:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Fri Aug 20 15:16:27 2010 +0200
@@ -143,9 +143,8 @@
       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
       handle THM _ =>
              (* A type variable of sort "{}" will make abstraction fail. *)
-             case kind of
-               Axiom => HOLogic.true_const
-             | Conjecture => HOLogic.false_const
+             if kind = Conjecture then HOLogic.false_const
+             else HOLogic.true_const
   end
 
 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
@@ -175,7 +174,7 @@
   in perhaps (try aux) end
 
 (* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (name, kind, t) =
+fun make_formula ctxt presimp name kind t =
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
@@ -185,7 +184,7 @@
               |> presimp ? presimplify_term thy
               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
-              |> kind = Conjecture ? freeze_term
+              |> kind <> Axiom ? freeze_term
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
     FOLFormula {name = name, combformula = combformula, kind = kind,
@@ -193,10 +192,13 @@
   end
 
 fun make_axiom ctxt presimp (name, th) =
-  (name, make_formula ctxt presimp (name, Axiom, prop_of th))
-fun make_conjectures ctxt ts =
-  map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
-       (0 upto length ts - 1) ts
+  (name, make_formula ctxt presimp name Axiom (prop_of th))
+fun make_conjecture ctxt ts =
+  let val last = length ts - 1 in
+    map2 (fn j => make_formula ctxt true (Int.toString j)
+                               (if j = last then Conjecture else Hypothesis))
+         (0 upto last) ts
+  end
 
 (** Helper facts **)
 
@@ -237,8 +239,6 @@
     |> map (snd o make_axiom ctxt false)
   end
 
-fun meta_not t = @{const "==>"} $ t $ @{prop False}
-
 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
   let
     val thy = ProofContext.theory_of ctxt
@@ -259,7 +259,7 @@
     val supers = tvar_classes_of_terms axiom_ts
     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
     (* TFrees in the conjecture; TVars in the axioms *)
-    val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
+    val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
     val (axiom_names, axioms) =
       ListPair.unzip (map (make_axiom ctxt true) axioms)
     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
@@ -359,7 +359,7 @@
   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type lit =
-  Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
+  Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
 fun problem_lines_for_free_types conjectures =
   let
     val litss = map free_type_literals_for_conjecture conjectures