src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Tue Jan 27 09:44:14 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Jan 27 15:39:51 2004 +0100
@@ -210,6 +210,9 @@
 lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"
   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
 
+lemma minus_mult_commute: "(- a) * b = a * (- b::'a::ring)"
+  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+
 lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
 by (simp add: right_distrib diff_minus 
               minus_mult_left [symmetric] minus_mult_right [symmetric]) 
@@ -889,6 +892,10 @@
 apply (simp add: mult_assoc [symmetric] add_commute)
 done
 
+lemma inverse_divide [simp]:
+      "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
+  by (simp add: divide_inverse_zero mult_commute)
+
 lemma nonzero_mult_divide_cancel_left:
   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
     shows "(c*a)/(c*b) = a/(b::'a::field)"
@@ -1139,6 +1146,43 @@
 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
 
+subsection{*Inverses and the Number One*}
+
+lemma one_less_inverse_iff:
+    "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"proof cases
+  assume "0 < x"
+    with inverse_less_iff_less [OF zero_less_one, of x]
+    show ?thesis by simp
+next
+  assume notless: "~ (0 < x)"
+  have "~ (1 < inverse x)"
+  proof
+    assume "1 < inverse x"
+    also with notless have "... \<le> 0" by (simp add: linorder_not_less)
+    also have "... < 1" by (rule zero_less_one) 
+    finally show False by auto
+  qed
+  with notless show ?thesis by simp
+qed
+
+lemma inverse_eq_1_iff [simp]:
+    "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
+by (insert inverse_eq_iff_eq [of x 1], simp) 
+
+lemma one_le_inverse_iff:
+   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
+by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
+                    eq_commute [of 1]) 
+
+lemma inverse_less_1_iff:
+   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
+by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
+
+lemma inverse_le_1_iff:
+   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
+by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
+
+
 subsection{*Division and Signs*}
 
 lemma zero_less_divide_iff:
@@ -1412,13 +1456,16 @@
 
 subsection {* Ordered Fields are Dense *}
 
-lemma zero_less_two: "0 < (1+1::'a::ordered_field)"
+lemma less_add_one: "a < (a+1::'a::ordered_semiring)"
 proof -
-  have "0 + 0 <  (1+1::'a::ordered_field)"
-    by (blast intro: zero_less_one add_strict_mono) 
+  have "a+0 < (a+1::'a::ordered_semiring)"
+    by (blast intro: zero_less_one add_strict_left_mono) 
   thus ?thesis by simp
 qed
 
+lemma zero_less_two: "0 < (1+1::'a::ordered_semiring)"
+  by (blast intro: order_less_trans zero_less_one less_add_one) 
+
 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
 by (simp add: zero_less_two pos_less_divide_eq right_distrib) 
 
@@ -1610,6 +1657,7 @@
 val minus_mult_left = thm"minus_mult_left";
 val minus_mult_right = thm"minus_mult_right";
 val minus_mult_minus = thm"minus_mult_minus";
+val minus_mult_commute = thm"minus_mult_commute";
 val right_diff_distrib = thm"right_diff_distrib";
 val left_diff_distrib = thm"left_diff_distrib";
 val minus_diff_eq = thm"minus_diff_eq";
@@ -1700,6 +1748,7 @@
 val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
 val divide_self = thm"divide_self";
 val divide_inverse_zero = thm"divide_inverse_zero";
+val inverse_divide = thm"inverse_divide";
 val divide_zero_left = thm"divide_zero_left";
 val inverse_eq_divide = thm"inverse_eq_divide";
 val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";