--- a/src/HOL/Isar_Examples/Peirce.thy Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Isar_Examples/Peirce.thy
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
*)
section \<open>Peirce's Law\<close>
@@ -8,15 +8,16 @@
imports Main
begin
-text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
- non-intuitionistic statement, so its proof will certainly involve some
- form of classical contradiction.
+text \<open>
+ We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. 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.}\<close>
+ contradiction.\<^footnote>\<open>The rule involved there is negation elimination; it holds in
+ intuitionistic logic as well.\<close>\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -33,17 +34,19 @@
qed
qed
-text \<open>In the subsequent version the reasoning is rearranged by means of
- ``weak assumptions'' (as introduced by \isacommand{presume}). Before
- assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put
- into place in order to solve the main problem. Nevertheless, we do not get
- anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall
- effect is that of a logical \<^emph>\<open>cut\<close>.
+text \<open>
+ In the subsequent version the reasoning is rearranged by means of ``weak
+ assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated
+ goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to
+ solve the main problem. Nevertheless, we do not get anything for free, but
+ have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical
+ \<^emph>\<open>cut\<close>.
- 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.\<close>
+ Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> 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
+ \<^theory_text>\<open>assume\<close>) are solved immediately.
+\<close>
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
@@ -62,20 +65,22 @@
qed
qed
-text \<open>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.
+text \<open>
+ 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>\<open>and\<close> 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
+ 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>\<open>and\<close> 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.\<close>
+ while weak ones would quickly lead to great confusion, eventually demanding
+ even some backtracking.
+\<close>
end