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