summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Peirce.thy

author | wenzelm |

Tue Oct 07 20:59:46 2014 +0200 (2014-10-07) | |

changeset 58614 | 7338eb25226c |

parent 55640 | abc140f21caa |

child 58882 | 6e2010ab8bd9 |

permissions | -rw-r--r-- |

more cartouches;

more antiquotations;

more antiquotations;

1 (* Title: HOL/Isar_Examples/Peirce.thy

2 Author: Markus Wenzel, TU Muenchen

3 *)

5 header \<open>Peirce's Law\<close>

7 theory Peirce

8 imports Main

9 begin

11 text \<open>We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.

12 This is an inherently non-intuitionistic statement, so its proof

13 will certainly involve some form of classical contradiction.

15 The first proof is again a well-balanced combination of plain

16 backward and forward reasoning. The actual classical step is where

17 the negated goal may be introduced as additional assumption. This

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

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

20 well.}\<close>

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

23 proof

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

25 show A

26 proof (rule classical)

27 assume "\<not> A"

28 have "A \<longrightarrow> B"

29 proof

30 assume A

31 with \<open>\<not> A\<close> show B by contradiction

32 qed

33 with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..

34 qed

35 qed

37 text \<open>In the subsequent version the reasoning is rearranged by means

38 of ``weak assumptions'' (as introduced by \isacommand{presume}).

39 Before assuming the negated goal $\neg A$, its intended consequence

40 $A \impl B$ is put into place in order to solve the main problem.

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

42 $A \impl B$ later on. The overall effect is that of a logical

43 \emph{cut}.

45 Technically speaking, whenever some goal is solved by

46 \isacommand{show} in the context of weak assumptions then the latter

47 give rise to new subgoals, which may be established separately. In

48 contrast, strong assumptions (as introduced by \isacommand{assume})

49 are solved immediately.\<close>

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

52 proof

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

54 show A

55 proof (rule classical)

56 presume "A \<longrightarrow> B"

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

58 next

59 assume "\<not> A"

60 show "A \<longrightarrow> B"

61 proof

62 assume A

63 with \<open>\<not> A\<close> show B by contradiction

64 qed

65 qed

66 qed

68 text \<open>Note that the goals stemming from weak assumptions may be even

69 left until qed time, where they get eventually solved ``by

70 assumption'' as well. In that case there is really no fundamental

71 difference between the two kinds of assumptions, apart from the

72 order of reducing the individual parts of the proof configuration.

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

75 important in practice to achieve robustness of proof text

76 interpretation. By forcing both the conclusion \emph{and} the

77 assumptions to unify with the pending goal to be solved, goal

78 selection becomes quite deterministic. For example, decomposition

79 with rules of the ``case-analysis'' type usually gives rise to

80 several goals that only differ in there local contexts. With strong

81 assumptions these may be still solved in any order in a predictable

82 way, while weak ones would quickly lead to great confusion,

83 eventually demanding even some backtracking.\<close>

85 end