author blanchet Thu, 10 May 2012 16:56:23 +0200 changeset 47905 9b6afe0eb69c parent 47904 67663c968d70 child 47906 09a896d295bd
cleaner handling of bi-implication for THF output of first-order type encodings
```--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 10 16:56:23 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 10 16:56:23 2012 +0200
@@ -1162,7 +1162,7 @@
| filt _ tm = tm
in filt 0 end

-fun iformula_from_prop ctxt type_enc eq_as_iff =
+fun iformula_from_prop ctxt type_enc iff_for_eq =
let
val thy = Proof_Context.theory_of ctxt
fun do_term bs t atomic_Ts =
@@ -1203,7 +1203,7 @@
| @{const HOL.implies} \$ t1 \$ t2 =>
do_conn bs AImplies (Option.map not pos) t1 pos t2
| Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) \$ t1 \$ t2 =>
-        if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
+        if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
| _ => do_term bs t
in do_formula [] end

@@ -1252,10 +1252,17 @@
end
handle TERM _ => @{const True}

-fun make_formula ctxt type_enc eq_as_iff name stature kind t =
+(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
+   for obscure technical reasons. *)
+fun should_use_iff_for_eq CNF _ = false
+  | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
+  | should_use_iff_for_eq _ _ = true
+
+fun make_formula ctxt format type_enc iff_for_eq name stature kind t =
let
+    val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
val (iformula, atomic_Ts) =
-      iformula_from_prop ctxt type_enc eq_as_iff (SOME (kind <> Conjecture)) t
+      iformula_from_prop ctxt type_enc iff_for_eq (SOME (kind <> Conjecture)) t
[]
|>> close_iformula_universally
in
@@ -1263,16 +1270,8 @@
atomic_types = atomic_Ts}
end

-(* Satallax prefers "=" to "<=>" *)
-fun is_format_eq_as_iff FOF = true
-  | is_format_eq_as_iff (TFF _) = true
-  | is_format_eq_as_iff (DFG _) = true
-  | is_format_eq_as_iff _ = false
-
-fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
-  case t |> make_formula ctxt type_enc
-                         (eq_as_iff andalso is_format_eq_as_iff format) name
-                         stature Axiom of
+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
@@ -1287,8 +1286,7 @@
fun make_conjecture ctxt format type_enc =
map (fn ((name, stature), (kind, t)) =>
t |> kind = Conjecture ? s_not
-            |> make_formula ctxt type_enc (is_format_eq_as_iff format) name
-                            stature kind)
+            |> make_formula ctxt format type_enc true name stature kind)

(** Finite and infinite type inference **)
```