# HG changeset patch
# User chaieb
# Date 1182080369 -7200
# Node ID 167b53019d6fd57c740e4519dd55f8b1c1a1e2f4
# Parent  8993b3144358eb58e5affc527b687f661351dee7
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub

diff -r 8993b3144358 -r 167b53019d6f src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Jun 17 13:39:27 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sun Jun 17 13:39:29 2007 +0200
@@ -1007,7 +1007,6 @@
 apply (cases "b = 0")
 apply (simp_all add: nonzero_mult_divide_cancel_right)
 done
-
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   by (simp add: divide_inverse)
 
@@ -1040,6 +1039,25 @@
 done
 
 
+lemma nonzero_mult_divide_cancel_right':
+  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
+proof -
+  assume b: "b \<noteq> 0"
+  have "a * b / b = a * (b / b)" by (simp add: times_divide_eq_right)
+  also have "\<dots> = a" by (simp add: divide_self b)
+  finally show "a * b / b = a" .
+qed
+
+lemma nonzero_mult_divide_cancel_left':
+  "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
+proof -
+  assume b: "a \<noteq> 0"
+  have "a * b / a = b * a / a" by (simp add: mult_commute)
+  also have "\<dots> = b * (a / a)" by (simp add: times_divide_eq_right)
+  also have "\<dots> = b" by (simp add: divide_self b)
+  finally show "a * b / a = b" .
+qed
+
 subsubsection{*Special Cancellation Simprules for Division*}
 
 (* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
@@ -1217,6 +1235,23 @@
       "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric])
 
+lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
+proof
+  fix x::'a
+  have m1: "- (1::'a) < 0" by simp
+  from add_strict_right_mono[OF m1, where c=x] 
+  have "(- 1) + x < x" by simp
+  thus "\<exists>y. y < x" by blast
+qed
+
+lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"
+proof
+  fix x::'a
+  have m1: " (1::'a) > 0" by simp
+  from add_strict_right_mono[OF m1, where c=x] 
+  have "1 + x > x" by simp
+  thus "\<exists>y. y > x" by blast
+qed
 
 subsection{*Anti-Monotonicity of @{term inverse}*}