# HG changeset patch # User haftmann # Date 1245229214 -7200 # Node ID 358cdcdf56d2f2ce48183740e6f90c8ec7b990b8 # Parent 127e8a8b8cde6806beb8efc1ea373572d6aa493b corrected some issues diff -r 127e8a8b8cde -r 358cdcdf56d2 doc-src/TutorialI/Types/Axioms.thy --- a/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 10:34:02 2009 +0200 +++ b/doc-src/TutorialI/Types/Axioms.thy Wed Jun 17 11:00:14 2009 +0200 @@ -13,8 +13,7 @@ subsubsection {* Semigroups *} -text{* We specify \emph{semigroups} as subclass of @{class plus} -where certain axioms need to hold: *} +text{* We specify \emph{semigroups} as subclass of @{class plus}: *} class semigroup = plus + assumes assoc: "(x \ y) \ z = x \ (y \ z)" @@ -35,8 +34,8 @@ "'a"} restricts instantiations of @{typ "'a"} to types of class @{class semigroup} and during the proof enables us to use the fact @{fact assoc} whose type parameter is itself constrained to class -@{class semigroup}. The main advantage is that theorems can be proved -in the abstract and freely reused for each instance. +@{class semigroup}. The main advantage of classes is that theorems +can be proved in the abstract and freely reused for each instance. On instantiation, we have to give a proof that the given operations obey the class axioms: *} @@ -107,7 +106,7 @@ end -text {* \noindent Unless in the above examples, we here have both +text {* \noindent In contrast to the examples above, we here have both specification of class operations and a non-trivial instance proof. This covers products as well: diff -r 127e8a8b8cde -r 358cdcdf56d2 doc-src/TutorialI/Types/Overloading.thy --- a/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 10:34:02 2009 +0200 +++ b/doc-src/TutorialI/Types/Overloading.thy Wed Jun 17 11:00:14 2009 +0200 @@ -16,7 +16,7 @@ text {* \noindent This introduces a new class @{class [source] plus}, along with a constant @{const [source] plus} with nice infix syntax. @{const [source] plus} is also named \emph{class operation}. The type -of @{const [source] plus} carries a sort constraint @{typ [source] "'a +of @{const [source] plus} carries a class constraint @{typ [source] "'a :: plus"} on its type variable, meaning that only types of class @{class [source] plus} can be instantiated for @{typ [source] "'a"}. To breathe life into @{class [source] plus} we need to declare a type diff -r 127e8a8b8cde -r 358cdcdf56d2 doc-src/TutorialI/Types/document/Axioms.tex --- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 10:34:02 2009 +0200 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jun 17 11:00:14 2009 +0200 @@ -36,8 +36,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -We specify \emph{semigroups} as subclass of \isa{plus} -where certain axioms need to hold:% +We specify \emph{semigroups} as subclass of \isa{plus}:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{class}\isamarkupfalse% @@ -75,8 +74,8 @@ \noindent The \isa{semigroup} constraint on type \isa{{\isacharprime}a} restricts instantiations of \isa{{\isacharprime}a} to types of class \isa{semigroup} and during the proof enables us to use the fact \hyperlink{fact.assoc}{\mbox{\isa{assoc}}} whose type parameter is itself constrained to class -\isa{semigroup}. The main advantage is that theorems can be proved -in the abstract and freely reused for each instance. +\isa{semigroup}. The main advantage of classes is that theorems +can be proved in the abstract and freely reused for each instance. On instantiation, we have to give a proof that the given operations obey the class axioms:% @@ -220,7 +219,7 @@ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% -\noindent Unless in the above examples, we here have both +\noindent In contrast to the examples above, we here have both specification of class operations and a non-trivial instance proof. This covers products as well:% diff -r 127e8a8b8cde -r 358cdcdf56d2 doc-src/TutorialI/Types/document/Overloading.tex --- a/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 10:34:02 2009 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jun 17 11:00:14 2009 +0200 @@ -37,7 +37,7 @@ \noindent This introduces a new class \isa{plus}, along with a constant \isa{plus} with nice infix syntax. \isa{plus} is also named \emph{class operation}. The type -of \isa{plus} carries a sort constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class +of \isa{plus} carries a class constraint \isa{{\isachardoublequote}{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ plus{\isachardoublequote}} on its type variable, meaning that only types of class \isa{plus} can be instantiated for \isa{{\isachardoublequote}{\isacharprime}a{\isachardoublequote}}. To breathe life into \isa{plus} we need to declare a type to be an \bfindex{instance} of \isa{plus}:% diff -r 127e8a8b8cde -r 358cdcdf56d2 doc-src/TutorialI/Types/numerics.tex --- a/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 10:34:02 2009 +0200 +++ b/doc-src/TutorialI/Types/numerics.tex Wed Jun 17 11:00:14 2009 +0200 @@ -1,4 +1,3 @@ -% $Id$ \section{Numbers} \label{sec:numbers} @@ -82,14 +81,14 @@ \end{warn} \begin{warn} -\index{recdef@\isacommand {recdef} (command)!and numeric literals} +\index{function@\isacommand {function} (command)!and numeric literals} Numeric literals are not constructors and therefore must not be used in patterns. For example, this declaration is rejected: \begin{isabelle} -\isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline +\isacommand{function}\ h\ \isakeyword{where}\isanewline "h\ 3\ =\ 2"\isanewline -"h\ i\ \ =\ i" +\isacharbar "h\ i\ \ =\ i" \end{isabelle} You should use a conditional expression instead: @@ -531,7 +530,7 @@ \subsubsection{Raising to a Power} -Another type class, \tcdx{ringppower}, specifies rings that also have +Another type class, \tcdx{ordered\_idom}, specifies rings that also have exponentation to a natural number power, defined using the obvious primitive recursion. Theory \thydx{Power} proves various theorems, such as the following.