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

src/HOL/Isar_Examples/Puzzle.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 34915 | 7894c7dab132 |

child 37671 | fa53d267dab3 |

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

more speaking names

1 header {* An old chestnut *}

3 theory Puzzle

4 imports Main

5 begin

7 text_raw {*

8 \footnote{A question from ``Bundeswettbewerb Mathematik''. Original

9 pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by

10 Tobias Nipkow.}

11 *}

13 text {*

14 \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such

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

16 Demonstrate that $f$ is the identity.

17 *}

19 theorem

20 assumes f_ax: "\<And>n. f (f n) < f (Suc n)"

21 shows "f n = n"

22 proof (rule order_antisym)

23 {

24 fix n show "n \<le> f n"

25 proof (induct "f n" arbitrary: n rule: less_induct)

26 case less

27 show "n \<le> f n"

28 proof (cases n)

29 case (Suc m)

30 from f_ax have "f (f m) < f n" by (simp only: Suc)

31 with less have "f m \<le> f (f m)" .

32 also from f_ax have "\<dots> < f n" by (simp only: Suc)

33 finally have "f m < f n" .

34 with less have "m \<le> f m" .

35 also note `\<dots> < f n`

36 finally have "m < f n" .

37 then have "n \<le> f n" by (simp only: Suc)

38 then show ?thesis .

39 next

40 case 0

41 then show ?thesis by simp

42 qed

43 qed

44 } note ge = this

46 {

47 fix m n :: nat

48 assume "m \<le> n"

49 then have "f m \<le> f n"

50 proof (induct n)

51 case 0

52 then have "m = 0" by simp

53 then show ?case by simp

54 next

55 case (Suc n)

56 from Suc.prems show "f m \<le> f (Suc n)"

57 proof (rule le_SucE)

58 assume "m \<le> n"

59 with Suc.hyps have "f m \<le> f n" .

60 also from ge f_ax have "\<dots> < f (Suc n)"

61 by (rule le_less_trans)

62 finally show ?thesis by simp

63 next

64 assume "m = Suc n"

65 then show ?thesis by simp

66 qed

67 qed

68 } note mono = this

70 show "f n \<le> n"

71 proof -

72 have "\<not> n < f n"

73 proof

74 assume "n < f n"

75 then have "Suc n \<le> f n" by simp

76 then have "f (Suc n) \<le> f (f n)" by (rule mono)

77 also have "\<dots> < f (Suc n)" by (rule f_ax)

78 finally have "\<dots> < \<dots>" . then show False ..

79 qed

80 then show ?thesis by simp

81 qed

82 qed

84 end