src/HOL/ex/Classical.thy

 text\<open>The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.\<close>
 
 text\<open>Taken from \<open>FOL/Classical.thy\<close>. When porting examples from
 first-order logic, beware of the precedence of \<open>=\<close> versus \<open>\<leftrightarrow>\<close>.\<close>
 
-lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
+lemma "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P\<longrightarrow>Q) \<or> (P\<longrightarrow>R)"
 by blast
 
 text\<open>If and only if\<close>
 
 lemma "(P=Q) = (Q = (P::bool))"
 by blast
 
-lemma "~ (P = (~P))"
+lemma "\<not> (P = (\<not>P))"
 by blast
 
 
 text\<open>Sample problems from
   F. J. Pelletier,

 \<close>
 
 subsubsection\<open>Pelletier's examples\<close>
 
 text\<open>1\<close>
-lemma "(P-->Q)  =  (~Q --> ~P)"
+lemma "(P\<longrightarrow>Q)  =  (\<not>Q \<longrightarrow> \<not>P)"
 by blast
 
 text\<open>2\<close>
-lemma "(~ ~ P) =  P"
+lemma "(\<not> \<not> P) =  P"
 by blast
 
 text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
+lemma "\<not>(P\<longrightarrow>Q) \<longrightarrow> (Q\<longrightarrow>P)"
 by blast
 
 text\<open>4\<close>
-lemma "(~P-->Q)  =  (~Q --> P)"
+lemma "(\<not>P\<longrightarrow>Q)  =  (\<not>Q \<longrightarrow> P)"
 by blast
 
 text\<open>5\<close>
-lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
+lemma "((P\<or>Q)\<longrightarrow>(P\<or>R)) \<longrightarrow> (P\<or>(Q\<longrightarrow>R))"
 by blast
 
 text\<open>6\<close>
-lemma "P | ~ P"
+lemma "P \<or> \<not> P"
 by blast
 
 text\<open>7\<close>
-lemma "P | ~ ~ ~ P"
+lemma "P \<or> \<not> \<not> \<not> P"
 by blast
 
 text\<open>8.  Peirce's law\<close>
-lemma "((P-->Q) --> P)  -->  P"
+lemma "((P\<longrightarrow>Q) \<longrightarrow> P)  \<longrightarrow>  P"
 by blast
 
 text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+lemma "((P\<or>Q) \<and> (\<not>P\<or>Q) \<and> (P\<or> \<not>Q)) \<longrightarrow> \<not> (\<not>P \<or> \<not>Q)"
 by blast
 
 text\<open>10\<close>
-lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
+lemma "(Q\<longrightarrow>R) \<and> (R\<longrightarrow>P\<and>Q) \<and> (P\<longrightarrow>Q\<or>R) \<longrightarrow> (P=Q)"
 by blast
 
 text\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
 lemma "P=(P::bool)"
 by blast

 text\<open>12.  "Dijkstra's law"\<close>
 lemma "((P = Q) = R) = (P = (Q = R))"
 by blast
 
 text\<open>13.  Distributive law\<close>
-lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
+lemma "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))"
 by blast
 
 text\<open>14\<close>
-lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
+lemma "(P = Q) = ((Q \<or> \<not>P) \<and> (\<not>Q\<or>P))"
 by blast
 
 text\<open>15\<close>
-lemma "(P --> Q) = (~P | Q)"
+lemma "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
 by blast
 
 text\<open>16\<close>
-lemma "(P-->Q) | (Q-->P)"
+lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)"
 by blast
 
 text\<open>17\<close>
-lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
+lemma "((P \<and> (Q\<longrightarrow>R))\<longrightarrow>S)  =  ((\<not>P \<or> Q \<or> S) \<and> (\<not>P \<or> \<not>R \<or> S))"
 by blast
 
 subsubsection\<open>Classical Logic: examples with quantifiers\<close>
 
-lemma "(\<forall>x. P(x) & Q(x)) = ((\<forall>x. P(x)) & (\<forall>x. Q(x)))"
-by blast
-
-lemma "(\<exists>x. P-->Q(x))  =  (P --> (\<exists>x. Q(x)))"
-by blast
-
-lemma "(\<exists>x. P(x)-->Q) = ((\<forall>x. P(x)) --> Q)"
-by blast
-
-lemma "((\<forall>x. P(x)) | Q)  =  (\<forall>x. P(x) | Q)"
+lemma "(\<forall>x. P(x) \<and> Q(x)) = ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))"
+by blast
+
+lemma "(\<exists>x. P\<longrightarrow>Q(x))  =  (P \<longrightarrow> (\<exists>x. Q(x)))"
+by blast
+
+lemma "(\<exists>x. P(x)\<longrightarrow>Q) = ((\<forall>x. P(x)) \<longrightarrow> Q)"
+by blast
+
+lemma "((\<forall>x. P(x)) \<or> Q)  =  (\<forall>x. P(x) \<or> Q)"
 by blast
 
 text\<open>From Wishnu Prasetya\<close>
-lemma "(\<forall>s. q(s) --> r(s)) & ~r(s) & (\<forall>s. ~r(s) & ~q(s) --> p(t) | q(t))
-    --> p(t) | r(t)"
+lemma "(\<forall>x. Q(x) \<longrightarrow> R(x)) \<and> \<not>R(a) \<and> (\<forall>x. \<not>R(x) \<and> \<not>Q(x) \<longrightarrow> P(b) \<or> Q(b))
+    \<longrightarrow> P(b) \<or> R(b)"
 by blast
 
 
 subsubsection\<open>Problems requiring quantifier duplication\<close>
 
 text\<open>Theorem B of Peter Andrews, Theorem Proving via General Matings,
   JACM 28 (1981).\<close>
-lemma "(\<exists>x. \<forall>y. P(x) = P(y)) --> ((\<exists>x. P(x)) = (\<forall>y. P(y)))"
+lemma "(\<exists>x. \<forall>y. P(x) = P(y)) \<longrightarrow> ((\<exists>x. P(x)) = (\<forall>y. P(y)))"
 by blast
 
 text\<open>Needs multiple instantiation of the quantifier.\<close>
-lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
+lemma "(\<forall>x. P(x)\<longrightarrow>P(f(x)))  \<and>  P(d)\<longrightarrow>P(f(f(f(d))))"
 by blast
 
 text\<open>Needs double instantiation of the quantifier\<close>
-lemma "\<exists>x. P(x) --> P(a) & P(b)"
-by blast
-
-lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
-by blast
-
-lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
+lemma "\<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
+by blast
+
+lemma "\<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
+by blast
+
+lemma "\<exists>x. (\<exists>y. P(y)) \<longrightarrow> P(x)"
 by blast
 
 subsubsection\<open>Hard examples with quantifiers\<close>
 
 text\<open>Problem 18\<close>
-lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
+lemma "\<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
 by blast
 
 text\<open>Problem 19\<close>
-lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+lemma "\<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
 by blast
 
 text\<open>Problem 20\<close>
-lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))
-    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
+lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)\<and>Q(y)\<longrightarrow>R(z)\<and>S(w)))
+    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
 by blast
 
 text\<open>Problem 21\<close>
-lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P=Q(x))"
+lemma "(\<exists>x. P\<longrightarrow>Q(x)) \<and> (\<exists>x. Q(x)\<longrightarrow>P) \<longrightarrow> (\<exists>x. P=Q(x))"
 by blast
 
 text\<open>Problem 22\<close>
-lemma "(\<forall>x. P = Q(x))  -->  (P = (\<forall>x. Q(x)))"
+lemma "(\<forall>x. P = Q(x))  \<longrightarrow>  (P = (\<forall>x. Q(x)))"
 by blast
 
 text\<open>Problem 23\<close>
-lemma "(\<forall>x. P | Q(x))  =  (P | (\<forall>x. Q(x)))"
+lemma "(\<forall>x. P \<or> Q(x))  =  (P \<or> (\<forall>x. Q(x)))"
 by blast
 
 text\<open>Problem 24\<close>
-lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &
-     (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))
-    --> (\<exists>x. P(x)&R(x))"
+lemma "\<not>(\<exists>x. S(x)\<and>Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x)\<or>R(x)) \<and>
+     (\<not>(\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x)\<or>R(x) \<longrightarrow> S(x))
+    \<longrightarrow> (\<exists>x. P(x)\<and>R(x))"
 by blast
 
 text\<open>Problem 25\<close>
-lemma "(\<exists>x. P(x)) &
-        (\<forall>x. L(x) --> ~ (M(x) & R(x))) &
-        (\<forall>x. P(x) --> (M(x) & L(x))) &
-        ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))
-    --> (\<exists>x. Q(x)&P(x))"
+lemma "(\<exists>x. P(x)) \<and>
+        (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
+        (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
+        ((\<forall>x. P(x)\<longrightarrow>Q(x)) \<or> (\<exists>x. P(x)\<and>R(x)))
+    \<longrightarrow> (\<exists>x. Q(x)\<and>P(x))"
 by blast
 
 text\<open>Problem 26\<close>
-lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) &
-      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) = s(y)))
-  --> ((\<forall>x. p(x)-->r(x)) = (\<forall>x. q(x)-->s(x)))"
+lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) \<and>
+      (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) = s(y)))
+  \<longrightarrow> ((\<forall>x. p(x)\<longrightarrow>r(x)) = (\<forall>x. q(x)\<longrightarrow>s(x)))"
 by blast
 
 text\<open>Problem 27\<close>
-lemma "(\<exists>x. P(x) & ~Q(x)) &
-              (\<forall>x. P(x) --> R(x)) &
-              (\<forall>x. M(x) & L(x) --> P(x)) &
-              ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))
-          --> (\<forall>x. M(x) --> ~L(x))"
+lemma "(\<exists>x. P(x) \<and> \<not>Q(x)) \<and>
+              (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
+              (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
+              ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
+          \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not>L(x))"
 by blast
 
 text\<open>Problem 28.  AMENDED\<close>
-lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &
-        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &
-        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))
-    --> (\<forall>x. P(x) & L(x) --> M(x))"
+lemma "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+        ((\<forall>x. Q(x)\<or>R(x)) \<longrightarrow> (\<exists>x. Q(x)\<and>S(x))) \<and>
+        ((\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
+    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
 by blast
 
 text\<open>Problem 29.  Essentially the same as Principia Mathematica *11.71\<close>
-lemma "(\<exists>x. F(x)) & (\<exists>y. G(y))
-    --> ( ((\<forall>x. F(x)-->H(x)) & (\<forall>y. G(y)-->J(y)))  =
-          (\<forall>x y. F(x) & G(y) --> H(x) & J(y)))"
+lemma "(\<exists>x. F(x)) \<and> (\<exists>y. G(y))
+    \<longrightarrow> ( ((\<forall>x. F(x)\<longrightarrow>H(x)) \<and> (\<forall>y. G(y)\<longrightarrow>J(y)))  =
+          (\<forall>x y. F(x) \<and> G(y) \<longrightarrow> H(x) \<and> J(y)))"
 by blast
 
 text\<open>Problem 30\<close>
-lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &
-        (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
-    --> (\<forall>x. S(x))"
+lemma "(\<forall>x. P(x) \<or> Q(x) \<longrightarrow> \<not> R(x)) \<and>
+        (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
+    \<longrightarrow> (\<forall>x. S(x))"
 by blast
 
 text\<open>Problem 31\<close>
-lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &
-        (\<exists>x. L(x) & P(x)) &
-        (\<forall>x. ~ R(x) --> M(x))
-    --> (\<exists>x. L(x) & M(x))"
+lemma "\<not>(\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+        (\<exists>x. L(x) \<and> P(x)) \<and>
+        (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
+    \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
 by blast
 
 text\<open>Problem 32\<close>
-lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &
-        (\<forall>x. S(x) & R(x) --> L(x)) &
-        (\<forall>x. M(x) --> R(x))
-    --> (\<forall>x. P(x) & M(x) --> L(x))"
+lemma "(\<forall>x. P(x) \<and> (Q(x)\<or>R(x))\<longrightarrow>S(x)) \<and>
+        (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
+        (\<forall>x. M(x) \<longrightarrow> R(x))
+    \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
 by blast
 
 text\<open>Problem 33\<close>
-lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  =
-     (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
+lemma "(\<forall>x. P(a) \<and> (P(x)\<longrightarrow>P(b))\<longrightarrow>P(c))  =
+     (\<forall>x. (\<not>P(a) \<or> P(x) \<or> P(c)) \<and> (\<not>P(a) \<or> \<not>P(b) \<or> P(c)))"
 by blast
 
 text\<open>Problem 34  AMENDED (TWICE!!)\<close>
 text\<open>Andrews's challenge\<close>
 lemma "((\<exists>x. \<forall>y. p(x) = p(y))  =

               ((\<exists>x. \<forall>y. q(x) = q(y))  =
                ((\<exists>x. p(x)) = (\<forall>y. q(y))))"
 by blast
 
 text\<open>Problem 35\<close>
-lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
+lemma "\<exists>x y. P x y \<longrightarrow>  (\<forall>u v. P u v)"
 by blast
 
 text\<open>Problem 36\<close>
-lemma "(\<forall>x. \<exists>y. J x y) &
-        (\<forall>x. \<exists>y. G x y) &
-        (\<forall>x y. J x y | G x y -->
-        (\<forall>z. J y z | G y z --> H x z))
-    --> (\<forall>x. \<exists>y. H x y)"
+lemma "(\<forall>x. \<exists>y. J x y) \<and>
+        (\<forall>x. \<exists>y. G x y) \<and>
+        (\<forall>x y. J x y \<or> G x y \<longrightarrow>
+        (\<forall>z. J y z \<or> G y z \<longrightarrow> H x z))
+    \<longrightarrow> (\<forall>x. \<exists>y. H x y)"
 by blast
 
 text\<open>Problem 37\<close>
 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
-           (P x z -->P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &
-        (\<forall>x z. ~(P x z) --> (\<exists>y. Q y z)) &
-        ((\<exists>x y. Q x y) --> (\<forall>x. R x x))
-    --> (\<forall>x. \<exists>y. R x y)"
+           (P x z \<longrightarrow>P y w) \<and> P y z \<and> (P y w \<longrightarrow> (\<exists>u. Q u w))) \<and>
+        (\<forall>x z. \<not>(P x z) \<longrightarrow> (\<exists>y. Q y z)) \<and>
+        ((\<exists>x y. Q x y) \<longrightarrow> (\<forall>x. R x x))
+    \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
 by blast
 
 text\<open>Problem 38\<close>
-lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r x y)) -->
-           (\<exists>z. \<exists>w. p(z) & r x w & r w z))  =
-     (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r x w & r w z)) &
-           (~p(a) | ~(\<exists>y. p(y) & r x y) |
-            (\<exists>z. \<exists>w. p(z) & r x w & r w z)))"
+lemma "(\<forall>x. p(a) \<and> (p(x) \<longrightarrow> (\<exists>y. p(y) \<and> r x y)) \<longrightarrow>
+           (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z))  =
+     (\<forall>x. (\<not>p(a) \<or> p(x) \<or> (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z)) \<and>
+           (\<not>p(a) \<or> \<not>(\<exists>y. p(y) \<and> r x y) \<or>
+            (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z)))"
 by blast (*beats fast!*)
 
 text\<open>Problem 39\<close>
-lemma "~ (\<exists>x. \<forall>y. F y x = (~ F y y))"
+lemma "\<not> (\<exists>x. \<forall>y. F y x = (\<not> F y y))"
 by blast
 
 text\<open>Problem 40.  AMENDED\<close>
 lemma "(\<exists>y. \<forall>x. F x y = F x x)
-        -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~ F z x))"
+        \<longrightarrow>  \<not> (\<forall>x. \<exists>y. \<forall>z. F z y = (\<not> F z x))"
 by blast
 
 text\<open>Problem 41\<close>
-lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z & ~ f x x))
-               --> ~ (\<exists>z. \<forall>x. f x z)"
+lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z \<and> \<not> f x x))
+               \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
 by blast
 
 text\<open>Problem 42\<close>
-lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
+lemma "\<not> (\<exists>y. \<forall>x. p x y = (\<not> (\<exists>z. p x z \<and> p z x)))"
 by blast
 
 text\<open>Problem 43!!\<close>
-lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x = (p z y::bool)))
-  --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
+lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x \<longleftrightarrow> (p z y)))
+  \<longrightarrow> (\<forall>x. (\<forall>y. q x y \<longleftrightarrow> (q y x)))"
 by blast
 
 text\<open>Problem 44\<close>
-lemma "(\<forall>x. f(x) -->
-              (\<exists>y. g(y) & h x y & (\<exists>y. g(y) & ~ h x y)))  &
-              (\<exists>x. j(x) & (\<forall>y. g(y) --> h x y))
-              --> (\<exists>x. j(x) & ~f(x))"
+lemma "(\<forall>x. f(x) \<longrightarrow>
+              (\<exists>y. g(y) \<and> h x y \<and> (\<exists>y. g(y) \<and> \<not> h x y)))  \<and>
+              (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h x y))
+              \<longrightarrow> (\<exists>x. j(x) \<and> \<not>f(x))"
 by blast
 
 text\<open>Problem 45\<close>
-lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h x y --> j x y)
-                      --> (\<forall>y. g(y) & h x y --> k(y))) &
-     ~ (\<exists>y. l(y) & k(y)) &
-     (\<exists>x. f(x) & (\<forall>y. h x y --> l(y))
-                & (\<forall>y. g(y) & h x y --> j x y))
-      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h x y))"
+lemma "(\<forall>x. f(x) \<and> (\<forall>y. g(y) \<and> h x y \<longrightarrow> j x y)
+                      \<longrightarrow> (\<forall>y. g(y) \<and> h x y \<longrightarrow> k(y))) \<and>
+     \<not> (\<exists>y. l(y) \<and> k(y)) \<and>
+     (\<exists>x. f(x) \<and> (\<forall>y. h x y \<longrightarrow> l(y))
+                \<and> (\<forall>y. g(y) \<and> h x y \<longrightarrow> j x y))
+      \<longrightarrow> (\<exists>x. f(x) \<and> \<not> (\<exists>y. g(y) \<and> h x y))"
 by blast
 
 
 subsubsection\<open>Problems (mainly) involving equality or functions\<close>
 
 text\<open>Problem 48\<close>
-lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+lemma "(a=b \<or> c=d) \<and> (a=c \<or> b=d) \<longrightarrow> a=d \<or> b=c"
 by blast
 
 text\<open>Problem 49  NOT PROVED AUTOMATICALLY.
      Hard because it involves substitution for Vars
   the type constraint ensures that x,y,z have the same type as a,b,u.\<close>
-lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b)
-                --> (\<forall>u::'a. P(u))"
+lemma "(\<exists>x y::'a. \<forall>z. z=x \<or> z=y) \<and> P(a) \<and> P(b) \<and> (\<not>a=b)
+                \<longrightarrow> (\<forall>u::'a. P(u))"
 by metis
 
 text\<open>Problem 50.  (What has this to do with equality?)\<close>
-lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
+lemma "(\<forall>x. P a x \<or> (\<forall>y. P x y)) \<longrightarrow> (\<exists>x. \<forall>y. P x y)"
 by blast
 
 text\<open>Problem 51\<close>
-lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->
+lemma "(\<exists>z w. \<forall>x y. P x y = (x=z \<and> y=w)) \<longrightarrow>
      (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))"
 by blast
 
 text\<open>Problem 52. Almost the same as 51.\<close>
-lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->
+lemma "(\<exists>z w. \<forall>x y. P x y = (x=z \<and> y=w)) \<longrightarrow>
      (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))"
 by blast
 
 text\<open>Problem 55\<close>
 
 text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   fast DISCOVERS who killed Agatha.\<close>
-schematic_goal "lives(agatha) & lives(butler) & lives(charles) &
-   (killed agatha agatha | killed butler agatha | killed charles agatha) &
-   (\<forall>x y. killed x y --> hates x y & ~richer x y) &
-   (\<forall>x. hates agatha x --> ~hates charles x) &
-   (hates agatha agatha & hates agatha charles) &
-   (\<forall>x. lives(x) & ~richer x agatha --> hates butler x) &
-   (\<forall>x. hates agatha x --> hates butler x) &
-   (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
+schematic_goal "lives(agatha) \<and> lives(butler) \<and> lives(charles) \<and>
+   (killed agatha agatha \<or> killed butler agatha \<or> killed charles agatha) \<and>
+   (\<forall>x y. killed x y \<longrightarrow> hates x y \<and> \<not>richer x y) \<and>
+   (\<forall>x. hates agatha x \<longrightarrow> \<not>hates charles x) \<and>
+   (hates agatha agatha \<and> hates agatha charles) \<and>
+   (\<forall>x. lives(x) \<and> \<not>richer x agatha \<longrightarrow> hates butler x) \<and>
+   (\<forall>x. hates agatha x \<longrightarrow> hates butler x) \<and>
+   (\<forall>x. \<not>hates x agatha \<or> \<not>hates x butler \<or> \<not>hates x charles) \<longrightarrow>
     killed ?who agatha"
 by fast
 
 text\<open>Problem 56\<close>
-lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) = (\<forall>x. P(x) --> P(f(x)))"
+lemma "(\<forall>x. (\<exists>y. P(y) \<and> x=f(y)) \<longrightarrow> P(x)) = (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
 by blast
 
 text\<open>Problem 57\<close>
-lemma "P (f a b) (f b c) & P (f b c) (f a c) &
-     (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
+lemma "P (f a b) (f b c) \<and> P (f b c) (f a c) \<and>
+     (\<forall>x y z. P x y \<and> P y z \<longrightarrow> P x z)    \<longrightarrow>   P (f a b) (f a c)"
 by blast
 
 text\<open>Problem 58  NOT PROVED AUTOMATICALLY\<close>
-lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
+lemma "(\<forall>x y. f(x)=g(y)) \<longrightarrow> (\<forall>x y. f(f(x))=f(g(y)))"
 by (fast intro: arg_cong [of concl: f])
 
 text\<open>Problem 59\<close>
-lemma "(\<forall>x. P(x) = (~P(f(x)))) --> (\<exists>x. P(x) & ~P(f(x)))"
+lemma "(\<forall>x. P(x) = (\<not>P(f(x)))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not>P(f(x)))"
 by blast
 
 text\<open>Problem 60\<close>
-lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
+lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y \<longrightarrow> P z (f x)) \<and> P x y)"
 by blast
 
 text\<open>Problem 62 as corrected in JAR 18 (1997), page 135\<close>
-lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =
-      (\<forall>x. (~ p a | p x | p(f(f x))) &
-              (~ p a | ~ p(f x) | p(f(f x))))"
+lemma "(\<forall>x. p a \<and> (p x \<longrightarrow> p(f x)) \<longrightarrow> p(f(f x)))  =
+      (\<forall>x. (\<not> p a \<or> p x \<or> p(f(f x))) \<and>
+              (\<not> p a \<or> \<not> p(f x) \<or> p(f(f x))))"
 by blast
 
 text\<open>From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   fast indeed copes!\<close>
-lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &
-       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &
-       (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
+lemma "(\<forall>x. F(x) \<and> \<not>G(x) \<longrightarrow> (\<exists>y. H(x,y) \<and> J(y))) \<and>
+       (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y))) \<and>
+       (\<forall>x. K(x) \<longrightarrow> \<not>G(x))  \<longrightarrow>  (\<exists>x. K(x) \<and> J(x))"
 by fast
 
 text\<open>From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
   It does seem obvious!\<close>
-lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &
-       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &
-       (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
+lemma "(\<forall>x. F(x) \<and> \<not>G(x) \<longrightarrow> (\<exists>y. H(x,y) \<and> J(y))) \<and>
+       (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y)))  \<and>
+       (\<forall>x. K(x) \<longrightarrow> \<not>G(x))   \<longrightarrow>   (\<exists>x. K(x) \<longrightarrow> \<not>G(x))"
 by fast
 
 text\<open>Attributed to Lewis Carroll by S. G. Pulman.  The first or last
 assumption can be deleted.\<close>
-lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &
-      ~ (\<exists>x. grocer(x) & healthy(x)) &
-      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &
-      (\<forall>x. cyclist(x) --> industrious(x)) &
-      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))
-      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
-by blast
-
-lemma "(\<forall>x y. R(x,y) | R(y,x)) &
-       (\<forall>x y. S(x,y) & S(y,x) --> x=y) &
-       (\<forall>x y. R(x,y) --> S(x,y))    -->   (\<forall>x y. S(x,y) --> R(x,y))"
+lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
+      \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
+      (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
+      (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
+      (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
+      \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
+by blast
+
+lemma "(\<forall>x y. R(x,y) \<or> R(y,x)) \<and>
+       (\<forall>x y. S(x,y) \<and> S(y,x) \<longrightarrow> x=y) \<and>
+       (\<forall>x y. R(x,y) \<longrightarrow> S(x,y))    \<longrightarrow>   (\<forall>x y. S(x,y) \<longrightarrow> R(x,y))"
 by blast
 
 
 subsection\<open>Model Elimination Prover\<close>
 
 
 text\<open>Trying out meson with arguments\<close>
-lemma "x < y & y < z --> ~ (z < (x::nat))"
+lemma "x < y \<and> y < z \<longrightarrow> \<not> (z < (x::nat))"
 by (meson order_less_irrefl order_less_trans)
 
 text\<open>The "small example" from Bezem, Hendriks and de Nivelle,
 Automatic Proof Construction in Type Theory Using Resolution,
 JAR 29: 3-4 (2002), pages 253-275\<close>
-lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
-       (\<forall>x. \<exists>y. R(x,y)) -->
-       ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
+lemma "(\<forall>x y z. R(x,y) \<and> R(y,z) \<longrightarrow> R(x,z)) \<and>
+       (\<forall>x. \<exists>y. R(x,y)) \<longrightarrow>
+       \<not> (\<forall>x. P x = (\<forall>y. R(x,y) \<longrightarrow> \<not> P y))"
 by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
     \<comment> \<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>
 
 
 subsubsection\<open>Pelletier's examples\<close>
 text\<open>1\<close>
-lemma "(P --> Q)  =  (~Q --> ~P)"
+lemma "(P \<longrightarrow> Q)  =  (\<not>Q \<longrightarrow> \<not>P)"
 by blast
 
 text\<open>2\<close>
-lemma "(~ ~ P) =  P"
+lemma "(\<not> \<not> P) =  P"
 by blast
 
 text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
+lemma "\<not>(P\<longrightarrow>Q) \<longrightarrow> (Q\<longrightarrow>P)"
 by blast
 
 text\<open>4\<close>
-lemma "(~P-->Q)  =  (~Q --> P)"
+lemma "(\<not>P\<longrightarrow>Q)  =  (\<not>Q \<longrightarrow> P)"
 by blast
 
 text\<open>5\<close>
-lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
+lemma "((P\<or>Q)\<longrightarrow>(P\<or>R)) \<longrightarrow> (P\<or>(Q\<longrightarrow>R))"
 by blast
 
 text\<open>6\<close>
-lemma "P | ~ P"
+lemma "P \<or> \<not> P"
 by blast
 
 text\<open>7\<close>
-lemma "P | ~ ~ ~ P"
+lemma "P \<or> \<not> \<not> \<not> P"
 by blast
 
 text\<open>8.  Peirce's law\<close>
-lemma "((P-->Q) --> P)  -->  P"
+lemma "((P\<longrightarrow>Q) \<longrightarrow> P)  \<longrightarrow>  P"
 by blast
 
 text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+lemma "((P\<or>Q) \<and> (\<not>P\<or>Q) \<and> (P\<or> \<not>Q)) \<longrightarrow> \<not> (\<not>P \<or> \<not>Q)"
 by blast
 
 text\<open>10\<close>
-lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
+lemma "(Q\<longrightarrow>R) \<and> (R\<longrightarrow>P\<and>Q) \<and> (P\<longrightarrow>Q\<or>R) \<longrightarrow> (P=Q)"
 by blast
 
 text\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
 lemma "P=(P::bool)"
 by blast

 text\<open>12.  "Dijkstra's law"\<close>
 lemma "((P = Q) = R) = (P = (Q = R))"
 by blast
 
 text\<open>13.  Distributive law\<close>
-lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
+lemma "(P \<or> (Q \<and> R)) = ((P \<or> Q) \<and> (P \<or> R))"
 by blast
 
 text\<open>14\<close>
-lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
+lemma "(P = Q) = ((Q \<or> \<not>P) \<and> (\<not>Q\<or>P))"
 by blast
 
 text\<open>15\<close>
-lemma "(P --> Q) = (~P | Q)"
+lemma "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
 by blast
 
 text\<open>16\<close>
-lemma "(P-->Q) | (Q-->P)"
+lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)"
 by blast
 
 text\<open>17\<close>
-lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
+lemma "((P \<and> (Q\<longrightarrow>R))\<longrightarrow>S)  =  ((\<not>P \<or> Q \<or> S) \<and> (\<not>P \<or> \<not>R \<or> S))"
 by blast
 
 subsubsection\<open>Classical Logic: examples with quantifiers\<close>
 
-lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))"
-by blast
-
-lemma "(\<exists>x. P --> Q x)  =  (P --> (\<exists>x. Q x))"
-by blast
-
-lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)"
-by blast
-
-lemma "((\<forall>x. P x) | Q)  =  (\<forall>x. P x | Q)"
-by blast
-
-lemma "(\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
+lemma "(\<forall>x. P x \<and> Q x) = ((\<forall>x. P x) \<and> (\<forall>x. Q x))"
+by blast
+
+lemma "(\<exists>x. P \<longrightarrow> Q x)  =  (P \<longrightarrow> (\<exists>x. Q x))"
+by blast
+
+lemma "(\<exists>x. P x \<longrightarrow> Q) = ((\<forall>x. P x) \<longrightarrow> Q)"
+by blast
+
+lemma "((\<forall>x. P x) \<or> Q)  =  (\<forall>x. P x \<or> Q)"
+by blast
+
+lemma "(\<forall>x. P x \<longrightarrow> P(f x))  \<and>  P d \<longrightarrow> P(f(f(f d)))"
 by blast
 
 text\<open>Needs double instantiation of EXISTS\<close>
-lemma "\<exists>x. P x --> P a & P b"
-by blast
-
-lemma "\<exists>z. P z --> (\<forall>x. P x)"
+lemma "\<exists>x. P x \<longrightarrow> P a \<and> P b"
+by blast
+
+lemma "\<exists>z. P z \<longrightarrow> (\<forall>x. P x)"
 by blast
 
 text\<open>From a paper by Claire Quigley\<close>
-lemma "\<exists>y. ((P c & Q y) | (\<exists>z. ~ Q z)) | (\<exists>x. ~ P x & Q d)"
+lemma "\<exists>y. ((P c \<and> Q y) \<or> (\<exists>z. \<not> Q z)) \<or> (\<exists>x. \<not> P x \<and> Q d)"
 by fast
 
 subsubsection\<open>Hard examples with quantifiers\<close>
 
 text\<open>Problem 18\<close>
-lemma "\<exists>y. \<forall>x. P y --> P x"
+lemma "\<exists>y. \<forall>x. P y \<longrightarrow> P x"
 by blast
 
 text\<open>Problem 19\<close>
-lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)"
+lemma "\<exists>x. \<forall>y z. (P y \<longrightarrow> Q z) \<longrightarrow> (P x \<longrightarrow> Q x)"
 by blast
 
 text\<open>Problem 20\<close>
-lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w))
-    --> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)"
+lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x \<and> Q y \<longrightarrow> R z \<and> S w))
+    \<longrightarrow> (\<exists>x y. P x \<and> Q y) \<longrightarrow> (\<exists>z. R z)"
 by blast
 
 text\<open>Problem 21\<close>
-lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)"
+lemma "(\<exists>x. P \<longrightarrow> Q x) \<and> (\<exists>x. Q x \<longrightarrow> P) \<longrightarrow> (\<exists>x. P=Q x)"
 by blast
 
 text\<open>Problem 22\<close>
-lemma "(\<forall>x. P = Q x)  -->  (P = (\<forall>x. Q x))"
+lemma "(\<forall>x. P = Q x)  \<longrightarrow>  (P = (\<forall>x. Q x))"
 by blast
 
 text\<open>Problem 23\<close>
-lemma "(\<forall>x. P | Q x)  =  (P | (\<forall>x. Q x))"
+lemma "(\<forall>x. P \<or> Q x)  =  (P \<or> (\<forall>x. Q x))"
 by blast
 
 text\<open>Problem 24\<close>  (*The first goal clause is useless*)
-lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) &
-      (~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x)
-    --> (\<exists>x. P x & R x)"
+lemma "\<not>(\<exists>x. S x \<and> Q x) \<and> (\<forall>x. P x \<longrightarrow> Q x \<or> R x) \<and>
+      (\<not>(\<exists>x. P x) \<longrightarrow> (\<exists>x. Q x)) \<and> (\<forall>x. Q x \<or> R x \<longrightarrow> S x)
+    \<longrightarrow> (\<exists>x. P x \<and> R x)"
 by blast
 
 text\<open>Problem 25\<close>
-lemma "(\<exists>x. P x) &
-      (\<forall>x. L x --> ~ (M x & R x)) &
-      (\<forall>x. P x --> (M x & L x)) &
-      ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x))
-    --> (\<exists>x. Q x & P x)"
+lemma "(\<exists>x. P x) \<and>
+      (\<forall>x. L x \<longrightarrow> \<not> (M x \<and> R x)) \<and>
+      (\<forall>x. P x \<longrightarrow> (M x \<and> L x)) \<and>
+      ((\<forall>x. P x \<longrightarrow> Q x) \<or> (\<exists>x. P x \<and> R x))
+    \<longrightarrow> (\<exists>x. Q x \<and> P x)"
 by blast
 
 text\<open>Problem 26; has 24 Horn clauses\<close>
-lemma "((\<exists>x. p x) = (\<exists>x. q x)) &
-      (\<forall>x. \<forall>y. p x & q y --> (r x = s y))
-  --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
+lemma "((\<exists>x. p x) = (\<exists>x. q x)) \<and>
+      (\<forall>x. \<forall>y. p x \<and> q y \<longrightarrow> (r x = s y))
+  \<longrightarrow> ((\<forall>x. p x \<longrightarrow> r x) = (\<forall>x. q x \<longrightarrow> s x))"
 by blast
 
 text\<open>Problem 27; has 13 Horn clauses\<close>
-lemma "(\<exists>x. P x & ~Q x) &
-      (\<forall>x. P x --> R x) &
-      (\<forall>x. M x & L x --> P x) &
-      ((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x))
-      --> (\<forall>x. M x --> ~L x)"
+lemma "(\<exists>x. P x \<and> \<not>Q x) \<and>
+      (\<forall>x. P x \<longrightarrow> R x) \<and>
+      (\<forall>x. M x \<and> L x \<longrightarrow> P x) \<and>
+      ((\<exists>x. R x \<and> \<not> Q x) \<longrightarrow> (\<forall>x. L x \<longrightarrow> \<not> R x))
+      \<longrightarrow> (\<forall>x. M x \<longrightarrow> \<not>L x)"
 by blast
 
 text\<open>Problem 28.  AMENDED; has 14 Horn clauses\<close>
-lemma "(\<forall>x. P x --> (\<forall>x. Q x)) &
-      ((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) &
-      ((\<exists>x. S x) --> (\<forall>x. L x --> M x))
-    --> (\<forall>x. P x & L x --> M x)"
+lemma "(\<forall>x. P x \<longrightarrow> (\<forall>x. Q x)) \<and>
+      ((\<forall>x. Q x \<or> R x) \<longrightarrow> (\<exists>x. Q x \<and> S x)) \<and>
+      ((\<exists>x. S x) \<longrightarrow> (\<forall>x. L x \<longrightarrow> M x))
+    \<longrightarrow> (\<forall>x. P x \<and> L x \<longrightarrow> M x)"
 by blast
 
 text\<open>Problem 29.  Essentially the same as Principia Mathematica *11.71.
       62 Horn clauses\<close>
-lemma "(\<exists>x. F x) & (\<exists>y. G y)
-    --> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y))  =
-          (\<forall>x y. F x & G y --> H x & J y))"
+lemma "(\<exists>x. F x) \<and> (\<exists>y. G y)
+    \<longrightarrow> ( ((\<forall>x. F x \<longrightarrow> H x) \<and> (\<forall>y. G y \<longrightarrow> J y))  =
+          (\<forall>x y. F x \<and> G y \<longrightarrow> H x \<and> J y))"
 by blast
 
 
 text\<open>Problem 30\<close>
-lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x)
-       --> (\<forall>x. S x)"
+lemma "(\<forall>x. P x \<or> Q x \<longrightarrow> \<not> R x) \<and> (\<forall>x. (Q x \<longrightarrow> \<not> S x) \<longrightarrow> P x \<and> R x)
+       \<longrightarrow> (\<forall>x. S x)"
 by blast
 
 text\<open>Problem 31; has 10 Horn clauses; first negative clauses is useless\<close>
-lemma "~(\<exists>x. P x & (Q x | R x)) &
-      (\<exists>x. L x & P x) &
-      (\<forall>x. ~ R x --> M x)
-    --> (\<exists>x. L x & M x)"
+lemma "\<not>(\<exists>x. P x \<and> (Q x \<or> R x)) \<and>
+      (\<exists>x. L x \<and> P x) \<and>
+      (\<forall>x. \<not> R x \<longrightarrow> M x)
+    \<longrightarrow> (\<exists>x. L x \<and> M x)"
 by blast
 
 text\<open>Problem 32\<close>
-lemma "(\<forall>x. P x & (Q x | R x)-->S x) &
-      (\<forall>x. S x & R x --> L x) &
-      (\<forall>x. M x --> R x)
-    --> (\<forall>x. P x & M x --> L x)"
+lemma "(\<forall>x. P x \<and> (Q x \<or> R x)\<longrightarrow>S x) \<and>
+      (\<forall>x. S x \<and> R x \<longrightarrow> L x) \<and>
+      (\<forall>x. M x \<longrightarrow> R x)
+    \<longrightarrow> (\<forall>x. P x \<and> M x \<longrightarrow> L x)"
 by blast
 
 text\<open>Problem 33; has 55 Horn clauses\<close>
-lemma "(\<forall>x. P a & (P x --> P b)-->P c)  =
-      (\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"
+lemma "(\<forall>x. P a \<and> (P x \<longrightarrow> P b)\<longrightarrow>P c)  =
+      (\<forall>x. (\<not>P a \<or> P x \<or> P c) \<and> (\<not>P a \<or> \<not>P b \<or> P c))"
 by blast
 
 text\<open>Problem 34: Andrews's challenge has 924 Horn clauses\<close>
 lemma "((\<exists>x. \<forall>y. p x = p y)  = ((\<exists>x. q x) = (\<forall>y. p y)))     =
       ((\<exists>x. \<forall>y. q x = q y)  = ((\<exists>x. p x) = (\<forall>y. q y)))"
 by blast
 
 text\<open>Problem 35\<close>
-lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
+lemma "\<exists>x y. P x y \<longrightarrow>  (\<forall>u v. P u v)"
 by blast
 
 text\<open>Problem 36; has 15 Horn clauses\<close>
-lemma "(\<forall>x. \<exists>y. J x y) & (\<forall>x. \<exists>y. G x y) &
-       (\<forall>x y. J x y | G x y --> (\<forall>z. J y z | G y z --> H x z))
-       --> (\<forall>x. \<exists>y. H x y)"
+lemma "(\<forall>x. \<exists>y. J x y) \<and> (\<forall>x. \<exists>y. G x y) \<and>
+       (\<forall>x y. J x y \<or> G x y \<longrightarrow> (\<forall>z. J y z \<or> G y z \<longrightarrow> H x z))
+       \<longrightarrow> (\<forall>x. \<exists>y. H x y)"
 by blast
 
 text\<open>Problem 37; has 10 Horn clauses\<close>
 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
-           (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &
-      (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &
-      ((\<exists>x y. Q x y) --> (\<forall>x. R x x))
-    --> (\<forall>x. \<exists>y. R x y)"
+           (P x z \<longrightarrow> P y w) \<and> P y z \<and> (P y w \<longrightarrow> (\<exists>u. Q u w))) \<and>
+      (\<forall>x z. \<not>P x z \<longrightarrow> (\<exists>y. Q y z)) \<and>
+      ((\<exists>x y. Q x y) \<longrightarrow> (\<forall>x. R x x))
+    \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
 by blast \<comment> \<open>causes unification tracing messages\<close>
 
 
 text\<open>Problem 38\<close>  text\<open>Quite hard: 422 Horn clauses!!\<close>
-lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) -->
-           (\<exists>z. \<exists>w. p z & r x w & r w z))  =
-      (\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) &
-            (~p a | ~(\<exists>y. p y & r x y) |
-             (\<exists>z. \<exists>w. p z & r x w & r w z)))"
+lemma "(\<forall>x. p a \<and> (p x \<longrightarrow> (\<exists>y. p y \<and> r x y)) \<longrightarrow>
+           (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z))  =
+      (\<forall>x. (\<not>p a \<or> p x \<or> (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z)) \<and>
+            (\<not>p a \<or> \<not>(\<exists>y. p y \<and> r x y) \<or>
+             (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z)))"
 by blast
 
 text\<open>Problem 39\<close>
-lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))"
+lemma "\<not> (\<exists>x. \<forall>y. F y x = (\<not>F y y))"
 by blast
 
 text\<open>Problem 40.  AMENDED\<close>
 lemma "(\<exists>y. \<forall>x. F x y = F x x)
-      -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))"
+      \<longrightarrow>  \<not> (\<forall>x. \<exists>y. \<forall>z. F z y = (\<not>F z x))"
 by blast
 
 text\<open>Problem 41\<close>
-lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x))))
-      --> ~ (\<exists>z. \<forall>x. f x z)"
+lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z \<and> \<not> f x x))))
+      \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
 by blast
 
 text\<open>Problem 42\<close>
-lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
+lemma "\<not> (\<exists>y. \<forall>x. p x y = (\<not> (\<exists>z. p x z \<and> p z x)))"
 by blast
 
 text\<open>Problem 43  NOW PROVED AUTOMATICALLY!!\<close>
 lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool)))
-      --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
+      \<longrightarrow> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
 by blast
 
 text\<open>Problem 44: 13 Horn clauses; 7-step proof\<close>
-lemma "(\<forall>x. f x --> (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y)))  &
-       (\<exists>x. j x & (\<forall>y. g y --> h x y))
-       --> (\<exists>x. j x & ~f x)"
+lemma "(\<forall>x. f x \<longrightarrow> (\<exists>y. g y \<and> h x y \<and> (\<exists>y. g y \<and> \<not> h x y)))  \<and>
+       (\<exists>x. j x \<and> (\<forall>y. g y \<longrightarrow> h x y))
+       \<longrightarrow> (\<exists>x. j x \<and> \<not>f x)"
 by blast
 
 text\<open>Problem 45; has 27 Horn clauses; 54-step proof\<close>
-lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y)
-            --> (\<forall>y. g y & h x y --> k y)) &
-      ~ (\<exists>y. l y & k y) &
-      (\<exists>x. f x & (\<forall>y. h x y --> l y)
-                & (\<forall>y. g y & h x y --> j x y))
-      --> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))"
+lemma "(\<forall>x. f x \<and> (\<forall>y. g y \<and> h x y \<longrightarrow> j x y)
+            \<longrightarrow> (\<forall>y. g y \<and> h x y \<longrightarrow> k y)) \<and>
+      \<not> (\<exists>y. l y \<and> k y) \<and>
+      (\<exists>x. f x \<and> (\<forall>y. h x y \<longrightarrow> l y)
+                \<and> (\<forall>y. g y \<and> h x y \<longrightarrow> j x y))
+      \<longrightarrow> (\<exists>x. f x \<and> \<not> (\<exists>y. g y \<and> h x y))"
 by blast
 
 text\<open>Problem 46; has 26 Horn clauses; 21-step proof\<close>
-lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) &
-       ((\<exists>x. f x & ~g x) -->
-       (\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) &
-       (\<forall>x y. f x & f y & h x y --> ~j y x)
-       --> (\<forall>x. f x --> g x)"
+lemma "(\<forall>x. f x \<and> (\<forall>y. f y \<and> h y x \<longrightarrow> g y) \<longrightarrow> g x) \<and>
+       ((\<exists>x. f x \<and> \<not>g x) \<longrightarrow>
+       (\<exists>x. f x \<and> \<not>g x \<and> (\<forall>y. f y \<and> \<not>g y \<longrightarrow> j x y))) \<and>
+       (\<forall>x y. f x \<and> f y \<and> h x y \<longrightarrow> \<not>j y x)
+       \<longrightarrow> (\<forall>x. f x \<longrightarrow> g x)"
 by blast
 
 text\<open>Problem 47.  Schubert's Steamroller.
       26 clauses; 63 Horn clauses.
       87094 inferences so far.  Searching to depth 36\<close>
-lemma "(\<forall>x. wolf x \<longrightarrow> animal x) & (\<exists>x. wolf x) &
-       (\<forall>x. fox x \<longrightarrow> animal x) & (\<exists>x. fox x) &
-       (\<forall>x. bird x \<longrightarrow> animal x) & (\<exists>x. bird x) &
-       (\<forall>x. caterpillar x \<longrightarrow> animal x) & (\<exists>x. caterpillar x) &
-       (\<forall>x. snail x \<longrightarrow> animal x) & (\<exists>x. snail x) &
-       (\<forall>x. grain x \<longrightarrow> plant x) & (\<exists>x. grain x) &
+lemma "(\<forall>x. wolf x \<longrightarrow> animal x) \<and> (\<exists>x. wolf x) \<and>
+       (\<forall>x. fox x \<longrightarrow> animal x) \<and> (\<exists>x. fox x) \<and>
+       (\<forall>x. bird x \<longrightarrow> animal x) \<and> (\<exists>x. bird x) \<and>
+       (\<forall>x. caterpillar x \<longrightarrow> animal x) \<and> (\<exists>x. caterpillar x) \<and>
+       (\<forall>x. snail x \<longrightarrow> animal x) \<and> (\<exists>x. snail x) \<and>
+       (\<forall>x. grain x \<longrightarrow> plant x) \<and> (\<exists>x. grain x) \<and>
        (\<forall>x. animal x \<longrightarrow>
              ((\<forall>y. plant y \<longrightarrow> eats x y)  \<or> 
-              (\<forall>y. animal y & smaller_than y x &
-                    (\<exists>z. plant z & eats y z) \<longrightarrow> eats x y))) &
-       (\<forall>x y. bird y & (snail x \<or> caterpillar x) \<longrightarrow> smaller_than x y) &
-       (\<forall>x y. bird x & fox y \<longrightarrow> smaller_than x y) &
-       (\<forall>x y. fox x & wolf y \<longrightarrow> smaller_than x y) &
-       (\<forall>x y. wolf x & (fox y \<or> grain y) \<longrightarrow> ~eats x y) &
-       (\<forall>x y. bird x & caterpillar y \<longrightarrow> eats x y) &
-       (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
-       (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
-       \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
+              (\<forall>y. animal y \<and> smaller_than y x \<and>
+                    (\<exists>z. plant z \<and> eats y z) \<longrightarrow> eats x y))) \<and>
+       (\<forall>x y. bird y \<and> (snail x \<or> caterpillar x) \<longrightarrow> smaller_than x y) \<and>
+       (\<forall>x y. bird x \<and> fox y \<longrightarrow> smaller_than x y) \<and>
+       (\<forall>x y. fox x \<and> wolf y \<longrightarrow> smaller_than x y) \<and>
+       (\<forall>x y. wolf x \<and> (fox y \<or> grain y) \<longrightarrow> \<not>eats x y) \<and>
+       (\<forall>x y. bird x \<and> caterpillar y \<longrightarrow> eats x y) \<and>
+       (\<forall>x y. bird x \<and> snail y \<longrightarrow> \<not>eats x y) \<and>
+       (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y \<and> eats x y))
+       \<longrightarrow> (\<exists>x y. animal x \<and> animal y \<and> (\<exists>z. grain z \<and> eats y z \<and> eats x y))"
 by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
     \<comment> \<open>Nearly twice as fast as \<open>meson\<close>,
         which performs iterative deepening rather than best-first search\<close>
 
 text\<open>The Los problem. Circulated by John Harrison\<close>
-lemma "(\<forall>x y z. P x y & P y z --> P x z) &
-       (\<forall>x y z. Q x y & Q y z --> Q x z) &
-       (\<forall>x y. P x y --> P y x) &
-       (\<forall>x y. P x y | Q x y)
-       --> (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
+lemma "(\<forall>x y z. P x y \<and> P y z \<longrightarrow> P x z) \<and>
+       (\<forall>x y z. Q x y \<and> Q y z \<longrightarrow> Q x z) \<and>
+       (\<forall>x y. P x y \<longrightarrow> P y x) \<and>
+       (\<forall>x y. P x y \<or> Q x y)
+       \<longrightarrow> (\<forall>x y. P x y) \<or> (\<forall>x y. Q x y)"
 by meson
 
 text\<open>A similar example, suggested by Johannes Schumann and
  credited to Pelletier\<close>
-lemma "(\<forall>x y z. P x y --> P y z --> P x z) -->
-       (\<forall>x y z. Q x y --> Q y z --> Q x z) -->
-       (\<forall>x y. Q x y --> Q y x) -->  (\<forall>x y. P x y | Q x y) -->
-       (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
+lemma "(\<forall>x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow>
+       (\<forall>x y z. Q x y \<longrightarrow> Q y z \<longrightarrow> Q x z) \<longrightarrow>
+       (\<forall>x y. Q x y \<longrightarrow> Q y x) \<longrightarrow>  (\<forall>x y. P x y \<or> Q x y) \<longrightarrow>
+       (\<forall>x y. P x y) \<or> (\<forall>x y. Q x y)"
 by meson
 
 text\<open>Problem 50.  What has this to do with equality?\<close>
-lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
+lemma "(\<forall>x. P a x \<or> (\<forall>y. P x y)) \<longrightarrow> (\<exists>x. \<forall>y. P x y)"
 by blast
 
 text\<open>Problem 54: NOT PROVED\<close>
-lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) -->
-      ~ (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u --> (\<exists>y. F y u & ~ (\<exists>z. F z u & F z y))))"
+lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) \<longrightarrow>
+      \<not> (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u \<longrightarrow> (\<exists>y. F y u \<and> \<not> (\<exists>z. F z u \<and> F z y))))"
 oops 
 
 
 text\<open>Problem 55\<close>
 
 text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   \<open>meson\<close> cannot report who killed Agatha.\<close>
-lemma "lives agatha & lives butler & lives charles &
-       (killed agatha agatha | killed butler agatha | killed charles agatha) &
-       (\<forall>x y. killed x y --> hates x y & ~richer x y) &
-       (\<forall>x. hates agatha x --> ~hates charles x) &
-       (hates agatha agatha & hates agatha charles) &
-       (\<forall>x. lives x & ~richer x agatha --> hates butler x) &
-       (\<forall>x. hates agatha x --> hates butler x) &
-       (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
+lemma "lives agatha \<and> lives butler \<and> lives charles \<and>
+       (killed agatha agatha \<or> killed butler agatha \<or> killed charles agatha) \<and>
+       (\<forall>x y. killed x y \<longrightarrow> hates x y \<and> \<not>richer x y) \<and>
+       (\<forall>x. hates agatha x \<longrightarrow> \<not>hates charles x) \<and>
+       (hates agatha agatha \<and> hates agatha charles) \<and>
+       (\<forall>x. lives x \<and> \<not>richer x agatha \<longrightarrow> hates butler x) \<and>
+       (\<forall>x. hates agatha x \<longrightarrow> hates butler x) \<and>
+       (\<forall>x. \<not>hates x agatha \<or> \<not>hates x butler \<or> \<not>hates x charles) \<longrightarrow>
        (\<exists>x. killed x agatha)"
 by meson
 
 text\<open>Problem 57\<close>
-lemma "P (f a b) (f b c) & P (f b c) (f a c) &
-      (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
+lemma "P (f a b) (f b c) \<and> P (f b c) (f a c) \<and>
+      (\<forall>x y z. P x y \<and> P y z \<longrightarrow> P x z)    \<longrightarrow>   P (f a b) (f a c)"
 by blast
 
 text\<open>Problem 58: Challenge found on info-hol\<close>
-lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
+lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x \<and> Q y \<longrightarrow> (P v \<or> R w) \<and> (R z \<longrightarrow> Q v)"
 by blast
 
 text\<open>Problem 59\<close>
-lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))"
+lemma "(\<forall>x. P x = (\<not>P(f x))) \<longrightarrow> (\<exists>x. P x \<and> \<not>P(f x))"
 by blast
 
 text\<open>Problem 60\<close>
-lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
+lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y \<longrightarrow> P z (f x)) \<and> P x y)"
 by blast
 
 text\<open>Problem 62 as corrected in JAR 18 (1997), page 135\<close>
-lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =
-       (\<forall>x. (~ p a | p x | p(f(f x))) &
-            (~ p a | ~ p(f x) | p(f(f x))))"
+lemma "(\<forall>x. p a \<and> (p x \<longrightarrow> p(f x)) \<longrightarrow> p(f(f x)))  =
+       (\<forall>x. (\<not> p a \<or> p x \<or> p(f(f x))) \<and>
+            (\<not> p a \<or> \<not> p(f x) \<or> p(f(f x))))"
 by blast
 
 text\<open>Charles Morgan's problems\<close>
 context
   fixes T i n
   assumes a: "\<forall>x y. T(i x(i y x))"
     and b: "\<forall>x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
     and c: "\<forall>x y. T(i (i (n x) (n y)) (i y x))"
     and c': "\<forall>x y. T(i (i y x) (i (n x) (n y)))"
-    and d: "\<forall>x y. T(i x y) & T x --> T y"
+    and d: "\<forall>x y. T(i x y) \<and> T x \<longrightarrow> T y"
 begin
 
 lemma "\<forall>x. T(i x x)"
   using a b d by blast