# HG changeset patch
# User krauss
# Date 1162888427 -3600
# Node ID 2d83f93c358088de481457468fab62430ccec09a
# Parent  48b8d8b8334de9b24bf7c7a1597992f60d0b7940
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
Richer structures do not inherit from semiring_0 anymore, because
anihilation is a theorem there, not an axiom.

* Generalized axclass "recpower" to arbitrary monoid, not just
commutative semirings.

diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -1645,7 +1645,7 @@
 done
 
 
-lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::recpower)) = y^(card A)"
+lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{recpower, comm_monoid_mult})) = y^(card A)"
   apply (erule finite_induct)
   apply (auto simp add: power_Suc)
   done
diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Hyperreal/Deriv.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -241,7 +241,7 @@
 done
 
 lemma DERIV_power_Suc:
-  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower,comm_monoid_mult}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) *# (D * f x ^ n)"
 proof (induct n)
@@ -255,7 +255,7 @@
 qed
 
 lemma DERIV_power:
-  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower,comm_monoid_mult}"
   assumes f: "DERIV f x :> D"
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n *# (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f)
diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -361,7 +361,9 @@
 apply (transfer, rule right_distrib)
 done
 
-instance star :: (semiring_0) semiring_0 ..
+instance star :: (semiring_0) semiring_0 
+by intro_classes (transfer, simp)+
+
 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
 instance star :: (comm_semiring) comm_semiring
@@ -417,7 +419,7 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule pordered_comm_semiring_class.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.mult_mono)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
 
diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -334,7 +334,7 @@
 done
 
 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
-by (simp add: power_mult power_mult_distrib power2_eq_square)
+by (subst mult_commute) (simp add: power_mult)
 
 lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
 by (simp add: power_even_eq) 
diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Power.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -11,17 +11,17 @@
 imports Divides
 begin
 
-subsection{*Powers for Arbitrary Semirings*}
+subsection{*Powers for Arbitrary Monoids*}
 
-axclass recpower \<subseteq> comm_semiring_1_cancel, power
+axclass recpower \<subseteq> monoid_mult, power
   power_0 [simp]: "a ^ 0       = 1"
   power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
 
-lemma power_0_Suc [simp]: "(0::'a::recpower) ^ (Suc n) = 0"
+lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
 by (simp add: power_Suc)
 
 text{*It looks plausible as a simprule, but its effect can be strange.*}
-lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::recpower))"
+lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
 by (induct "n", auto)
 
 lemma power_one [simp]: "1^n = (1::'a::recpower)"
@@ -32,17 +32,20 @@
 lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
 by (simp add: power_Suc)
 
+lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
+by (induct "n") (simp_all add:power_Suc mult_assoc)
+
 lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
-apply (induct "n")
+apply (induct "m")
 apply (simp_all add: power_Suc mult_ac)
 done
 
 lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
-apply (induct "n")
+apply (induct "n") 
 apply (simp_all add: power_Suc power_add)
 done
 
-lemma power_mult_distrib: "((a::'a::recpower) * b) ^ n = (a^n) * (b^n)"
+lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
 apply (induct "n")
 apply (auto simp add: power_Suc mult_ac)
 done
diff -r 48b8d8b8334d -r 2d83f93c3580 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Nov 07 08:03:46 2006 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Nov 07 09:33:47 2006 +0100
@@ -27,9 +27,27 @@
   left_distrib: "(a + b) * c = a * c + b * c"
   right_distrib: "a * (b + c) = a * b + a * c"
 
-axclass semiring_0 \<subseteq> semiring, comm_monoid_add
+axclass mult_zero \<subseteq> times, zero
+  mult_zero_left [simp]: "0 * a = 0"
+  mult_zero_right [simp]: "a * 0 = 0"
+
+axclass semiring_0 \<subseteq> semiring, comm_monoid_add, mult_zero
+
+axclass semiring_0_cancel \<subseteq> semiring, comm_monoid_add, cancel_ab_semigroup_add
 
-axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
+instance semiring_0_cancel \<subseteq> semiring_0
+proof
+  fix a :: 'a
+  have "0 * a + 0 * a = 0 * a + 0"
+    by (simp add: left_distrib [symmetric])
+  thus "0 * a = 0"
+    by (simp only: add_left_cancel)
+
+  have "a * 0 + a * 0 = a * 0 + 0"
+    by (simp add: right_distrib [symmetric])
+  thus "a * 0 = 0"
+    by (simp only: add_left_cancel)
+qed
 
 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
   distrib: "(a + b) * c = a * c + b * c"
@@ -44,14 +62,16 @@
   finally show "a * (b + c) = a * b + a * c" by blast
 qed
 
-axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add
+axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add, mult_zero
 
 instance comm_semiring_0 \<subseteq> semiring_0 ..
 
-axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
+axclass comm_semiring_0_cancel \<subseteq> comm_semiring, comm_monoid_add, cancel_ab_semigroup_add
 
 instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
 
+instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
+
 axclass zero_neq_one \<subseteq> zero, one
   zero_neq_one [simp]: "0 \<noteq> 1"
 
@@ -64,31 +84,37 @@
 axclass no_zero_divisors \<subseteq> zero, times
   no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
-axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
+axclass semiring_1_cancel \<subseteq> semiring, comm_monoid_add, zero_neq_one, cancel_ab_semigroup_add, monoid_mult
 
 instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
 
-axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
+instance semiring_1_cancel \<subseteq> semiring_1 ..
+
+axclass comm_semiring_1_cancel \<subseteq> 
+  comm_semiring, comm_monoid_add, comm_monoid_mult,
+  zero_neq_one, cancel_ab_semigroup_add
 
 instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
 
 instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
 
+instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
+
 axclass ring \<subseteq> semiring, ab_group_add
 
 instance ring \<subseteq> semiring_0_cancel ..
 
-axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
+axclass comm_ring \<subseteq> comm_semiring, ab_group_add
 
 instance comm_ring \<subseteq> ring ..
 
 instance comm_ring \<subseteq> comm_semiring_0_cancel ..
 
-axclass ring_1 \<subseteq> ring, semiring_1
+axclass ring_1 \<subseteq> ring, zero_neq_one, monoid_mult
 
 instance ring_1 \<subseteq> semiring_1_cancel ..
 
-axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
+axclass comm_ring_1 \<subseteq> comm_ring, zero_neq_one, comm_monoid_mult (* previously ring *)
 
 instance comm_ring_1 \<subseteq> ring_1 ..
 
@@ -115,22 +141,6 @@
 instance field \<subseteq> division_ring
 by (intro_classes, erule field_left_inverse, erule field_right_inverse)
 
-lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
-proof -
-  have "0*a + 0*a = 0*a + 0"
-    by (simp add: left_distrib [symmetric])
-  thus ?thesis 
-    by (simp only: add_left_cancel)
-qed
-
-lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
-proof -
-  have "a*0 + a*0 = a*0 + 0"
-    by (simp add: right_distrib [symmetric])
-  thus ?thesis 
-    by (simp only: add_left_cancel)
-qed
-
 lemma field_mult_eq_0_iff [simp]:
   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
 proof cases
@@ -182,15 +192,22 @@
 by (simp add: left_distrib diff_minus 
               minus_mult_left [symmetric] minus_mult_right [symmetric]) 
 
-axclass pordered_semiring \<subseteq> semiring_0, pordered_ab_semigroup_add 
+axclass mult_mono \<subseteq> times, zero, ord
   mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
   mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
 
-axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
+axclass pordered_semiring \<subseteq> mult_mono, semiring_0, pordered_ab_semigroup_add 
+
+axclass pordered_cancel_semiring \<subseteq> 
+  mult_mono, pordered_ab_semigroup_add,
+  semiring, comm_monoid_add, 
+  pordered_ab_semigroup_add, cancel_ab_semigroup_add
 
 instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
 
-axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
+instance pordered_cancel_semiring \<subseteq> pordered_semiring .. 
+
+axclass ordered_semiring_strict \<subseteq> semiring, comm_monoid_add, ordered_cancel_ab_semigroup_add
   mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 
@@ -204,18 +221,30 @@
 apply (simp add: mult_strict_right_mono)
 done
 
-axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add
+axclass mult_mono1 \<subseteq> times, zero, ord
   mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
 
-axclass pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring, cancel_ab_semigroup_add
+axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add, mult_mono1
 
+axclass pordered_cancel_comm_semiring \<subseteq> 
+  comm_semiring_0_cancel, pordered_ab_semigroup_add, mult_mono1
+  
 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
 
 axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
   mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
 
 instance pordered_comm_semiring \<subseteq> pordered_semiring
-by (intro_classes, insert mult_mono, simp_all add: mult_commute, blast+)
+proof
+  fix a b c :: 'a
+  assume A: "a <= b" "0 <= c"
+  with mult_mono show "c * a <= c * b" .
+
+  from mult_commute have "a * c = c * a" ..
+  also from mult_mono A have "\<dots> <= c * b" .
+  also from mult_commute have "c * b = b * c" ..
+  finally show "a * c <= b * c" .
+qed
 
 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..
 
@@ -229,12 +258,10 @@
 apply (auto simp add: mult_strict_left_mono order_le_less)
 done
 
-axclass pordered_ring \<subseteq> ring, pordered_semiring 
+axclass pordered_ring \<subseteq> ring, pordered_cancel_semiring 
 
 instance pordered_ring \<subseteq> pordered_ab_group_add ..
 
-instance pordered_ring \<subseteq> pordered_cancel_semiring ..
-
 axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
 
 instance lordered_ring \<subseteq> lordered_ab_group_meet ..