--- a/src/FOLP/ex/quant.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/quant.ML Fri Oct 10 16:29:41 1997 +0200
@@ -9,40 +9,40 @@
writeln"File FOLP/ex/quant.ML";
-goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))";
+goal thy "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
result();
-goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))";
+goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
result();
(*Converse is false*)
-goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
+goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
result();
-goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))";
+goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
result();
-goal thy "?p : (ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)";
+goal thy "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
result();
writeln"Some harder ones";
-goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
+goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
result();
(*6 secs*)
(*Converse is false*)
-goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))";
+goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
by tac;
result();
@@ -70,26 +70,26 @@
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal thy "?p : P(?a) --> (ALL x.P(x))";
+goal thy "?p : P(?a) --> (ALL x. P(x))";
by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
goal thy
- "?p : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+ "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
writeln"Back to things that are provable...";
-goal thy "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
by tac;
result();
(*An example of why exI should be delayed as long as possible*)
-goal thy "?p : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
+goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
by tac;
result();