src/HOL/Isar_examples/Puzzle.thy
author wenzelm
Sun Sep 17 22:19:02 2000 +0200 (2000-09-17)
changeset 10007 64bf7da1994a
parent 9941 fe05af7ec816
child 10436 98c421dd5972
permissions -rw-r--r--
isar-strip-terminators;
     1 
     2 header {* An old chestnut *}
     3 
     4 theory Puzzle = Main:
     5 
     6 text_raw {*
     7  \footnote{A question from ``Bundeswettbewerb Mathematik''.
     8  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
     9  script by Tobias Nipkow.}
    10 *}
    11 
    12 
    13 subsection {* Generalized mathematical induction *}
    14 
    15 text {*
    16  The following derived rule admits induction over some expression
    17  $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
    18 *}
    19 
    20 lemma gen_less_induct:
    21   "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
    22     ==> P x (f x :: nat)"
    23   (is "(!!x. ?H x ==> ?C x) ==> _")
    24 proof -
    25   assume asm: "!!x. ?H x ==> ?C x"
    26   {
    27     fix k
    28     have "ALL x. k = f x --> ?C x" (is "?Q k")
    29     proof (rule nat_less_induct)
    30       fix k assume hyp: "ALL m<k. ?Q m"
    31       show "?Q k"
    32       proof
    33 	fix x show "k = f x --> ?C x"
    34 	proof
    35 	  assume "k = f x"
    36 	  with hyp have "?H x" by blast
    37 	  thus "?C x" by (rule asm)
    38 	qed
    39       qed
    40     qed
    41   }
    42   thus "?C x" by simp
    43 qed
    44 
    45 
    46 subsection {* The problem *}
    47 
    48 text {*
    49  Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap
    50  n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
    51  the identity.
    52 *}
    53 
    54 consts f :: "nat => nat"
    55 axioms f_ax: "f (f n) < f (Suc n)"
    56 
    57 theorem "f n = n"
    58 proof (rule order_antisym)
    59   txt {*
    60     Note that the generalized form of $n \le f \ap n$ is required
    61     later for monotonicity as well.
    62   *}
    63   show ge: "!!n. n <= f n"
    64   proof -
    65     fix n
    66     show "?thesis n" (is "?P n (f n)")
    67     proof (rule gen_less_induct [of f ?P])
    68       fix n assume hyp: "ALL m. f m < f n --> ?P m (f m)"
    69       show "?P n (f n)"
    70       proof (rule nat.exhaust)
    71 	assume "n = 0" thus ?thesis by simp
    72       next
    73 	fix m assume n_Suc: "n = Suc m"
    74 	from f_ax have "f (f m) < f (Suc m)" .
    75 	with hyp n_Suc have "f m <= f (f m)" by blast
    76 	also from f_ax have "... < f (Suc m)" .
    77 	finally have lt: "f m < f (Suc m)" .
    78 	with hyp n_Suc have "m <= f m" by blast
    79 	also note lt
    80 	finally have "m < f (Suc m)" .
    81 	thus "n <= f n" by (simp only: n_Suc)
    82       qed
    83     qed
    84   qed
    85 
    86   txt {*
    87     In order to show the other direction, we first establish
    88     monotonicity of $f$.
    89   *}
    90   have mono: "!!m n. m <= n --> f m <= f n"
    91   proof -
    92     fix m n
    93     show "?thesis m n" (is "?P n")
    94     proof (induct n)
    95       show "?P 0" by simp
    96       fix n assume hyp: "?P n"
    97       show "?P (Suc n)"
    98       proof
    99 	assume "m <= Suc n"
   100 	thus "f m <= f (Suc n)"
   101 	proof (rule le_SucE)
   102 	  assume "m <= n"
   103 	  with hyp have "f m <= f n" ..
   104 	  also from ge f_ax have "... < f (Suc n)"
   105 	    by (rule le_less_trans)
   106 	  finally show ?thesis by simp
   107 	next
   108 	  assume "m = Suc n"
   109 	  thus ?thesis by simp
   110 	qed
   111       qed
   112     qed
   113   qed
   114 
   115   show "f n <= n"
   116   proof (rule leI)
   117     show "~ n < f n"
   118     proof
   119       assume "n < f n"
   120       hence "Suc n <= f n" by (rule Suc_leI)
   121       hence "f (Suc n) <= f (f n)" by (rule mono [rule_format])
   122       also have "... < f (Suc n)" by (rule f_ax)
   123       finally have "... < ..." . thus False ..
   124     qed
   125   qed
   126 qed
   127 
   128 end