summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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 |