--- a/src/FOL/ex/Classical.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Classical.thy Mon Oct 19 23:00:07 2015 +0200
@@ -3,490 +3,526 @@
Copyright 1994 University of Cambridge
*)
-section\<open>Classical Predicate Calculus Problems\<close>
-
-theory Classical imports FOL begin
-
-lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
-by blast
+section \<open>Classical Predicate Calculus Problems\<close>
-text\<open>If and only if\<close>
+theory Classical
+imports FOL
+begin
-lemma "(P<->Q) <-> (Q<->P)"
-by blast
-
-lemma "~ (P <-> ~P)"
-by blast
+lemma "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
+ by blast
-text\<open>Sample problems from
- F. J. Pelletier,
- Seventy-Five Problems for Testing Automatic Theorem Provers,
- J. Automated Reasoning 2 (1986), 191-216.
- Errata, JAR 4 (1988), 236-236.
+subsubsection \<open>If and only if\<close>
+
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+ by blast
+
+lemma "\<not> (P \<longleftrightarrow> \<not> P)"
+ by blast
+
+
+subsection \<open>Pelletier's examples\<close>
-The hardest problems -- judging by experience with several theorem provers,
-including matrix ones -- are 34 and 43.
+text \<open>
+ Sample problems from
+
+ \<^item> F. J. Pelletier,
+ Seventy-Five Problems for Testing Automatic Theorem Provers,
+ J. Automated Reasoning 2 (1986), 191-216.
+ Errata, JAR 4 (1988), 236-236.
+
+ The hardest problems -- judging by experience with several theorem
+ provers, including matrix ones -- are 34 and 43.
\<close>
-subsection\<open>Pelletier's examples\<close>
-
text\<open>1\<close>
-lemma "(P-->Q) <-> (~Q --> ~P)"
-by blast
+lemma "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
+ by blast
text\<open>2\<close>
-lemma "~ ~ P <-> P"
-by blast
+lemma "\<not> \<not> P \<longleftrightarrow> P"
+ by blast
text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
-by blast
+lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+ by blast
text\<open>4\<close>
-lemma "(~P-->Q) <-> (~Q --> P)"
-by blast
+lemma "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
+ by blast
text\<open>5\<close>
-lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
-by blast
+lemma "((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
+ by blast
text\<open>6\<close>
-lemma "P | ~ P"
-by blast
+lemma "P \<or> \<not> P"
+ by blast
text\<open>7\<close>
-lemma "P | ~ ~ ~ P"
-by blast
+lemma "P \<or> \<not> \<not> \<not> P"
+ by blast
-text\<open>8. Peirce's law\<close>
-lemma "((P-->Q) --> P) --> P"
-by blast
+text\<open>8. Peirce's law\<close>
+lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+ by blast
text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by blast
+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)"
-by blast
+lemma "(Q \<longrightarrow> R) \<and> (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longleftrightarrow> Q)"
+ by blast
-text\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
-lemma "P<->P"
-by blast
+text\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
+lemma "P \<longleftrightarrow> P"
+ by blast
-text\<open>12. "Dijkstra's law"\<close>
-lemma "((P <-> Q) <-> R) <-> (P <-> (Q <-> R))"
-by blast
+text\<open>12. "Dijkstra's law"\<close>
+lemma "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+ by blast
-text\<open>13. Distributive law\<close>
-lemma "P | (Q & R) <-> (P | Q) & (P | R)"
-by blast
+text\<open>13. Distributive law\<close>
+lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+ by blast
text\<open>14\<close>
-lemma "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"
-by blast
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
+ by blast
text\<open>15\<close>
-lemma "(P --> Q) <-> (~P | Q)"
-by blast
+lemma "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+ by blast
text\<open>16\<close>
-lemma "(P-->Q) | (Q-->P)"
-by blast
+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))"
-by blast
+lemma "((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
+ by blast
+
-subsection\<open>Classical Logic: examples with quantifiers\<close>
+subsection \<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 "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+ by blast
-lemma "(\<exists>x. P-->Q(x)) <-> (P --> (\<exists>x. Q(x)))"
-by blast
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+ by blast
-lemma "(\<exists>x. P(x)-->Q) <-> (\<forall>x. P(x)) --> Q"
-by blast
+lemma "(\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+ by blast
-lemma "(\<forall>x. P(x)) | Q <-> (\<forall>x. P(x) | Q)"
-by blast
+lemma "(\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+ by blast
text\<open>Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
JAR 10 (265-281), 1993. Proof is trivial!\<close>
-lemma "~((\<exists>x.~P(x)) & ((\<exists>x. P(x)) | (\<exists>x. P(x) & Q(x))) & ~ (\<exists>x. P(x)))"
-by blast
+lemma "\<not> ((\<exists>x. \<not> P(x)) \<and> ((\<exists>x. P(x)) \<or> (\<exists>x. P(x) \<and> Q(x))) \<and> \<not> (\<exists>x. P(x)))"
+ by blast
-subsection\<open>Problems requiring quantifier duplication\<close>
-text\<open>Theorem B of Peter Andrews, Theorem Proving via General Matings,
+subsection \<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)))"
-by blast
+lemma "(\<exists>x. \<forall>y. P(x) \<longleftrightarrow> P(y)) \<longrightarrow> ((\<exists>x. P(x)) \<longleftrightarrow> (\<forall>y. P(y)))"
+ by blast
text\<open>Needs multiple instantiation of ALL.\<close>
-lemma "(\<forall>x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"
-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 the quantifier\<close>
-lemma "\<exists>x. P(x) --> P(a) & P(b)"
-by blast
+lemma "\<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
+ by blast
-lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
-by blast
+lemma "\<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
+ by blast
-lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
-by blast
+lemma "\<exists>x. (\<exists>y. P(y)) \<longrightarrow> P(x)"
+ by blast
-text\<open>V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED\<close>
-lemma "\<exists>x x'. \<forall>y. \<exists>z z'.
- (~P(y,y) | P(x,x) | ~S(z,x)) &
- (S(x,y) | ~S(y,z) | Q(z',z')) &
- (Q(x',y) | ~Q(y,z') | S(x',x'))"
-oops
+text\<open>V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.\<close>
+lemma
+ "\<exists>x x'. \<forall>y. \<exists>z z'.
+ (\<not> P(y,y) \<or> P(x,x) \<or> \<not> S(z,x)) \<and>
+ (S(x,y) \<or> \<not> S(y,z) \<or> Q(z',z')) \<and>
+ (Q(x',y) \<or> \<not> Q(y,z') \<or> S(x',x'))"
+ oops
-
-subsection\<open>Hard examples with quantifiers\<close>
+subsection \<open>Hard examples with quantifiers\<close>
text\<open>18\<close>
-lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
-by blast
+lemma "\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x)"
+ by blast
text\<open>19\<close>
-lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
-by blast
+lemma "\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x))"
+ by blast
text\<open>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))"
-by blast
+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>21\<close>
-lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P<->Q(x))"
-by blast
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
+ by blast
text\<open>22\<close>
-lemma "(\<forall>x. P <-> Q(x)) --> (P <-> (\<forall>x. Q(x)))"
-by blast
+lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+ by blast
text\<open>23\<close>
-lemma "(\<forall>x. P | Q(x)) <-> (P | (\<forall>x. Q(x)))"
-by blast
+lemma "(\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
+ by blast
text\<open>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))"
-by blast
+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>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))"
-by blast
+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>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)))"
-by blast
+lemma
+ "((\<exists>x. p(x)) \<longleftrightarrow> (\<exists>x. q(x))) \<and>
+ (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
+ \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
+ by blast
text\<open>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))"
-by blast
+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>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))"
-by blast
+text\<open>28. AMENDED\<close>
+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>29. Essentially the same as Principia Mathematica *11.71\<close>
-lemma "(\<exists>x. P(x)) & (\<exists>y. Q(y))
- --> ((\<forall>x. P(x)-->R(x)) & (\<forall>y. Q(y)-->S(y)) <->
- (\<forall>x y. P(x) & Q(y) --> R(x) & S(y)))"
-by blast
+text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
+lemma
+ "(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+ \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
+ (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
+ by blast
text\<open>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))"
-by blast
+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>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))"
-by blast
+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>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))"
-by blast
+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>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)))"
-by blast
+lemma
+ "(\<forall>x. P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c)) \<longleftrightarrow>
+ (\<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>34 AMENDED (TWICE!!). Andrews's challenge\<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>34. AMENDED (TWICE!!). Andrews's challenge.\<close>
+lemma
+ "((\<exists>x. \<forall>y. p(x) \<longleftrightarrow> p(y)) \<longleftrightarrow> ((\<exists>x. q(x)) \<longleftrightarrow> (\<forall>y. p(y)))) \<longleftrightarrow>
+ ((\<exists>x. \<forall>y. q(x) \<longleftrightarrow> q(y)) \<longleftrightarrow> ((\<exists>x. p(x)) \<longleftrightarrow> (\<forall>y. q(y))))"
+ by blast
text\<open>35\<close>
-lemma "\<exists>x y. P(x,y) --> (\<forall>u v. P(u,v))"
-by blast
+lemma "\<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
+ by blast
text\<open>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))"
-by blast
+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>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))"
-by blast
+lemma
+ "(\<forall>z. \<exists>w. \<forall>x. \<exists>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>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))))"
-by blast
+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))) \<longleftrightarrow>
+ (\<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>39\<close>
-lemma "~ (\<exists>x. \<forall>y. F(y,x) <-> ~F(y,y))"
-by blast
+lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+ by blast
-text\<open>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))"
-by blast
+text\<open>40. AMENDED\<close>
+lemma
+ "(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+ \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
+ by blast
text\<open>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))"
-by blast
+lemma
+ "(\<forall>z. \<exists>y. \<forall>x. f(x,y) \<longleftrightarrow> f(x,z) \<and> \<not> f(x,x))
+ \<longrightarrow> \<not> (\<exists>z. \<forall>x. f(x,z))"
+ by blast
text\<open>42\<close>
-lemma "~ (\<exists>y. \<forall>x. p(x,y) <-> ~ (\<exists>z. p(x,z) & p(z,x)))"
-by blast
+lemma "\<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
+ by blast
text\<open>43\<close>
-lemma "(\<forall>x. \<forall>y. q(x,y) <-> (\<forall>z. p(z,x) <-> p(z,y)))
- --> (\<forall>x. \<forall>y. q(x,y) <-> q(y,x))"
-by blast
+lemma
+ "(\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
+ \<longrightarrow> (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> q(y,x))"
+ by blast
-(*Other proofs: Can use auto, which cheats by using rewriting!
+text \<open>
+ Other proofs: Can use @{text auto}, which cheats by using rewriting!
Deepen_tac alone requires 253 secs. Or
- by (mini_tac @{context} 1 THEN Deepen_tac 5 1) *)
+ by (mini_tac 1 THEN Deepen_tac 5 1)
+\<close>
text\<open>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))"
-by blast
+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>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)))"
-by blast
+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>46\<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))"
-by blast
+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
-subsection\<open>Problems (mainly) involving equality or functions\<close>
+subsection \<open>Problems (mainly) involving equality or functions\<close>
text\<open>48\<close>
-lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by blast
+lemma "(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+ by blast
-text\<open>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))"
-apply safe
-apply (rule_tac x = a in allE, assumption)
-apply (rule_tac x = b in allE, assumption, fast)
- --\<open>blast's treatment of equality can't do it\<close>
-done
+text\<open>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 \<or> z = y) \<and> P(a) \<and> P(b) \<and> a \<noteq> b \<longrightarrow> (\<forall>u::'a. P(u))"
+ apply safe
+ apply (rule_tac x = a in allE, assumption)
+ apply (rule_tac x = b in allE, assumption)
+ apply fast -- \<open>blast's treatment of equality can't do it\<close>
+ done
-text\<open>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))"
-by blast
+text\<open>50. (What has this to do with equality?)\<close>
+lemma "(\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
+ by blast
text\<open>51\<close>
-lemma "(\<exists>z w. \<forall>x y. P(x,y) <-> (x=z & y=w)) -->
- (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) <-> y=w) <-> x=z)"
-by blast
+lemma
+ "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y=w) \<longleftrightarrow> x = z)"
+ by blast
text\<open>52\<close>
text\<open>Almost the same as 51.\<close>
-lemma "(\<exists>z w. \<forall>x y. P(x,y) <-> (x=z & y=w)) -->
- (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) <-> x=z) <-> y=w)"
-by blast
+lemma
+ "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
+ by blast
text\<open>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 --\<open>MUCH faster than blast\<close>
+ by fast -- \<open>MUCH faster than blast\<close>
text\<open>56\<close>
-lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) <-> (\<forall>x. P(x) --> P(f(x)))"
-by blast
+lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+ by blast
text\<open>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))"
-by blast
+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>58 NOT PROVED AUTOMATICALLY\<close>
-lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
-by (slow elim: subst_context)
+lemma "(\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
+ by (slow elim: subst_context)
text\<open>59\<close>
-lemma "(\<forall>x. P(x) <-> ~P(f(x))) --> (\<exists>x. P(x) & ~P(f(x)))"
-by blast
+lemma "(\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+ by blast
text\<open>60\<close>
-lemma "\<forall>x. P(x,f(x)) <-> (\<exists>y. (\<forall>z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by blast
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+ by blast
text\<open>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)))))"
-by blast
+lemma
+ "(\<forall>x. p(a) \<and> (p(x) \<longrightarrow> p(f(x))) \<longrightarrow> p(f(f(x)))) \<longleftrightarrow>
+ (\<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
+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))"
-by fast
+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.
+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))"
-by fast
+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>Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
- author U. Egly\<close>
-lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->
- (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))
- &
- (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->
- (\<forall>y z.
- (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &
- (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))
- &
- (\<forall>w. C(w) &
- (\<forall>y z.
- (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &
- (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))) -->
- (\<exists>v. C(v) &
- (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &
- ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))
- -->
- ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (blast 12)
- --\<open>Needed because the search for depths below 12 is very slow\<close>
+text \<open>Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
+ author U. Egly.\<close>
+lemma
+ "((\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z)))) \<longrightarrow>
+ (\<exists>w. C(w) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(w,y,z)))))
+ \<and>
+ (\<forall>w. C(w) \<and> (\<forall>u. C(u) \<longrightarrow> (\<forall>v. D(w,u,v))) \<longrightarrow>
+ (\<forall>y z.
+ (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+ (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))))
+ \<and>
+ (\<forall>w. C(w) \<and>
+ (\<forall>y z.
+ (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+ (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))) \<longrightarrow>
+ (\<exists>v. C(v) \<and>
+ (\<forall>y. ((C(y) \<and> Q(w,y,y)) \<and> OO(w,g) \<longrightarrow> \<not> P(v,y)) \<and>
+ ((C(y) \<and> Q(w,y,y)) \<and> OO(w,b) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
+ \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
+ by (blast 12)
+ -- \<open>Needed because the search for depths below 12 is very slow.\<close>
-text\<open>Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105\<close>
-lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->
- (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))
- &
- (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->
- (\<forall>y z.
- (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &
- (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))
- &
- ((\<exists>w. C(w) & (\<forall>y. (C(y) & P(y,y) --> Q(w,y,y) & OO(w,g)) &
- (C(y) & ~P(y,y) --> Q(w,y,y) & OO(w,b))))
- -->
- (\<exists>v. C(v) & (\<forall>y. (C(y) & P(y,y) --> P(v,y) & OO(v,g)) &
- (C(y) & ~P(y,y) --> P(v,y) & OO(v,b)))))
- -->
- ((\<exists>v. C(v) & (\<forall>y. (C(y) & P(y,y) --> P(v,y) & OO(v,g)) &
- (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))
- -->
- (\<exists>u. C(u) & (\<forall>y. (C(y) & P(y,y) --> ~P(u,y)) &
- (C(y) & ~P(y,y) --> P(u,y) & OO(u,b)))))
- -->
- ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by blast
+text \<open>
+ Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
+ p. 105.
+\<close>
+lemma
+ "((\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z)))) \<longrightarrow>
+ (\<exists>w. C(w) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(w,y,z)))))
+ \<and>
+ (\<forall>w. C(w) \<and> (\<forall>u. C(u) \<longrightarrow> (\<forall>v. D(w,u,v))) \<longrightarrow>
+ (\<forall>y z.
+ (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+ (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))))
+ \<and>
+ ((\<exists>w. C(w) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> Q(w,y,y) \<and> OO(w,g)) \<and>
+ (C(y) \<and> \<not> P(y,y) \<longrightarrow> Q(w,y,y) \<and> OO(w,b))))
+ \<longrightarrow>
+ (\<exists>v. C(v) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,g)) \<and>
+ (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
+ \<longrightarrow>
+ ((\<exists>v. C(v) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,g)) \<and>
+ (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,b))))
+ \<longrightarrow>
+ (\<exists>u. C(u) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> \<not> P(u,y)) \<and>
+ (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(u,y) \<and> OO(u,b)))))
+ \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
+ by blast
-text\<open>Challenge found on info-hol\<close>
-lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"
-by blast
+text \<open>Challenge found on info-hol.\<close>
+lemma "\<forall>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>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
+text \<open>
+ Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption
+ can be deleted.\<close>
+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
(*Runtimes for old versions of this file:
-Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]
-Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]
-Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip]
-Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]
+Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]
+Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]
+Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip]
+Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]
Further runtimes on a Sun-4
-Tue Mar 4 1997: loaded in 93s (version 94-7)
+Tue Mar 4 1997: loaded in 93s (version 94-7)
Tue Mar 4 1997: loaded in 89s
Thu Apr 3 1997: loaded in 44s--using mostly Blast_tac
Thu Apr 3 1997: loaded in 96s--addition of two Halting Probs
@@ -497,4 +533,3 @@
*)
end
-
--- a/src/FOL/ex/Foundation.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Foundation.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,7 +9,7 @@
imports IFOL
begin
-lemma "A&B --> (C-->A&C)"
+lemma "A \<and> B \<longrightarrow> (C \<longrightarrow> A \<and> C)"
apply (rule impI)
apply (rule impI)
apply (rule conjI)
@@ -20,8 +20,8 @@
text \<open>A form of conj-elimination\<close>
lemma
- assumes "A & B"
- and "A ==> B ==> C"
+ assumes "A \<and> B"
+ and "A \<Longrightarrow> B \<Longrightarrow> C"
shows C
apply (rule assms)
apply (rule conjunct1)
@@ -31,26 +31,26 @@
done
lemma
- assumes "!!A. ~ ~A ==> A"
- shows "B | ~B"
+ assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A"
+ shows "B \<or> \<not> B"
apply (rule assms)
apply (rule notI)
-apply (rule_tac P = "~B" in notE)
+apply (rule_tac P = "\<not> B" in notE)
apply (rule_tac [2] notI)
-apply (rule_tac [2] P = "B | ~B" in notE)
+apply (rule_tac [2] P = "B \<or> \<not> B" in notE)
prefer 2 apply assumption
apply (rule_tac [2] disjI1)
prefer 2 apply assumption
apply (rule notI)
-apply (rule_tac P = "B | ~B" in notE)
+apply (rule_tac P = "B \<or> \<not> B" in notE)
apply assumption
apply (rule disjI2)
apply assumption
done
lemma
- assumes "!!A. ~ ~A ==> A"
- shows "B | ~B"
+ assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A"
+ shows "B \<or> \<not> B"
apply (rule assms)
apply (rule notI)
apply (rule notE)
@@ -64,14 +64,14 @@
lemma
- assumes "A | ~A"
- and "~ ~A"
+ assumes "A \<or> \<not> A"
+ and "\<not> \<not> A"
shows A
apply (rule disjE)
apply (rule assms)
apply assumption
apply (rule FalseE)
-apply (rule_tac P = "~A" in notE)
+apply (rule_tac P = "\<not> A" in notE)
apply (rule assms)
apply assumption
done
@@ -80,27 +80,27 @@
subsection "Examples with quantifiers"
lemma
- assumes "ALL z. G(z)"
- shows "ALL z. G(z)|H(z)"
+ assumes "\<forall>z. G(z)"
+ shows "\<forall>z. G(z) \<or> H(z)"
apply (rule allI)
apply (rule disjI1)
apply (rule assms [THEN spec])
done
-lemma "ALL x. EX y. x=y"
+lemma "\<forall>x. \<exists>y. x = y"
apply (rule allI)
apply (rule exI)
apply (rule refl)
done
-lemma "EX y. ALL x. x=y"
+lemma "\<exists>y. \<forall>x. x = y"
apply (rule exI)
apply (rule allI)
apply (rule refl)?
oops
text \<open>Parallel lifting example.\<close>
-lemma "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
+lemma "\<exists>u. \<forall>x. \<exists>v. \<forall>y. \<exists>w. P(u,x,v,y,w)"
apply (rule exI allI)
apply (rule exI allI)
apply (rule exI allI)
@@ -109,8 +109,8 @@
oops
lemma
- assumes "(EX z. F(z)) & B"
- shows "EX z. F(z) & B"
+ assumes "(\<exists>z. F(z)) \<and> B"
+ shows "\<exists>z. F(z) \<and> B"
apply (rule conjE)
apply (rule assms)
apply (rule exE)
@@ -122,7 +122,7 @@
done
text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
-lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
apply (rule impI)
apply (rule allI)
apply (rule exE, assumption)
--- a/src/FOL/ex/If.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/If.thy Mon Oct 19 23:00:07 2015 +0200
@@ -5,57 +5,56 @@
section \<open>First-Order Logic: the 'if' example\<close>
-theory If imports FOL begin
-
-definition "if" :: "[o,o,o]=>o" where
- "if(P,Q,R) == P&Q | ~P&R"
+theory If
+imports FOL
+begin
-lemma ifI:
- "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
-apply (simp add: if_def, blast)
-done
+definition "if" :: "[o,o,o]=>o"
+ where "if(P,Q,R) \<equiv> P \<and> Q \<or> \<not> P \<and> R"
+
+lemma ifI: "\<lbrakk>P \<Longrightarrow> Q; \<not> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> if(P,Q,R)"
+ unfolding if_def by blast
-lemma ifE:
- "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
-apply (simp add: if_def, blast)
-done
+lemma ifE: "\<lbrakk>if(P,Q,R); \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> S; \<lbrakk>\<not> P; R\<rbrakk> \<Longrightarrow> S\<rbrakk> \<Longrightarrow> S"
+ unfolding if_def by blast
-lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-apply (rule iffI)
-apply (erule ifE)
-apply (erule ifE)
-apply (rule ifI)
-apply (rule ifI)
-oops
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))"
+ apply (rule iffI)
+ apply (erule ifE)
+ apply (erule ifE)
+ apply (rule ifI)
+ apply (rule ifI)
+ oops
text\<open>Trying again from the beginning in order to use @{text blast}\<close>
declare ifI [intro!]
declare ifE [elim!]
-lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-by blast
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))"
+ by blast
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-by blast
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))"
+ by blast
text\<open>Trying again from the beginning in order to prove from the definitions\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-by (simp add: if_def, blast)
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))"
+ unfolding if_def by blast
-text\<open>An invalid formula. High-level rules permit a simpler diagnosis\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
-apply auto
- -- \<open>The next step will fail unless subgoals remain\<close>
-apply (tactic all_tac)
-oops
+text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close>
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
+ apply auto
+ -- \<open>The next step will fail unless subgoals remain\<close>
+ apply (tactic all_tac)
+ oops
-text\<open>Trying again from the beginning in order to prove from the definitions\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
-apply (simp add: if_def, auto)
- -- \<open>The next step will fail unless subgoals remain\<close>
-apply (tactic all_tac)
-oops
+text \<open>Trying again from the beginning in order to prove from the definitions.\<close>
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
+ unfolding if_def
+ apply auto
+ -- \<open>The next step will fail unless subgoals remain\<close>
+ apply (tactic all_tac)
+ oops
end
--- a/src/FOL/ex/Intro.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Intro.thy Mon Oct 19 23:00:07 2015 +0200
@@ -13,7 +13,7 @@
subsubsection \<open>Some simple backward proofs\<close>
-lemma mythm: "P|P --> P"
+lemma mythm: "P \<or> P \<longrightarrow> P"
apply (rule impI)
apply (rule disjE)
prefer 3 apply (assumption)
@@ -21,7 +21,7 @@
apply assumption
done
-lemma "(P & Q) | R --> (P | R)"
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)"
apply (rule impI)
apply (erule disjE)
apply (drule conjunct1)
@@ -30,8 +30,8 @@
apply assumption+
done
-(*Correct version, delaying use of "spec" until last*)
-lemma "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
+text \<open>Correct version, delaying use of @{text spec} until last.\<close>
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))"
apply (rule impI)
apply (rule allI)
apply (rule allI)
@@ -43,14 +43,12 @@
subsubsection \<open>Demonstration of @{text "fast"}\<close>
-lemma "(EX y. ALL x. J(y,x) <-> ~J(x,x))
- --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
+lemma "(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))"
apply fast
done
-lemma "ALL x. P(x,f(x)) <->
- (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
apply fast
done
@@ -58,8 +56,8 @@
subsubsection \<open>Derivation of conjunction elimination rule\<close>
lemma
- assumes major: "P&Q"
- and minor: "[| P; Q |] ==> R"
+ assumes major: "P \<and> Q"
+ and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
shows R
apply (rule minor)
apply (rule major [THEN conjunct1])
@@ -72,8 +70,8 @@
text \<open>Derivation of negation introduction\<close>
lemma
- assumes "P ==> False"
- shows "~ P"
+ assumes "P \<Longrightarrow> False"
+ shows "\<not> P"
apply (unfold not_def)
apply (rule impI)
apply (rule assms)
@@ -81,7 +79,7 @@
done
lemma
- assumes major: "~P"
+ assumes major: "\<not> P"
and minor: P
shows R
apply (rule FalseE)
@@ -92,7 +90,7 @@
text \<open>Alternative proof of the result above\<close>
lemma
- assumes major: "~P"
+ assumes major: "\<not> P"
and minor: P
shows R
apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
--- a/src/FOL/ex/Intuitionistic.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Intuitionistic.thy Mon Oct 19 23:00:07 2015 +0200
@@ -36,390 +36,417 @@
intuitionistically provable. Finally, if $P$ is a negation then $\neg\neg P$
is intuitionstically equivalent to $P$. [Andy Pitts]\<close>
-lemma "~~(P&Q) <-> ~~P & ~~Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (P \<and> Q) \<longleftrightarrow> \<not> \<not> P \<and> \<not> \<not> Q"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longrightarrow> (\<not> P \<longrightarrow> \<not> Q) \<longrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>Double-negation does NOT distribute over disjunction\<close>
+text \<open>Double-negation does NOT distribute over disjunction.\<close>
-lemma "~~(P-->Q) <-> (~~P --> ~~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> \<not> P \<longrightarrow> \<not> \<not> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "~~~P <-> ~P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> \<not> P \<longleftrightarrow> \<not> P"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "~~((P --> Q | R) --> (P-->Q) | (P-->R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> ((P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "(P<->Q) <-> (Q<->P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "((P --> (Q | (Q-->R))) --> R) --> R"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((P \<longrightarrow> (Q \<or> (Q \<longrightarrow> R))) \<longrightarrow> R) \<longrightarrow> R"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
- --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
- --> (((F-->A)-->B) --> I) --> E"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+ "(((G \<longrightarrow> A) \<longrightarrow> J) \<longrightarrow> D \<longrightarrow> E) \<longrightarrow> (((H \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> C \<longrightarrow> J)
+ \<longrightarrow> (A \<longrightarrow> H) \<longrightarrow> F \<longrightarrow> G \<longrightarrow> (((C \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> D) \<longrightarrow> (A \<longrightarrow> C)
+ \<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>Lemmas for the propositional double-negation translation\<close>
+subsection \<open>Lemmas for the propositional double-negation translation\<close>
-lemma "P --> ~~P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "P \<longrightarrow> \<not> \<not> P"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "~~(~~P --> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (\<not> \<not> P \<longrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-lemma "~~P & ~~(P --> Q) --> ~~Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> P \<and> \<not> \<not> (P \<longrightarrow> Q) \<longrightarrow> \<not> \<not> Q"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>The following are classically but not constructively valid.
- The attempt to prove them terminates quickly!\<close>
-lemma "((P-->Q) --> P) --> P"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
+text \<open>The following are classically but not constructively valid.
+ The attempt to prove them terminates quickly!\<close>
+lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
oops
-lemma "(P&Q-->R) --> (P-->R) | (Q-->R)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
+lemma "(P \<and> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R) \<or> (Q \<longrightarrow> R)"
+apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
oops
-subsection\<open>de Bruijn formulae\<close>
+subsection \<open>de Bruijn formulae\<close>
-text\<open>de Bruijn formula with three predicates\<close>
-lemma "((P<->Q) --> P&Q&R) &
- ((Q<->R) --> P&Q&R) &
- ((R<->P) --> P&Q&R) --> P&Q&R"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>de Bruijn formula with three predicates\<close>
+lemma
+ "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R) \<and>
+ ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R) \<and>
+ ((R \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R) \<longrightarrow> P \<and> Q \<and> R"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>de Bruijn formula with five predicates\<close>
-lemma "((P<->Q) --> P&Q&R&S&T) &
- ((Q<->R) --> P&Q&R&S&T) &
- ((R<->S) --> P&Q&R&S&T) &
- ((S<->T) --> P&Q&R&S&T) &
- ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>de Bruijn formula with five predicates\<close>
+lemma
+ "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+ ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+ ((R \<longleftrightarrow> S) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+ ((S \<longleftrightarrow> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+ ((T \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-(*** Problems from of Sahlin, Franzen and Haridi,
- An Intuitionistic Predicate Logic Theorem Prover.
- J. Logic and Comp. 2 (5), October 1992, 619-656.
-***)
+text \<open>
+ Problems from of Sahlin, Franzen and Haridi,
+ An Intuitionistic Predicate Logic Theorem Prover.
+ J. Logic and Comp. 2 (5), October 1992, 619-656.
+\<close>
text\<open>Problem 1.1\<close>
-lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->
- (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
-by (tactic\<open>IntPr.best_dup_tac @{context} 1\<close>) --\<open>SLOW\<close>
+lemma
+ "(\<forall>x. \<exists>y. \<forall>z. p(x) \<and> q(y) \<and> r(z)) \<longleftrightarrow>
+ (\<forall>z. \<exists>y. \<forall>x. p(x) \<and> q(y) \<and> r(z))"
+ by (tactic \<open>IntPr.best_dup_tac @{context} 1\<close>) --\<open>SLOW\<close>
text\<open>Problem 3.1\<close>
-lemma "~ (EX x. ALL y. mem(y,x) <-> ~ mem(x,x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (\<exists>x. \<forall>y. mem(y,x) \<longleftrightarrow> \<not> mem(x,x))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>Problem 4.1: hopeless!\<close>
-lemma "(ALL x. p(x) --> p(h(x)) | p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))
- --> (EX x. p(g(g(g(g(g(x)))))))"
-oops
+lemma
+ "(\<forall>x. p(x) \<longrightarrow> p(h(x)) \<or> p(g(x))) \<and> (\<exists>x. p(x)) \<and> (\<forall>x. \<not> p(h(x)))
+ \<longrightarrow> (\<exists>x. p(g(g(g(g(g(x)))))))"
+ oops
-subsection\<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
+subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
-text\<open>~~1\<close>
-lemma "~~((P-->Q) <-> (~Q --> ~P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>1\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~2\<close>
-lemma "~~(~~P <-> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>2\<close>
+lemma "\<not> \<not> (\<not> \<not> P \<longleftrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~4\<close>
-lemma "~~((~P-->Q) <-> (~Q --> P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>4\<close>
+lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~5\<close>
-lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>5\<close>
+lemma "\<not>\<not>((P \<or> Q \<longrightarrow> P \<or> R) \<longrightarrow> P \<or> (Q \<longrightarrow> R))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~6\<close>
-lemma "~~(P | ~P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>6\<close>
+lemma "\<not> \<not> (P \<or> \<not> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~7\<close>
-lemma "~~(P | ~~~P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>7\<close>
+lemma "\<not> \<not> (P \<or> \<not> \<not> \<not> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~8. Peirce's law\<close>
-lemma "~~(((P-->Q) --> P) --> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>8. Peirce's law\<close>
+lemma "\<not> \<not> (((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>10\<close>
-lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-subsection\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
-lemma "P<->P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~12. Dijkstra's law\<close>
-lemma "~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-lemma "((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>13. Distributive law\<close>
-lemma "P | (Q & R) <-> (P | Q) & (P | R)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~14\<close>
-lemma "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~15\<close>
-lemma "~~((P --> Q) <-> (~P | Q))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~16\<close>
-lemma "~~((P-->Q) | (Q-->P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~17\<close>
-lemma "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>Dijkstra's "Golden Rule"\<close>
-lemma "(P&Q) <-> P <-> Q <-> (P|Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(Q \<longrightarrow> R) \<longrightarrow> (R \<longrightarrow> P \<and> Q) \<longrightarrow> (P \<longrightarrow> (Q \<or> R)) \<longrightarrow> (P \<longleftrightarrow> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-subsection\<open>****Examples with quantifiers****\<close>
+subsection\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
+
+lemma "P \<longleftrightarrow> P"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>12. Dijkstra's law\<close>
+lemma "\<not> \<not> (((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longrightarrow> \<not> \<not> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>13. Distributive law\<close>
+lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>14\<close>
+lemma "\<not> \<not> ((P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>15\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>16\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>17\<close>
+lemma "\<not> \<not> (((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text \<open>Dijkstra's ``Golden Rule''\<close>
+lemma "(P \<and> Q) \<longleftrightarrow> P \<longleftrightarrow> Q \<longleftrightarrow> (P \<or> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+
+section \<open>Examples with quantifiers\<close>
+
+subsection \<open>The converse is classical in the following implications \dots\<close>
+
+lemma "(\<exists>x. P(x) \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. P(x) \<and> \<not> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((\<forall>x. \<not> P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. \<not> (P(x) \<or> Q))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "(\<forall>x. P(x)) \<or> Q \<longrightarrow> (\<forall>x. P(x) \<or> Q)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<longrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-subsection\<open>The converse is classical in the following implications...\<close>
+subsection \<open>The following are not constructively valid!\<close>
+text \<open>The attempt to prove them terminates quickly!\<close>
-lemma "(EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)"
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+ apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+ oops
-lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<longrightarrow> (\<exists>x. P \<longrightarrow> Q(x))"
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+ apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+ oops
-lemma "((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. P(x) \<or> Q) \<longrightarrow> ((\<forall>x. P(x)) \<or> Q)"
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+ apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+ oops
-lemma "(ALL x. P(x)) | Q --> (ALL x. P(x) | Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+ apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+ oops
-lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-
+text \<open>Classically but not intuitionistically valid. Proved by a bug in 1986!\<close>
+lemma "\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))"
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+ apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+ oops
-subsection\<open>The following are not constructively valid!\<close>
-text\<open>The attempt to prove them terminates quickly!\<close>
-
-lemma "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
+subsection \<open>Hard examples with quantifiers\<close>
-lemma "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
-lemma "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
+text \<open>
+ The ones that have not been proved are not known to be valid! Some will
+ require quantifier duplication -- not currently available.
+\<close>
-lemma "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
-text\<open>Classically but not intuitionistically valid. Proved by a bug in 1986!\<close>
-lemma "EX x. Q(x) --> (ALL x. Q(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
+text\<open>\<not>\<not>18\<close>
+lemma "\<not> \<not> (\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x))"
+ oops -- \<open>NOT PROVED\<close>
-subsection\<open>Hard examples with quantifiers\<close>
-
-text\<open>The ones that have not been proved are not known to be valid!
- Some will require quantifier duplication -- not currently available\<close>
-
-text\<open>~~18\<close>
-lemma "~~(EX y. ALL x. P(y)-->P(x))"
-oops --\<open>NOT PROVED\<close>
-
-text\<open>~~19\<close>
-lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
-oops --\<open>NOT PROVED\<close>
+text\<open>\<not>\<not>19\<close>
+lemma "\<not> \<not> (\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x)))"
+ oops -- \<open>NOT PROVED\<close>
text\<open>20\<close>
-lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
- --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>21\<close>
-lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"
-oops --\<open>NOT PROVED; needs quantifier duplication\<close>
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> \<not> \<not> (\<exists>x. P \<longleftrightarrow> Q(x))"
+ oops -- \<open>NOT PROVED; needs quantifier duplication\<close>
text\<open>22\<close>
-lemma "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~23\<close>
-lemma "~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>23\<close>
+lemma "\<not> \<not> ((\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x))))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>24\<close>
-lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
- (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
- --> ~~(EX x. P(x)&R(x))"
-txt\<open>Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and
- @{text ITER_DEEPEN} all take forever\<close>
-apply (tactic\<open>IntPr.safe_tac @{context}\<close>)
-apply (erule impE)
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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> \<not> \<not> (\<exists>x. P(x) \<and> R(x))"
+text \<open>
+ Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and
+ @{text ITER_DEEPEN} all take forever.
+\<close>
+ apply (tactic \<open>IntPr.safe_tac @{context}\<close>)
+ apply (erule impE)
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+ apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+ done
text\<open>25\<close>
-lemma "(EX x. P(x)) &
- (ALL x. L(x) --> ~ (M(x) & R(x))) &
- (ALL x. P(x) --> (M(x) & L(x))) &
- ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
- --> (EX x. Q(x)&P(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~26\<close>
-lemma "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &
- (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
- --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
-oops --\<open>NOT PROVED\<close>
+text\<open>\<not>\<not>26\<close>
+lemma
+ "(\<not> \<not> (\<exists>x. p(x)) \<longleftrightarrow> \<not> \<not> (\<exists>x. q(x))) \<and>
+ (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
+ \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
+ oops --\<open>NOT PROVED\<close>
text\<open>27\<close>
-lemma "(EX x. P(x) & ~Q(x)) &
- (ALL x. P(x) --> R(x)) &
- (ALL x. M(x) & L(x) --> P(x)) &
- ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
- --> (ALL x. M(x) --> ~L(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~28. AMENDED\<close>
-lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
- (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
- (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
- --> (ALL x. P(x) & L(x) --> M(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>28. AMENDED\<close>
+lemma
+ "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+ (\<not> \<not> (\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
+ (\<not> \<not> (\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
+ \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
-lemma "(EX x. P(x)) & (EX y. Q(y))
- --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <->
- (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
+lemma
+ "(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+ \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
+ (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~30\<close>
-lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
- (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
- --> (ALL x. ~~S(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>30\<close>
+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. \<not> \<not> S(x))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>31\<close>
-lemma "~(EX x. P(x) & (Q(x) | R(x))) &
- (EX x. L(x) & P(x)) &
- (ALL x. ~ R(x) --> M(x))
- --> (EX x. L(x) & M(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>32\<close>
-lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
- (ALL x. S(x) & R(x) --> L(x)) &
- (ALL x. M(x) --> R(x))
- --> (ALL x. P(x) & M(x) --> L(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>~~33\<close>
-lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c))) <->
- (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
-apply (tactic\<open>IntPr.best_tac @{context} 1\<close>)
-done
+text\<open>\<not>\<not>33\<close>
+lemma
+ "(\<forall>x. \<not> \<not> (P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c))) \<longleftrightarrow>
+ (\<forall>x. \<not> \<not> ((\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c))))"
+ apply (tactic \<open>IntPr.best_tac @{context} 1\<close>)
+ done
text\<open>36\<close>
-lemma "(ALL x. EX y. J(x,y)) &
- (ALL x. EX y. G(x,y)) &
- (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
- --> (ALL x. EX y. H(x,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>37\<close>
-lemma "(ALL z. EX w. ALL x. EX y.
- ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &
- (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
- (~~(EX x y. Q(x,y)) --> (ALL x. R(x,x)))
- --> ~~(ALL x. EX y. R(x,y))"
-oops --\<open>NOT PROVED\<close>
+lemma
+ "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+ \<not> \<not> (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>
+ (\<not> \<not> (\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
+ \<longrightarrow> \<not> \<not> (\<forall>x. \<exists>y. R(x,y))"
+ oops --\<open>NOT PROVED\<close>
text\<open>39\<close>
-lemma "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
-text\<open>40. AMENDED\<close>
-lemma "(EX y. ALL x. F(x,y) <-> F(x,x)) -->
- ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>40. AMENDED\<close>
+lemma
+ "(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+ \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>44\<close>
-lemma "(ALL x. f(x) -->
- (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) &
- (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
- --> (EX x. j(x) & ~f(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>48\<close>
-lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>51\<close>
-lemma "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
- (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+ "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>52\<close>
-text\<open>Almost the same as 51.\<close>
-lemma "(EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) -->
- (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>Almost the same as 51.\<close>
+lemma
+ "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+ (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>56\<close>
-lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>57\<close>
-lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
- (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+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 (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
text\<open>60\<close>
-lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+ by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
end
-
--- a/src/FOL/ex/Locale_Test/Locale_Test.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test.thy Mon Oct 19 23:00:07 2015 +0200
@@ -16,9 +16,9 @@
lemmas less_mixin_thy_merge2 = le'.less_def
end
-lemma "gless(x, y) <-> gle(x, y) & x ~= y" (* mixin from first interpretation applied *)
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" (* mixin from first interpretation applied *)
by (rule le1.less_mixin_thy_merge1)
-lemma "gless'(x, y) <-> gle'(x, y) & x ~= y" (* mixin from second interpretation applied *)
+lemma "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y" (* mixin from second interpretation applied *)
by (rule le1.less_mixin_thy_merge2)
end
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Oct 19 23:00:07 2015 +0200
@@ -114,8 +114,8 @@
and P :: "'a => 'b => o"
begin
-definition test :: "'a => o" where
- "test(x) <-> (ALL b. P(x, b))"
+definition test :: "'a => o"
+ where "test(x) \<longleftrightarrow> (\<forall>b. P(x, b))"
end
@@ -133,8 +133,8 @@
and p2 :: "'b => o"
begin
-definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
-definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
+definition d1 :: "'a => o" where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
+definition d2 :: "'b => o" where "d2(x) \<longleftrightarrow> \<not> p2(x)"
thm d1_def d2_def
@@ -222,10 +222,10 @@
(* A somewhat arcane homomorphism example *)
definition semi_hom where
- "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
+ "semi_hom(prod, sum, h) \<longleftrightarrow> (\<forall>x y. h(prod(x, y)) = sum(h(x), h(y)))"
lemma semi_hom_mult:
- "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
+ "semi_hom(prod, sum, h) \<Longrightarrow> h(prod(x, y)) = sum(h(x), h(y))"
by (simp add: semi_hom_def)
locale semi_hom_loc = prod: semi prod + sum: semi sum
@@ -242,7 +242,7 @@
(* Referring to facts from within a context specification *)
lemma
- assumes x: "P <-> P"
+ assumes x: "P \<longleftrightarrow> P"
notes y = x
shows True ..
@@ -250,7 +250,7 @@
section \<open>Theorem statements\<close>
lemma (in lgrp) lcancel:
- "x ** y = x ** z <-> y = z"
+ "x ** y = x ** z \<longleftrightarrow> y = z"
proof
assume "x ** y = x ** z"
then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
@@ -266,7 +266,7 @@
begin
lemma rcancel:
- "y ** x = z ** x <-> y = z"
+ "y ** x = z ** x \<longleftrightarrow> y = z"
proof
assume "y ** x = z ** x"
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
@@ -322,7 +322,7 @@
(* use of derived theorem *)
lemma (in lgrp)
- "y ** x = z ** x <-> y = z"
+ "y ** x = z ** x \<longleftrightarrow> y = z"
apply (rule rcancel)
done
@@ -372,7 +372,7 @@
begin
definition greater :: "'a => 'a => o" (infix ">>" 50) where
- "x >> y <-> y << x"
+ "x >> y \<longleftrightarrow> y << x"
end
@@ -392,7 +392,7 @@
locale A5 =
fixes A and B and C and D and E
- assumes eq: "A <-> B <-> C <-> D <-> E"
+ assumes eq: "A \<longleftrightarrow> B \<longleftrightarrow> C \<longleftrightarrow> D \<longleftrightarrow> E"
sublocale A5 < 1: A5 _ _ D E C
print_facts
@@ -415,7 +415,7 @@
locale trivial =
fixes P and Q :: o
- assumes Q: "P <-> P <-> Q"
+ assumes Q: "P \<longleftrightarrow> P \<longleftrightarrow> Q"
begin
lemma Q_triv: "Q" using Q by fast
@@ -494,28 +494,28 @@
locale logic_o =
fixes land (infixl "&&" 55)
and lnot ("-- _" [60] 60)
- assumes assoc_o: "(x && y) && z <-> x && (y && z)"
- and notnot_o: "-- (-- x) <-> x"
+ assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
+ and notnot_o: "-- (-- x) \<longleftrightarrow> x"
begin
definition lor_o (infixl "||" 50) where
- "x || y <-> --(-- x && -- y)"
+ "x || y \<longleftrightarrow> --(-- x && -- y)"
end
-interpretation x: logic_o "op &" "Not"
- where bool_logic_o: "x.lor_o(x, y) <-> x | y"
+interpretation x: logic_o "op \<and>" "Not"
+ where bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
proof -
- show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
- show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+ show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
+ show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
qed
thm x.lor_o_def bool_logic_o
-lemma lor_triv: "z <-> z" ..
+lemma lor_triv: "z \<longleftrightarrow> z" ..
-lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+lemma (in logic_o) lor_triv: "x || y \<longleftrightarrow> x || y" by fast
thm lor_triv [where z = True] (* Check strict prefix. *)
x.lor_triv
@@ -528,7 +528,7 @@
assumes refl: "x \<sqsubseteq> x"
begin
-definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
+definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
end
@@ -536,8 +536,8 @@
gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
where
- grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
- grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+ grefl: "gle(x, x)" and gless_def: "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" and
+ grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y"
text \<open>Setup\<close>
@@ -546,11 +546,11 @@
lemmas less_thm = less_def
end
-interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
+interpretation le: mixin gle where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin(gle)" by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin_def]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -565,7 +565,7 @@
by unfold_locales
thm le.less_thm2 (* rewrite morphism applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le.less_thm2)
text \<open>Rewrite morphism does not leak to a side branch.\<close>
@@ -579,7 +579,7 @@
by unfold_locales
thm le.less_thm3 (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" by (rule le.less_thm3)
text \<open>Rewrite morphism only available in original context\<close>
@@ -588,11 +588,11 @@
locale mixin4_mixin = mixin4_base
interpretation le: mixin4_mixin gle
- where "reflexive.less(gle, x, y) <-> gless(x, y)"
+ where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -610,7 +610,7 @@
by unfold_locales (rule grefl')
thm le4.less_thm4' (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le4.less_thm4')
text \<open>Inherited rewrite morphism applied to new theorem\<close>
@@ -620,11 +620,11 @@
locale mixin5_inherited = mixin5_base
interpretation le5: mixin5_base gle
- where "reflexive.less(gle, x, y) <-> gless(x, y)"
+ where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin5_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin5_base_def mixin_def]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -634,7 +634,7 @@
lemmas (in mixin5_inherited) less_thm5 = less_def
thm le5.less_thm5 (* rewrite morphism applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le5.less_thm5)
text \<open>Rewrite morphism pushed down to existing inherited locale\<close>
@@ -648,18 +648,18 @@
interpretation le6: mixin6_inherited gle
by unfold_locales
interpretation le6: mixin6_base gle
- where "reflexive.less(gle, x, y) <-> gless(x, y)"
+ where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin6_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin6_base_def mixin_def]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
lemmas (in mixin6_inherited) less_thm6 = less_def
thm le6.less_thm6 (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le6.less_thm6)
text \<open>Existing rewrite morphism inherited through sublocale relation\<close>
@@ -669,11 +669,11 @@
locale mixin7_inherited = reflexive
interpretation le7: mixin7_base gle
- where "reflexive.less(gle, x, y) <-> gless(x, y)"
+ where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin7_base(gle)" by unfold_locales
note reflexive = this[unfolded mixin7_base_def mixin_def]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
@@ -683,7 +683,7 @@
lemmas (in mixin7_inherited) less_thm7 = less_def
thm le7.less_thm7 (* before, rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le7.less_thm7)
sublocale mixin7_inherited < mixin7_base
@@ -692,7 +692,7 @@
lemmas (in mixin7_inherited) less_thm7b = less_def
thm le7.less_thm7b (* after, mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
by (rule le7.less_thm7b)
@@ -764,11 +764,11 @@
text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
-locale roundup = fixes x assumes true: "x <-> True"
+locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
-sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True"
+sublocale roundup \<subseteq> sub: roundup x where "x \<longleftrightarrow> True \<and> True"
apply unfold_locales apply (simp add: true) done
-lemma (in roundup) "True & True <-> True" by (rule sub.true)
+lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
section \<open>Interpretation in named contexts\<close>
@@ -812,19 +812,19 @@
proof
{
fix pand and pnot and por
- assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
- and pnotnot: "!!x. pnot(pnot(x)) <-> x"
- and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
+ assume passoc: "\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))"
+ and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
+ and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
interpret loc: logic_o pand pnot
- where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)" (* FIXME *)
+ where por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)" (* FIXME *)
proof -
show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
fix x y
- show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
+ show "logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"
by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
qed
print_interps logic_o
- have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
+ have "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
}
qed
--- a/src/FOL/ex/Locale_Test/Locale_Test2.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,11 +9,11 @@
begin
interpretation le1: mixin_thy_merge gle gle'
- where "reflexive.less(gle, x, y) <-> gless(x, y)"
+ where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
proof -
show "mixin_thy_merge(gle, gle')" by unfold_locales
note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1]
- show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
--- a/src/FOL/ex/Locale_Test/Locale_Test3.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,11 +9,11 @@
begin
interpretation le2: mixin_thy_merge gle gle'
- where "reflexive.less(gle', x, y) <-> gless'(x, y)"
+ where "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
proof -
show "mixin_thy_merge(gle, gle')" by unfold_locales
note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
- show "reflexive.less(gle', x, y) <-> gless'(x, y)"
+ show "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
by (simp add: reflexive.less_def[OF reflexive] gless'_def)
qed
--- a/src/FOL/ex/Miniscope.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Miniscope.thy Mon Oct 19 23:00:07 2015 +0200
@@ -11,7 +11,6 @@
imports FOL
begin
-
lemmas ccontr = FalseE [THEN classical]
subsection \<open>Negation Normal Form\<close>
@@ -19,20 +18,20 @@
subsubsection \<open>de Morgan laws\<close>
lemma demorgans:
- "~(P&Q) <-> ~P | ~Q"
- "~(P|Q) <-> ~P & ~Q"
- "~~P <-> P"
- "!!P. ~(ALL x. P(x)) <-> (EX x. ~P(x))"
- "!!P. ~(EX x. P(x)) <-> (ALL x. ~P(x))"
+ "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
+ "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
+ "\<not> \<not> P \<longleftrightarrow> P"
+ "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
+ "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
by blast+
(*** Removal of --> and <-> (positive and negative occurrences) ***)
(*Last one is important for computing a compact CNF*)
lemma nnf_simps:
- "(P-->Q) <-> (~P | Q)"
- "~(P-->Q) <-> (P & ~Q)"
- "(P<->Q) <-> (~P | Q) & (~Q | P)"
- "~(P<->Q) <-> (P | Q) & (~P | ~Q)"
+ "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+ "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)"
+ "(P \<longleftrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q) \<and> (\<not> Q \<or> P)"
+ "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<or> Q) \<and> (\<not> P \<or> \<not> Q)"
by blast+
@@ -41,24 +40,24 @@
subsubsection \<open>Pushing in the existential quantifiers\<close>
lemma ex_simps:
- "(EX x. P) <-> P"
- "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
- "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
- "!!P Q. (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
- "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
- "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+ "(\<exists>x. P) \<longleftrightarrow> P"
+ "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+ "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+ "\<And>P Q. (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
+ "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+ "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
by blast+
subsubsection \<open>Pushing in the universal quantifiers\<close>
lemma all_simps:
- "(ALL x. P) <-> P"
- "!!P Q. (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
- "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
- "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
- "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
- "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+ "(\<forall>x. P) \<longleftrightarrow> P"
+ "\<And>P Q. (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+ "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+ "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+ "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+ "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
by blast+
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
--- a/src/FOL/ex/Nat.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Nat.thy Mon Oct 19 23:00:07 2015 +0200
@@ -29,7 +29,7 @@
subsection \<open>Proofs about the natural numbers\<close>
-lemma Suc_n_not_n: "Suc(k) ~= k"
+lemma Suc_n_not_n: "Suc(k) \<noteq> k"
apply (rule_tac n = k in induct)
apply (rule notI)
apply (erule Suc_neq_0)
--- a/src/FOL/ex/Prolog.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Prolog.thy Mon Oct 19 23:00:07 2015 +0200
@@ -83,7 +83,7 @@
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences
total inferences = 2 + 1 + 17 + 561 = 581*)
-schematic_goal "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
+schematic_goal "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x \<and> app(?x,?x,?y) \<and> rev(?y,?w)"
apply (tactic \<open>
DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
done
--- a/src/FOL/ex/Propositional_Cla.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,109 +9,112 @@
imports FOL
begin
-text \<open>commutative laws of @{text "&"} and @{text "|"}\<close>
+text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
-lemma "P & Q --> Q & P"
+lemma "P \<and> Q \<longrightarrow> Q \<and> P"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "P | Q --> Q | P"
+lemma "P \<or> Q \<longrightarrow> Q \<or> P"
by fast
-text \<open>associative laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) & R --> P & (Q & R)"
+text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
by fast
-lemma "(P | Q) | R --> P | (Q | R)"
+lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
by fast
-text \<open>distributive laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) | R --> (P | R) & (Q | R)"
+text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
by fast
-lemma "(P | R) & (Q | R) --> (P & Q) | R"
+lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
by fast
-lemma "(P | Q) & R --> (P & R) | (Q & R)"
+lemma "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
by fast
-lemma "(P & R) | (Q & R) --> (P | Q) & R"
+lemma "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
by fast
text \<open>Laws involving implication\<close>
-lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
+lemma "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
by fast
-lemma "(P & Q --> R) <-> (P--> (Q-->R))"
+lemma "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
by fast
-lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+lemma "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
by fast
-lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+lemma "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
by fast
-lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)"
+lemma "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
by fast
text \<open>Propositions-as-types\<close>
-- \<open>The combinator K\<close>
-lemma "P --> (Q --> P)"
+lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
by fast
-- \<open>The combinator S\<close>
-lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)"
+lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
by fast
-- \<open>Converse is classical\<close>
-lemma "(P-->Q) | (P-->R) --> (P --> Q | R)"
+lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
by fast
-lemma "(P-->Q) --> (~Q --> ~P)"
+lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
by fast
text \<open>Schwichtenberg's examples (via T. Nipkow)\<close>
-lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+lemma stab_imp: "(((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q"
by fast
lemma stab_to_peirce:
- "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
- --> ((P --> Q) --> P) --> P"
+ "(((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> (((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q)
+ \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
by fast
-lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)
- --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
- by fast
-
-lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+lemma peirce_imp1:
+ "(((Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> Q)
+ \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
by fast
-lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
+lemma peirce_imp2: "(((P \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> ((P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P"
+ by fast
+
+lemma mints: "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
by fast
-lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+lemma mints_solovev: "(P \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R"
by fast
-lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)
- --> (((P8 --> P2) --> P9) --> P3 --> P10)
- --> (P1 --> P8) --> P6 --> P7
- --> (((P3 --> P2) --> P9) --> P4)
- --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
+lemma tatsuta:
+ "(((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+ \<longrightarrow> (((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+ \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7
+ \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+ \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P5"
by fast
-lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)
- --> (((P3 --> P2) --> P9) --> P4)
- --> (((P6 --> P1) --> P2) --> P9)
- --> (((P7 --> P1) --> P10) --> P4 --> P5)
- --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
+lemma tatsuta1:
+ "(((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+ \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+ \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9)
+ \<longrightarrow> (((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+ \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7 \<longrightarrow> P5"
by fast
end
--- a/src/FOL/ex/Propositional_Int.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Propositional_Int.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,109 +9,112 @@
imports IFOL
begin
-text \<open>commutative laws of @{text "&"} and @{text "|"}\<close>
+text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
-lemma "P & Q --> Q & P"
+lemma "P \<and> Q \<longrightarrow> Q \<and> P"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "P | Q --> Q | P"
+lemma "P \<or> Q \<longrightarrow> Q \<or> P"
by (tactic "IntPr.fast_tac @{context} 1")
-text \<open>associative laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) & R --> P & (Q & R)"
+text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P | Q) | R --> P | (Q | R)"
+lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-text \<open>distributive laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) | R --> (P | R) & (Q | R)"
+text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P | R) & (Q | R) --> (P & Q) | R"
+lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P | Q) & R --> (P & R) | (Q & R)"
+lemma "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P & R) | (Q & R) --> (P | Q) & R"
+lemma "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Laws involving implication\<close>
-lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
+lemma "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P & Q --> R) <-> (P--> (Q-->R))"
+lemma "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+lemma "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+lemma "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P --> Q & R) <-> (P-->Q) & (P-->R)"
+lemma "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Propositions-as-types\<close>
-- \<open>The combinator K\<close>
-lemma "P --> (Q --> P)"
+lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
by (tactic "IntPr.fast_tac @{context} 1")
-- \<open>The combinator S\<close>
-lemma "(P-->Q-->R) --> (P-->Q) --> (P-->R)"
+lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-- \<open>Converse is classical\<close>
-lemma "(P-->Q) | (P-->R) --> (P --> Q | R)"
+lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(P-->Q) --> (~Q --> ~P)"
+lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Schwichtenberg's examples (via T. Nipkow)\<close>
-lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+lemma stab_imp: "(((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q"
by (tactic "IntPr.fast_tac @{context} 1")
lemma stab_to_peirce:
- "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)
- --> ((P --> Q) --> P) --> P"
+ "(((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> (((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q)
+ \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)
- --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
- by (tactic "IntPr.fast_tac @{context} 1")
-
-lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+lemma peirce_imp1:
+ "(((Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> Q)
+ \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
+lemma peirce_imp2: "(((P \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> ((P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P"
+ by (tactic "IntPr.fast_tac @{context} 1")
+
+lemma mints: "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+lemma mints_solovev: "(P \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)
- --> (((P8 --> P2) --> P9) --> P3 --> P10)
- --> (P1 --> P8) --> P6 --> P7
- --> (((P3 --> P2) --> P9) --> P4)
- --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
+lemma tatsuta:
+ "(((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+ \<longrightarrow> (((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+ \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7
+ \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+ \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P5"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)
- --> (((P3 --> P2) --> P9) --> P4)
- --> (((P6 --> P1) --> P2) --> P9)
- --> (((P7 --> P1) --> P10) --> P4 --> P5)
- --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
+lemma tatsuta1:
+ "(((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+ \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+ \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9)
+ \<longrightarrow> (((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+ \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7 \<longrightarrow> P5"
by (tactic "IntPr.fast_tac @{context} 1")
end
--- a/src/FOL/ex/Quantifiers_Cla.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Quantifiers_Cla.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,92 +9,92 @@
imports FOL
begin
-lemma "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
by fast
-lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
+lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
by fast
--- \<open>Converse is false\<close>
-lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+text \<open>Converse is false.\<close>
+lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
by fast
-lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
+lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
by fast
-lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
by fast
-text \<open>Some harder ones\<close>
+text \<open>Some harder ones.\<close>
-lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
by fast
--- \<open>Converse is false\<close>
-lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
+-- \<open>Converse is false.\<close>
+lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
by fast
-text \<open>Basic test of quantifier reasoning\<close>
+text \<open>Basic test of quantifier reasoning.\<close>
-- \<open>TRUE\<close>
-lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
by fast
-lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
text \<open>The following should fail, as they are false!\<close>
-lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
+lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
apply fast?
oops
-lemma "(EX x. Q(x)) --> (ALL x. Q(x))"
+lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
apply fast?
oops
-schematic_goal "P(?a) --> (ALL x. P(x))"
+schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
apply fast?
oops
-schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
apply fast?
oops
text \<open>Back to things that are provable \dots\<close>
-lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
--- \<open>An example of why exI should be delayed as long as possible\<close>
-lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+text \<open>An example of why @{text exI} should be delayed as long as possible.\<close>
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
by fast
-schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
by fast
-lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by fast
text \<open>Some slow ones\<close>
--- \<open>Principia Mathematica *11.53\<close>
-lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+text \<open>Principia Mathematica *11.53\<close>
+lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
by fast
(*Principia Mathematica *11.55 *)
-lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
by fast
(*Principia Mathematica *11.61 *)
-lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
by fast
end
--- a/src/FOL/ex/Quantifiers_Int.thy Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy Mon Oct 19 23:00:07 2015 +0200
@@ -9,92 +9,92 @@
imports IFOL
begin
-lemma "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))"
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
+lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
by (tactic "IntPr.fast_tac @{context} 1")
-- \<open>Converse is false\<close>
-lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"
+lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Some harder ones\<close>
-lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
-- \<open>Converse is false\<close>
-lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Basic test of quantifier reasoning\<close>
-- \<open>TRUE\<close>
-lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>The following should fail, as they are false!\<close>
-lemma "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"
+lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
apply (tactic "IntPr.fast_tac @{context} 1")?
oops
-lemma "(EX x. Q(x)) --> (ALL x. Q(x))"
+lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
apply (tactic "IntPr.fast_tac @{context} 1")?
oops
-schematic_goal "P(?a) --> (ALL x. P(x))"
+schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
apply (tactic "IntPr.fast_tac @{context} 1")?
oops
-schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
apply (tactic "IntPr.fast_tac @{context} 1")?
oops
text \<open>Back to things that are provable \dots\<close>
-lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
-- \<open>An example of why exI should be delayed as long as possible\<close>
-lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
-schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
by (tactic "IntPr.fast_tac @{context} 1")
-lemma "(ALL x. Q(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
by (tactic "IntPr.fast_tac @{context} 1")
text \<open>Some slow ones\<close>
-- \<open>Principia Mathematica *11.53\<close>
-lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
by (tactic "IntPr.fast_tac @{context} 1")
(*Principia Mathematica *11.55 *)
-lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
by (tactic "IntPr.fast_tac @{context} 1")
(*Principia Mathematica *11.61 *)
-lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
by (tactic "IntPr.fast_tac @{context} 1")
end