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 

haftmann@16417

8 
theory Peirce imports Main begin

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 nonintuitionistic 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 wellbalanced 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 ``caseanalysis'' 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
