author blanchet Fri, 20 Aug 2010 15:16:27 +0200 changeset 38613 4ca2cae2653f parent 38612 fa7e19c6be74 child 38614 61672fa2983a
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; avoids relying on inconsistently implemented feature of TPTP format
```--- 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" ::```
```--- 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```