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