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

16 
backward and forward reasoning. The actual classical reasoning step

wenzelm@7860

17 
is where the negated goal is introduced as additional assumption.

wenzelm@7860

18 
This eventually leads to a contradiction.\footnote{The rule involved

wenzelm@7860

19 
here is negation elimination; it holds in intuitionistic logic as

wenzelm@7860

20 
well.}

wenzelm@7860

21 
*};

wenzelm@7860

22 

wenzelm@6493

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

wenzelm@6444

24 
proof;

wenzelm@6892

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

wenzelm@6444

26 
show A;

wenzelm@6444

27 
proof (rule classical);

wenzelm@7448

28 
assume "~ A";

wenzelm@7448

29 
have "A > B";

wenzelm@6444

30 
proof;

wenzelm@7448

31 
assume A;

wenzelm@7448

32 
thus B; by contradiction;

wenzelm@6444

33 
qed;

wenzelm@7448

34 
with aba; show A; ..;

wenzelm@6444

35 
qed;

wenzelm@6444

36 
qed;

wenzelm@6444

37 

wenzelm@7860

38 
text {*

wenzelm@7860

39 
The subsequent version rearranges the reasoning by means of ``weak

wenzelm@7860

40 
assumptions'' (as introduced by \isacommand{presume}). Before

wenzelm@7860

41 
assuming the negated goal $\neg A$, its intended consequence $A \impl

wenzelm@7860

42 
B$ is put into place in order to solve the main problem.

wenzelm@7860

43 
Nevertheless, we do not get anything for free, but have to establish

wenzelm@7860

44 
$A \impl B$ later on. The overall effect is that of a \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@6892

61 
assume not_a: "~ A";

wenzelm@6444

62 
show "A > B";

wenzelm@6444

63 
proof;

wenzelm@7448

64 
assume A;

wenzelm@7448

65 
with not_a; show B; ..;

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

73 
well. In that case there is really no big difference between the two

wenzelm@7860

74 
kinds of assumptions, apart from the order of reducing the individual

wenzelm@7860

75 
parts of the proof configuration.

wenzelm@7860

76 

wenzelm@7860

77 
Nevertheless, the ``strong'' mode of plain assumptions is quite

wenzelm@7860

78 
important in practice to achieve robustness of proof document

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

82 
with ``caseanalysis'' type rules usually give rise to several goals

wenzelm@7869

83 
that only differ in there local contexts. With strong assumptions

wenzelm@7869

84 
these may be still solved in any order in a predictable way, while

wenzelm@7869

85 
weak ones would quickly lead to great confusion, eventually demanding

wenzelm@7869

86 
even some backtracking.

wenzelm@7860

87 
*};

wenzelm@7860

88 

wenzelm@6444

89 
end;
