1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 07 08:03:46 2006 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 07 09:33:47 2006 +0100
     1.3 @@ -1645,7 +1645,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
     1.8 +lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
     1.9    apply (erule finite_induct)
    1.10    apply (auto simp add: power_Suc)
    1.11    done

     2.1 --- a/src/HOL/Hyperreal/Deriv.thy	Tue Nov 07 08:03:46 2006 +0100
     2.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Tue Nov 07 09:33:47 2006 +0100
     2.3 @@ -241,7 +241,7 @@
     2.4  done
     2.5  
     2.6  lemma DERIV_power_Suc:
     2.7 -  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
     2.8 +  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower,comm_monoid_mult}"
     2.9    assumes f: "DERIV f x :> D"
    2.10    shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) *# (D * f x ^ n)"
    2.11  proof (induct n)
    2.12 @@ -255,7 +255,7 @@
    2.13  qed
    2.14  
    2.15  lemma DERIV_power:
    2.16 -  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
    2.17 +  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower,comm_monoid_mult}"
    2.18    assumes f: "DERIV f x :> D"
    2.19    shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n *# (D * f x ^ (n - Suc 0))"
    2.20  by (cases "n", simp, simp add: DERIV_power_Suc f)

     3.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 08:03:46 2006 +0100
     3.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 09:33:47 2006 +0100
     3.3 @@ -361,7 +361,9 @@
     3.4  apply (transfer, rule right_distrib)
     3.5  done
     3.6  
     3.7 -instance star :: (semiring_0) semiring_0 ..
     3.8 +instance star :: (semiring_0) semiring_0 
     3.9 +by intro_classes (transfer, simp)+
    3.10 +
    3.11  instance star :: (semiring_0_cancel) semiring_0_cancel ..
    3.12  
    3.13  instance star :: (comm_semiring) comm_semiring
    3.14 @@ -417,7 +419,7 @@
    3.15  done
    3.16  
    3.17  instance star :: (pordered_comm_semiring) pordered_comm_semiring
    3.18 -by (intro_classes, transfer, rule pordered_comm_semiring_class.mult_mono)
    3.19 +by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
    3.20  
    3.21  instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
    3.22  

     4.1 --- a/src/HOL/Integ/NatBin.thy	Tue Nov 07 08:03:46 2006 +0100
     4.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Nov 07 09:33:47 2006 +0100
     4.3 @@ -334,7 +334,7 @@
     4.4  done
     4.5  
     4.6  lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
     4.7 -by (simp add: power_mult power_mult_distrib power2_eq_square)
     4.8 +by (subst mult_commute) (simp add: power_mult)
     4.9  
    4.10  lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
    4.11  by (simp add: power_even_eq) 

     5.1 --- a/src/HOL/Power.thy	Tue Nov 07 08:03:46 2006 +0100
     5.2 +++ b/src/HOL/Power.thy	Tue Nov 07 09:33:47 2006 +0100
     5.3 @@ -11,17 +11,17 @@
     5.4  imports Divides
     5.5  begin
     5.6  
     5.7 -subsection{*Powers for Arbitrary Semirings*}
     5.8 +subsection{*Powers for Arbitrary Monoids*}
     5.9  
    5.10 -axclass recpower \<subseteq> comm_semiring_1_cancel, power
    5.11 +axclass recpower \<subseteq> monoid_mult, power
    5.12    power_0 [simp]: "a ^ 0       = 1"
    5.13    power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
    5.14  
    5.15 -lemma power_0_Suc [simp]: "(0::'a::recpower) ^ (Suc n) = 0"
    5.16 +lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
    5.17  by (simp add: power_Suc)
    5.18  
    5.19  text{*It looks plausible as a simprule, but its effect can be strange.*}
    5.20 -lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
    5.21 +lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
    5.22  by (induct "n", auto)
    5.23  
    5.24  lemma power_one [simp]: "1^n = (1::'a::recpower)"
    5.25 @@ -32,17 +32,20 @@
    5.26  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
    5.27  by (simp add: power_Suc)
    5.28  
    5.29 +lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
    5.30 +by (induct "n") (simp_all add:power_Suc mult_assoc)
    5.31 +
    5.32  lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
    5.33 -apply (induct "n")
    5.34 +apply (induct "m")
    5.35  apply (simp_all add: power_Suc mult_ac)
    5.36  done
    5.37  
    5.38  lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
    5.39 -apply (induct "n")
    5.40 +apply (induct "n") 
    5.41  apply (simp_all add: power_Suc power_add)
    5.42  done
    5.43  
    5.44 -lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
    5.45 +lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
    5.46  apply (induct "n")
    5.47  apply (auto simp add: power_Suc mult_ac)
    5.48  done

     6.1 --- a/src/HOL/Ring_and_Field.thy	Tue Nov 07 08:03:46 2006 +0100
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Nov 07 09:33:47 2006 +0100
     6.3 @@ -27,9 +27,27 @@
     6.4    left_distrib: "(a + b) * c = a * c + b * c"
     6.5    right_distrib: "a * (b + c) = a * b + a * c"
     6.6  
     6.7 -axclass semiring_0 \<subseteq> semiring, comm_monoid_add
     6.8 +axclass mult_zero \<subseteq> times, zero
     6.9 +  mult_zero_left [simp]: "0 * a = 0"
    6.10 +  mult_zero_right [simp]: "a * 0 = 0"
    6.11  
    6.12 -axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
    6.13 +axclass semiring_0 \<subseteq> semiring, comm_monoid_add, mult_zero
    6.14 +
    6.15 +axclass semiring_0_cancel \<subseteq> semiring, comm_monoid_add, cancel_ab_semigroup_add
    6.16 +
    6.17 +instance semiring_0_cancel \<subseteq> semiring_0
    6.18 +proof
    6.19 +  fix a :: 'a
    6.20 +  have "0 * a + 0 * a = 0 * a + 0"
    6.21 +    by (simp add: left_distrib [symmetric])
    6.22 +  thus "0 * a = 0"
    6.23 +    by (simp only: add_left_cancel)
    6.24 +
    6.25 +  have "a * 0 + a * 0 = a * 0 + 0"
    6.26 +    by (simp add: right_distrib [symmetric])
    6.27 +  thus "a * 0 = 0"
    6.28 +    by (simp only: add_left_cancel)
    6.29 +qed
    6.30  
    6.31  axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
    6.32    distrib: "(a + b) * c = a * c + b * c"
    6.33 @@ -44,14 +62,16 @@
    6.34    finally show "a * (b + c) = a * b + a * c" by blast
    6.35  qed
    6.36  
    6.37 -axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add
    6.38 +axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add, mult_zero
    6.39  
    6.40  instance comm_semiring_0 \<subseteq> semiring_0 ..
    6.41  
    6.42 -axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
    6.43 +axclass comm_semiring_0_cancel \<subseteq> comm_semiring, comm_monoid_add, cancel_ab_semigroup_add
    6.44  
    6.45  instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
    6.46  
    6.47 +instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
    6.48 +
    6.49  axclass zero_neq_one \<subseteq> zero, one
    6.50    zero_neq_one [simp]: "0 \<noteq> 1"
    6.51  
    6.52 @@ -64,31 +84,37 @@
    6.53  axclass no_zero_divisors \<subseteq> zero, times
    6.54    no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    6.55  
    6.56 -axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
    6.57 +axclass semiring_1_cancel \<subseteq> semiring, comm_monoid_add, zero_neq_one, cancel_ab_semigroup_add, monoid_mult
    6.58  
    6.59  instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
    6.60  
    6.61 -axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
    6.62 +instance semiring_1_cancel \<subseteq> semiring_1 ..
    6.63 +
    6.64 +axclass comm_semiring_1_cancel \<subseteq> 
    6.65 +  comm_semiring, comm_monoid_add, comm_monoid_mult,
    6.66 +  zero_neq_one, cancel_ab_semigroup_add
    6.67  
    6.68  instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
    6.69  
    6.70  instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
    6.71  
    6.72 +instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
    6.73 +
    6.74  axclass ring \<subseteq> semiring, ab_group_add
    6.75  
    6.76  instance ring \<subseteq> semiring_0_cancel ..
    6.77  
    6.78 -axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
    6.79 +axclass comm_ring \<subseteq> comm_semiring, ab_group_add
    6.80  
    6.81  instance comm_ring \<subseteq> ring ..
    6.82  
    6.83  instance comm_ring \<subseteq> comm_semiring_0_cancel ..
    6.84  
    6.85 -axclass ring_1 \<subseteq> ring, semiring_1
    6.86 +axclass ring_1 \<subseteq> ring, zero_neq_one, monoid_mult
    6.87  
    6.88  instance ring_1 \<subseteq> semiring_1_cancel ..
    6.89  
    6.90 -axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
    6.91 +axclass comm_ring_1 \<subseteq> comm_ring, zero_neq_one, comm_monoid_mult (* previously ring *)
    6.92  
    6.93  instance comm_ring_1 \<subseteq> ring_1 ..
    6.94  
    6.95 @@ -115,22 +141,6 @@
    6.96  instance field \<subseteq> division_ring
    6.97  by (intro_classes, erule field_left_inverse, erule field_right_inverse)
    6.98  
    6.99 -lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
   6.100 -proof -
   6.101 -  have "0*a + 0*a = 0*a + 0"
   6.102 -    by (simp add: left_distrib [symmetric])
   6.103 -  thus ?thesis 
   6.104 -    by (simp only: add_left_cancel)
   6.105 -qed
   6.106 -
   6.107 -lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
   6.108 -proof -
   6.109 -  have "a*0 + a*0 = a*0 + 0"
   6.110 -    by (simp add: right_distrib [symmetric])
   6.111 -  thus ?thesis 
   6.112 -    by (simp only: add_left_cancel)
   6.113 -qed
   6.114 -
   6.115  lemma field_mult_eq_0_iff [simp]:
   6.116    "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
   6.117  proof cases
   6.118 @@ -182,15 +192,22 @@
   6.119  by (simp add: left_distrib diff_minus 
   6.120                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   6.121  
   6.122 -axclass pordered_semiring \<subseteq> semiring_0, pordered_ab_semigroup_add 
   6.123 +axclass mult_mono \<subseteq> times, zero, ord
   6.124    mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   6.125    mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
   6.126  
   6.127 -axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
   6.128 +axclass pordered_semiring \<subseteq> mult_mono, semiring_0, pordered_ab_semigroup_add 
   6.129 +
   6.130 +axclass pordered_cancel_semiring \<subseteq> 
   6.131 +  mult_mono, pordered_ab_semigroup_add,
   6.132 +  semiring, comm_monoid_add, 
   6.133 +  pordered_ab_semigroup_add, cancel_ab_semigroup_add
   6.134  
   6.135  instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
   6.136  
   6.137 -axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
   6.138 +instance pordered_cancel_semiring \<subseteq> pordered_semiring .. 
   6.139 +
   6.140 +axclass ordered_semiring_strict \<subseteq> semiring, comm_monoid_add, ordered_cancel_ab_semigroup_add
   6.141    mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   6.142    mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
   6.143  
   6.144 @@ -204,18 +221,30 @@
   6.145  apply (simp add: mult_strict_right_mono)
   6.146  done
   6.147  
   6.148 -axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add
   6.149 +axclass mult_mono1 \<subseteq> times, zero, ord
   6.150    mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   6.151  
   6.152 -axclass pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring, cancel_ab_semigroup_add
   6.153 +axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add, mult_mono1
   6.154  
   6.155 +axclass pordered_cancel_comm_semiring \<subseteq> 
   6.156 +  comm_semiring_0_cancel, pordered_ab_semigroup_add, mult_mono1
   6.157 +  
   6.158  instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
   6.159  
   6.160  axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
   6.161    mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   6.162  
   6.163  instance pordered_comm_semiring \<subseteq> pordered_semiring
   6.164 -by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+)
   6.165 +proof
   6.166 +  fix a b c :: 'a
   6.167 +  assume A: "a <= b" "0 <= c"
   6.168 +  with mult_mono show "c * a <= c * b" .
   6.169 +
   6.170 +  from mult_commute have "a * c = c * a" ..
   6.171 +  also from mult_mono A have "\<dots> <= c * b" .
   6.172 +  also from mult_commute have "c * b = b * c" ..
   6.173 +  finally show "a * c <= b * c" .
   6.174 +qed
   6.175  
   6.176  instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
   6.177  
   6.178 @@ -229,12 +258,10 @@
   6.179  apply (auto simp add: mult_strict_left_mono order_le_less)
   6.180  done
   6.181  
   6.182 -axclass pordered_ring \<subseteq> ring, pordered_semiring 
   6.183 +axclass pordered_ring \<subseteq> ring, pordered_cancel_semiring 
   6.184  
   6.185  instance pordered_ring \<subseteq> pordered_ab_group_add ..
   6.186  
   6.187 -instance pordered_ring \<subseteq> pordered_cancel_semiring ..
   6.188 -
   6.189  axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
   6.190  
   6.191  instance lordered_ring \<subseteq> lordered_ab_group_meet ..