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