# HG changeset patch
# User paulson
# Date 1182865689 -7200
# Node ID 2b2323124e8e1bda77c0d59d068203a6a3dc6ac9
# Parent  234b83011a9b6c2c3b1793096de5b26cc8322646
changes for type class ring_no_zero_divisors

diff -r 234b83011a9b -r 2b2323124e8e doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 13:02:28 2007 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Tue Jun 26 15:48:09 2007 +0200
@@ -246,12 +246,18 @@
 
 @{thm[display] mult_cancel_right[no_vars]}
 \rulename{mult_cancel_right}
+
+@{thm[display] mult_cancel_left[no_vars]}
+\rulename{mult_cancel_left}
 *}
 
 ML{*set show_sorts*}
 
 text{*
 effect of show sorts on the above
+
+@{thm[display] mult_cancel_left[no_vars]}
+\rulename{mult_cancel_left}
 *}
 
 ML{*reset show_sorts*}
diff -r 234b83011a9b -r 2b2323124e8e doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Jun 26 13:02:28 2007 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Jun 26 15:48:09 2007 +0200
@@ -543,9 +543,9 @@
 \rulename{mult_cancel_right}
 
 \begin{isabelle}%
-{\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
+{\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
 \end{isabelle}
-\rulename{field_mult_cancel_right}%
+\rulename{mult_cancel_left}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -567,11 +567,11 @@
 effect of show sorts on the above
 
 \begin{isabelle}%
-{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharequal}\isanewline
-\isaindent{{\isacharparenleft}}{\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline
-{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
+{\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
+\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
 \end{isabelle}
-\rulename{field_mult_cancel_right}%
+\rulename{mult_cancel_left}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 234b83011a9b -r 2b2323124e8e doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Tue Jun 26 13:02:28 2007 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Tue Jun 26 15:48:09 2007 +0200
@@ -419,26 +419,23 @@
 Obviously, all properties involving orderings required an ordered
 structure.
 
-The following two theorems are less obvious. Although they
-mention no ordering, they require an ordered ring. However, if we have a 
-field, then an ordering is no longer required.
+The class \tcdx{ring_no_zero_divisors} of rings without zero divisors satisfies a number of natural cancellation laws, the first of which characterizes this class:
 \begin{isabelle}
 (a\ *\ b\ =\ (0::'a))\ =\ (a\ =\ (0::'a)\ \isasymor \ b\ =\ (0::'a))
 \rulename{mult_eq_0_iff}\isanewline
 (a\ *\ c\ =\ b\ *\ c)\ =\ (c\ =\ (0::'a)\ \isasymor \ a\ =\ b)
 \rulename{mult_cancel_right}
 \end{isabelle}
-Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
-express the same properties, only for fields.
 \begin{pgnote}
 Setting the flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$
 \pgmenu{Show Sorts} will display the type classes of all type variables.
 \end{pgnote}
 \noindent
-Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
+Here is how the theorem \isa{mult_cancel_left} appears with the flag set.
 \begin{isabelle}
-((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
-(c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
+((c::'a::ring_no_zero_divisors)\ *\ (a::'a::ring_no_zero_divisors) =\isanewline
+\ c\ *\ (b::'a::ring_no_zero_divisors))\ =\isanewline
+(c\ =\ (0::'a::ring_no_zero_divisors)\ \isasymor\ a\ =\ b)
 \end{isabelle}