1.1 --- a/src/HOL/ex/Numeral.thy	Thu Apr 30 11:14:04 2009 -0700
     1.2 +++ b/src/HOL/ex/Numeral.thy	Thu Apr 30 12:16:35 2009 -0700
     1.3 @@ -709,17 +709,17 @@
     1.4    unfolding of_num_pow ..
     1.5  
     1.6  lemma power_zero_of_num [numeral]:
     1.7 -  "0 ^ of_num n = (0::'a::{semiring_0,power})"
     1.8 +  "0 ^ of_num n = (0::'a::semiring_1)"
     1.9    using of_num_pos [where n=n and ?'a=nat]
    1.10    by (simp add: power_0_left)
    1.11  
    1.12  lemma power_minus_Dig0 [numeral]:
    1.13 -  fixes x :: "'a::{ring_1}"
    1.14 +  fixes x :: "'a::ring_1"
    1.15    shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
    1.16    by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc)
    1.17  
    1.18  lemma power_minus_Dig1 [numeral]:
    1.19 -  fixes x :: "'a::{ring_1}"
    1.20 +  fixes x :: "'a::ring_1"
    1.21    shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
    1.22    by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc)
    1.23  
    1.24 @@ -881,11 +881,45 @@
    1.25  
    1.26  subsection {* Numeral equations as default simplification rules *}
    1.27  
    1.28 -text {* TODO.  Be more precise here with respect to subsumed facts.  Or use named theorems anyway. *}
    1.29 -declare (in semiring_numeral) numeral [simp]
    1.30 -declare (in semiring_1) numeral [simp]
    1.31 -declare (in semiring_char_0) numeral [simp]
    1.32 -declare (in ring_1) numeral [simp]
    1.33 +declare (in semiring_numeral) of_num_One [simp]
    1.34 +declare (in semiring_numeral) of_num_plus_one [simp]
    1.35 +declare (in semiring_numeral) of_num_one_plus [simp]
    1.36 +declare (in semiring_numeral) of_num_plus [simp]
    1.37 +declare (in semiring_numeral) of_num_times [simp]
    1.38 +
    1.39 +declare (in semiring_1) of_nat_of_num [simp]
    1.40 +
    1.41 +declare (in semiring_char_0) of_num_eq_iff [simp]
    1.42 +declare (in semiring_char_0) of_num_eq_one_iff [simp]
    1.43 +declare (in semiring_char_0) one_eq_of_num_iff [simp]
    1.44 +
    1.45 +declare (in ordered_semidom) of_num_pos [simp]
    1.46 +declare (in ordered_semidom) of_num_less_eq_iff [simp]
    1.47 +declare (in ordered_semidom) of_num_less_eq_one_iff [simp]
    1.48 +declare (in ordered_semidom) one_less_eq_of_num_iff [simp]
    1.49 +declare (in ordered_semidom) of_num_less_iff [simp]
    1.50 +declare (in ordered_semidom) of_num_less_one_iff [simp]
    1.51 +declare (in ordered_semidom) one_less_of_num_iff [simp]
    1.52 +declare (in ordered_semidom) of_num_nonneg [simp]
    1.53 +declare (in ordered_semidom) of_num_less_zero_iff [simp]
    1.54 +declare (in ordered_semidom) of_num_le_zero_iff [simp]
    1.55 +
    1.56 +declare (in ordered_idom) le_signed_numeral_special [simp]
    1.57 +declare (in ordered_idom) less_signed_numeral_special [simp]
    1.58 +
    1.59 +declare (in semiring_1_minus) Dig_of_num_minus_one [simp]
    1.60 +declare (in semiring_1_minus) Dig_one_minus_of_num [simp]
    1.61 +
    1.62 +declare (in ring_1) Dig_plus_uminus [simp]
    1.63 +declare (in ring_1) of_int_of_num [simp]
    1.64 +
    1.65 +declare power_of_num [simp]
    1.66 +declare power_zero_of_num [simp]
    1.67 +declare power_minus_Dig0 [simp]
    1.68 +declare power_minus_Dig1 [simp]
    1.69 +
    1.70 +declare Suc_of_num [simp]
    1.71 +
    1.72  thm numeral
    1.73  
    1.74