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 *}