author haftmann Sun Sep 29 16:01:22 2013 +0200 (2013-09-29) changeset 53986 a269577d97c0 parent 53985 f6b7afa414f7 child 53987 16a0cd5293d9
tuned proofs
 src/HOL/Nat.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/Nat.thy	Sun Sep 29 14:07:47 2013 +0200
1.2 +++ b/src/HOL/Nat.thy	Sun Sep 29 16:01:22 2013 +0200
1.3 @@ -1564,38 +1564,44 @@
1.4  begin
1.6  lemma lift_Suc_mono_le:
1.7 -  assumes mono: "!!n. f n \<le> f(Suc n)" and "n\<le>n'"
1.8 +  assumes mono: "\<And>n. f n \<le> f (Suc n)" and "n \<le> n'"
1.9    shows "f n \<le> f n'"
1.10  proof (cases "n < n'")
1.11    case True
1.12 -  thus ?thesis
1.13 -    by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
1.14 -qed (insert `n \<le> n'`, auto) -- {*trivial for @{prop "n = n'"} *}
1.15 +  then show ?thesis
1.16 +    by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
1.17 +qed (insert `n \<le> n'`, auto) -- {* trivial for @{prop "n = n'"} *}
1.19  lemma lift_Suc_mono_less:
1.20 -  assumes mono: "!!n. f n < f(Suc n)" and "n < n'"
1.21 +  assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
1.22    shows "f n < f n'"
1.23  using `n < n'`
1.24 -by (induct n n' rule: less_Suc_induct[consumes 1]) (auto intro: mono)
1.25 +by (induct n n' rule: less_Suc_induct [consumes 1]) (auto intro: mono)
1.27  lemma lift_Suc_mono_less_iff:
1.28 -  "(!!n. f n < f(Suc n)) \<Longrightarrow> f(n) < f(m) \<longleftrightarrow> n<m"
1.29 -by(blast intro: less_asym' lift_Suc_mono_less[of f]
1.30 -         dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq[THEN iffD1])
1.31 +  "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
1.32 +  by (blast intro: less_asym' lift_Suc_mono_less [of f]
1.33 +    dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
1.35  end
1.37 -lemma mono_iff_le_Suc: "mono f = (\<forall>n. f n \<le> f (Suc n))"
1.38 +lemma mono_iff_le_Suc:
1.39 +  "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
1.40    unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
1.42  lemma mono_nat_linear_lb:
1.43 -  "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
1.44 -apply(induct_tac k)
1.45 - apply simp
1.46 -apply(erule_tac x="m+n" in meta_allE)
1.47 -apply(erule_tac x="Suc(m+n)" in meta_allE)
1.48 -apply simp
1.49 -done
1.50 +  fixes f :: "nat \<Rightarrow> nat"
1.51 +  assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
1.52 +  shows "f m + k \<le> f (m + k)"
1.53 +proof (induct k)
1.54 +  case 0 then show ?case by simp
1.55 +next
1.56 +  case (Suc k)
1.57 +  then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
1.58 +  also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))"
1.59 +    by (simp add: Suc_le_eq)
1.60 +  finally show ?case by simp
1.61 +qed
1.64  text{*Subtraction laws, mostly by Clemens Ballarin*}
1.65 @@ -1840,11 +1846,11 @@
1.66      case False then have "s < r" by (simp add: not_le)
1.67      with * have "m * r + q - m * s = m * s - m * s" by simp
1.68      then have "m * r + q - m * s = 0" by simp
1.69 -    with `m > 0` `s < r` have "m * r - m * s + q = 0" by simp
1.70 +    with `m > 0` `s < r` have "m * r - m * s + q = 0" by (unfold less_le_not_le) auto
1.71      then have "m * (r - s) + q = 0" by auto
1.72      then have "m * (r - s) = 0" by simp
1.73      then have "m = 0 \<or> r - s = 0" by simp
1.74 -    with `s < r` have "m = 0" by arith
1.75 +    with `s < r` have "m = 0" by (simp add: less_le_not_le)
1.76      with `m > 0` show thesis by auto
1.77    next
1.78      case True with * have "m * r + q - m * r = m * s - m * r" by simp