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)
```