author blanchet Wed, 23 May 2012 21:19:48 +0200 changeset 47971 2aea51a14200 parent 47970 257fc09aa8a1 child 47972 96c9b8381909
generate THF definitions
```--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 17:57:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 23 21:19:48 2012 +0200
@@ -1297,11 +1297,26 @@
atomic_types = atomic_Ts}
end

-fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
-  case t |> make_formula ctxt format type_enc iff_for_eq name stature Axiom of
-    formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
-    if s = tptp_true then NONE else SOME formula
-  | formula => SOME formula
+fun is_legitimate_thf_def (Const (@{const_name HOL.eq}, _) \$ t \$ u) =
+    (is_Const t orelse is_Free t) andalso
+    not (exists_subterm (curry (op =) t) u)
+  | is_legitimate_thf_def _ = false
+
+fun make_fact ctxt format type_enc iff_for_eq
+              ((name, stature as (_, status)), t) =
+  let
+    val role =
+      if is_type_enc_higher_order type_enc andalso status = Def andalso
+         is_legitimate_thf_def t then
+        Definition
+      else
+        Axiom
+  in
+    case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
+      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+      if s = tptp_true then NONE else SOME formula
+    | formula => SOME formula
+  end

fun s_not_prop (@{const Trueprop} \$ t) = @{const Trueprop} \$ s_not t
| s_not_prop _ = @{prop True} (* "t" is too meta for "metis" *)
@@ -2878,8 +2893,7 @@
else
I
| add_eq_deps _ _ = I
-    fun has_status status (_, info) =
-      extract_isabelle_status info = SOME status
+    fun has_status status (_, info) = extract_isabelle_status info = SOME status
fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
val graph =
Graph.empty```