219 theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> |
219 theorem exE_realizer': "P (snd p) (fst p) \<Longrightarrow> |
220 (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp |
220 (\<And>x y. P y x \<Longrightarrow> Q) \<Longrightarrow> Q" by (cases p) simp |
221 |
221 |
222 realizers |
222 realizers |
223 impI (P, Q): "\<lambda>pq. pq" |
223 impI (P, Q): "\<lambda>pq. pq" |
224 "\<Lambda>P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
224 "\<Lambda> P Q pq (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
225 |
225 |
226 impI (P): "Null" |
226 impI (P): "Null" |
227 "\<Lambda>P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
227 "\<Lambda> P Q (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h \<cdot> x))" |
228 |
228 |
229 impI (Q): "\<lambda>q. q" "\<Lambda>P Q q. impI \<cdot> _ \<cdot> _" |
229 impI (Q): "\<lambda>q. q" "\<Lambda> P Q q. impI \<cdot> _ \<cdot> _" |
230 |
230 |
231 impI: "Null" "impI" |
231 impI: "Null" "impI" |
232 |
232 |
233 mp (P, Q): "\<lambda>pq. pq" |
233 mp (P, Q): "\<lambda>pq. pq" |
234 "\<Lambda>P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
234 "\<Lambda> P Q pq (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
235 |
235 |
236 mp (P): "Null" |
236 mp (P): "Null" |
237 "\<Lambda>P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
237 "\<Lambda> P Q (h: _) p. mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
238 |
238 |
239 mp (Q): "\<lambda>q. q" "\<Lambda>P Q q. mp \<cdot> _ \<cdot> _" |
239 mp (Q): "\<lambda>q. q" "\<Lambda> P Q q. mp \<cdot> _ \<cdot> _" |
240 |
240 |
241 mp: "Null" "mp" |
241 mp: "Null" "mp" |
242 |
242 |
243 allI (P): "\<lambda>p. p" "\<Lambda>P p. allI \<cdot> _" |
243 allI (P): "\<lambda>p. p" "\<Lambda> P p. allI \<cdot> _" |
244 |
244 |
245 allI: "Null" "allI" |
245 allI: "Null" "allI" |
246 |
246 |
247 spec (P): "\<lambda>x p. p x" "\<Lambda>P x p. spec \<cdot> _ \<cdot> x" |
247 spec (P): "\<lambda>x p. p x" "\<Lambda> P x p. spec \<cdot> _ \<cdot> x" |
248 |
248 |
249 spec: "Null" "spec" |
249 spec: "Null" "spec" |
250 |
250 |
251 exI (P): "\<lambda>x p. (x, p)" "\<Lambda>P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x" |
251 exI (P): "\<lambda>x p. (x, p)" "\<Lambda> P x p. exI_realizer \<cdot> P \<cdot> p \<cdot> x" |
252 |
252 |
253 exI: "\<lambda>x. x" "\<Lambda>P x (h: _). h" |
253 exI: "\<lambda>x. x" "\<Lambda> P x (h: _). h" |
254 |
254 |
255 exE (P, Q): "\<lambda>p pq. case p of (x, y) \<Rightarrow> pq x y" |
255 exE (P, Q): "\<lambda>p pq. case p of (x, y) \<Rightarrow> pq x y" |
256 "\<Lambda>P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h" |
256 "\<Lambda> P Q p (h: _) pq. exE_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> pq \<bullet> h" |
257 |
257 |
258 exE (P): "Null" |
258 exE (P): "Null" |
259 "\<Lambda>P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" |
259 "\<Lambda> P Q p. exE_realizer' \<cdot> _ \<cdot> _ \<cdot> _" |
260 |
260 |
261 exE (Q): "\<lambda>x pq. pq x" |
261 exE (Q): "\<lambda>x pq. pq x" |
262 "\<Lambda>P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
262 "\<Lambda> P Q x (h1: _) pq (h2: _). h2 \<cdot> x \<bullet> h1" |
263 |
263 |
264 exE: "Null" |
264 exE: "Null" |
265 "\<Lambda>P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
265 "\<Lambda> P Q x (h1: _) (h2: _). h2 \<cdot> x \<bullet> h1" |
266 |
266 |
267 conjI (P, Q): "Pair" |
267 conjI (P, Q): "Pair" |
268 "\<Lambda>P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h" |
268 "\<Lambda> P Q p (h: _) q. conjI_realizer \<cdot> P \<cdot> p \<cdot> Q \<cdot> q \<bullet> h" |
269 |
269 |
270 conjI (P): "\<lambda>p. p" |
270 conjI (P): "\<lambda>p. p" |
271 "\<Lambda>P Q p. conjI \<cdot> _ \<cdot> _" |
271 "\<Lambda> P Q p. conjI \<cdot> _ \<cdot> _" |
272 |
272 |
273 conjI (Q): "\<lambda>q. q" |
273 conjI (Q): "\<lambda>q. q" |
274 "\<Lambda>P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
274 "\<Lambda> P Q (h: _) q. conjI \<cdot> _ \<cdot> _ \<bullet> h" |
275 |
275 |
276 conjI: "Null" "conjI" |
276 conjI: "Null" "conjI" |
277 |
277 |
278 conjunct1 (P, Q): "fst" |
278 conjunct1 (P, Q): "fst" |
279 "\<Lambda>P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
279 "\<Lambda> P Q pq. conjunct1 \<cdot> _ \<cdot> _" |
280 |
280 |
281 conjunct1 (P): "\<lambda>p. p" |
281 conjunct1 (P): "\<lambda>p. p" |
282 "\<Lambda>P Q p. conjunct1 \<cdot> _ \<cdot> _" |
282 "\<Lambda> P Q p. conjunct1 \<cdot> _ \<cdot> _" |
283 |
283 |
284 conjunct1 (Q): "Null" |
284 conjunct1 (Q): "Null" |
285 "\<Lambda>P Q q. conjunct1 \<cdot> _ \<cdot> _" |
285 "\<Lambda> P Q q. conjunct1 \<cdot> _ \<cdot> _" |
286 |
286 |
287 conjunct1: "Null" "conjunct1" |
287 conjunct1: "Null" "conjunct1" |
288 |
288 |
289 conjunct2 (P, Q): "snd" |
289 conjunct2 (P, Q): "snd" |
290 "\<Lambda>P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
290 "\<Lambda> P Q pq. conjunct2 \<cdot> _ \<cdot> _" |
291 |
291 |
292 conjunct2 (P): "Null" |
292 conjunct2 (P): "Null" |
293 "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _" |
293 "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
294 |
294 |
295 conjunct2 (Q): "\<lambda>p. p" |
295 conjunct2 (Q): "\<lambda>p. p" |
296 "\<Lambda>P Q p. conjunct2 \<cdot> _ \<cdot> _" |
296 "\<Lambda> P Q p. conjunct2 \<cdot> _ \<cdot> _" |
297 |
297 |
298 conjunct2: "Null" "conjunct2" |
298 conjunct2: "Null" "conjunct2" |
299 |
299 |
300 disjI1 (P, Q): "Inl" |
300 disjI1 (P, Q): "Inl" |
301 "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)" |
301 "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_1 \<cdot> P \<cdot> _ \<cdot> p)" |
302 |
302 |
303 disjI1 (P): "Some" |
303 disjI1 (P): "Some" |
304 "\<Lambda>P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)" |
304 "\<Lambda> P Q p. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> P \<cdot> p)" |
305 |
305 |
306 disjI1 (Q): "None" |
306 disjI1 (Q): "None" |
307 "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
307 "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
308 |
308 |
309 disjI1: "Left" |
309 disjI1: "Left" |
310 "\<Lambda>P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" |
310 "\<Lambda> P Q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_1 \<cdot> _ \<cdot> _)" |
311 |
311 |
312 disjI2 (P, Q): "Inr" |
312 disjI2 (P, Q): "Inr" |
313 "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
313 "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sum.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
314 |
314 |
315 disjI2 (P): "None" |
315 disjI2 (P): "None" |
316 "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
316 "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_1 \<cdot> _ \<cdot> _)" |
317 |
317 |
318 disjI2 (Q): "Some" |
318 disjI2 (Q): "Some" |
319 "\<Lambda>Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
319 "\<Lambda> Q P q. iffD2 \<cdot> _ \<cdot> _ \<bullet> (option.cases_2 \<cdot> _ \<cdot> Q \<cdot> q)" |
320 |
320 |
321 disjI2: "Right" |
321 disjI2: "Right" |
322 "\<Lambda>Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" |
322 "\<Lambda> Q P. iffD2 \<cdot> _ \<cdot> _ \<bullet> (sumbool.cases_2 \<cdot> _ \<cdot> _)" |
323 |
323 |
324 disjE (P, Q, R): "\<lambda>pq pr qr. |
324 disjE (P, Q, R): "\<lambda>pq pr qr. |
325 (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
325 (case pq of Inl p \<Rightarrow> pr p | Inr q \<Rightarrow> qr q)" |
326 "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
326 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
327 disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
327 disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
328 |
328 |
329 disjE (Q, R): "\<lambda>pq pr qr. |
329 disjE (Q, R): "\<lambda>pq pr qr. |
330 (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
330 (case pq of None \<Rightarrow> pr | Some q \<Rightarrow> qr q)" |
331 "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
331 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
332 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
332 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
333 |
333 |
334 disjE (P, R): "\<lambda>pq pr qr. |
334 disjE (P, R): "\<lambda>pq pr qr. |
335 (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
335 (case pq of None \<Rightarrow> qr | Some p \<Rightarrow> pr p)" |
336 "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
336 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr (h3: _). |
337 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" |
337 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> qr \<cdot> pr \<bullet> h1 \<bullet> h3 \<bullet> h2" |
338 |
338 |
339 disjE (R): "\<lambda>pq pr qr. |
339 disjE (R): "\<lambda>pq pr qr. |
340 (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
340 (case pq of Left \<Rightarrow> pr | Right \<Rightarrow> qr)" |
341 "\<Lambda>P Q R pq (h1: _) pr (h2: _) qr. |
341 "\<Lambda> P Q R pq (h1: _) pr (h2: _) qr. |
342 disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
342 disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> R \<cdot> pr \<cdot> qr \<bullet> h1 \<bullet> h2" |
343 |
343 |
344 disjE (P, Q): "Null" |
344 disjE (P, Q): "Null" |
345 "\<Lambda>P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
345 "\<Lambda> P Q R pq. disjE_realizer \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
346 |
346 |
347 disjE (Q): "Null" |
347 disjE (Q): "Null" |
348 "\<Lambda>P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
348 "\<Lambda> P Q R pq. disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
349 |
349 |
350 disjE (P): "Null" |
350 disjE (P): "Null" |
351 "\<Lambda>P Q R pq (h1: _) (h2: _) (h3: _). |
351 "\<Lambda> P Q R pq (h1: _) (h2: _) (h3: _). |
352 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" |
352 disjE_realizer2 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _ \<bullet> h1 \<bullet> h3 \<bullet> h2" |
353 |
353 |
354 disjE: "Null" |
354 disjE: "Null" |
355 "\<Lambda>P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
355 "\<Lambda> P Q R pq. disjE_realizer3 \<cdot> _ \<cdot> _ \<cdot> pq \<cdot> (\<lambda>x. R) \<cdot> _ \<cdot> _" |
356 |
356 |
357 FalseE (P): "arbitrary" |
357 FalseE (P): "arbitrary" |
358 "\<Lambda>P. FalseE \<cdot> _" |
358 "\<Lambda> P. FalseE \<cdot> _" |
359 |
359 |
360 FalseE: "Null" "FalseE" |
360 FalseE: "Null" "FalseE" |
361 |
361 |
362 notI (P): "Null" |
362 notI (P): "Null" |
363 "\<Lambda>P (h: _). allI \<cdot> _ \<bullet> (\<Lambda>x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
363 "\<Lambda> P (h: _). allI \<cdot> _ \<bullet> (\<Lambda> x. notI \<cdot> _ \<bullet> (h \<cdot> x))" |
364 |
364 |
365 notI: "Null" "notI" |
365 notI: "Null" "notI" |
366 |
366 |
367 notE (P, R): "\<lambda>p. arbitrary" |
367 notE (P, R): "\<lambda>p. arbitrary" |
368 "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
368 "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
369 |
369 |
370 notE (P): "Null" |
370 notE (P): "Null" |
371 "\<Lambda>P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
371 "\<Lambda> P R (h: _) p. notE \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> h)" |
372 |
372 |
373 notE (R): "arbitrary" |
373 notE (R): "arbitrary" |
374 "\<Lambda>P R. notE \<cdot> _ \<cdot> _" |
374 "\<Lambda> P R. notE \<cdot> _ \<cdot> _" |
375 |
375 |
376 notE: "Null" "notE" |
376 notE: "Null" "notE" |
377 |
377 |
378 subst (P): "\<lambda>s t ps. ps" |
378 subst (P): "\<lambda>s t ps. ps" |
379 "\<Lambda>s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h" |
379 "\<Lambda> s t P (h: _) ps. subst \<cdot> s \<cdot> t \<cdot> P ps \<bullet> h" |
380 |
380 |
381 subst: "Null" "subst" |
381 subst: "Null" "subst" |
382 |
382 |
383 iffD1 (P, Q): "fst" |
383 iffD1 (P, Q): "fst" |
384 "\<Lambda>Q P pq (h: _) p. |
384 "\<Lambda> Q P pq (h: _) p. |
385 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
385 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> p \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
386 |
386 |
387 iffD1 (P): "\<lambda>p. p" |
387 iffD1 (P): "\<lambda>p. p" |
388 "\<Lambda>Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
388 "\<Lambda> Q P p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h)" |
389 |
389 |
390 iffD1 (Q): "Null" |
390 iffD1 (Q): "Null" |
391 "\<Lambda>Q P q1 (h: _) q2. |
391 "\<Lambda> Q P q1 (h: _) q2. |
392 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
392 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct1 \<cdot> _ \<cdot> _ \<bullet> h))" |
393 |
393 |
394 iffD1: "Null" "iffD1" |
394 iffD1: "Null" "iffD1" |
395 |
395 |
396 iffD2 (P, Q): "snd" |
396 iffD2 (P, Q): "snd" |
397 "\<Lambda>P Q pq (h: _) q. |
397 "\<Lambda> P Q pq (h: _) q. |
398 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
398 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
399 |
399 |
400 iffD2 (P): "\<lambda>p. p" |
400 iffD2 (P): "\<lambda>p. p" |
401 "\<Lambda>P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
401 "\<Lambda> P Q p (h: _). mp \<cdot> _ \<cdot> _ \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h)" |
402 |
402 |
403 iffD2 (Q): "Null" |
403 iffD2 (Q): "Null" |
404 "\<Lambda>P Q q1 (h: _) q2. |
404 "\<Lambda> P Q q1 (h: _) q2. |
405 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
405 mp \<cdot> _ \<cdot> _ \<bullet> (spec \<cdot> _ \<cdot> q2 \<bullet> (conjunct2 \<cdot> _ \<cdot> _ \<bullet> h))" |
406 |
406 |
407 iffD2: "Null" "iffD2" |
407 iffD2: "Null" "iffD2" |
408 |
408 |
409 iffI (P, Q): "Pair" |
409 iffI (P, Q): "Pair" |
410 "\<Lambda>P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
410 "\<Lambda> P Q pq (h1 : _) qp (h2 : _). conjI_realizer \<cdot> |
411 (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> |
411 (\<lambda>pq. \<forall>x. P x \<longrightarrow> Q (pq x)) \<cdot> pq \<cdot> |
412 (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> |
412 (\<lambda>qp. \<forall>x. Q x \<longrightarrow> P (qp x)) \<cdot> qp \<bullet> |
413 (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
413 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
414 (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
414 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
415 |
415 |
416 iffI (P): "\<lambda>p. p" |
416 iffI (P): "\<lambda>p. p" |
417 "\<Lambda>P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
417 "\<Lambda> P Q (h1 : _) p (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
418 (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
418 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h1 \<cdot> x))) \<bullet> |
419 (impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
419 (impI \<cdot> _ \<cdot> _ \<bullet> h2)" |
420 |
420 |
421 iffI (Q): "\<lambda>q. q" |
421 iffI (Q): "\<lambda>q. q" |
422 "\<Lambda>P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
422 "\<Lambda> P Q q (h1 : _) (h2 : _). conjI \<cdot> _ \<cdot> _ \<bullet> |
423 (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
423 (impI \<cdot> _ \<cdot> _ \<bullet> h1) \<bullet> |
424 (allI \<cdot> _ \<bullet> (\<Lambda>x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
424 (allI \<cdot> _ \<bullet> (\<Lambda> x. impI \<cdot> _ \<cdot> _ \<bullet> (h2 \<cdot> x)))" |
425 |
425 |
426 iffI: "Null" "iffI" |
426 iffI: "Null" "iffI" |
427 |
427 |
428 (* |
428 (* |
429 classical: "Null" |
429 classical: "Null" |
430 "\<Lambda>P. classical \<cdot> _" |
430 "\<Lambda> P. classical \<cdot> _" |
431 *) |
431 *) |
432 |
432 |
433 end |
433 end |