# HG changeset patch
# User Rene Thiemann
# Date 1427697178 7200
# Mon Mar 30 08:32:58 2015 +0200
# Node ID 7c4e571423f87cd6363a507c07737780e7a91aca
# Parent db0b87085c168d028a394c5fc011d4c3f4a678de
added locale for semirings
diff r db0b87085c16 r 7c4e571423f8 src/HOL/Algebra/Ring.thy
 a/src/HOL/Algebra/Ring.thy Tue Mar 24 23:39:42 2015 +0100
+++ b/src/HOL/Algebra/Ring.thy Mon Mar 30 08:32:58 2015 +0200
@@ 226,11 +226,19 @@
subsection {* Rings: Basic Definitions *}
locale ring = abelian_group R + monoid R for R (structure) +
+locale semiring = abelian_monoid R + monoid R for R (structure) +
assumes l_distr: "[ x \ carrier R; y \ carrier R; z \ carrier R ]
==> (x \ y) \ z = x \ z \ y \ z"
and r_distr: "[ x \ carrier R; y \ carrier R; z \ carrier R ]
==> z \ (x \ y) = z \ x \ z \ y"
+ and l_null[simp]: "x \ carrier R ==> \ \ x = \"
+ and r_null[simp]: "x \ carrier R ==> x \ \ = \"
+
+locale ring = abelian_group R + monoid R for R (structure) +
+ assumes "[ x \ carrier R; y \ carrier R; z \ carrier R ]
+ ==> (x \ y) \ z = x \ z \ y \ z"
+ and "[ x \ carrier R; y \ carrier R; z \ carrier R ]
+ ==> z \ (x \ y) = z \ x \ z \ y"
locale cring = ring + comm_monoid R
@@ 336,26 +344,24 @@
The following proofs are from Jacobson, Basic Algebra I, pp.~8889.
*}
lemma l_null [simp]:
 "x \ carrier R ==> \ \ x = \"
+sublocale semiring
proof 
 assume R: "x \ carrier R"
 then have "\ \ x \ \ \ x = (\ \ \) \ x"
 by (simp add: l_distr del: l_zero r_zero)
 also from R have "... = \ \ x \ \" by simp
 finally have "\ \ x \ \ \ x = \ \ x \ \" .
 with R show ?thesis by (simp del: r_zero)
qed

lemma r_null [simp]:
 "x \ carrier R ==> x \ \ = \"
proof 
 assume R: "x \ carrier R"
 then have "x \ \ \ x \ \ = x \ (\ \ \)"
 by (simp add: r_distr del: l_zero r_zero)
 also from R have "... = x \ \ \ \" by simp
 finally have "x \ \ \ x \ \ = x \ \ \ \" .
 with R show ?thesis by (simp del: r_zero)
+ note [simp] = ring_axioms[unfolded ring_def ring_axioms_def]
+ show "semiring R"
+ proof (unfold_locales)
+ fix x
+ assume R: "x \ carrier R"
+ then have "\ \ x \ \ \ x = (\ \ \) \ x"
+ by (simp del: l_zero r_zero)
+ also from R have "... = \ \ x \ \" by simp
+ finally have "\ \ x \ \ \ x = \ \ x \ \" .
+ with R show "\ \ x = \" by (simp del: r_zero)
+ from R have "x \ \ \ x \ \ = x \ (\ \ \)"
+ by (simp del: l_zero r_zero)
+ also from R have "... = x \ \ \ \" by simp
+ finally have "x \ \ \ x \ \ = x \ \ \ \" .
+ with R show "x \ \ = \" by (simp del: r_zero)
+ qed auto
qed
lemma l_minus:
@@ 401,6 +407,12 @@
Scan.succeed (SIMPLE_METHOD' o Ringsimp.algebra_tac)
*} "normalisation of algebraic structure"
+lemmas (in semiring) semiring_simprules
+ [algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
+ a_closed zero_closed m_closed one_closed
+ a_assoc l_zero a_comm m_assoc l_one l_distr r_zero
+ a_lcomm r_distr l_null r_null
+
lemmas (in ring) ring_simprules
[algebra ring "zero R" "add R" "a_inv R" "a_minus R" "one R" "mult R"] =
a_closed zero_closed a_inv_closed minus_closed m_closed one_closed
@@ 419,11 +431,11 @@
r_zero r_neg r_neg2 r_neg1 minus_add minus_minus minus_zero
a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
lemma (in cring) nat_pow_zero:
+lemma (in semiring) nat_pow_zero:
"(n::nat) ~= 0 ==> \ (^) n = \"
by (induct n) simp_all
context ring begin
+context semiring begin
lemma one_zeroD:
assumes onezero: "\ = \"
@@ 482,7 +494,7 @@
subsubsection {* Sums over Finite Sets *}
lemma (in ring) finsum_ldistr:
+lemma (in semiring) finsum_ldistr:
"[ finite A; a \ carrier R; f \ A > carrier R ] ==>
finsum R f A \ a = finsum R (%i. f i \ a) A"
proof (induct set: finite)
@@ 491,7 +503,7 @@
case (insert x F) then show ?case by (simp add: Pi_def l_distr)
qed
lemma (in ring) finsum_rdistr:
+lemma (in semiring) finsum_rdistr:
"[ finite A; a \ carrier R; f \ A > carrier R ] ==>
a \ finsum R f A = finsum R (%i. a \ f i) A"
proof (induct set: finite)