rename class dom to ring_1_no_zero_divisors
authorhuffman
Tue Jul 03 17:28:36 2007 +0200 (2007-07-03)
changeset 235444b4165cb3e0d
parent 23543 12271cfad085
child 23545 2fddae6056ab
rename class dom to ring_1_no_zero_divisors
src/HOL/Power.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Power.thy	Tue Jul 03 17:17:17 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Tue Jul 03 17:28:36 2007 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  done
     1.5  
     1.6  lemma power_eq_0_iff [simp]:
     1.7 -     "(a^n = 0) = (a = (0::'a::{dom,recpower}) & 0<n)"
     1.8 +     "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & 0<n)"
     1.9  apply (induct "n")
    1.10  apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.11  done
    1.12 @@ -142,7 +142,7 @@
    1.13       "(a^n = 0) = (a = (0::'a::{division_ring,recpower}) & 0<n)"
    1.14  by simp (* TODO: delete *)
    1.15  
    1.16 -lemma field_power_not_zero: "a \<noteq> (0::'a::{dom,recpower}) ==> a^n \<noteq> 0"
    1.17 +lemma field_power_not_zero: "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    1.18  by force
    1.19  
    1.20  lemma nonzero_power_inverse:
     2.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:17:17 2007 +0200
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jul 03 17:28:36 2007 +0200
     2.3 @@ -124,18 +124,17 @@
     2.4  
     2.5  class ring_no_zero_divisors = ring + no_zero_divisors
     2.6  
     2.7 -class dom = ring_1 + ring_no_zero_divisors
     2.8 -hide const dom
     2.9 +class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
    2.10  
    2.11  class idom = comm_ring_1 + no_zero_divisors
    2.12  
    2.13 -instance idom \<subseteq> dom ..
    2.14 +instance idom \<subseteq> ring_1_no_zero_divisors ..
    2.15  
    2.16  class division_ring = ring_1 + inverse +
    2.17    assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
    2.18    assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
    2.19  
    2.20 -instance division_ring \<subseteq> dom
    2.21 +instance division_ring \<subseteq> ring_1_no_zero_divisors
    2.22  proof
    2.23    fix a b :: 'a
    2.24    assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
    2.25 @@ -717,22 +716,22 @@
    2.26  by (insert mult_less_cancel_left [of c a 1], simp)
    2.27  
    2.28  lemma mult_cancel_right1 [simp]:
    2.29 -  fixes c :: "'a :: dom"
    2.30 +  fixes c :: "'a :: ring_1_no_zero_divisors"
    2.31    shows "(c = b*c) = (c = 0 | b=1)"
    2.32  by (insert mult_cancel_right [of 1 c b], force)
    2.33  
    2.34  lemma mult_cancel_right2 [simp]:
    2.35 -  fixes c :: "'a :: dom"
    2.36 +  fixes c :: "'a :: ring_1_no_zero_divisors"
    2.37    shows "(a*c = c) = (c = 0 | a=1)"
    2.38  by (insert mult_cancel_right [of a c 1], simp)
    2.39   
    2.40  lemma mult_cancel_left1 [simp]:
    2.41 -  fixes c :: "'a :: dom"
    2.42 +  fixes c :: "'a :: ring_1_no_zero_divisors"
    2.43    shows "(c = c*b) = (c = 0 | b=1)"
    2.44  by (insert mult_cancel_left [of c 1 b], force)
    2.45  
    2.46  lemma mult_cancel_left2 [simp]:
    2.47 -  fixes c :: "'a :: dom"
    2.48 +  fixes c :: "'a :: ring_1_no_zero_divisors"
    2.49    shows "(c*a = c) = (c = 0 | a=1)"
    2.50  by (insert mult_cancel_left [of c a 1], simp)
    2.51