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