| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/Isar_Examples/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 2 kB |
|
Quelle Puzzle.thySprache: Isabelle |
|||||||||||||||
|
section ‹An old chestnut› theory Puzzle imports Main begin 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
¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26