generalized less_Suc_induct
authorkrauss
Thu Jun 18 19:54:21 2009 +0200 (2009-06-18)
changeset 31714347e9d18f372
parent 31713 e7922e3f3bdc
child 31716 32f07b47f9c5
generalized less_Suc_induct
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Thu Jun 18 19:10:22 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Jun 18 19:54:21 2009 +0200
     1.3 @@ -849,17 +849,20 @@
     1.4  lemma less_Suc_induct:
     1.5    assumes less:  "i < j"
     1.6       and  step:  "!!i. P i (Suc i)"
     1.7 -     and  trans: "!!i j k. P i j ==> P j k ==> P i k"
     1.8 +     and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
     1.9    shows "P i j"
    1.10  proof -
    1.11 -  from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add)
    1.12 +  from less obtain k where j: "j = Suc (i + k)" by (auto dest: less_imp_Suc_add)
    1.13    have "P i (Suc (i + k))"
    1.14    proof (induct k)
    1.15      case 0
    1.16      show ?case by (simp add: step)
    1.17    next
    1.18      case (Suc k)
    1.19 -    thus ?case by (auto intro: assms)
    1.20 +    have "0 + i < Suc k + i" by (rule add_less_mono1) simp
    1.21 +    hence "i < Suc (i + k)" by (simp add: add_commute)
    1.22 +    from trans[OF this lessI Suc step]
    1.23 +    show ?case by simp
    1.24    qed
    1.25    thus "P i j" by (simp add: j)
    1.26  qed