summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | krauss |

Thu, 18 Jun 2009 19:54:21 +0200 | |

changeset 31714 | 347e9d18f372 |

parent 31713 | e7922e3f3bdc |

child 31716 | 32f07b47f9c5 |

generalized less_Suc_induct

src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |

--- 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