src/FOLP/ex/quant.ML
changeset 18678 dd0c569fa43d
parent 17480 fd19f77dcf60
equal deleted inserted replaced
18677:01265301db7f 18678:dd0c569fa43d
    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