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 nonintuitionistic 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 wellbalanced 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@55640

22 
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"

wenzelm@10007

23 
proof

wenzelm@55640

24 
assume "(A \<longrightarrow> B) \<longrightarrow> A"

wenzelm@10007

25 
show A

wenzelm@10007

26 
proof (rule classical)

wenzelm@55640

27 
assume "\<not> A"

wenzelm@55640

28 
have "A \<longrightarrow> B"

wenzelm@10007

29 
proof

wenzelm@10007

30 
assume A

wenzelm@55640

31 
with `\<not> A` show B by contradiction

wenzelm@10007

32 
qed

wenzelm@55640

33 
with `(A \<longrightarrow> B) \<longrightarrow> 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@55640

51 
theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"

wenzelm@10007

52 
proof

wenzelm@55640

53 
assume "(A \<longrightarrow> B) \<longrightarrow> A"

wenzelm@10007

54 
show A

wenzelm@10007

55 
proof (rule classical)

wenzelm@55640

56 
presume "A \<longrightarrow> B"

wenzelm@55640

57 
with `(A \<longrightarrow> B) \<longrightarrow> A` show A ..

wenzelm@10007

58 
next

wenzelm@55640

59 
assume "\<not> A"

wenzelm@55640

60 
show "A \<longrightarrow> B"

wenzelm@10007

61 
proof

wenzelm@10007

62 
assume A

wenzelm@55640

63 
with `\<not> 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 ``caseanalysis'' 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
