28 |
28 |
29 theory Intuitionistic |
29 theory Intuitionistic |
30 imports IFOLP |
30 imports IFOLP |
31 begin |
31 begin |
32 |
32 |
33 schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q" |
33 schematic_goal "?p : ~~(P&Q) <-> ~~P & ~~Q" |
34 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
34 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
35 |
35 |
36 schematic_lemma "?p : ~~~P <-> ~P" |
36 schematic_goal "?p : ~~~P <-> ~P" |
37 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
37 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
38 |
38 |
39 schematic_lemma "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))" |
39 schematic_goal "?p : ~~((P --> Q | R) --> (P-->Q) | (P-->R))" |
40 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
40 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
41 |
41 |
42 schematic_lemma "?p : (P<->Q) <-> (Q<->P)" |
42 schematic_goal "?p : (P<->Q) <-> (Q<->P)" |
43 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
43 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
44 |
44 |
45 |
45 |
46 subsection \<open>Lemmas for the propositional double-negation translation\<close> |
46 subsection \<open>Lemmas for the propositional double-negation translation\<close> |
47 |
47 |
48 schematic_lemma "?p : P --> ~~P" |
48 schematic_goal "?p : P --> ~~P" |
49 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
49 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
50 |
50 |
51 schematic_lemma "?p : ~~(~~P --> P)" |
51 schematic_goal "?p : ~~(~~P --> P)" |
52 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
52 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
53 |
53 |
54 schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q" |
54 schematic_goal "?p : ~~P & ~~(P --> Q) --> ~~Q" |
55 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
55 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
56 |
56 |
57 |
57 |
58 subsection \<open>The following are classically but not constructively valid\<close> |
58 subsection \<open>The following are classically but not constructively valid\<close> |
59 |
59 |
60 (*The attempt to prove them terminates quickly!*) |
60 (*The attempt to prove them terminates quickly!*) |
61 schematic_lemma "?p : ((P-->Q) --> P) --> P" |
61 schematic_goal "?p : ((P-->Q) --> P) --> P" |
62 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
62 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
63 oops |
63 oops |
64 |
64 |
65 schematic_lemma "?p : (P&Q-->R) --> (P-->R) | (Q-->R)" |
65 schematic_goal "?p : (P&Q-->R) --> (P-->R) | (Q-->R)" |
66 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
66 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
67 oops |
67 oops |
68 |
68 |
69 |
69 |
70 subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier\<close> |
70 subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier\<close> |
71 |
71 |
72 text "Problem ~~1" |
72 text "Problem ~~1" |
73 schematic_lemma "?p : ~~((P-->Q) <-> (~Q --> ~P))" |
73 schematic_goal "?p : ~~((P-->Q) <-> (~Q --> ~P))" |
74 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
74 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
75 |
75 |
76 text "Problem ~~2" |
76 text "Problem ~~2" |
77 schematic_lemma "?p : ~~(~~P <-> P)" |
77 schematic_goal "?p : ~~(~~P <-> P)" |
78 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
78 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
79 |
79 |
80 text "Problem 3" |
80 text "Problem 3" |
81 schematic_lemma "?p : ~(P-->Q) --> (Q-->P)" |
81 schematic_goal "?p : ~(P-->Q) --> (Q-->P)" |
82 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
82 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
83 |
83 |
84 text "Problem ~~4" |
84 text "Problem ~~4" |
85 schematic_lemma "?p : ~~((~P-->Q) <-> (~Q --> P))" |
85 schematic_goal "?p : ~~((~P-->Q) <-> (~Q --> P))" |
86 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
86 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
87 |
87 |
88 text "Problem ~~5" |
88 text "Problem ~~5" |
89 schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))" |
89 schematic_goal "?p : ~~((P|Q-->P|R) --> P|(Q-->R))" |
90 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
90 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
91 |
91 |
92 text "Problem ~~6" |
92 text "Problem ~~6" |
93 schematic_lemma "?p : ~~(P | ~P)" |
93 schematic_goal "?p : ~~(P | ~P)" |
94 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
94 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
95 |
95 |
96 text "Problem ~~7" |
96 text "Problem ~~7" |
97 schematic_lemma "?p : ~~(P | ~~~P)" |
97 schematic_goal "?p : ~~(P | ~~~P)" |
98 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
98 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
99 |
99 |
100 text "Problem ~~8. Peirce's law" |
100 text "Problem ~~8. Peirce's law" |
101 schematic_lemma "?p : ~~(((P-->Q) --> P) --> P)" |
101 schematic_goal "?p : ~~(((P-->Q) --> P) --> P)" |
102 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
102 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
103 |
103 |
104 text "Problem 9" |
104 text "Problem 9" |
105 schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
105 schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
106 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
106 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
107 |
107 |
108 text "Problem 10" |
108 text "Problem 10" |
109 schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)" |
109 schematic_goal "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)" |
110 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
110 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
111 |
111 |
112 text "11. Proved in each direction (incorrectly, says Pelletier!!) " |
112 text "11. Proved in each direction (incorrectly, says Pelletier!!) " |
113 schematic_lemma "?p : P<->P" |
113 schematic_goal "?p : P<->P" |
114 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
114 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
115 |
115 |
116 text "Problem ~~12. Dijkstra's law " |
116 text "Problem ~~12. Dijkstra's law " |
117 schematic_lemma "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))" |
117 schematic_goal "?p : ~~(((P <-> Q) <-> R) <-> (P <-> (Q <-> R)))" |
118 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
118 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
119 |
119 |
120 schematic_lemma "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))" |
120 schematic_goal "?p : ((P <-> Q) <-> R) --> ~~(P <-> (Q <-> R))" |
121 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
121 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
122 |
122 |
123 text "Problem 13. Distributive law" |
123 text "Problem 13. Distributive law" |
124 schematic_lemma "?p : P | (Q & R) <-> (P | Q) & (P | R)" |
124 schematic_goal "?p : P | (Q & R) <-> (P | Q) & (P | R)" |
125 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
125 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
126 |
126 |
127 text "Problem ~~14" |
127 text "Problem ~~14" |
128 schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))" |
128 schematic_goal "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))" |
129 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
129 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
130 |
130 |
131 text "Problem ~~15" |
131 text "Problem ~~15" |
132 schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))" |
132 schematic_goal "?p : ~~((P --> Q) <-> (~P | Q))" |
133 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
133 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
134 |
134 |
135 text "Problem ~~16" |
135 text "Problem ~~16" |
136 schematic_lemma "?p : ~~((P-->Q) | (Q-->P))" |
136 schematic_goal "?p : ~~((P-->Q) | (Q-->P))" |
137 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
137 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
138 |
138 |
139 text "Problem ~~17" |
139 text "Problem ~~17" |
140 schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))" |
140 schematic_goal "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))" |
141 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) -- slow |
141 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) -- slow |
142 |
142 |
143 |
143 |
144 subsection \<open>Examples with quantifiers\<close> |
144 subsection \<open>Examples with quantifiers\<close> |
145 |
145 |
146 text "The converse is classical in the following implications..." |
146 text "The converse is classical in the following implications..." |
147 |
147 |
148 schematic_lemma "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" |
148 schematic_goal "?p : (EX x. P(x)-->Q) --> (ALL x. P(x)) --> Q" |
149 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
149 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
150 |
150 |
151 schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" |
151 schematic_goal "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)" |
152 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
152 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
153 |
153 |
154 schematic_lemma "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" |
154 schematic_goal "?p : ((ALL x. ~P(x))-->Q) --> ~ (ALL x. ~ (P(x)|Q))" |
155 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
155 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
156 |
156 |
157 schematic_lemma "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" |
157 schematic_goal "?p : (ALL x. P(x)) | Q --> (ALL x. P(x) | Q)" |
158 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
158 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
159 |
159 |
160 schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" |
160 schematic_goal "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))" |
161 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
161 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
162 |
162 |
163 |
163 |
164 text "The following are not constructively valid!" |
164 text "The following are not constructively valid!" |
165 text "The attempt to prove them terminates quickly!" |
165 text "The attempt to prove them terminates quickly!" |
166 |
166 |
167 schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)" |
167 schematic_goal "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)" |
168 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
168 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
169 oops |
169 oops |
170 |
170 |
171 schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))" |
171 schematic_goal "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))" |
172 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
172 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
173 oops |
173 oops |
174 |
174 |
175 schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)" |
175 schematic_goal "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)" |
176 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
176 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
177 oops |
177 oops |
178 |
178 |
179 schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))" |
179 schematic_goal "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))" |
180 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
180 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
181 oops |
181 oops |
182 |
182 |
183 (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) |
183 (*Classically but not intuitionistically valid. Proved by a bug in 1986!*) |
184 schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))" |
184 schematic_goal "?p : EX x. Q(x) --> (ALL x. Q(x))" |
185 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
185 apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)? |
186 oops |
186 oops |
187 |
187 |
188 |
188 |
189 subsection "Hard examples with quantifiers" |
189 subsection "Hard examples with quantifiers" |
192 The ones that have not been proved are not known to be valid! |
192 The ones that have not been proved are not known to be valid! |
193 Some will require quantifier duplication -- not currently available. |
193 Some will require quantifier duplication -- not currently available. |
194 \<close> |
194 \<close> |
195 |
195 |
196 text "Problem ~~18" |
196 text "Problem ~~18" |
197 schematic_lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops |
197 schematic_goal "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops |
198 (*NOT PROVED*) |
198 (*NOT PROVED*) |
199 |
199 |
200 text "Problem ~~19" |
200 text "Problem ~~19" |
201 schematic_lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops |
201 schematic_goal "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops |
202 (*NOT PROVED*) |
202 (*NOT PROVED*) |
203 |
203 |
204 text "Problem 20" |
204 text "Problem 20" |
205 schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
205 schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
206 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
206 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
207 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
207 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
208 |
208 |
209 text "Problem 21" |
209 text "Problem 21" |
210 schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops |
210 schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops |
211 (*NOT PROVED*) |
211 (*NOT PROVED*) |
212 |
212 |
213 text "Problem 22" |
213 text "Problem 22" |
214 schematic_lemma "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" |
214 schematic_goal "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" |
215 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
215 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
216 |
216 |
217 text "Problem ~~23" |
217 text "Problem ~~23" |
218 schematic_lemma "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))" |
218 schematic_goal "?p : ~~ ((ALL x. P | Q(x)) <-> (P | (ALL x. Q(x))))" |
219 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
219 by (tactic \<open>IntPr.fast_tac @{context} 1\<close>) |
220 |
220 |
221 text "Problem 24" |
221 text "Problem 24" |
222 schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & |
222 schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & |
223 (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) |
223 (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) |
224 --> ~~(EX x. P(x)&R(x))" |
224 --> ~~(EX x. P(x)&R(x))" |
225 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) |
225 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) |
226 apply (tactic "IntPr.safe_tac @{context}") |
226 apply (tactic "IntPr.safe_tac @{context}") |
227 apply (erule impE) |
227 apply (erule impE) |
228 apply (tactic "IntPr.fast_tac @{context} 1") |
228 apply (tactic "IntPr.fast_tac @{context} 1") |
229 apply (tactic "IntPr.fast_tac @{context} 1") |
229 apply (tactic "IntPr.fast_tac @{context} 1") |
230 done |
230 done |
231 |
231 |
232 text "Problem 25" |
232 text "Problem 25" |
233 schematic_lemma "?p : (EX x. P(x)) & |
233 schematic_goal "?p : (EX x. P(x)) & |
234 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
234 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
235 (ALL x. P(x) --> (M(x) & L(x))) & |
235 (ALL x. P(x) --> (M(x) & L(x))) & |
236 ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) |
236 ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x))) |
237 --> (EX x. Q(x)&P(x))" |
237 --> (EX x. Q(x)&P(x))" |
238 by (tactic "IntPr.best_tac @{context} 1") |
238 by (tactic "IntPr.best_tac @{context} 1") |
239 |
239 |
240 text "Problem 29. Essentially the same as Principia Mathematica *11.71" |
240 text "Problem 29. Essentially the same as Principia Mathematica *11.71" |
241 schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y)) |
241 schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y)) |
242 --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> |
242 --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> |
243 (ALL x y. P(x) & Q(y) --> R(x) & S(y)))" |
243 (ALL x y. P(x) & Q(y) --> R(x) & S(y)))" |
244 by (tactic "IntPr.fast_tac @{context} 1") |
244 by (tactic "IntPr.fast_tac @{context} 1") |
245 |
245 |
246 text "Problem ~~30" |
246 text "Problem ~~30" |
247 schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & |
247 schematic_goal "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & |
248 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
248 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
249 --> (ALL x. ~~S(x))" |
249 --> (ALL x. ~~S(x))" |
250 by (tactic "IntPr.fast_tac @{context} 1") |
250 by (tactic "IntPr.fast_tac @{context} 1") |
251 |
251 |
252 text "Problem 31" |
252 text "Problem 31" |
253 schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) & |
253 schematic_goal "?p : ~(EX x. P(x) & (Q(x) | R(x))) & |
254 (EX x. L(x) & P(x)) & |
254 (EX x. L(x) & P(x)) & |
255 (ALL x. ~ R(x) --> M(x)) |
255 (ALL x. ~ R(x) --> M(x)) |
256 --> (EX x. L(x) & M(x))" |
256 --> (EX x. L(x) & M(x))" |
257 by (tactic "IntPr.fast_tac @{context} 1") |
257 by (tactic "IntPr.fast_tac @{context} 1") |
258 |
258 |
259 text "Problem 32" |
259 text "Problem 32" |
260 schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
260 schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
261 (ALL x. S(x) & R(x) --> L(x)) & |
261 (ALL x. S(x) & R(x) --> L(x)) & |
262 (ALL x. M(x) --> R(x)) |
262 (ALL x. M(x) --> R(x)) |
263 --> (ALL x. P(x) & M(x) --> L(x))" |
263 --> (ALL x. P(x) & M(x) --> L(x))" |
264 by (tactic "IntPr.best_tac @{context} 1") -- slow |
264 by (tactic "IntPr.best_tac @{context} 1") -- slow |
265 |
265 |
266 text "Problem 39" |
266 text "Problem 39" |
267 schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" |
267 schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" |
268 by (tactic "IntPr.best_tac @{context} 1") |
268 by (tactic "IntPr.best_tac @{context} 1") |
269 |
269 |
270 text "Problem 40. AMENDED" |
270 text "Problem 40. AMENDED" |
271 schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> |
271 schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> |
272 ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))" |
272 ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))" |
273 by (tactic "IntPr.best_tac @{context} 1") -- slow |
273 by (tactic "IntPr.best_tac @{context} 1") -- slow |
274 |
274 |
275 text "Problem 44" |
275 text "Problem 44" |
276 schematic_lemma "?p : (ALL x. f(x) --> |
276 schematic_goal "?p : (ALL x. f(x) --> |
277 (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & |
277 (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & |
278 (EX x. j(x) & (ALL y. g(y) --> h(x,y))) |
278 (EX x. j(x) & (ALL y. g(y) --> h(x,y))) |
279 --> (EX x. j(x) & ~f(x))" |
279 --> (EX x. j(x) & ~f(x))" |
280 by (tactic "IntPr.best_tac @{context} 1") |
280 by (tactic "IntPr.best_tac @{context} 1") |
281 |
281 |
282 text "Problem 48" |
282 text "Problem 48" |
283 schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
283 schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
284 by (tactic "IntPr.best_tac @{context} 1") |
284 by (tactic "IntPr.best_tac @{context} 1") |
285 |
285 |
286 text "Problem 51" |
286 text "Problem 51" |
287 schematic_lemma |
287 schematic_goal |
288 "?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> |
288 "?p : (EX z w. ALL x y. P(x,y) <-> (x=z & y=w)) --> |
289 (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)" |
289 (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)" |
290 by (tactic "IntPr.best_tac @{context} 1") -- \<open>60 seconds\<close> |
290 by (tactic "IntPr.best_tac @{context} 1") -- \<open>60 seconds\<close> |
291 |
291 |
292 text "Problem 56" |
292 text "Problem 56" |
293 schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" |
293 schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" |
294 by (tactic "IntPr.best_tac @{context} 1") |
294 by (tactic "IntPr.best_tac @{context} 1") |
295 |
295 |
296 text "Problem 57" |
296 text "Problem 57" |
297 schematic_lemma |
297 schematic_goal |
298 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & |
298 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & |
299 (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))" |
299 (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))" |
300 by (tactic "IntPr.best_tac @{context} 1") |
300 by (tactic "IntPr.best_tac @{context} 1") |
301 |
301 |
302 text "Problem 60" |
302 text "Problem 60" |
303 schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
303 schematic_goal "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
304 by (tactic "IntPr.best_tac @{context} 1") |
304 by (tactic "IntPr.best_tac @{context} 1") |
305 |
305 |
306 end |
306 end |