Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Puzzle.thy Sprache: Isabelle

Original von: Isabelle^©

section \<open>An old chestnut\<close>

theory Puzzle
  imports Main
begin

text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias
  Nipkow.\<close>\<close>

text \<open>
  \<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that \<open>f (f n) < f (Suc n)\<close>
  for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.
\<close>

theorem
  assumes f_ax: "\n. f (f n) < f (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) < f n" by (simp only: Suc)
      with less have "f m \ f (f m)" .
      also from f_ax have "\ < f n" by (simp only: Suc)
      finally have "f m < f n" .
      with less have "m \ f m" .
      also note \<open>\<dots> < f n\<close>
      finally have "m < f 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 "\ < 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

  show "f n \ n"
  proof -
    have "\ n < f n"
    proof
      assume "n < f n"
      then have "Suc n \ f n" by simp
      then have "f (Suc n) \ f (f n)" by (rule mono)
      also have "\ < f (Suc n)" by (rule f_ax)
      finally have "\ < \" . then show False ..
    qed
    then show ?thesis by simp
  qed
qed

end

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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 ist noch experimentell.