src/HOL/Rings.thy
changeset 56544 b60d5d119489
parent 56536 aefb4a8da31f
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Rings.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -568,7 +568,7 @@
     1.4    "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
     1.5  by (force simp add: mult_strict_right_mono not_less [symmetric])
     1.6  
     1.7 -lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
     1.8 +lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
     1.9  using mult_strict_left_mono [of 0 b a] by simp
    1.10  
    1.11  lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
    1.12 @@ -602,7 +602,7 @@
    1.13    assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
    1.14    shows "a * c < b * d"
    1.15    using assms apply (cases "c=0")
    1.16 -  apply (simp add: mult_pos_pos)
    1.17 +  apply (simp)
    1.18    apply (erule mult_strict_right_mono [THEN less_trans])
    1.19    apply (force simp add: le_less)
    1.20    apply (erule mult_strict_left_mono, assumption)
    1.21 @@ -824,7 +824,7 @@
    1.22        show ?thesis by (auto dest: mult_strict_right_mono_neg)
    1.23      next
    1.24        case False with B have "0 < b" by auto
    1.25 -      with A' show ?thesis by (auto dest: mult_pos_pos)
    1.26 +      with A' show ?thesis by auto
    1.27      qed
    1.28    qed
    1.29    then show "a * b \<noteq> 0" by (simp add: neq_iff)
    1.30 @@ -832,7 +832,7 @@
    1.31  
    1.32  lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    1.33    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
    1.34 -     (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
    1.35 +     (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
    1.36  
    1.37  lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
    1.38    by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)