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

src/HOL/Isar_examples/Puzzle.thy

author | wenzelm |

Wed Nov 17 15:03:23 1999 +0100 (1999-11-17) | |

changeset 8020 | 2823ce1753a5 |

child 8902 | a705822f4e2a |

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

added Isar_examples/Puzzle.thy;

2 header {* An old chestnut *};

4 theory Puzzle = Main:;

6 text_raw {*

7 \footnote{A question from ``Bundeswettbewerb Mathematik''.

8 Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic

9 script by Tobias Nipkow.}

10 *};

13 subsection {* Generalized mathematical induction *};

15 text {*

16 The following derived rule admits induction over some expression

17 $f(x)$ wrt.\ the ${<}$ relation on natural numbers.

18 *};

20 lemma gen_less_induct:

21 "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))

22 ==> P x (f x :: nat)"

23 (is "(!!x. ?H x ==> ?C x) ==> _");

24 proof -;

25 assume asm: "!!x. ?H x ==> ?C x";

26 {{;

27 fix k;

28 have "ALL x. k = f x --> ?C x" (is "?Q k");

29 proof (rule less_induct);

30 fix k; assume hyp: "ALL m<k. ?Q m";

31 show "?Q k";

32 proof;

33 fix x; show "k = f x --> ?C x";

34 proof;

35 assume "k = f x";

36 with hyp; have "?H x"; by blast;

37 thus "?C x"; by (rule asm);

38 qed;

39 qed;

40 qed;

41 }};

42 thus "?C x"; by simp;

43 qed;

46 subsection {* The problem *};

48 text {*

49 Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap

50 n) < f \ap (\idt{Suc} \ap n)$ for all $n$. Demonstrate that $f$ is

51 the identity.

52 *};

54 consts f :: "nat => nat";

55 axioms f_ax: "f (f n) < f (Suc n)";

57 theorem "f n = n";

58 proof (rule order_antisym);

59 txt {*

60 Note that the generalized form of $n \le f \ap n$ is required

61 later for monotonicity as well.

62 *};

63 show ge: "!!n. n <= f n";

64 proof -;

65 fix n;

66 show "?thesis n" (is "?P n (f n)");

67 proof (rule gen_less_induct [of f ?P]);

68 fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";

69 show "?P n (f n)";

70 proof (rule nat.exhaust);

71 assume "n = 0"; thus ?thesis; by simp;

72 next;

73 fix m; assume n_Suc: "n = Suc m";

74 from f_ax; have "f (f m) < f (Suc m)"; .;

75 with hyp n_Suc; have "f m <= f (f m)"; by blast;

76 also; from f_ax; have "... < f (Suc m)"; .;

77 finally; have lt: "f m < f (Suc m)"; .;

78 with hyp n_Suc; have "m <= f m"; by blast;

79 also; note lt;

80 finally; have "m < f (Suc m)"; .;

81 thus "n <= f n"; by (simp only: n_Suc);

82 qed;

83 qed;

84 qed;

86 txt {*

87 In order to show the other direction, we first establish

88 monotonicity of $f$.

89 *};

90 have mono: "!!m n. m <= n --> f m <= f n";

91 proof -;

92 fix m n;

93 show "?thesis m n" (is "?P n");

94 proof (induct n);

95 show "?P 0"; by simp;

96 fix n; assume hyp: "?P n";

97 show "?P (Suc n)";

98 proof;

99 assume "m <= Suc n";

100 thus "f m <= f (Suc n)";

101 proof (rule le_SucE);

102 assume "m <= n";

103 with hyp; have "f m <= f n"; ..;

104 also; from ge f_ax; have "... < f (Suc n)";

105 by (rule le_less_trans);

106 finally; show ?thesis; by simp;

107 next;

108 assume "m = Suc n";

109 thus ?thesis; by simp;

110 qed;

111 qed;

112 qed;

113 qed;

115 show "f n <= n";

116 proof (rule leI);

117 show "~ n < f n";

118 proof;

119 assume "n < f n";

120 hence "Suc n <= f n"; by (rule Suc_leI);

121 hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);

122 also; have "... < f (Suc n)"; by (rule f_ax);

123 finally; have "... < ..."; .; thus False; ..;

124 qed;

125 qed;

126 qed;

128 end;