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

src/HOL/Isar_examples/Puzzle.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 16417 | 9bc16273c2d4 |

child 18191 | ef29685acef0 |

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

Constant "If" is now local

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.}

11 \medskip \textbf{Problem.} Given some function $f\colon \Nat \to

12 \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all

13 $n$. Demonstrate that $f$ is the identity.

14 *}

16 theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"

17 proof (rule order_antisym)

18 assume f_ax: "!!n. f (f n) < f (Suc n)"

20 txt {*

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

22 later for monotonicity as well.

23 *}

24 show ge: "!!n. n <= f n"

25 proof -

26 fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")

27 proof (induct k rule: less_induct)

28 fix k assume hyp: "!!m. m < k ==> PROP ?P m"

29 fix n assume k_def: "k == f n"

30 show "n <= k"

31 proof (cases n)

32 assume "n = 0" thus ?thesis by simp

33 next

34 fix m assume Suc: "n = Suc m"

35 from f_ax have "f (f m) < f (Suc m)" .

36 with hyp k_def Suc have "f m <= f (f m)" by simp

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

38 finally have less: "f m < f (Suc m)" .

39 with hyp k_def Suc have "m <= f m" by simp

40 also note less

41 finally have "m < f (Suc m)" .

42 hence "n <= f n" by (simp only: Suc)

43 thus ?thesis by (simp only: k_def)

44 qed

45 qed

46 qed

48 txt {*

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

50 monotonicity of $f$.

51 *}

52 {

53 fix m n

54 have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?P n")

55 proof (induct n)

56 assume "m <= 0" hence "m = 0" by simp

57 thus "f m <= f 0" by simp

58 next

59 fix n assume hyp: "PROP ?P n"

60 assume "m <= Suc n"

61 thus "f m <= f (Suc n)"

62 proof (rule le_SucE)

63 assume "m <= n"

64 with hyp have "f m <= f n" .

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

66 by (rule le_less_trans)

67 finally show ?thesis by simp

68 next

69 assume "m = Suc n"

70 thus ?thesis by simp

71 qed

72 qed

73 } note mono = this

75 show "f n <= n"

76 proof -

77 have "~ n < f n"

78 proof

79 assume "n < f n"

80 hence "Suc n <= f n" by simp

81 hence "f (Suc n) <= f (f n)" by (rule mono)

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

83 finally have "... < ..." . thus False ..

84 qed

85 thus ?thesis by simp

86 qed

87 qed

89 end