src/HOL/Library/Lattice_Algebras.thy
 changeset 37884 314a88278715 parent 36976 e78d1e06d855 child 41528 276078f01ada
```     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 12:17:38 2010 +0200
1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Jul 19 16:09:43 2010 +0200
1.3 @@ -376,9 +376,10 @@
1.4    "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
1.5  proof -
1.6    assume "a+b <= c"
1.7 -  hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
1.8 -  have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
1.9 -  show ?thesis by (rule le_add_right_mono[OF 2 3])
1.10 +  then have "a <= c+(-b)" by (simp add: algebra_simps)
1.11 +  have "(-b) <= abs b" by (rule abs_ge_minus_self)
1.12 +  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
1.13 +  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
1.14  qed
1.15
1.16  class lattice_ring = ordered_ring + lattice_ab_group_add_abs
1.17 @@ -411,7 +412,7 @@
1.18      apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1.19      done
1.20    have yx: "?y <= ?x"
1.21 -    apply (simp add:diff_def)
1.22 +    apply (simp add:diff_minus)
1.23      apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
1.24      apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
1.25      done
```