--- a/src/HOL/Ring_and_Field.thy Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Jan 12 16:51:45 2004 +0100
@@ -7,13 +7,11 @@
header {*
\title{Ring and field structures}
- \author{Gertrud Bauer and Markus Wenzel}
+ \author{Gertrud Bauer, L. C. Paulson and Markus Wenzel}
*}
theory Ring_and_Field = Inductive:
-text{*Lemmas and extension to semirings by L. C. Paulson*}
-
subsection {* Abstract algebraic structures *}
axclass semiring \<subseteq> zero, one, plus, times
@@ -167,14 +165,14 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
+lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring)"
proof -
have "0*a + 0*a = 0*a + 0"
by (simp add: left_distrib [symmetric])
thus ?thesis by (simp only: add_left_cancel)
qed
-lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
+lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring)"
by (simp add: mult_commute)
@@ -1333,6 +1331,39 @@
apply (simp add: divide_inverse_zero field_mult_cancel_left)
done
+subsection {* Division and the Number One *}
+
+text{*Simplify expressions equated with 1*}
+lemma divide_eq_1_iff [simp]:
+ "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+apply (case_tac "b=0", simp)
+apply (simp add: right_inverse_eq)
+done
+
+
+lemma one_eq_divide_iff [simp]:
+ "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+by (simp add: eq_commute [of 1])
+
+lemma zero_eq_1_divide_iff [simp]:
+ "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
+apply (case_tac "a=0", simp)
+apply (auto simp add: nonzero_eq_divide_eq)
+done
+
+lemma one_divide_eq_0_iff [simp]:
+ "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
+apply (case_tac "a=0", simp)
+apply (insert zero_neq_one [THEN not_sym])
+apply (auto simp add: nonzero_divide_eq_eq)
+done
+
+text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
+declare zero_less_divide_iff [of "1", simp]
+declare divide_less_0_iff [of "1", simp]
+declare zero_le_divide_iff [of "1", simp]
+declare divide_le_0_iff [of "1", simp]
+
subsection {* Ordering Rules for Division *}
@@ -1413,7 +1444,6 @@
minus_mult_left [symmetric] minus_mult_right [symmetric])
done
-
lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
by (simp add: abs_if)
@@ -1571,8 +1601,8 @@
val mult_1 = thm"mult_1";
val mult_1_right = thm"mult_1_right";
val mult_left_commute = thm"mult_left_commute";
-val mult_left_zero = thm"mult_left_zero";
-val mult_right_zero = thm"mult_right_zero";
+val mult_zero_left = thm"mult_zero_left";
+val mult_zero_right = thm"mult_zero_right";
val left_distrib = thm "left_distrib";
val right_distrib = thm"right_distrib";
val combine_common_factor = thm"combine_common_factor";