indentation
authorpaulson
Mon May 17 10:37:07 1999 +0200 (1999-05-17)
changeset 66456c62700fa48a
parent 6644 123b215882ae
child 6646 3ea726909fff
indentation
src/FOL/ex/cla.ML
     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