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