src/HOL/Ring_and_Field.thy
 changeset 18649 bb99c2e705ca parent 18623 9a5419d5ca01 child 19404 9bf2cdc9e8e8
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Wed Jan 11 10:59:55 2006 +0100
1.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Jan 11 11:00:26 2006 +0100
1.3 @@ -1647,47 +1647,52 @@
1.4
1.5  lemma le_divide_eq_1_pos [simp]:
1.6    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.7 -  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
1.8 +  shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
1.9  by (auto simp add: le_divide_eq)
1.10
1.11  lemma le_divide_eq_1_neg [simp]:
1.12    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.13 -  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
1.14 +  shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
1.15  by (auto simp add: le_divide_eq)
1.16
1.17  lemma divide_le_eq_1_pos [simp]:
1.18    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.19 -  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
1.20 +  shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
1.21  by (auto simp add: divide_le_eq)
1.22
1.23  lemma divide_le_eq_1_neg [simp]:
1.24    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.25 -  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
1.26 +  shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
1.27  by (auto simp add: divide_le_eq)
1.28
1.29  lemma less_divide_eq_1_pos [simp]:
1.30    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.31 -  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
1.32 +  shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
1.33  by (auto simp add: less_divide_eq)
1.34
1.35  lemma less_divide_eq_1_neg [simp]:
1.36    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.37 -  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
1.38 +  shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
1.39  by (auto simp add: less_divide_eq)
1.40
1.41  lemma divide_less_eq_1_pos [simp]:
1.42    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.43 -  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
1.44 +  shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
1.45 +by (auto simp add: divide_less_eq)
1.46 +
1.47 +lemma divide_less_eq_1_neg [simp]:
1.48 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
1.49 +  shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
1.50  by (auto simp add: divide_less_eq)
1.51
1.52  lemma eq_divide_eq_1 [simp]:
1.53    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.54 -  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
1.55 +  shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
1.56  by (auto simp add: eq_divide_eq)
1.57
1.58  lemma divide_eq_eq_1 [simp]:
1.59    fixes a :: "'a :: {ordered_field,division_by_zero}"
1.60 -  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
1.61 +  shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
1.62  by (auto simp add: divide_eq_eq)
1.63
1.64  subsection {* Reasoning about inequalities with division *}
```