tuned proofs
authorhaftmann
Sun Sep 29 16:01:22 2013 +0200 (2013-09-29)
changeset 53986a269577d97c0
parent 53985 f6b7afa414f7
child 53987 16a0cd5293d9
tuned proofs
src/HOL/Nat.thy
     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.5  
     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.18  
    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.26  
    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.34  
    1.35  end
    1.36  
    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.41  
    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.62  
    1.63  
    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