diff -r fc7841f31388 -r 813fabceec00 doc-src/AxClass/generated/Group.tex --- a/doc-src/AxClass/generated/Group.tex Mon May 22 10:31:44 2000 +0200 +++ b/doc-src/AxClass/generated/Group.tex Mon May 22 11:56:55 2000 +0200 @@ -3,13 +3,13 @@ \isamarkupheader{Basic group theory} \isacommand{theory}~Group~=~Main:% \begin{isamarkuptext}% -\medskip\noindent The meta type system of Isabelle supports +\medskip\noindent The meta-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.% + general groups and Abelian groups.% \end{isamarkuptext}% % \isamarkupsubsection{Monoids and Groups} @@ -42,9 +42,9 @@ % \begin{isamarkuptext}% \medskip Independently of $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 the class - name; thus we may re-use common names such as $assoc$.% + 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 $assoc$.% \end{isamarkuptext}% \isacommand{axclass}\isanewline ~~semigroup~<~{"}term{"}\isanewline @@ -53,14 +53,14 @@ \isacommand{axclass}\isanewline ~~group~<~semigroup\isanewline ~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline -~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline +~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline \isanewline \isacommand{axclass}\isanewline ~~agroup~<~group\isanewline ~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}% \begin{isamarkuptext}% \noindent Class $group$ inherits associativity of $\TIMES$ from - $semigroup$ and adds the other two group axioms. Similarly, $agroup$ + $semigroup$ and adds two further group axioms. Similarly, $agroup$ is defined as the subset of $group$ such that for all of its elements $\tau$, the operation $\TIMES :: \tau \To \tau \To \tau$ is even commutative.% @@ -71,8 +71,8 @@ \begin{isamarkuptext}% In a sense, axiomatic type classes may be viewed as \emph{abstract theories}. Above class definitions gives rise to abstract axioms - $assoc$, $left_unit$, $left_inverse$, $commute$, where all of these - contain type a variable $\alpha :: c$ that is restricted to types of + $assoc$, $left_unit$, $left_inverse$, $commute$, where any of these + contain a type variable $\alpha :: c$ that is restricted to types of the corresponding class $c$. \emph{Sort constraints} like this express a logical precondition for the whole formula. For example, $assoc$ states that for all $\tau$, provided that $\tau :: @@ -83,13 +83,13 @@ 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 - laws of general groups.% + well-known laws of general groups.% \end{isamarkuptext}% \isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline \isacommand{proof}~-\isanewline ~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline ~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~({\isasymunit}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline +~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline ~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline ~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline ~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline @@ -138,7 +138,8 @@ as an axiom, but for groups both $right_unit$ and $right_inverse$ are derivable from the other axioms. With $group_right_unit$ derived as a theorem of group theory (see page~\pageref{thm:group-right-unit}), - we may now instantiate $group \subseteq monoid$ properly as follows + we may now instantiate $monoid \subseteq semigroup$ and $group + \subseteq monoid$ properly as follows (cf.\ \figref{fig:monoid-group}). \begin{figure}[htbp] @@ -166,13 +167,7 @@ \caption{Monoids and groups: according to definition, and by proof} \label{fig:monoid-group} \end{center} - \end{figure} - - We know by definition that $\TIMES$ is associative for monoids, i.e.\ - $monoid \subseteq semigroup$. Furthermore we have $assoc$, - $left_unit$ and $right_unit$ for groups (where $right_unit$ is - derivable from the group axioms), that is $group \subseteq monoid$. - Thus we may establish the following class instantiations.% + \end{figure}% \end{isamarkuptext}% \isacommand{instance}~monoid~<~semigroup\isanewline \isacommand{proof}~intro\_classes\isanewline @@ -193,14 +188,19 @@ \isacommand{qed}% \begin{isamarkuptext}% \medskip The $\isakeyword{instance}$ command sets up an appropriate - goal that represents the class inclusion (or type arity) to be proven + goal that represents the class inclusion (or type arity, see + \secref{sec:inst-arity}) to be proven (see also \cite{isabelle-isar-ref}). The $intro_classes$ proof method does back-chaining of class membership statements wrt.\ the hierarchy of any classes defined in the current theory; the effect is - to reduce to any logical class axioms as subgoals.% + 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. + + any logical class axioms as subgoals.% \end{isamarkuptext}% % -\isamarkupsubsection{Concrete instantiation} +\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}} % \begin{isamarkuptext}% So far we have covered the case of the form @@ -212,11 +212,9 @@ class membership may be established at the logical level and then transferred to Isabelle's type signature level. - \medskip - - As an typical example, we show that type $bool$ with exclusive-or as - operation $\TIMES$, identity as $\isasyminv$, and $False$ as $1$ - forms an Abelian group.% + \medskip As a typical example, we show that type $bool$ with + exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and + $False$ as $1$ forms an Abelian group.% \end{isamarkuptext}% \isacommand{defs}\isanewline ~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline @@ -224,12 +222,12 @@ ~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}% \begin{isamarkuptext}% \medskip It is important to note that above $\DEFS$ are just - overloaded meta-level constant definitions. In particular, 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 of proper - definitional extensions in any version of HOL - \cite{Wenzel:1997:TPHOL}. Nevertheless, overloaded definitions are + 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 $\DEFS$ of the generic group @@ -239,25 +237,25 @@ \isacommand{instance}~bool~::~agroup\isanewline \isacommand{proof}~(intro\_classes,\isanewline ~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline -~~\isacommand{fix}~x~y~z~::~bool\isanewline +~~\isacommand{fix}~x~y~z\isanewline ~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline ~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline ~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline ~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline \isacommand{qed}% \begin{isamarkuptext}% -The result of $\isakeyword{instance}$ is both expressed as a theorem - of Isabelle's meta-logic, and a type arity statement of the type - signature. The latter enables the type-inference system to take care - of this new instance automatically. +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 In a similarly fashion, we could also instantiate our group - theory classes to many other concrete types. For example, $int :: - agroup$ (e.g.\ by defining $\TIMES$ as addition, $\isasyminv$ as - negation and $1$ as zero) or $list :: (term)semigroup$ (e.g.\ if - $\TIMES$ is defined as list append). Thus, the characteristic - constants $\TIMES$, $\isasyminv$, $1$ really become overloaded, i.e.\ - have different meanings on different types.% + \medskip We could now also instantiate our group theory classes to + many other concrete types. For example, $int :: agroup$ (e.g.\ by + defining $\TIMES$ as addition, $\isasyminv$ as negation and $1$ as + zero) or $list :: (term)semigroup$ (e.g.\ if $\TIMES$ is defined as + list append). Thus, the characteristic constants $\TIMES$, + $\isasyminv$, $1$ really become overloaded, i.e.\ have different + meanings on different types.% \end{isamarkuptext}% % \isamarkupsubsection{Lifting and Functors} @@ -271,20 +269,19 @@ This feature enables us to \emph{lift operations}, say to Cartesian products, direct sums or function spaces. Subsequently we lift - $\TIMES$ component-wise to binary Cartesian products $\alpha \times - \beta$.% + $\TIMES$ component-wise to binary products $\alpha \times \beta$.% \end{isamarkuptext}% \isacommand{defs}\isanewline -~~prod\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}% +~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}% \begin{isamarkuptext}% -It is very easy to see that associativity of $\TIMES^\alpha$, +It is very easy to see that associativity of $\TIMES^\alpha$ and $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence the binary type constructor $\times$ maps semigroups to semigroups. This may be established formally as follows.% \end{isamarkuptext}% \isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline -\isacommand{proof}~(intro\_classes,~unfold~prod\_prod\_def)\isanewline -~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~*~'b{\isasymColon}semigroup{"}\isanewline +\isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline +~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline ~~\isacommand{show}\isanewline ~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline ~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline @@ -294,8 +291,8 @@ \isacommand{qed}% \begin{isamarkuptext}% Thus, if we view class instances as ``structures'', then overloaded - constant definitions with primitive recursion over types indirectly - provide some kind of ``functors'' --- i.e.\ mappings between abstract + constant definitions with recursion over types indirectly provide + some kind of ``functors'' --- i.e.\ mappings between abstract theories.% \end{isamarkuptext}% \isacommand{end}\end{isabelle}%