src/HOL/Ring_and_Field.thy
 changeset 23544 4b4165cb3e0d parent 23527 c1d2fa4b76df child 23550 d4f1d6ef119c
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:17:17 2007 +0200
1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:28:36 2007 +0200
1.3 @@ -124,18 +124,17 @@
1.4
1.5  class ring_no_zero_divisors = ring + no_zero_divisors
1.6
1.7 -class dom = ring_1 + ring_no_zero_divisors
1.8 -hide const dom
1.9 +class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
1.10
1.11  class idom = comm_ring_1 + no_zero_divisors
1.12
1.13 -instance idom \<subseteq> dom ..
1.14 +instance idom \<subseteq> ring_1_no_zero_divisors ..
1.15
1.16  class division_ring = ring_1 + inverse +
1.17    assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
1.18    assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
1.19
1.20 -instance division_ring \<subseteq> dom
1.21 +instance division_ring \<subseteq> ring_1_no_zero_divisors
1.22  proof
1.23    fix a b :: 'a
1.24    assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
1.25 @@ -717,22 +716,22 @@
1.26  by (insert mult_less_cancel_left [of c a 1], simp)
1.27
1.28  lemma mult_cancel_right1 [simp]:
1.29 -  fixes c :: "'a :: dom"
1.30 +  fixes c :: "'a :: ring_1_no_zero_divisors"
1.31    shows "(c = b*c) = (c = 0 | b=1)"
1.32  by (insert mult_cancel_right [of 1 c b], force)
1.33
1.34  lemma mult_cancel_right2 [simp]:
1.35 -  fixes c :: "'a :: dom"
1.36 +  fixes c :: "'a :: ring_1_no_zero_divisors"
1.37    shows "(a*c = c) = (c = 0 | a=1)"
1.38  by (insert mult_cancel_right [of a c 1], simp)
1.39
1.40  lemma mult_cancel_left1 [simp]:
1.41 -  fixes c :: "'a :: dom"
1.42 +  fixes c :: "'a :: ring_1_no_zero_divisors"
1.43    shows "(c = c*b) = (c = 0 | b=1)"
1.44  by (insert mult_cancel_left [of c 1 b], force)
1.45
1.46  lemma mult_cancel_left2 [simp]:
1.47 -  fixes c :: "'a :: dom"
1.48 +  fixes c :: "'a :: ring_1_no_zero_divisors"
1.49    shows "(c*a = c) = (c = 0 | a=1)"
1.50  by (insert mult_cancel_left [of c a 1], simp)
1.51
```