src/HOL/Isar_Examples/Puzzle.thy
 author wenzelm Tue Sep 26 20:54:40 2017 +0200 (23 months ago) changeset 66695 91500c024c7f parent 63583 a39baba12732 permissions -rw-r--r--
tuned;
 wenzelm@58882 ` 1` ```section \An old chestnut\ ``` wenzelm@8020 ` 2` wenzelm@31758 ` 3` ```theory Puzzle ``` wenzelm@63583 ` 4` ``` imports Main ``` wenzelm@31758 ` 5` ```begin ``` wenzelm@8020 ` 6` wenzelm@61932 ` 7` ```text_raw \\<^footnote>\A question from ``Bundeswettbewerb Mathematik''. Original ``` wenzelm@61932 ` 8` ``` pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias ``` wenzelm@61932 ` 9` ``` Nipkow.\\ ``` wenzelm@8020 ` 10` wenzelm@61932 ` 11` ```text \ ``` wenzelm@61932 ` 12` ``` \<^bold>\Problem.\ Given some function \f: \ \ \\ such that \f (f n) < f (Suc n)\ ``` wenzelm@61932 ` 13` ``` for all \n\. Demonstrate that \f\ is the identity. ``` wenzelm@61932 ` 14` ```\ ``` wenzelm@8020 ` 15` wenzelm@18191 ` 16` ```theorem ``` wenzelm@18191 ` 17` ``` assumes f_ax: "\n. f (f n) < f (Suc n)" ``` wenzelm@18191 ` 18` ``` shows "f n = n" ``` wenzelm@10436 ` 19` ```proof (rule order_antisym) ``` wenzelm@60410 ` 20` ``` show ge: "n \ f n" for n ``` wenzelm@60410 ` 21` ``` proof (induct "f n" arbitrary: n rule: less_induct) ``` wenzelm@60410 ` 22` ``` case less ``` wenzelm@60410 ` 23` ``` show "n \ f n" ``` wenzelm@60410 ` 24` ``` proof (cases n) ``` wenzelm@60410 ` 25` ``` case (Suc m) ``` wenzelm@60410 ` 26` ``` from f_ax have "f (f m) < f n" by (simp only: Suc) ``` wenzelm@60410 ` 27` ``` with less have "f m \ f (f m)" . ``` wenzelm@60410 ` 28` ``` also from f_ax have "\ < f n" by (simp only: Suc) ``` wenzelm@60410 ` 29` ``` finally have "f m < f n" . ``` wenzelm@60410 ` 30` ``` with less have "m \ f m" . ``` wenzelm@60410 ` 31` ``` also note \\ < f n\ ``` wenzelm@60410 ` 32` ``` finally have "m < f n" . ``` wenzelm@60410 ` 33` ``` then have "n \ f n" by (simp only: Suc) ``` wenzelm@60410 ` 34` ``` then show ?thesis . ``` wenzelm@60410 ` 35` ``` next ``` wenzelm@60410 ` 36` ``` case 0 ``` wenzelm@60410 ` 37` ``` then show ?thesis by simp ``` wenzelm@10007 ` 38` ``` qed ``` wenzelm@60410 ` 39` ``` qed ``` wenzelm@8020 ` 40` wenzelm@60410 ` 41` ``` have mono: "m \ n \ f m \ f n" for m n :: nat ``` wenzelm@60410 ` 42` ``` proof (induct n) ``` wenzelm@60410 ` 43` ``` case 0 ``` wenzelm@60410 ` 44` ``` then have "m = 0" by simp ``` wenzelm@60410 ` 45` ``` then show ?case by simp ``` wenzelm@60410 ` 46` ``` next ``` wenzelm@60410 ` 47` ``` case (Suc n) ``` wenzelm@60410 ` 48` ``` from Suc.prems show "f m \ f (Suc n)" ``` wenzelm@60410 ` 49` ``` proof (rule le_SucE) ``` wenzelm@60410 ` 50` ``` assume "m \ n" ``` wenzelm@60410 ` 51` ``` with Suc.hyps have "f m \ f n" . ``` wenzelm@60410 ` 52` ``` also from ge f_ax have "\ < f (Suc n)" ``` wenzelm@60410 ` 53` ``` by (rule le_less_trans) ``` wenzelm@60410 ` 54` ``` finally show ?thesis by simp ``` wenzelm@10436 ` 55` ``` next ``` wenzelm@60410 ` 56` ``` assume "m = Suc n" ``` wenzelm@60410 ` 57` ``` then show ?thesis by simp ``` wenzelm@10007 ` 58` ``` qed ``` wenzelm@60410 ` 59` ``` qed ``` wenzelm@8020 ` 60` wenzelm@18191 ` 61` ``` show "f n \ n" ``` wenzelm@10436 ` 62` ``` proof - ``` wenzelm@18191 ` 63` ``` have "\ n < f n" ``` wenzelm@10007 ` 64` ``` proof ``` wenzelm@10007 ` 65` ``` assume "n < f n" ``` wenzelm@18191 ` 66` ``` then have "Suc n \ f n" by simp ``` wenzelm@18191 ` 67` ``` then have "f (Suc n) \ f (f n)" by (rule mono) ``` wenzelm@18191 ` 68` ``` also have "\ < f (Suc n)" by (rule f_ax) ``` wenzelm@18191 ` 69` ``` finally have "\ < \" . then show False .. ``` wenzelm@10007 ` 70` ``` qed ``` wenzelm@18191 ` 71` ``` then show ?thesis by simp ``` wenzelm@10007 ` 72` ``` qed ``` wenzelm@10007 ` 73` ```qed ``` wenzelm@8020 ` 74` wenzelm@10007 ` 75` ```end ```