# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID 31babd4b1552be3e882d20817fe3faa58ab23001
# Parent  9a8acc5adfa35b8f65316e7c488f8c1f2e7b50f4
killed odd connectives

diff -r 9a8acc5adfa3 -r 31babd4b1552 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -9,7 +9,7 @@
 sig
   datatype 'a fo_term = ATerm of 'a * 'a fo_term list
   datatype quantifier = AForall | AExists
-  datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+  datatype connective = ANot | AAnd | AOr | AImplies | AIff
   datatype ('a, 'b, 'c) formula =
     AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
     AConn of connective * ('a, 'b, 'c) formula list |
@@ -93,7 +93,7 @@
 
 datatype 'a fo_term = ATerm of 'a * 'a fo_term list
 datatype quantifier = AForall | AExists
-datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
+datatype connective = ANot | AAnd | AOr | AImplies | AIff
 datatype ('a, 'b, 'c) formula =
   AQuant of quantifier * ('a * 'b option) list * ('a, 'b, 'c) formula |
   AConn of connective * ('a, 'b, 'c) formula list |
@@ -147,9 +147,7 @@
   | raw_polarities_of_conn AAnd = (SOME true, SOME true)
   | raw_polarities_of_conn AOr = (SOME true, SOME true)
   | raw_polarities_of_conn AImplies = (SOME false, SOME true)
-  | raw_polarities_of_conn AIf = (SOME true, SOME false)
   | raw_polarities_of_conn AIff = (NONE, NONE)
-  | raw_polarities_of_conn ANotIff = (NONE, NONE)
 fun polarities_of_conn NONE = K (NONE, NONE)
   | polarities_of_conn (SOME pos) =
     raw_polarities_of_conn #> not pos ? pairself (Option.map not)
@@ -235,9 +233,7 @@
   | string_for_connective AAnd = tptp_and
   | string_for_connective AOr = tptp_or
   | string_for_connective AImplies = tptp_implies
-  | string_for_connective AIf = tptp_if
   | string_for_connective AIff = tptp_iff
-  | string_for_connective ANotIff = tptp_not_iff
 
 fun string_for_bound_var format (s, ty) =
   s ^ (if format = TFF orelse format = THF then
@@ -341,14 +337,10 @@
     AConn (AOr, map (clausify_formula1 true) phis)
   | clausify_formula1 true (AConn (AImplies, [phi1, phi2])) =
     AConn (AOr, [clausify_formula1 false phi1, clausify_formula1 true phi2])
-  | clausify_formula1 true (AConn (AIf, phis)) =
-    clausify_formula1 true (AConn (AImplies, rev phis))
   | clausify_formula1 _ _ = raise CLAUSIFY ()
 fun clausify_formula true (AConn (AIff, phis)) =
-    [clausify_formula1 true (AConn (AIf, phis)),
+    [clausify_formula1 true (AConn (AImplies, rev phis)),
      clausify_formula1 true (AConn (AImplies, phis))]
-  | clausify_formula false (AConn (ANotIff, phis)) =
-    clausify_formula true (AConn (AIff, phis))
   | clausify_formula pos phi = [clausify_formula1 pos phi]
 
 fun clausify_formula_line (Formula (ident, kind, phi, source, info)) =
diff -r 9a8acc5adfa3 -r 31babd4b1552 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -307,15 +307,21 @@
       >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
 and parse_formula x =
   (parse_literal
-   -- Scan.option ((Scan.this_string tptp_implies >> K AImplies
-                    || Scan.this_string tptp_iff >> K AIff
-                    || Scan.this_string tptp_not_iff >> K ANotIff
-                    || Scan.this_string tptp_if >> K AIf
-                    || $$ tptp_or >> K AOr
-                    || $$ tptp_and >> K AAnd)
-                   -- parse_formula)
+   -- Scan.option ((Scan.this_string tptp_implies
+                    || Scan.this_string tptp_iff
+                    || Scan.this_string tptp_not_iff
+                    || Scan.this_string tptp_if
+                    || $$ tptp_or
+                    || $$ tptp_and) -- parse_formula)
    >> (fn (phi1, NONE) => phi1
-        | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x
+        | (phi1, SOME (c, phi2)) =>
+          if c = tptp_implies then mk_aconn AImplies phi1 phi2
+          else if c = tptp_iff then mk_aconn AIff phi1 phi2
+          else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2)
+          else if c = tptp_if then mk_aconn AImplies phi2 phi1
+          else if c = tptp_or then mk_aconn AOr phi1 phi2
+          else if c = tptp_and then mk_aconn AAnd phi1 phi2
+          else raise Fail ("impossible connective " ^ quote c))) x
 and parse_quantified_formula x =
   (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
    --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
diff -r 9a8acc5adfa3 -r 31babd4b1552 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -568,10 +568,8 @@
                AAnd => s_conj
              | AOr => s_disj
              | AImplies => s_imp
-             | AIf => s_imp o swap
              | AIff => s_iff
-             | ANotIff => s_not o s_iff
-             | _ => raise Fail "unexpected connective")
+             | ANot => raise Fail "impossible connective")
       | AAtom tm => term_from_atom ctxt textual sym_tab pos tm
       | _ => raise FORMULA [phi]
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end