summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Peirce.thy

changeset 37671 | fa53d267dab3 |

parent 33026 | 8f35633c4922 |

child 55640 | abc140f21caa |

1.1 --- a/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 14:32:57 2010 +0200 1.2 +++ b/src/HOL/Isar_Examples/Peirce.thy Thu Jul 01 18:31:46 2010 +0200 1.3 @@ -8,17 +8,16 @@ 1.4 imports Main 1.5 begin 1.6 1.7 -text {* 1.8 - We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is 1.9 - an inherently non-intuitionistic statement, so its proof will 1.10 - certainly involve some form of classical contradiction. 1.11 +text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. 1.12 + This is an inherently non-intuitionistic statement, so its proof 1.13 + will certainly involve some form of classical contradiction. 1.14 1.15 - The first proof is again a well-balanced combination of plain 1.16 - backward and forward reasoning. The actual classical step is where 1.17 - the negated goal may be introduced as additional assumption. This 1.18 - eventually leads to a contradiction.\footnote{The rule involved there 1.19 - is negation elimination; it holds in intuitionistic logic as well.} 1.20 -*} 1.21 + The first proof is again a well-balanced combination of plain 1.22 + backward and forward reasoning. The actual classical step is where 1.23 + the negated goal may be introduced as additional assumption. This 1.24 + eventually leads to a contradiction.\footnote{The rule involved 1.25 + there is negation elimination; it holds in intuitionistic logic as 1.26 + well.} *} 1.27 1.28 theorem "((A --> B) --> A) --> A" 1.29 proof 1.30 @@ -35,21 +34,19 @@ 1.31 qed 1.32 qed 1.33 1.34 -text {* 1.35 - In the subsequent version the reasoning is rearranged by means of 1.36 - ``weak assumptions'' (as introduced by \isacommand{presume}). Before 1.37 - assuming the negated goal $\neg A$, its intended consequence $A \impl 1.38 - B$ is put into place in order to solve the main problem. 1.39 - Nevertheless, we do not get anything for free, but have to establish 1.40 - $A \impl B$ later on. The overall effect is that of a logical 1.41 - \emph{cut}. 1.42 +text {* In the subsequent version the reasoning is rearranged by means 1.43 + of ``weak assumptions'' (as introduced by \isacommand{presume}). 1.44 + Before assuming the negated goal $\neg A$, its intended consequence 1.45 + $A \impl B$ is put into place in order to solve the main problem. 1.46 + Nevertheless, we do not get anything for free, but have to establish 1.47 + $A \impl B$ later on. The overall effect is that of a logical 1.48 + \emph{cut}. 1.49 1.50 - Technically speaking, whenever some goal is solved by 1.51 - \isacommand{show} in the context of weak assumptions then the latter 1.52 - give rise to new subgoals, which may be established separately. In 1.53 - contrast, strong assumptions (as introduced by \isacommand{assume}) 1.54 - are solved immediately. 1.55 -*} 1.56 + Technically speaking, whenever some goal is solved by 1.57 + \isacommand{show} in the context of weak assumptions then the latter 1.58 + give rise to new subgoals, which may be established separately. In 1.59 + contrast, strong assumptions (as introduced by \isacommand{assume}) 1.60 + are solved immediately. *} 1.61 1.62 theorem "((A --> B) --> A) --> A" 1.63 proof 1.64 @@ -68,23 +65,21 @@ 1.65 qed 1.66 qed 1.67 1.68 -text {* 1.69 - Note that the goals stemming from weak assumptions may be even left 1.70 - until qed time, where they get eventually solved ``by assumption'' as 1.71 - well. In that case there is really no fundamental difference between 1.72 - the two kinds of assumptions, apart from the order of reducing the 1.73 - individual parts of the proof configuration. 1.74 +text {* Note that the goals stemming from weak assumptions may be even 1.75 + left until qed time, where they get eventually solved ``by 1.76 + assumption'' as well. In that case there is really no fundamental 1.77 + difference between the two kinds of assumptions, apart from the 1.78 + order of reducing the individual parts of the proof configuration. 1.79 1.80 - Nevertheless, the ``strong'' mode of plain assumptions is quite 1.81 - important in practice to achieve robustness of proof text 1.82 - interpretation. By forcing both the conclusion \emph{and} the 1.83 - assumptions to unify with the pending goal to be solved, goal 1.84 - selection becomes quite deterministic. For example, decomposition 1.85 - with rules of the ``case-analysis'' type usually gives rise to 1.86 - several goals that only differ in there local contexts. With strong 1.87 - assumptions these may be still solved in any order in a predictable 1.88 - way, while weak ones would quickly lead to great confusion, 1.89 - eventually demanding even some backtracking. 1.90 -*} 1.91 + Nevertheless, the ``strong'' mode of plain assumptions is quite 1.92 + important in practice to achieve robustness of proof text 1.93 + interpretation. By forcing both the conclusion \emph{and} the 1.94 + assumptions to unify with the pending goal to be solved, goal 1.95 + selection becomes quite deterministic. For example, decomposition 1.96 + with rules of the ``case-analysis'' type usually gives rise to 1.97 + several goals that only differ in there local contexts. With strong 1.98 + assumptions these may be still solved in any order in a predictable 1.99 + way, while weak ones would quickly lead to great confusion, 1.100 + eventually demanding even some backtracking. *} 1.101 1.102 end