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

src/HOL/Isar_examples/Peirce.thy

author | krauss |

Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) | |

changeset 21512 | 3786eb1b69d6 |

parent 16417 | 9bc16273c2d4 |

child 23373 | ead82c82da9e |

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

Lemma "fundef_default_value" uses predicate instead of set.

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

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Peirce's Law *}

8 theory Peirce imports Main begin

10 text {*

11 We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is

12 an inherently non-intuitionistic statement, so its proof will

13 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 there

19 is negation elimination; it holds in intuitionistic logic as well.}

20 *}

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

23 proof

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

25 show A

26 proof (rule classical)

27 assume "~ A"

28 have "A --> B"

29 proof

30 assume A

31 thus B by contradiction

32 qed

33 with aba show A ..

34 qed

35 qed

37 text {*

38 In the subsequent version the reasoning is rearranged by means of

39 ``weak assumptions'' (as introduced by \isacommand{presume}). Before

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

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

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

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

44 \emph{cut}.

46 Technically speaking, whenever some goal is solved by

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

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

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

50 are solved immediately.

51 *}

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

54 proof

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

56 show A

57 proof (rule classical)

58 presume "A --> B"

59 with aba show A ..

60 next

61 assume "~ A"

62 show "A --> B"

63 proof

64 assume A

65 thus B by contradiction

66 qed

67 qed

68 qed

70 text {*

71 Note that the goals stemming from weak assumptions may be even left

72 until qed time, where they get eventually solved ``by assumption'' as

73 well. In that case there is really no fundamental difference between

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

75 individual parts of the proof configuration.

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

78 important in practice to achieve robustness of proof text

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

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

81 selection becomes quite deterministic. For example, decomposition

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

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

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

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

86 eventually demanding even some backtracking.

87 *}

89 end