equal
deleted
inserted
replaced
2 |
2 |
3 theory Puzzle |
3 theory Puzzle |
4 imports Main |
4 imports Main |
5 begin |
5 begin |
6 |
6 |
7 text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''. |
7 text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original |
8 Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic |
8 pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias |
9 script by Tobias Nipkow.}\<close> |
9 Nipkow.\<close>\<close> |
10 |
10 |
11 text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that |
11 text \<open> |
12 \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close> |
12 \<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that \<open>f (f n) < f (Suc n)\<close> |
|
13 for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity. |
|
14 \<close> |
13 |
15 |
14 theorem |
16 theorem |
15 assumes f_ax: "\<And>n. f (f n) < f (Suc n)" |
17 assumes f_ax: "\<And>n. f (f n) < f (Suc n)" |
16 shows "f n = n" |
18 shows "f n = n" |
17 proof (rule order_antisym) |
19 proof (rule order_antisym) |