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@7860

6 
header {* Peirce's Law *};

wenzelm@6444

7 

wenzelm@7748

8 
theory Peirce = Main:;

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@7860

20 
*};

wenzelm@7860

21 

wenzelm@6493

22 
theorem "((A > B) > A) > A";

wenzelm@6444

23 
proof;

wenzelm@6892

24 
assume aba: "(A > B) > A";

wenzelm@6444

25 
show A;

wenzelm@6444

26 
proof (rule classical);

wenzelm@7448

27 
assume "~ A";

wenzelm@7448

28 
have "A > B";

wenzelm@6444

29 
proof;

wenzelm@7448

30 
assume A;

wenzelm@7448

31 
thus B; by contradiction;

wenzelm@6444

32 
qed;

wenzelm@7448

33 
with aba; show A; ..;

wenzelm@6444

34 
qed;

wenzelm@6444

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@7860

51 
*};

wenzelm@7860

52 

wenzelm@6493

53 
theorem "((A > B) > A) > A";

wenzelm@6444

54 
proof;

wenzelm@6892

55 
assume aba: "(A > B) > A";

wenzelm@6444

56 
show A;

wenzelm@6444

57 
proof (rule classical);

wenzelm@7448

58 
presume "A > B";

wenzelm@7448

59 
with aba; show A; ..;

wenzelm@6854

60 
next;

wenzelm@7874

61 
assume "~ A";

wenzelm@6444

62 
show "A > B";

wenzelm@6444

63 
proof;

wenzelm@7448

64 
assume A;

wenzelm@7874

65 
thus B; by contradiction;

wenzelm@6444

66 
qed;

wenzelm@6444

67 
qed;

wenzelm@6444

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@7860

87 
*};

wenzelm@7860

88 

wenzelm@6444

89 
end;
