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

src/HOL/Isar_examples/Puzzle.thy

author | wenzelm |

Mon Sep 11 21:35:19 2006 +0200 (2006-09-11) | |

changeset 20503 | 503ac4c5ef91 |

parent 18204 | c3caf13f621d |

child 31758 | 3edd5f813f01 |

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

induct method: renamed 'fixing' to 'arbitrary';

2 header {* An old chestnut *}

4 theory Puzzle imports Main begin

6 text_raw {*

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

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

9 Tobias Nipkow.}

10 *}

12 text {*

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

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

15 Demonstrate that $f$ is the identity.

16 *}

18 theorem

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

20 shows "f n = n"

21 proof (rule order_antisym)

22 {

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

24 proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct)

25 case (less k n)

26 then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:)

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 hyp 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 hyp 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