# HG changeset patch
# User haftmann
# Date 1380463282 -7200
# Node ID a269577d97c07e7d0ce421efe9760d930b178b53
# Parent  f6b7afa414f7a308da609fd688ecd5336a7f8c76
tuned proofs

diff -r f6b7afa414f7 -r a269577d97c0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Sep 29 14:07:47 2013 +0200
+++ b/src/HOL/Nat.thy	Sun Sep 29 16:01:22 2013 +0200
@@ -1564,38 +1564,44 @@
 begin
 
 lemma lift_Suc_mono_le:
-  assumes mono: "!!n. f n \<le> f(Suc n)" and "n\<le>n'"
+  assumes mono: "\<And>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'"} *}
+  then show ?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)" and "n < n'"
+  assumes mono: "\<And>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)
+by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
 
 lemma lift_Suc_mono_less_iff:
-  "(!!n. f n < f(Suc n)) \<Longrightarrow> f(n) < f(m) \<longleftrightarrow> n<m"
-by(blast intro: less_asym' lift_Suc_mono_less[of f]
-         dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq[THEN iffD1])
+  "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
+  by (blast intro: less_asym' lift_Suc_mono_less [of f]
+    dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
 
 end
 
-lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
+lemma mono_iff_le_Suc:
+  "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
   unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
 
 lemma mono_nat_linear_lb:
-  "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
-apply(induct_tac k)
- apply simp
-apply(erule_tac x="m+n" in meta_allE)
-apply(erule_tac x="Suc(m+n)" in meta_allE)
-apply simp
-done
+  fixes f :: "nat \<Rightarrow> nat"
+  assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
+  shows "f m + k \<le> f (m + k)"
+proof (induct k)
+  case 0 then show ?case by simp
+next
+  case (Suc k)
+  then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
+  also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))"
+    by (simp add: Suc_le_eq)
+  finally show ?case by simp
+qed
 
 
 text{*Subtraction laws, mostly by Clemens Ballarin*}
@@ -1840,11 +1846,11 @@
     case False then have "s < r" by (simp add: not_le)
     with * have "m * r + q - m * s = m * s - m * s" by simp
     then have "m * r + q - m * s = 0" by simp
-    with `m > 0` `s < r` have "m * r - m * s + q = 0" by simp
+    with `m > 0` `s < r` have "m * r - m * s + q = 0" by (unfold less_le_not_le) auto
     then have "m * (r - s) + q = 0" by auto
     then have "m * (r - s) = 0" by simp
     then have "m = 0 \<or> r - s = 0" by simp
-    with `s < r` have "m = 0" by arith
+    with `s < r` have "m = 0" by (simp add: less_le_not_le)
     with `m > 0` show thesis by auto
   next
     case True with * have "m * r + q - m * r = m * s - m * r" by simp