src/HOL/Isar_Examples/Peirce.thy
 author nipkow Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) changeset 46372 6fa9cdb8b850 parent 37671 fa53d267dab3 child 55640 abc140f21caa permissions -rw-r--r--
 wenzelm@33026  1 (* Title: HOL/Isar_Examples/Peirce.thy  wenzelm@6444  2  Author: Markus Wenzel, TU Muenchen  wenzelm@6444  3 *)  wenzelm@6444  4 wenzelm@10007  5 header {* Peirce's Law *}  wenzelm@6444  6 wenzelm@31758  7 theory Peirce  wenzelm@31758  8 imports Main  wenzelm@31758  9 begin  wenzelm@6444  10 wenzelm@37671  11 text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  wenzelm@37671  12  This is an inherently non-intuitionistic statement, so its proof  wenzelm@37671  13  will certainly involve some form of classical contradiction.  wenzelm@7860  14 wenzelm@37671  15  The first proof is again a well-balanced combination of plain  wenzelm@37671  16  backward and forward reasoning. The actual classical step is where  wenzelm@37671  17  the negated goal may be introduced as additional assumption. This  wenzelm@37671  18  eventually leads to a contradiction.\footnote{The rule involved  wenzelm@37671  19  there is negation elimination; it holds in intuitionistic logic as  wenzelm@37671  20  well.} *}  wenzelm@7860  21 wenzelm@10007  22 theorem "((A --> B) --> A) --> A"  wenzelm@10007  23 proof  wenzelm@23373  24  assume "(A --> B) --> A"  wenzelm@10007  25  show A  wenzelm@10007  26  proof (rule classical)  wenzelm@10007  27  assume "~ A"  wenzelm@10007  28  have "A --> B"  wenzelm@10007  29  proof  wenzelm@10007  30  assume A  wenzelm@23373  31  with ~ A show B by contradiction  wenzelm@10007  32  qed  wenzelm@23373  33  with (A --> B) --> A show A ..  wenzelm@10007  34  qed  wenzelm@10007  35 qed  wenzelm@6444  36 wenzelm@37671  37 text {* In the subsequent version the reasoning is rearranged by means  wenzelm@37671  38  of weak assumptions'' (as introduced by \isacommand{presume}).  wenzelm@37671  39  Before assuming the negated goal $\neg A$, its intended consequence  wenzelm@37671  40  $A \impl B$ is put into place in order to solve the main problem.  wenzelm@37671  41  Nevertheless, we do not get anything for free, but have to establish  wenzelm@37671  42  $A \impl B$ later on. The overall effect is that of a logical  wenzelm@37671  43  \emph{cut}.  wenzelm@7860  44 wenzelm@37671  45  Technically speaking, whenever some goal is solved by  wenzelm@37671  46  \isacommand{show} in the context of weak assumptions then the latter  wenzelm@37671  47  give rise to new subgoals, which may be established separately. In  wenzelm@37671  48  contrast, strong assumptions (as introduced by \isacommand{assume})  wenzelm@37671  49  are solved immediately. *}  wenzelm@7860  50 wenzelm@10007  51 theorem "((A --> B) --> A) --> A"  wenzelm@10007  52 proof  wenzelm@23373  53  assume "(A --> B) --> A"  wenzelm@10007  54  show A  wenzelm@10007  55  proof (rule classical)  wenzelm@10007  56  presume "A --> B"  wenzelm@23373  57  with (A --> B) --> A show A ..  wenzelm@10007  58  next  wenzelm@10007  59  assume "~ A"  wenzelm@10007  60  show "A --> B"  wenzelm@10007  61  proof  wenzelm@10007  62  assume A  wenzelm@23373  63  with ~ A show B by contradiction  wenzelm@10007  64  qed  wenzelm@10007  65  qed  wenzelm@10007  66 qed  wenzelm@6444  67 wenzelm@37671  68 text {* Note that the goals stemming from weak assumptions may be even  wenzelm@37671  69  left until qed time, where they get eventually solved by  wenzelm@37671  70  assumption'' as well. In that case there is really no fundamental  wenzelm@37671  71  difference between the two kinds of assumptions, apart from the  wenzelm@37671  72  order of reducing the individual parts of the proof configuration.  wenzelm@7860  73 wenzelm@37671  74  Nevertheless, the strong'' mode of plain assumptions is quite  wenzelm@37671  75  important in practice to achieve robustness of proof text  wenzelm@37671  76  interpretation. By forcing both the conclusion \emph{and} the  wenzelm@37671  77  assumptions to unify with the pending goal to be solved, goal  wenzelm@37671  78  selection becomes quite deterministic. For example, decomposition  wenzelm@37671  79  with rules of the case-analysis'' type usually gives rise to  wenzelm@37671  80  several goals that only differ in there local contexts. With strong  wenzelm@37671  81  assumptions these may be still solved in any order in a predictable  wenzelm@37671  82  way, while weak ones would quickly lead to great confusion,  wenzelm@37671  83  eventually demanding even some backtracking. *}  wenzelm@7860  84 wenzelm@10007  85 end