# HG changeset patch
# User blanchet
# Date 1444074408 -7200
# Node ID 426c9c85809927b49945f04f9239bdede2be80e8
# Parent  fa7a46489285281a6a7c96d76e859ba9e810ac3f
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs

diff -r fa7a46489285 -r 426c9c858099 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Oct 05 18:03:58 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Oct 05 21:46:48 2015 +0200
@@ -309,24 +309,15 @@
     NONE
 
 val proxy_table =
-  [("c_False", (@{const_name False}, (@{thm fFalse_def},
-       ("fFalse", @{const_name ATP.fFalse})))),
-   ("c_True", (@{const_name True}, (@{thm fTrue_def},
-       ("fTrue", @{const_name ATP.fTrue})))),
-   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
-       ("fNot", @{const_name ATP.fNot})))),
-   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
-       ("fconj", @{const_name ATP.fconj})))),
-   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
-       ("fdisj", @{const_name ATP.fdisj})))),
-   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
-       ("fimplies", @{const_name ATP.fimplies})))),
-   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
-       ("fequal", @{const_name ATP.fequal})))),
-   ("c_All", (@{const_name All}, (@{thm fAll_def},
-       ("fAll", @{const_name ATP.fAll})))),
-   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
-       ("fEx", @{const_name ATP.fEx}))))]
+  [("c_False", (@{const_name False}, (@{thm fFalse_def}, ("fFalse", @{const_name fFalse})))),
+   ("c_True", (@{const_name True}, (@{thm fTrue_def}, ("fTrue", @{const_name fTrue})))),
+   ("c_Not", (@{const_name Not}, (@{thm fNot_def}, ("fNot", @{const_name fNot})))),
+   ("c_conj", (@{const_name conj}, (@{thm fconj_def}, ("fconj", @{const_name fconj})))),
+   ("c_disj", (@{const_name disj}, (@{thm fdisj_def}, ("fdisj", @{const_name fdisj})))),
+   ("c_implies", (@{const_name implies}, (@{thm fimplies_def}, ("fimplies", @{const_name fimplies})))),
+   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def}, ("fequal", @{const_name fequal})))),
+   ("c_All", (@{const_name All}, (@{thm fAll_def}, ("fAll", @{const_name fAll})))),
+   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def}, ("fEx", @{const_name fEx}))))]
 
 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
 
@@ -1534,7 +1525,7 @@
     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => pred_sym andalso min_ary = max_ary
   | NONE => false)
 
-val fTrue_iconst = IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
+val fTrue_iconst = IConst ((const_prefix ^ "fTrue", @{const_name fTrue}), @{typ bool}, [])
 val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
 
 fun predicatify completish tm =
diff -r fa7a46489285 -r 426c9c858099 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 05 18:03:58 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 05 21:46:48 2015 +0200
@@ -486,7 +486,7 @@
 
 val tptp_binary_ops =
   [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
-   tptp_equal, tptp_app]
+   tptp_equal, tptp_not_equal, tptp_app]
 
 fun parse_one_in_list xs =
   foldl1 (op ||) (map Scan.this_string xs)
@@ -515,12 +515,13 @@
   else raise Fail ("unrecognized quantification: " ^ q)
 
 fun remove_thf_app (ATerm ((x, ty), arg)) =
-  if x = tptp_app then
-    (case arg of
-      ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t))
-    | [AAbs ((var, tvar), phi), t] =>
-      remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t])))
-  else ATerm ((x, ty), map remove_thf_app arg)
+    if x = tptp_app then
+      (case arg of
+        ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t))
+      | [AAbs ((var, tvar), phi), t] =>
+        remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t])))
+    else
+      ATerm ((x, ty), map remove_thf_app arg)
   | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t)
 
 fun parse_thf0_typed_var x =
@@ -540,16 +541,13 @@
                     else I))
             ys t)
   || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
-  || scan_general_id --| $$ tptp_has_type -- parse_thf0_type
-    >> (fn (var, typ) => ATerm ((var, [typ]), []))
+  || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_thf0_type)
+    >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), []))
   || parse_ho_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_thf0_term --| $$ ")"
-  || scan_general_id >> mk_simple_aterm
   || parse_binary_op >> mk_simple_aterm) x
 and parse_thf0_term x =
-  (parse_simple_thf0_term
-      -- Scan.option (parse_binary_op
-      -- parse_thf0_term)
+  (parse_simple_thf0_term -- Scan.option (parse_binary_op -- parse_thf0_term)
     >> (fn (t1, SOME (c, t2)) =>
            if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2]
          | (t, NONE) => t)) x
@@ -557,10 +555,9 @@
 fun parse_thf0_formula x = (parse_thf0_term #>> remove_thf_app #>> AAtom) x
 
 fun parse_tstp_thf0_line problem =
-  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
-    || Scan.this_string tptp_tff || Scan.this_string tptp_thf)
-  -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
-  -- parse_thf0_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
+  (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ ","
+  -- Symbol.scan_ascii_id --| $$ "," -- parse_thf0_formula -- parse_tstp_extra_arguments --| $$ ")"
+  --| $$ "."
   >> (fn (((num, role), phi), deps) =>
       let
         val role' = role_of_tptp_string role
diff -r fa7a46489285 -r 426c9c858099 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Oct 05 18:03:58 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Oct 05 21:46:48 2015 +0200
@@ -271,11 +271,11 @@
                 |> map (apsnd Thm.prop_of)
                 |> (if waldmeister_new then
                       generate_waldmeister_problem ctxt hyp_ts concl_t
-                        #> (fn (a,b,c,d,e) => (a,b,c,d,SOME e))
+                      #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
                     else
                       generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
                         uncurried_aliases readable_names true hyp_ts concl_t
-                        #> (fn (a,b,c,d) => (a,b,c,d,NONE)))
+                      #> (fn (a, b, c, d) => (a, b, c, d, NONE)))
 
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem