# HG changeset patch
# User wenzelm
# Date 973879528 -3600
# Node ID 98c421dd597246c9ec6983f26b71858428fde50b
# Parent  b100e8d2c355893cfc757c1ff52cf9a79958facd
simplified induction;

diff -r b100e8d2c355 -r 98c421dd5972 src/HOL/Isar_examples/Puzzle.thy
--- a/src/HOL/Isar_examples/Puzzle.thy	Fri Nov 10 19:04:31 2000 +0100
+++ b/src/HOL/Isar_examples/Puzzle.thy	Fri Nov 10 19:05:28 2000 +0100
@@ -4,81 +4,44 @@
 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.}
-*}
-
+ \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.
+ \medskip \textbf{Problem.}  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.
 *}
 
-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 nat_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
+theorem "(!!n::nat. f (f n) < f (Suc n)) ==> f n = n"
+proof (rule order_antisym)
+  assume f_ax: "!!n. f (f n) < f (Suc n)"
 
-
-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
+    fix k show "!!n. k == f n ==> n <= k" (is "PROP ?P k")
+    proof (induct k
+        rule: nat_less_induct [rule_format])
+      fix k assume hyp: "!!m. m < k ==> PROP ?P m"
+      fix n assume k_def: "k == f n"
+      show "n <= k"
+      proof (cases n)
+        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)
+        fix m assume Suc: "n = Suc m"
+        from f_ax have "f (f m) < f (Suc m)" .
+        with hyp k_def Suc have "f m <= f (f m)" by simp
+        also from f_ax have "... < f (Suc m)" .
+        finally have less: "f m < f (Suc m)" .
+        with hyp k_def Suc have "m <= f m" by simp
+        also note less
+        finally have "m < f (Suc m)" .
+        hence "n <= f n" by (simp only: Suc)
+        thus ?thesis by (simp only: k_def)
       qed
     qed
   qed
@@ -87,41 +50,40 @@
     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")
+    have "m <= n \<Longrightarrow> f m <= f n" (is "PROP ?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
+      assume "m <= 0" hence "m = 0" by simp
+      thus "f m <= f 0" by simp
+    next
+      fix n assume hyp: "PROP ?P n"
+      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
+  } note mono = this
 
   show "f n <= n"
-  proof (rule leI)
-    show "~ n < f n"
+  proof -
+    have "~ 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 [rule_format])
+      hence "Suc n <= f n" by simp
+      hence "f (Suc n) <= f (f n)" by (rule mono)
       also have "... < f (Suc n)" by (rule f_ax)
       finally have "... < ..." . thus False ..
     qed
+    thus ?thesis by simp
   qed
 qed