--- 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*}
--- 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%
%
--- 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}