author wenzelm Wed, 06 Dec 2000 21:53:05 +0100 changeset 10620 ef6c65d992b6 parent 10619 0cf191f57a54 child 10621 3d15596ee644
tuned;
```--- a/src/HOL/Library/Ring_and_Field.thy	Wed Dec 06 21:52:49 2000 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Wed Dec 06 21:53:05 2000 +0100
@@ -17,7 +17,7 @@
add_commute: "a + b = b + a"
left_zero [simp]: "0 + a = a"
left_minus [simp]: "- a + a = 0"
-  diff_minus [simp]: "a - b = a + (-b)"
+  diff_minus: "a - b = a + (-b)"
zero_number: "0 = #0"

mult_assoc: "(a * b) * c = a * (b * c)"
@@ -33,10 +33,14 @@

axclass field < ring, inverse
left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = #1"
-  divides_inverse [simp]: "b \<noteq> 0 ==> a / b = a * inverse b" (* FIXME unconditional ?? *)
+  divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"

axclass ordered_field < ordered_ring, field

+axclass division_by_zero < zero, inverse
+  inverse_zero: "inverse 0 = 0"
+  divide_zero: "a / 0 = 0"
+

subsection {* Derived rules *}
@@ -66,16 +70,18 @@
finally show ?thesis .
qed

-lemma right_minus_eq [simp]: "(a - b = 0) = (a = (b::'a::ring))"
+lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ring))"
proof
-  have "a = a - b + b" by (simp add: ring_add_ac)
+  have "a = a - b + b" by (simp add: diff_minus ring_add_ac)
also assume "a - b = 0"
finally show "a = b" by simp
-qed simp
+next
+  assume "a = b"
+  thus "a - b = 0" by (simp add: diff_minus)
+qed

lemma diff_self [simp]: "a - (a::'a::ring) = 0"
-  by simp
-

subsubsection {* Derived rules for multiplication *}
@@ -104,17 +110,21 @@
finally show ?thesis .
qed

-lemma right_inverse_eq [simp]: "b \<noteq> 0 \<Longrightarrow> (a / b = #1) = (a = (b::'a::field))"
+lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> (a / b = #1) = (a = (b::'a::field))"
proof
-  assume "b \<noteq> 0"
-  hence "a = (a / b) * b" by (simp add: ring_mult_ac)
-  also assume "a / b = #1"
-  finally show "a = b" by simp
-qed simp
+  assume neq: "b \<noteq> 0"
+  {
+    hence "a = (a / b) * b" by (simp add: divide_inverse ring_mult_ac)
+    also assume "a / b = #1"
+    finally show "a = b" by simp
+  next
+    assume "a = b"
+    with neq show "a / b = #1" by (simp add: divide_inverse)
+  }
+qed

lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / (a::'a::field) = #1"
-  by simp
-