author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 37671  fa53d267dab3 
child 58614  7338eb25226c 
permissions  rwrr 
10007  1 
header {* An old chestnut *} 
8020  2 

31758  3 
theory Puzzle 
4 
imports Main 

5 
begin 

8020  6 

37671  7 
text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''. 
8 
Original penandpaper proof due to Herbert Ehler; Isabelle tactic 

9 
script by Tobias Nipkow.} *} 

8020  10 

37671  11 
text {* \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ 
12 
such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. 

13 
Demonstrate that $f$ is the identity. *} 

8020  14 

18191  15 
theorem 
16 
assumes f_ax: "\<And>n. f (f n) < f (Suc n)" 

17 
shows "f n = n" 

10436  18 
proof (rule order_antisym) 
18191  19 
{ 
20 
fix n show "n \<le> f n" 

34915  21 
proof (induct "f n" arbitrary: n rule: less_induct) 
22 
case less 

18191  23 
show "n \<le> f n" 
10436  24 
proof (cases n) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

25 
case (Suc m) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

26 
from f_ax have "f (f m) < f n" by (simp only: Suc) 
34915  27 
with less have "f m \<le> f (f m)" . 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

28 
also from f_ax have "\<dots> < f n" by (simp only: Suc) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

29 
finally have "f m < f n" . 
34915  30 
with less have "m \<le> f m" . 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

31 
also note `\<dots> < f n` 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

32 
finally have "m < f n" . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

33 
then have "n \<le> f n" by (simp only: Suc) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

34 
then show ?thesis . 
10007  35 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

36 
case 0 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31758
diff
changeset

37 
then show ?thesis by simp 
10007  38 
qed 
39 
qed 

18191  40 
} note ge = this 
8020  41 

10436  42 
{ 
18191  43 
fix m n :: nat 
44 
assume "m \<le> n" 

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

10007  46 
proof (induct n) 
18191  47 
case 0 
48 
then have "m = 0" by simp 

49 
then show ?case by simp 

10436  50 
next 
18191  51 
case (Suc n) 
52 
from Suc.prems show "f m \<le> f (Suc n)" 

10436  53 
proof (rule le_SucE) 
18191  54 
assume "m \<le> n" 
55 
with Suc.hyps have "f m \<le> f n" . 

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

10436  57 
by (rule le_less_trans) 
58 
finally show ?thesis by simp 

59 
next 

60 
assume "m = Suc n" 

18191  61 
then show ?thesis by simp 
10007  62 
qed 
63 
qed 

10436  64 
} note mono = this 
8020  65 

18191  66 
show "f n \<le> n" 
10436  67 
proof  
18191  68 
have "\<not> n < f n" 
10007  69 
proof 
70 
assume "n < f n" 

18191  71 
then have "Suc n \<le> f n" by simp 
72 
then have "f (Suc n) \<le> f (f n)" by (rule mono) 

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

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

10007  75 
qed 
18191  76 
then show ?thesis by simp 
10007  77 
qed 
78 
qed 

8020  79 

10007  80 
end 