1.1 --- a/src/HOL/Integ/NatBin.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -256,42 +256,42 @@
     1.4  We cannot prove general results about the numeral @{term "-1"}, so we have to
     1.5  use @{term "- 1"} instead.*}
     1.6  
     1.7 -lemma power2_eq_square: "(a::'a::{semiring,ringpower})\<twosuperior> = a * a"
     1.8 +lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = a * a"
     1.9    by (simp add: numeral_2_eq_2 Power.power_Suc)
    1.10  
    1.11 -lemma [simp]: "(0::'a::{semiring,ringpower})\<twosuperior> = 0"
    1.12 +lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 0"
    1.13    by (simp add: power2_eq_square)
    1.14  
    1.15 -lemma [simp]: "(1::'a::{semiring,ringpower})\<twosuperior> = 1"
    1.16 +lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 1"
    1.17    by (simp add: power2_eq_square)
    1.18  
    1.19  text{*Squares of literal numerals will be evaluated.*}
    1.20  declare power2_eq_square [of "number_of w", standard, simp]
    1.21  
    1.22 -lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_ring,ringpower})"
    1.23 +lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,ringpower})"
    1.24    by (simp add: power2_eq_square zero_le_square)
    1.25  
    1.26  lemma zero_less_power2 [simp]:
    1.27 -     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_ring,ringpower}))"
    1.28 +     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,ringpower}))"
    1.29    by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
    1.30  
    1.31  lemma zero_eq_power2 [simp]:
    1.32 -     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_ring,ringpower}))"
    1.33 +     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,ringpower}))"
    1.34    by (force simp add: power2_eq_square mult_eq_0_iff)
    1.35  
    1.36  lemma abs_power2 [simp]:
    1.37 -     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
    1.38 +     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,ringpower})"
    1.39    by (simp add: power2_eq_square abs_mult abs_mult_self)
    1.40  
    1.41  lemma power2_abs [simp]:
    1.42 -     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_ring,ringpower})"
    1.43 +     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,ringpower})"
    1.44    by (simp add: power2_eq_square abs_mult_self)
    1.45  
    1.46  lemma power2_minus [simp]:
    1.47 -     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{ring,ringpower})"
    1.48 +     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,ringpower})"
    1.49    by (simp add: power2_eq_square)
    1.50  
    1.51 -lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{ring,ringpower})"
    1.52 +lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,ringpower})"
    1.53  apply (induct_tac "n")
    1.54  apply (auto simp add: power_Suc power_add)
    1.55  done
    1.56 @@ -303,11 +303,11 @@
    1.57  by (simp add: power_even_eq) 
    1.58  
    1.59  lemma power_minus_even [simp]:
    1.60 -     "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)"
    1.61 +     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,ringpower}) ^ (2*n)"
    1.62  by (simp add: power_minus1_even power_minus [of a]) 
    1.63  
    1.64  lemma zero_le_even_power:
    1.65 -     "0 \<le> (a::'a::{ordered_ring,ringpower}) ^ (2*n)"
    1.66 +     "0 \<le> (a::'a::{ordered_idom,ringpower}) ^ (2*n)"
    1.67  proof (induct "n")
    1.68    case 0
    1.69      show ?case by (simp add: zero_le_one)
    1.70 @@ -320,7 +320,7 @@
    1.71  qed
    1.72  
    1.73  lemma odd_power_less_zero:
    1.74 -     "(a::'a::{ordered_ring,ringpower}) < 0 ==> a ^ Suc(2*n) < 0"
    1.75 +     "(a::'a::{ordered_idom,ringpower}) < 0 ==> a ^ Suc(2*n) < 0"
    1.76  proof (induct "n")
    1.77    case 0
    1.78      show ?case by (simp add: Power.power_Suc)
    1.79 @@ -333,7 +333,7 @@
    1.80  qed
    1.81  
    1.82  lemma odd_0_le_power_imp_0_le:
    1.83 -     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_ring,ringpower})"
    1.84 +     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,ringpower})"
    1.85  apply (insert odd_power_less_zero [of a n]) 
    1.86  apply (force simp add: linorder_not_less [symmetric]) 
    1.87  done
    1.88 @@ -473,7 +473,7 @@
    1.89       "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
    1.90        (x=y & (((number_of v) ::int) = number_of w))"
    1.91  by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
    1.92 -               Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0
    1.93 +               OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0
    1.94              split add: split_if cong: imp_cong) 
    1.95  
    1.96