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;