412 (*<*) |
412 (*<*) |
413 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
413 theorem "\<And>A. PROP A \<Longrightarrow> PROP A" |
414 proof - |
414 proof - |
415 (*>*) |
415 (*>*) |
416 |
416 |
417 txt_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
417 text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
418 |
418 |
419 have "A \<longrightarrow> B" |
419 have "A \<longrightarrow> B" |
420 proof |
420 proof |
421 assume A |
421 assume A |
422 show B sorry %noproof |
422 show B sorry %noproof |
423 qed |
423 qed |
424 |
424 |
425 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
425 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
426 |
426 |
427 have "A \<longrightarrow> B" and A sorry %noproof |
427 have "A \<longrightarrow> B" and A sorry %noproof |
428 then have B .. |
428 then have B .. |
429 |
429 |
430 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
430 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
431 |
431 |
432 have A sorry %noproof |
432 have A sorry %noproof |
433 then have "A \<or> B" .. |
433 then have "A \<or> B" .. |
434 |
434 |
435 have B sorry %noproof |
435 have B sorry %noproof |
436 then have "A \<or> B" .. |
436 then have "A \<or> B" .. |
437 |
437 |
438 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
438 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
439 |
439 |
440 have "A \<or> B" sorry %noproof |
440 have "A \<or> B" sorry %noproof |
441 then have C |
441 then have C |
442 proof |
442 proof |
443 assume A |
443 assume A |
445 next |
445 next |
446 assume B |
446 assume B |
447 then show C sorry %noproof |
447 then show C sorry %noproof |
448 qed |
448 qed |
449 |
449 |
450 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
450 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
451 |
451 |
452 have A and B sorry %noproof |
452 have A and B sorry %noproof |
453 then have "A \<and> B" .. |
453 then have "A \<and> B" .. |
454 |
454 |
455 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
455 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
456 |
456 |
457 have "A \<and> B" sorry %noproof |
457 have "A \<and> B" sorry %noproof |
458 then obtain A and B .. |
458 then obtain A and B .. |
459 |
459 |
460 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
460 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
461 |
461 |
462 have "\<bottom>" sorry %noproof |
462 have "\<bottom>" sorry %noproof |
463 then have A .. |
463 then have A .. |
464 |
464 |
465 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
465 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
466 |
466 |
467 have "\<top>" .. |
467 have "\<top>" .. |
468 |
468 |
469 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
469 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
470 |
470 |
471 have "\<not> A" |
471 have "\<not> A" |
472 proof |
472 proof |
473 assume A |
473 assume A |
474 then show "\<bottom>" sorry %noproof |
474 then show "\<bottom>" sorry %noproof |
475 qed |
475 qed |
476 |
476 |
477 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
477 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
478 |
478 |
479 have "\<not> A" and A sorry %noproof |
479 have "\<not> A" and A sorry %noproof |
480 then have B .. |
480 then have B .. |
481 |
481 |
482 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
482 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
483 |
483 |
484 have "\<forall>x. B x" |
484 have "\<forall>x. B x" |
485 proof |
485 proof |
486 fix x |
486 fix x |
487 show "B x" sorry %noproof |
487 show "B x" sorry %noproof |
488 qed |
488 qed |
489 |
489 |
490 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
490 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
491 |
491 |
492 have "\<forall>x. B x" sorry %noproof |
492 have "\<forall>x. B x" sorry %noproof |
493 then have "B a" .. |
493 then have "B a" .. |
494 |
494 |
495 txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
495 text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
496 |
496 |
497 have "\<exists>x. B x" |
497 have "\<exists>x. B x" |
498 proof |
498 proof |
499 show "B a" sorry %noproof |
499 show "B a" sorry %noproof |
500 qed |
500 qed |
501 |
501 |
502 txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
502 text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) |
503 |
503 |
504 have "\<exists>x. B x" sorry %noproof |
504 have "\<exists>x. B x" sorry %noproof |
505 then obtain a where "B a" .. |
505 then obtain a where "B a" .. |
506 |
506 |
507 txt_raw \<open>\end{minipage}\<close> |
507 text_raw \<open>\end{minipage}\<close> |
508 |
508 |
509 (*<*) |
509 (*<*) |
510 qed |
510 qed |
511 (*>*) |
511 (*>*) |
512 |
512 |