# HG changeset patch
# User krauss
# Date 1245347661 -7200
# Node ID 347e9d18f372641cecc5a2dba55e66e90f044c05
# Parent  e7922e3f3bdcfd130cc3cb42d83611a964f113e0
generalized less_Suc_induct

diff -r e7922e3f3bdc -r 347e9d18f372 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jun 18 19:10:22 2009 +0200
+++ b/src/HOL/Nat.thy	Thu Jun 18 19:54:21 2009 +0200
@@ -849,17 +849,20 @@
 lemma less_Suc_induct:
   assumes less:  "i < j"
      and  step:  "!!i. P i (Suc i)"
-     and  trans: "!!i j k. P i j ==> P j k ==> P i k"
+     and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
   shows "P i j"
 proof -
-  from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add)
+  from less obtain k where j: "j = Suc (i + k)" by (auto dest: less_imp_Suc_add)
   have "P i (Suc (i + k))"
   proof (induct k)
     case 0
     show ?case by (simp add: step)
   next
     case (Suc k)
-    thus ?case by (auto intro: assms)
+    have "0 + i < Suc k + i" by (rule add_less_mono1) simp
+    hence "i < Suc (i + k)" by (simp add: add_commute)
+    from trans[OF this lessI Suc step]
+    show ?case by simp
   qed
   thus "P i j" by (simp add: j)
 qed