src/HOL/Isar_examples/Puzzle.thy
changeset 8020 2823ce1753a5
child 8902 a705822f4e2a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 17 15:03:23 1999 +0100
     1.3 @@ -0,0 +1,128 @@
     1.4 +
     1.5 +header {* An old chestnut *};
     1.6 +
     1.7 +theory Puzzle = Main:;
     1.8 +
     1.9 +text_raw {*
    1.10 + \footnote{A question from ``Bundeswettbewerb Mathematik''.
    1.11 + Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
    1.12 + script by Tobias Nipkow.}
    1.13 +*};
    1.14 +
    1.15 +
    1.16 +subsection {* Generalized mathematical induction *};
    1.17 +
    1.18 +text {*
    1.19 + The following derived rule admits induction over some expression
    1.20 + $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
    1.21 +*};
    1.22 +
    1.23 +lemma gen_less_induct:
    1.24 +  "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
    1.25 +    ==> P x (f x :: nat)"
    1.26 +  (is "(!!x. ?H x ==> ?C x) ==> _");
    1.27 +proof -;
    1.28 +  assume asm: "!!x. ?H x ==> ?C x";
    1.29 +  {{;
    1.30 +    fix k;
    1.31 +    have "ALL x. k = f x --> ?C x" (is "?Q k");
    1.32 +    proof (rule less_induct);
    1.33 +      fix k; assume hyp: "ALL m<k. ?Q m";
    1.34 +      show "?Q k";
    1.35 +      proof;
    1.36 +	fix x; show "k = f x --> ?C x";
    1.37 +	proof;
    1.38 +	  assume "k = f x";
    1.39 +	  with hyp; have "?H x"; by blast;
    1.40 +	  thus "?C x"; by (rule asm);
    1.41 +	qed;
    1.42 +      qed;
    1.43 +    qed;
    1.44 +  }};
    1.45 +  thus "?C x"; by simp;
    1.46 +qed;
    1.47 +
    1.48 +
    1.49 +subsection {* The problem *};
    1.50 +
    1.51 +text {*
    1.52 + Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap
    1.53 + n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
    1.54 + the identity.
    1.55 +*};
    1.56 +
    1.57 +consts f :: "nat => nat";
    1.58 +axioms f_ax: "f (f n) < f (Suc n)";
    1.59 +
    1.60 +theorem "f n = n";
    1.61 +proof (rule order_antisym);
    1.62 +  txt {*
    1.63 +    Note that the generalized form of $n \le f \ap n$ is required
    1.64 +    later for monotonicity as well.
    1.65 +  *};
    1.66 +  show ge: "!!n. n <= f n";
    1.67 +  proof -;
    1.68 +    fix n;
    1.69 +    show "?thesis n" (is "?P n (f n)");
    1.70 +    proof (rule gen_less_induct [of f ?P]);
    1.71 +      fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";
    1.72 +      show "?P n (f n)";
    1.73 +      proof (rule nat.exhaust);
    1.74 +	assume "n = 0"; thus ?thesis; by simp;
    1.75 +      next;
    1.76 +	fix m; assume n_Suc: "n = Suc m";
    1.77 +	from f_ax; have "f (f m) < f (Suc m)"; .;
    1.78 +	with hyp n_Suc; have "f m <= f (f m)"; by blast;
    1.79 +	also; from f_ax; have "... < f (Suc m)"; .;
    1.80 +	finally; have lt: "f m < f (Suc m)"; .;
    1.81 +	with hyp n_Suc; have "m <= f m"; by blast;
    1.82 +	also; note lt;
    1.83 +	finally; have "m < f (Suc m)"; .;
    1.84 +	thus "n <= f n"; by (simp only: n_Suc);
    1.85 +      qed;
    1.86 +    qed;
    1.87 +  qed;
    1.88 +
    1.89 +  txt {*
    1.90 +    In order to show the other direction, we first establish
    1.91 +    monotonicity of $f$.
    1.92 +  *};
    1.93 +  have mono: "!!m n. m <= n --> f m <= f n";
    1.94 +  proof -;
    1.95 +    fix m n;
    1.96 +    show "?thesis m n" (is "?P n");
    1.97 +    proof (induct n);
    1.98 +      show "?P 0"; by simp;
    1.99 +      fix n; assume hyp: "?P n";
   1.100 +      show "?P (Suc n)";
   1.101 +      proof;
   1.102 +	assume "m <= Suc n";
   1.103 +	thus "f m <= f (Suc n)";
   1.104 +	proof (rule le_SucE);
   1.105 +	  assume "m <= n";
   1.106 +	  with hyp; have "f m <= f n"; ..;
   1.107 +	  also; from ge f_ax; have "... < f (Suc n)";
   1.108 +	    by (rule le_less_trans);
   1.109 +	  finally; show ?thesis; by simp;
   1.110 +	next;
   1.111 +	  assume "m = Suc n";
   1.112 +	  thus ?thesis; by simp;
   1.113 +	qed;
   1.114 +      qed;
   1.115 +    qed;
   1.116 +  qed;
   1.117 +
   1.118 +  show "f n <= n";
   1.119 +  proof (rule leI);
   1.120 +    show "~ n < f n";
   1.121 +    proof;
   1.122 +      assume "n < f n";
   1.123 +      hence "Suc n <= f n"; by (rule Suc_leI);
   1.124 +      hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
   1.125 +      also; have "... < f (Suc n)"; by (rule f_ax);
   1.126 +      finally; have "... < ..."; .; thus False; ..;
   1.127 +    qed;
   1.128 +  qed;
   1.129 +qed;
   1.130 +
   1.131 +end;