summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/Puzzle.thy

author | wenzelm |

Mon, 11 Sep 2006 21:35:19 +0200 | |

changeset 20503 | 503ac4c5ef91 |

parent 18204 | c3caf13f621d |

child 31758 | 3edd5f813f01 |

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

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

header {* An old chestnut *} theory Puzzle imports Main begin text_raw {* \footnote{A question from ``Bundeswettbewerb Mathematik''. Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias Nipkow.} *} text {* \textbf{Problem.} Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap n) < f \ap (\idt{Suc} \ap n)$ for all $n$. Demonstrate that $f$ is the identity. *} theorem assumes f_ax: "\<And>n. f (f n) < f (Suc n)" shows "f n = n" proof (rule order_antisym) { fix n show "n \<le> f n" proof (induct k \<equiv> "f n" arbitrary: n rule: less_induct) case (less k n) then have hyp: "\<And>m. f m < f n \<Longrightarrow> m \<le> f m" by (simp only:) show "n \<le> f n" proof (cases n) case (Suc m) from f_ax have "f (f m) < f n" by (simp only: Suc) with hyp have "f m \<le> f (f m)" . also from f_ax have "\<dots> < f n" by (simp only: Suc) finally have "f m < f n" . with hyp have "m \<le> f m" . also note `\<dots> < f n` finally have "m < f n" . then have "n \<le> f n" by (simp only: Suc) then show ?thesis . next case 0 then show ?thesis by simp qed qed } note ge = this { fix m n :: nat assume "m \<le> n" then have "f m \<le> f n" proof (induct n) case 0 then have "m = 0" by simp then show ?case by simp next case (Suc n) from Suc.prems show "f m \<le> f (Suc n)" proof (rule le_SucE) assume "m \<le> n" with Suc.hyps have "f m \<le> f n" . also from ge f_ax have "\<dots> < f (Suc n)" by (rule le_less_trans) finally show ?thesis by simp next assume "m = Suc n" then show ?thesis by simp qed qed } note mono = this show "f n \<le> n" proof - have "\<not> n < f n" proof assume "n < f n" then have "Suc n \<le> f n" by simp then have "f (Suc n) \<le> f (f n)" by (rule mono) also have "\<dots> < f (Suc n)" by (rule f_ax) finally have "\<dots> < \<dots>" . then show False .. qed then show ?thesis by simp qed qed end