58 |
58 |
59 |
59 |
60 writeln"The following should fail, as they are false!"; |
60 writeln"The following should fail, as they are false!"; |
61 |
61 |
62 Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; |
62 Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))"; |
63 by tac handle ERROR => writeln"Failed, as expected"; |
63 by tac handle ERROR _ => writeln"Failed, as expected"; |
64 (*Check that subgoals remain: proof failed.*) |
64 (*Check that subgoals remain: proof failed.*) |
65 getgoal 1; |
65 getgoal 1; |
66 |
66 |
67 Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
67 Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
68 by tac handle ERROR => writeln"Failed, as expected"; |
68 by tac handle ERROR _ => writeln"Failed, as expected"; |
69 getgoal 1; |
69 getgoal 1; |
70 |
70 |
71 Goal "?p : P(?a) --> (ALL x. P(x))"; |
71 Goal "?p : P(?a) --> (ALL x. P(x))"; |
72 by tac handle ERROR => writeln"Failed, as expected"; |
72 by tac handle ERROR _ => writeln"Failed, as expected"; |
73 (*Check that subgoals remain: proof failed.*) |
73 (*Check that subgoals remain: proof failed.*) |
74 getgoal 1; |
74 getgoal 1; |
75 |
75 |
76 Goal |
76 Goal |
77 "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
77 "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
78 by tac handle ERROR => writeln"Failed, as expected"; |
78 by tac handle ERROR _ => writeln"Failed, as expected"; |
79 getgoal 1; |
79 getgoal 1; |
80 |
80 |
81 |
81 |
82 writeln"Back to things that are provable..."; |
82 writeln"Back to things that are provable..."; |
83 |
83 |