# HG changeset patch
# User wenzelm
# Date 942847403 -3600
# Node ID 2823ce1753a5b93d2227e4fb31ffac417b8ec80f
# Parent  fead0dbf5b0a68c07a88c069a3c356e338359e1d
added Isar_examples/Puzzle.thy;

diff -r fead0dbf5b0a -r 2823ce1753a5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Nov 17 11:16:26 1999 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 17 15:03:23 1999 +0100
@@ -421,10 +421,10 @@
   Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \
   Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \
   Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
-  Isar_examples/Summation.thy Isar_examples/ROOT.ML \
-  Isar_examples/W_correct.thy Isar_examples/document/proof.sty \
-  Isar_examples/document/root.bib Isar_examples/document/root.tex \
-  Isar_examples/document/style.tex
+  Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
+  Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
+  Isar_examples/document/proof.sty Isar_examples/document/root.bib \
+  Isar_examples/document/root.tex Isar_examples/document/style.tex
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
 
 
diff -r fead0dbf5b0a -r 2823ce1753a5 src/HOL/Isar_examples/Puzzle.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Puzzle.thy	Wed Nov 17 15:03:23 1999 +0100
@@ -0,0 +1,128 @@
+
+header {* An old chestnut *};
+
+theory Puzzle = Main:;
+
+text_raw {*
+ \footnote{A question from ``Bundeswettbewerb Mathematik''.
+ Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
+ script by Tobias Nipkow.}
+*};
+
+
+subsection {* Generalized mathematical induction *};
+
+text {*
+ The following derived rule admits induction over some expression
+ $f(x)$ wrt.\ the ${<}$ relation on natural numbers.
+*};
+
+lemma gen_less_induct:
+  "(!!x. ALL y. f y < f x --> P y (f y) ==> P x (f x))
+    ==> P x (f x :: nat)"
+  (is "(!!x. ?H x ==> ?C x) ==> _");
+proof -;
+  assume asm: "!!x. ?H x ==> ?C x";
+  {{;
+    fix k;
+    have "ALL x. k = f x --> ?C x" (is "?Q k");
+    proof (rule less_induct);
+      fix k; assume hyp: "ALL m<k. ?Q m";
+      show "?Q k";
+      proof;
+	fix x; show "k = f x --> ?C x";
+	proof;
+	  assume "k = f x";
+	  with hyp; have "?H x"; by blast;
+	  thus "?C x"; by (rule asm);
+	qed;
+      qed;
+    qed;
+  }};
+  thus "?C x"; by simp;
+qed;
+
+
+subsection {* The problem *};
+
+text {*
+ Given some function $f\colon \Nat \to \Nat$ such that $f \ap (f \ap
+ n) < f \ap (\idt{Suc} \ap n)$ for all $n$.  Demonstrate that $f$ is
+ the identity.
+*};
+
+consts f :: "nat => nat";
+axioms f_ax: "f (f n) < f (Suc n)";
+
+theorem "f n = n";
+proof (rule order_antisym);
+  txt {*
+    Note that the generalized form of $n \le f \ap n$ is required
+    later for monotonicity as well.
+  *};
+  show ge: "!!n. n <= f n";
+  proof -;
+    fix n;
+    show "?thesis n" (is "?P n (f n)");
+    proof (rule gen_less_induct [of f ?P]);
+      fix n; assume hyp: "ALL m. f m < f n --> ?P m (f m)";
+      show "?P n (f n)";
+      proof (rule nat.exhaust);
+	assume "n = 0"; thus ?thesis; by simp;
+      next;
+	fix m; assume n_Suc: "n = Suc m";
+	from f_ax; have "f (f m) < f (Suc m)"; .;
+	with hyp n_Suc; have "f m <= f (f m)"; by blast;
+	also; from f_ax; have "... < f (Suc m)"; .;
+	finally; have lt: "f m < f (Suc m)"; .;
+	with hyp n_Suc; have "m <= f m"; by blast;
+	also; note lt;
+	finally; have "m < f (Suc m)"; .;
+	thus "n <= f n"; by (simp only: n_Suc);
+      qed;
+    qed;
+  qed;
+
+  txt {*
+    In order to show the other direction, we first establish
+    monotonicity of $f$.
+  *};
+  have mono: "!!m n. m <= n --> f m <= f n";
+  proof -;
+    fix m n;
+    show "?thesis m n" (is "?P n");
+    proof (induct n);
+      show "?P 0"; by simp;
+      fix n; assume hyp: "?P n";
+      show "?P (Suc n)";
+      proof;
+	assume "m <= Suc n";
+	thus "f m <= f (Suc n)";
+	proof (rule le_SucE);
+	  assume "m <= n";
+	  with hyp; 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";
+	  thus ?thesis; by simp;
+	qed;
+      qed;
+    qed;
+  qed;
+
+  show "f n <= n";
+  proof (rule leI);
+    show "~ n < f n";
+    proof;
+      assume "n < f n";
+      hence "Suc n <= f n"; by (rule Suc_leI);
+      hence "f (Suc n) <= f (f n)"; by (rule mono [rulify]);
+      also; have "... < f (Suc n)"; by (rule f_ax);
+      finally; have "... < ..."; .; thus False; ..;
+    qed;
+  qed;
+qed;
+
+end;
diff -r fead0dbf5b0a -r 2823ce1753a5 src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Wed Nov 17 11:16:26 1999 +0100
+++ b/src/HOL/Isar_examples/ROOT.ML	Wed Nov 17 15:03:23 1999 +0100
@@ -15,3 +15,4 @@
 time_use_thy "MutilatedCheckerboard";
 with_path "../Induct" time_use_thy "MultisetOrder";
 with_path "../W0" time_use_thy "W_correct";
+time_use_thy "Puzzle";
diff -r fead0dbf5b0a -r 2823ce1753a5 src/HOL/Isar_examples/document/style.tex
--- a/src/HOL/Isar_examples/document/style.tex	Wed Nov 17 11:16:26 1999 +0100
+++ b/src/HOL/Isar_examples/document/style.tex	Wed Nov 17 15:03:23 1999 +0100
@@ -24,6 +24,9 @@
 \newcommand{\disj}{\lor}
 \newcommand{\Impl}{\Longrightarrow}
 
+\newcommand{\Nat}{\mathord{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "root"