author paulson Mon May 17 10:37:07 1999 +0200 (1999-05-17) changeset 6645 6c62700fa48a parent 6644 123b215882ae child 6646 3ea726909fff
indentation
 src/FOL/ex/cla.ML file | annotate | diff | revisions
```     1.1 --- a/src/FOL/ex/cla.ML	Sat May 15 16:15:54 1999 +0200
1.2 +++ b/src/FOL/ex/cla.ML	Mon May 17 10:37:07 1999 +0200
1.3 @@ -143,7 +143,7 @@
1.4
1.5  (*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
1.6    JAR 10 (265-281), 1993.  Proof is trivial!*)
1.7 -Goal "~ ((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
1.8 +Goal "~((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
1.9  by (Blast_tac 1);
1.10  result();
1.11
1.12 @@ -216,16 +216,16 @@
1.13
1.14  writeln"Problem 24";
1.15  Goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
1.16 -\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
1.17 +\     (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
1.18  \   --> (EX x. P(x)&R(x))";
1.19  by (Blast_tac 1);
1.20  result();
1.21
1.22  writeln"Problem 25";
1.23  Goal "(EX x. P(x)) &  \
1.24 -\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
1.25 -\       (ALL x. P(x) --> (M(x) & L(x))) &   \
1.26 -\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
1.27 +\     (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
1.28 +\     (ALL x. P(x) --> (M(x) & L(x))) &   \
1.29 +\     ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
1.30  \   --> (EX x. Q(x)&P(x))";
1.31  by (Blast_tac 1);
1.32  result();
1.33 @@ -239,10 +239,10 @@
1.34
1.35  writeln"Problem 27";
1.36  Goal "(EX x. P(x) & ~Q(x)) &   \
1.37 -\             (ALL x. P(x) --> R(x)) &   \
1.38 -\             (ALL x. M(x) & L(x) --> P(x)) &   \
1.39 -\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
1.40 -\         --> (ALL x. M(x) --> ~L(x))";
1.41 +\     (ALL x. P(x) --> R(x)) &   \
1.42 +\     (ALL x. M(x) & L(x) --> P(x)) &   \
1.43 +\     ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
1.44 +\ --> (ALL x. M(x) --> ~L(x))";
1.45  by (Blast_tac 1);
1.46  result();
1.47
1.48 @@ -263,7 +263,7 @@
1.49
1.50  writeln"Problem 30";
1.51  Goal "(ALL x. P(x) | Q(x) --> ~ R(x)) & \
1.52 -\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
1.53 +\     (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
1.54  \   --> (ALL x. S(x))";
1.55  by (Blast_tac 1);
1.56  result();
1.57 @@ -278,24 +278,24 @@
1.58
1.59  writeln"Problem 32";
1.60  Goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
1.61 -\       (ALL x. S(x) & R(x) --> L(x)) & \
1.62 -\       (ALL x. M(x) --> R(x))  \
1.63 -\   --> (ALL x. P(x) & M(x) --> L(x))";
1.64 +\     (ALL x. S(x) & R(x) --> L(x)) & \
1.65 +\     (ALL x. M(x) --> R(x))  \
1.66 +\     --> (ALL x. P(x) & M(x) --> L(x))";
1.67  by (Blast_tac 1);
1.68  result();
1.69
1.70  writeln"Problem 33";
1.71  Goal "(ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
1.72 -\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
1.73 +\     (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
1.74  by (Blast_tac 1);
1.75  result();
1.76
1.77  writeln"Problem 34  AMENDED (TWICE!!)";
1.78  (*Andrews's challenge*)
1.79  Goal "((EX x. ALL y. p(x) <-> p(y))  <->                \
1.80 -\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
1.81 -\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
1.82 -\              ((EX x. p(x)) <-> (ALL y. q(y))))";
1.83 +\      ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
1.84 +\     ((EX x. ALL y. q(x) <-> q(y))  <->                \
1.85 +\      ((EX x. p(x)) <-> (ALL y. q(y))))";
1.86  by (Blast_tac 1);
1.87  result();
1.88
1.89 @@ -315,17 +315,17 @@
1.90  writeln"Problem 37";
1.91  Goal "(ALL z. EX w. ALL x. EX y. \
1.92  \          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
1.93 -\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
1.94 -\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
1.95 -\   --> (ALL x. EX y. R(x,y))";
1.96 +\     (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
1.97 +\     ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
1.98 +\     --> (ALL x. EX y. R(x,y))";
1.99  by (Blast_tac 1);
1.100  result();
1.101
1.102  writeln"Problem 38";
1.103  Goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
1.104  \            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
1.105 -\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
1.106 -\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
1.107 +\     (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
1.108 +\             (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
1.109  \             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
1.110  by (Blast_tac 1);  (*beats fast_tac!*)
1.111  result();
1.112 @@ -363,10 +363,9 @@
1.113  result();
1.114
1.115  writeln"Problem 44";
1.116 -Goal "(ALL x. f(x) -->                                          \
1.117 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
1.118 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
1.119 -\             --> (EX x. j(x) & ~f(x))";
1.120 +Goal "(ALL x. f(x) --> (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
1.121 +\     (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
1.122 +\     --> (EX x. j(x) & ~f(x))";
1.123  by (Blast_tac 1);
1.124  result();
1.125
1.126 @@ -383,10 +382,10 @@
1.127
1.128  writeln"Problem 46";
1.129  Goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) &      \
1.130 -\    ((EX x. f(x) & ~g(x)) -->                                    \
1.131 -\     (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) &    \
1.132 -\    (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                    \
1.133 -\     --> (ALL x. f(x) --> g(x))";
1.134 +\     ((EX x. f(x) & ~g(x)) -->                                    \
1.135 +\      (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) &    \
1.136 +\     (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                    \
1.137 +\      --> (ALL x. f(x) --> g(x))";
1.138  by (Blast_tac 1);
1.139  result();
1.140
1.141 @@ -419,14 +418,14 @@
1.142
1.143  writeln"Problem 51";
1.144  Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
1.145 -\    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
1.146 +\     (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
1.147  by (Blast_tac 1);
1.148  result();
1.149
1.150  writeln"Problem 52";
1.151  (*Almost the same as 51. *)
1.152  Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
1.153 -\    (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
1.154 +\     (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
1.155  by (Blast_tac 1);
1.156  result();
1.157
1.158 @@ -498,8 +497,8 @@
1.159
1.160  writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
1.161  Goal "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
1.162 -\    (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
1.163 -\            (~p(a) | ~p(f(x)) | p(f(f(x)))))";
1.164 +\     (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
1.165 +\             (~p(a) | ~p(f(x)) | p(f(f(x)))))";
1.166  by (Blast_tac 1);
1.167  result();
1.168
1.169 @@ -514,8 +513,8 @@
1.170  (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
1.171    It does seem obvious!*)
1.172  Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
1.173 -\    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
1.174 -\    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
1.175 +\     (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
1.176 +\     (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
1.177  by (Fast_tac 1);
1.178  result();
1.179
```