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