diff -r b094999e1d33 -r 37f47ea6fed1 doc-src/AxClass/Group/document/Group.tex --- a/doc-src/AxClass/Group/document/Group.tex Thu Feb 26 06:39:06 2009 -0800 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,512 +0,0 @@ -% -\begin{isabellebody}% -\def\isabellecontext{Group}% -% -\isamarkupheader{Basic group theory% -} -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{theory}\isamarkupfalse% -\ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -% -\begin{isamarkuptext}% -\medskip\noindent The meta-level type system of Isabelle supports - \emph{intersections} and \emph{inclusions} of type classes. These - directly correspond to intersections and inclusions of type - predicates in a purely set theoretic sense. This is sufficient as a - means to describe simple hierarchies of structures. As an - illustration, we use the well-known example of semigroups, monoids, - general groups and Abelian groups.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Monoids and Groups% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -First we declare some polymorphic constants required later for the - signature parts of our structures.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\isanewline -\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline -\ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline -\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}% -\begin{isamarkuptext}% -\noindent Next we define class \isa{monoid} of monoids with - operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class - axioms are allowed for user convenience --- they simply represent - the conjunction of their respective universal closures.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{axclass}\isamarkupfalse% -\ monoid\ {\isasymsubseteq}\ type\isanewline -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\noindent So class \isa{monoid} contains exactly those types - \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}} - are specified appropriately, such that \isa{{\isasymodot}} is associative and - \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}} - operation.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\begin{isamarkuptext}% -\medskip Independently of \isa{monoid}, we now define a linear - hierarchy of semigroups, general groups and Abelian groups. Note - that the names of class axioms are automatically qualified with each - class name, so we may re-use common names such as \isa{assoc}.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{axclass}\isamarkupfalse% -\ semigroup\ {\isasymsubseteq}\ type\isanewline -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{axclass}\isamarkupfalse% -\ group\ {\isasymsubseteq}\ semigroup\isanewline -\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\isanewline -\isacommand{axclass}\isamarkupfalse% -\ agroup\ {\isasymsubseteq}\ group\isanewline -\ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}} - from \isa{semigroup} and adds two further group axioms. Similarly, - \isa{agroup} is defined as the subset of \isa{group} such that - for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Abstract reasoning% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -In a sense, axiomatic type classes may be viewed as \emph{abstract - theories}. Above class definitions gives rise to abstract axioms - \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}. \emph{Sort constraints} like this express a logical - precondition for the whole formula. For example, \isa{assoc} - states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative. - - \medskip From a technical point of view, abstract axioms are just - ordinary Isabelle theorems, which may be used in proofs without - special treatment. Such ``abstract proofs'' usually yield new - ``abstract theorems''. For example, we may now derive the following - well-known laws of general groups.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{finally}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established - much easier.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{theorem}\isamarkupfalse% -\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\isamarkupfalse% -\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{finally}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse% -\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\medskip Abstract theorems may be instantiated to only those types - \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is - known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Abstract instantiation% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -From the definition, the \isa{monoid} and \isa{group} classes - have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} - had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other - axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group - theory (see page~\pageref{thm:group-right-unit}), we may now - instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}). - - \begin{figure}[htbp] - \begin{center} - \small - \unitlength 0.6mm - \begin{picture}(65,90)(0,-10) - \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} - \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}} - \put(15,5){\makebox(0,0){\isa{agroup}}} - \put(15,25){\makebox(0,0){\isa{group}}} - \put(15,45){\makebox(0,0){\isa{semigroup}}} - \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}} - \end{picture} - \hspace{4em} - \begin{picture}(30,90)(0,0) - \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}} - \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}} - \put(15,5){\makebox(0,0){\isa{agroup}}} - \put(15,25){\makebox(0,0){\isa{group}}} - \put(15,45){\makebox(0,0){\isa{monoid}}} - \put(15,65){\makebox(0,0){\isa{semigroup}}} - \put(15,85){\makebox(0,0){\isa{type}}} - \end{picture} - \caption{Monoids and groups: according to definition, and by proof} - \label{fig:monoid-group} - \end{center} - \end{figure}% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{instance}\isamarkupfalse% -\ monoid\ {\isasymsubseteq}\ semigroup\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\isacommand{instance}\isamarkupfalse% -\ group\ {\isasymsubseteq}\ monoid\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -\medskip The \isakeyword{instance} command sets up an appropriate - goal that represents the class inclusion (or type arity, see - \secref{sec:inst-arity}) to be proven (see also - \cite{isabelle-isar-ref}). The initial proof step causes - back-chaining of class membership statements wrt.\ the hierarchy of - any classes defined in the current theory; the effect is to reduce - to the initial statement to a number of goals that directly - correspond to any class axioms encountered on the path upwards - through the class hierarchy.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -So far we have covered the case of the form - \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely - \emph{abstract instantiation} --- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance of \isa{c\isactrlsub {\isadigit{2}}}. Even more - interesting for practical applications are \emph{concrete - instantiations} of axiomatic type classes. That is, certain simple - schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class - membership may be established at the logical level and then - transferred to Isabelle's type signature level. - - \medskip As a typical example, we show that type \isa{bool} with - exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and - \isa{False} as \isa{{\isasymone}} forms an Abelian group.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{defs}\isamarkupfalse% -\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline -\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline -\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\medskip It is important to note that above \isakeyword{defs} are - just overloaded meta-level constant definitions, where type classes - are not yet involved at all. This form of constant definition with - overloading (and optional recursion over the syntactic structure of - simple types) are admissible as definitional extensions of plain HOL - \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not - required for overloading. Nevertheless, overloaded definitions are - best applied in the context of type classes. - - \medskip Since we have chosen above \isakeyword{defs} of the generic - group operations on type \isa{bool} appropriately, the class - membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{instance}\isamarkupfalse% -\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline -\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ x\ y\ z\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ blast\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -The result of an \isakeyword{instance} statement is both expressed - as a theorem of Isabelle's meta-logic, and as a type arity of the - type signature. The latter enables type-inference system to take - care of this new instance automatically. - - \medskip We could now also instantiate our group theory classes to - many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup} - (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation - and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup} - (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the - characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}} - really become overloaded, i.e.\ have different meanings on different - types.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isamarkupsubsection{Lifting and Functors% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -As already mentioned above, overloading in the simply-typed HOL - systems may include recursion over the syntactic structure of types. - That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also - contain constants of name \isa{c} on the right-hand side --- if - these have types that are structurally simpler than \isa{{\isasymtau}}. - - This feature enables us to \emph{lift operations}, say to Cartesian - products, direct sums or function spaces. Subsequently we lift - \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{defs}\isamarkupfalse% -\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline -\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequoteclose}% -\begin{isamarkuptext}% -It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a} - and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups - to semigroups. This may be established formally as follows.% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{instance}\isamarkupfalse% -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% -\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline -\ \ \isacommand{show}\isamarkupfalse% -\isanewline -\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline -\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline -\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline -\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{by}\isamarkupfalse% -\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline -\isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -Thus, if we view class instances as ``structures'', then overloaded - constant definitions with recursion over types indirectly provide - some kind of ``functors'' --- i.e.\ mappings between abstract - theories.% -\end{isamarkuptext}% -\isamarkuptrue% -% -\isadelimtheory -% -\endisadelimtheory -% -\isatagtheory -\isacommand{end}\isamarkupfalse% -% -\endisatagtheory -{\isafoldtheory}% -% -\isadelimtheory -% -\endisadelimtheory -\isanewline -\end{isabellebody}% -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "root" -%%% End: