src/HOL/Algebra/Ring.thy
 changeset 27611 2c01c0bdb385 parent 26202 51f8a696cd8d child 27699 489e3f33af0e
```     1.1 --- a/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:02:10 2008 +0200
1.2 +++ b/src/HOL/Algebra/Ring.thy	Tue Jul 15 16:50:09 2008 +0200
1.3 @@ -539,16 +539,26 @@
1.4  text {* Two examples for use of method algebra *}
1.5
1.6  lemma
1.7 -  includes ring R + cring S
1.8 -  shows "[| a \<in> carrier R; b \<in> carrier R; c \<in> carrier S; d \<in> carrier S |] ==>
1.9 -  a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
1.10 -  by algebra
1.11 +  fixes R (structure) and S (structure)
1.12 +  assumes "ring R" "cring S"
1.13 +  assumes RS: "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier S" "d \<in> carrier S"
1.14 +  shows "a \<oplus> \<ominus> (a \<oplus> \<ominus> b) = b & c \<otimes>\<^bsub>S\<^esub> d = d \<otimes>\<^bsub>S\<^esub> c"
1.15 +proof -
1.16 +  interpret ring [R] by fact
1.17 +  interpret cring [S] by fact
1.18 +ML_val {* Algebra.print_structures @{context} *}
1.19 +  from RS show ?thesis by algebra
1.20 +qed
1.21
1.22  lemma
1.23 -  includes cring
1.24 -  shows "[| a \<in> carrier R; b \<in> carrier R |] ==> a \<ominus> (a \<ominus> b) = b"
1.25 -  by algebra
1.26 -
1.27 +  fixes R (structure)
1.28 +  assumes "ring R"
1.29 +  assumes R: "a \<in> carrier R" "b \<in> carrier R"
1.30 +  shows "a \<ominus> (a \<ominus> b) = b"
1.31 +proof -
1.32 +  interpret ring [R] by fact
1.33 +  from R show ?thesis by algebra
1.34 +qed
1.35
1.36  subsubsection {* Sums over Finite Sets *}
1.37
```