summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_Examples/Peirce.thy

author | wenzelm |

Sat, 07 Apr 2012 16:41:59 +0200 | |

changeset 47389 | e8552cba702d |

parent 37671 | fa53d267dab3 |

child 55640 | abc140f21caa |

permissions | -rw-r--r-- |

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(* Title: HOL/Isar_Examples/Peirce.thy Author: Markus Wenzel, TU Muenchen *) header {* Peirce's Law *} theory Peirce imports Main begin text {* We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is an inherently non-intuitionistic statement, so its proof will certainly involve some form of classical contradiction. The first proof is again a well-balanced combination of plain backward and forward reasoning. The actual classical step is where the negated goal may be introduced as additional assumption. This eventually leads to a contradiction.\footnote{The rule involved there is negation elimination; it holds in intuitionistic logic as well.} *} theorem "((A --> B) --> A) --> A" proof assume "(A --> B) --> A" show A proof (rule classical) assume "~ A" have "A --> B" proof assume A with `~ A` show B by contradiction qed with `(A --> B) --> A` show A .. qed qed text {* In the subsequent version the reasoning is rearranged by means of ``weak assumptions'' (as introduced by \isacommand{presume}). Before assuming the negated goal $\neg A$, its intended consequence $A \impl B$ is put into place in order to solve the main problem. Nevertheless, we do not get anything for free, but have to establish $A \impl B$ later on. The overall effect is that of a logical \emph{cut}. Technically speaking, whenever some goal is solved by \isacommand{show} in the context of weak assumptions then the latter give rise to new subgoals, which may be established separately. In contrast, strong assumptions (as introduced by \isacommand{assume}) are solved immediately. *} theorem "((A --> B) --> A) --> A" proof assume "(A --> B) --> A" show A proof (rule classical) presume "A --> B" with `(A --> B) --> A` show A .. next assume "~ A" show "A --> B" proof assume A with `~ A` show B by contradiction qed qed qed text {* Note that the goals stemming from weak assumptions may be even left until qed time, where they get eventually solved ``by assumption'' as well. In that case there is really no fundamental difference between the two kinds of assumptions, apart from the order of reducing the individual parts of the proof configuration. Nevertheless, the ``strong'' mode of plain assumptions is quite important in practice to achieve robustness of proof text interpretation. By forcing both the conclusion \emph{and} the assumptions to unify with the pending goal to be solved, goal selection becomes quite deterministic. For example, decomposition with rules of the ``case-analysis'' type usually gives rise to several goals that only differ in there local contexts. With strong assumptions these may be still solved in any order in a predictable way, while weak ones would quickly lead to great confusion, eventually demanding even some backtracking. *} end