# HG changeset patch
# User krauss
# Date 1216300912 -7200
# Node ID 93016de79b02fbe1fc8a0fed0248bbdd19d989de
# Parent  1a3507f86b394badf60ae78c5a4074fa0a50129b
simplified proofs

diff -r 1a3507f86b39 -r 93016de79b02 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jul 17 13:50:33 2008 +0200
+++ b/src/HOL/Nat.thy	Thu Jul 17 15:21:52 2008 +0200
@@ -1302,47 +1302,19 @@
 begin
 
 lemma lift_Suc_mono_le:
-  assumes mono: "!!n. f n \<le> f(Suc n)" shows "n\<le>n' \<Longrightarrow> f n \<le> f n'"
-proof(induct k == "n'-n" arbitrary:n')
-  case 0
-  moreover hence "n' <= n" by simp
-  ultimately have "n=n'" by(blast intro:order_antisym)
-  thus ?case by simp
-next
-  case (Suc k)
-  then obtain l where [simp]: "n' = Suc l"
-  proof(cases n')
-    case 0 thus ?thesis using Suc by simp
-  next
-    case Suc thus ?thesis using that by blast
-  qed
-  have "f n \<le> f l" using Suc by auto
-  also have "\<dots> \<le> f n'" using mono by auto
-  finally(order_trans) show ?case by auto
-qed
+  assumes mono: "!!n. f n \<le> f(Suc n)" and "n\<le>n'"
+  shows "f n \<le> f n'"
+proof (cases "n < n'")
+  case True
+  thus ?thesis
+    by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
+qed (insert `n \<le> n'`, auto) -- {*trivial for @{prop "n = n'"} *}
 
 lemma lift_Suc_mono_less:
-  assumes mono: "!!n. f n < f(Suc n)" shows "n<n' \<Longrightarrow> f n < f n'"
-proof(induct k == "n' - Suc n" arbitrary:n')
-  case 0
-  hence "~ n' <= n \<longrightarrow> n' = Suc n" by(simp add:le_Suc_eq)
-  moreover have "~ n' <= n"
-  proof
-    assume "n' <= n" thus False using `n<n'` by(auto dest: le_less_trans)
-  qed
-  ultimately show ?case by(simp add:mono)
-next
-  case (Suc k)
-  then obtain l where [simp]: "n' = Suc l"
-  proof(cases n')
-    case 0 thus ?thesis using Suc by simp
-  next
-    case Suc thus ?thesis using that by blast
-  qed
-  have "f n < f l" using Suc by auto
-  also have "\<dots> < f n'" using mono by auto
-  finally(less_trans) show ?case by auto
-qed
+  assumes mono: "!!n. f n < f(Suc n)" and "n < n'"
+  shows "f n < f n'"
+using `n < n'`
+by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
 
 end