simplify proof
authorhuffman
Mon May 17 18:51:25 2010 -0700 (2010-05-17)
changeset 36976e78d1e06d855
parent 36975 fa6244be5215
child 36977 71c8973a604b
simplify proof
src/HOL/Library/Lattice_Algebras.thy
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Mon May 17 16:52:34 2010 -0700
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Mon May 17 18:51:25 2010 -0700
     1.3 @@ -405,21 +405,15 @@
     1.4        done
     1.5    }
     1.6    note b = this[OF refl[of a] refl[of b]]
     1.7 -  note addm = add_mono[of "0::'a" _ "0::'a", simplified]
     1.8 -  note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
     1.9    have xy: "- ?x <= ?y"
    1.10      apply (simp)
    1.11 -    apply (rule_tac y="0::'a" in order_trans)
    1.12 -    apply (rule addm2)
    1.13 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
    1.14 -    apply (rule addm)
    1.15 +    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
    1.16      apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
    1.17      done
    1.18    have yx: "?y <= ?x"
    1.19      apply (simp add:diff_def)
    1.20 -    apply (rule_tac y=0 in order_trans)
    1.21 -    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
    1.22 -    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
    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
    1.26    have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
    1.27    have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)