author paulson Wed, 11 Jan 2006 11:00:26 +0100 changeset 18649 bb99c2e705ca parent 18648 22f96cd085d5 child 18650 e16fae1a58e9
tidied, and added missing thm divide_less_eq_1_neg
```--- a/src/HOL/Ring_and_Field.thy	Wed Jan 11 10:59:55 2006 +0100
+++ b/src/HOL/Ring_and_Field.thy	Wed Jan 11 11:00:26 2006 +0100
@@ -1647,47 +1647,52 @@

lemma le_divide_eq_1_pos [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
+  shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"

lemma le_divide_eq_1_neg [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
+  shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"

lemma divide_le_eq_1_pos [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
+  shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"

lemma divide_le_eq_1_neg [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
+  shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"

lemma less_divide_eq_1_pos [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
+  shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"

lemma less_divide_eq_1_neg [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
+  shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"

lemma divide_less_eq_1_pos [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
+  shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
+
+lemma divide_less_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"

lemma eq_divide_eq_1 [simp]:
fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
+  shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"