equal
deleted
inserted
replaced
1 (* Title: FOL/ex/prop |
1 (* Title: FOL/ex/prop |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 First-Order Logic: propositional examples (intuitionistic and classical) |
6 First-Order Logic: propositional examples (intuitionistic and classical) |
7 Needs declarations of the theory "thy" and the tactic "tac" |
7 Needs declarations of the theory "thy" and the tactic "tac" |
8 *) |
8 *) |
105 by tac; |
105 by tac; |
106 result(); |
106 result(); |
107 |
107 |
108 (* stab-to-peirce *) |
108 (* stab-to-peirce *) |
109 goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \ |
109 goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \ |
110 \ --> ((P --> Q) --> P) --> P"; |
110 \ --> ((P --> Q) --> P) --> P"; |
111 by tac; |
111 by tac; |
112 result(); |
112 result(); |
113 |
113 |
114 (* peirce-imp1 *) |
114 (* peirce-imp1 *) |
115 goal thy "?p : (((Q --> R) --> Q) --> Q) \ |
115 goal thy "?p : (((Q --> R) --> Q) --> Q) \ |
116 \ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"; |
116 \ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"; |
117 by tac; |
117 by tac; |
118 result(); |
118 result(); |
119 |
119 |
120 (* peirce-imp2 *) |
120 (* peirce-imp2 *) |
121 goal thy "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"; |
121 goal thy "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"; |
132 by tac; |
132 by tac; |
133 result(); |
133 result(); |
134 |
134 |
135 (* tatsuta *) |
135 (* tatsuta *) |
136 goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \ |
136 goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \ |
137 \ --> (((P8 --> P2) --> P9) --> P3 --> P10) \ |
137 \ --> (((P8 --> P2) --> P9) --> P3 --> P10) \ |
138 \ --> (P1 --> P8) --> P6 --> P7 \ |
138 \ --> (P1 --> P8) --> P6 --> P7 \ |
139 \ --> (((P3 --> P2) --> P9) --> P4) \ |
139 \ --> (((P3 --> P2) --> P9) --> P4) \ |
140 \ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"; |
140 \ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"; |
141 by tac; |
141 by tac; |
142 result(); |
142 result(); |
143 |
143 |
144 (* tatsuta1 *) |
144 (* tatsuta1 *) |
145 goal thy "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \ |
145 goal thy "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \ |