text_raw‹🪙‹A question from ``Bundeswettbewerb Mathematik''. Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias Nipkow.›\ text ‹ 🪙‹Problem.›Given some function ‹f: ℕ→ℕ› such that ‹f (f n) 🚫 (Suc n)› for all ‹n›. Demonstrate that ‹f› is the identity. › theorem assumes f_ax: "∧n. f (f n) 🚫 (Suc n)" shows "f n = n" proof (rule order_antisym) show ge: "n ≤ f n" for n proof (induct "f n" arbitrary: n rule: less_induct) case less show "n ≤ f n" proof (cases n) case (Suc m) from f_ax have "f (f m) 🚫 n" by (simp only: Suc) with less have "f m ≤ f (f m)" . also from f_ax have "…🚫 n" by (simp only: Suc) finally have "f m 🚫 n" . with less have "m ≤ f m" . also note ‹…🚫 n› finally have "m 🚫 n" . then have "n ≤ f n" by (simp only: Suc) then show ?thesis . next case 0 then show ?thesis by simp qed qed have mono: "m ≤ n ==> f m ≤ f n" for m n :: nat 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 ≤ f (Suc n)" proof (rule le_SucE) assume "m ≤ n" with Suc.hyps have "f m ≤ f n" . also from ge f_ax have "…🚫 (Suc n)" by (rule le_less_trans) finally show ?thesis by simp next assume "m = Suc n" then show ?thesis by simp qed qed show "f n ≤ n" proof - have "¬ n 🚫 n" proof assume "n 🚫 n" then have "Suc n ≤ f n" by simp then have "f (Suc n) ≤ f (f n)" by (rule mono) also have "…🚫 (Suc n)" by (rule f_ax) finally have "…🚫…" . then show False .. qed then show ?thesis by simp qed qed end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-04-27)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
