src/HOL/Nat.thy
 changeset 27627 93016de79b02 parent 27625 3a45b555001a child 27679 6392b92c3536
```     1.1 --- a/src/HOL/Nat.thy	Thu Jul 17 13:50:33 2008 +0200
1.2 +++ b/src/HOL/Nat.thy	Thu Jul 17 15:21:52 2008 +0200
1.3 @@ -1302,47 +1302,19 @@
1.4  begin
1.5
1.6  lemma lift_Suc_mono_le:
1.7 -  assumes mono: "!!n. f n \<le> f(Suc n)" shows "n\<le>n' \<Longrightarrow> f n \<le> f n'"
1.8 -proof(induct k == "n'-n" arbitrary:n')
1.9 -  case 0
1.10 -  moreover hence "n' <= n" by simp
1.11 -  ultimately have "n=n'" by(blast intro:order_antisym)
1.12 -  thus ?case by simp
1.13 -next
1.14 -  case (Suc k)
1.15 -  then obtain l where [simp]: "n' = Suc l"
1.16 -  proof(cases n')
1.17 -    case 0 thus ?thesis using Suc by simp
1.18 -  next
1.19 -    case Suc thus ?thesis using that by blast
1.20 -  qed
1.21 -  have "f n \<le> f l" using Suc by auto
1.22 -  also have "\<dots> \<le> f n'" using mono by auto
1.23 -  finally(order_trans) show ?case by auto
1.24 -qed
1.25 +  assumes mono: "!!n. f n \<le> f(Suc n)" and "n\<le>n'"
1.26 +  shows "f n \<le> f n'"
1.27 +proof (cases "n < n'")
1.28 +  case True
1.29 +  thus ?thesis
1.30 +    by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
1.31 +qed (insert `n \<le> n'`, auto) -- {*trivial for @{prop "n = n'"} *}
1.32
1.33  lemma lift_Suc_mono_less:
1.34 -  assumes mono: "!!n. f n < f(Suc n)" shows "n<n' \<Longrightarrow> f n < f n'"
1.35 -proof(induct k == "n' - Suc n" arbitrary:n')
1.36 -  case 0
1.37 -  hence "~ n' <= n \<longrightarrow> n' = Suc n" by(simp add:le_Suc_eq)
1.38 -  moreover have "~ n' <= n"
1.39 -  proof
1.40 -    assume "n' <= n" thus False using `n<n'` by(auto dest: le_less_trans)
1.41 -  qed
1.42 -  ultimately show ?case by(simp add:mono)
1.43 -next
1.44 -  case (Suc k)
1.45 -  then obtain l where [simp]: "n' = Suc l"
1.46 -  proof(cases n')
1.47 -    case 0 thus ?thesis using Suc by simp
1.48 -  next
1.49 -    case Suc thus ?thesis using that by blast
1.50 -  qed
1.51 -  have "f n < f l" using Suc by auto
1.52 -  also have "\<dots> < f n'" using mono by auto
1.53 -  finally(less_trans) show ?case by auto
1.54 -qed
1.55 +  assumes mono: "!!n. f n < f(Suc n)" and "n < n'"
1.56 +  shows "f n < f n'"
1.57 +using `n < n'`
1.58 +by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
1.59
1.60  end
1.61
```