# HG changeset patch # User wenzelm # Date 1004217222 -7200 # Node ID 828ea309dc21f90e799cdf7fad84cdd5aab9057b # Parent a6608d44a46b69e717c6f7e9026a0fd5eab4d09d updated; diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/Group.tex --- a/doc-src/AxClass/generated/Group.tex Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/Group.tex Sat Oct 27 23:13:42 2001 +0200 @@ -4,7 +4,9 @@ % \isamarkupheader{Basic group theory% } -\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}% +\isamarkuptrue% +\isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip\noindent The meta-level type system of Isabelle supports \emph{intersections} and \emph{inclusions} of type classes. These @@ -14,34 +16,41 @@ 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}\isanewline \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline \ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline -\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}% +\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymunit}{\isachardoublequote}{\isacharparenright}\isamarkupfalse% +% \begin{isamarkuptext}% \noindent Next we define class \isa{monoid} of monoids with operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. 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}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline -\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}% +\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% \noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are specified appropriately, such that \isa{{\isasymodot}} is associative and \isa{{\isasymunit}} 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 @@ -49,24 +58,30 @@ 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}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline \ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline \isanewline +\isamarkupfalse% \isacommand{axclass}\ group\ {\isasymsubseteq}\ semigroup\isanewline \ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline \ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline \isanewline +\isamarkupfalse% \isacommand{axclass}\ agroup\ {\isasymsubseteq}\ group\isanewline -\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}% +\ \ commute{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequote}\isamarkupfalse% +% \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 @@ -84,50 +99,100 @@ ``abstract theorems''. For example, we may now derive the following well-known laws of general groups.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline +\isamarkupfalse% \isacommand{proof}\ {\isacharminus}\isanewline -\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline -\isacommand{qed}% +\ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymunit}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{finally}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline +\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% +% \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}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline +\isamarkupfalse% \isacommand{proof}\ {\isacharminus}\isanewline -\ \ \isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline -\ \ \isacommand{also}\ \isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{finally}\ \isacommand{show}\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isanewline -\isacommand{qed}% +\ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymunit}\ {\isasymodot}\ x{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{finally}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline +\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% +% \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 @@ -165,23 +230,40 @@ \end{center} \end{figure}% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{instance}\ monoid\ {\isasymsubseteq}\ semigroup\isanewline +\isamarkupfalse% \isacommand{proof}\isanewline -\ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}monoid{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ monoid{\isachardot}assoc{\isacharparenright}\isanewline +\isamarkupfalse% \isacommand{qed}\isanewline \isanewline +\isamarkupfalse% \isacommand{instance}\ group\ {\isasymsubseteq}\ monoid\isanewline +\isamarkupfalse% \isacommand{proof}\isanewline -\ \ \isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline -\isacommand{qed}% +\ \ \isamarkupfalse% +\isacommand{fix}\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}group{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ group{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip The $\INSTANCE$ command sets up an appropriate goal that represents the class inclusion (or type arity, see @@ -193,9 +275,11 @@ 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 $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} --- @@ -210,10 +294,12 @@ exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and \isa{False} as \isa{{\isasymunit}} forms an Abelian group.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline \ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequote}\isanewline \ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequote}\isanewline -\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}% +\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymequiv}\ False{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip It is important to note that above $\DEFS$ are just overloaded meta-level constant definitions, where type classes are @@ -228,15 +314,28 @@ operations on type \isa{bool} appropriately, the class membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline +\isamarkupfalse% \isacommand{proof}\ {\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}\ x\ y\ z\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isacommand{by}\ blast\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isacommand{by}\ blast\isanewline -\ \ \isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isacommand{by}\ blast\isanewline -\isacommand{qed}% +\ \ \isamarkupfalse% +\isacommand{fix}\ x\ y\ z\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% +% \begin{isamarkuptext}% The result of an $\INSTANCE$ statement is both expressed as a theorem of Isabelle's meta-logic, and as a type arity of the type signature. @@ -252,9 +351,11 @@ 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 @@ -267,30 +368,41 @@ 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}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline -\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequote}% +\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% \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}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline +\isamarkupfalse% \isacommand{proof}\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline -\ \ \isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline -\ \ \isacommand{show}\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\isanewline \ \ \ \ {\isachardoublequote}{\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}{\isachardoublequote}\isanewline -\ \ \ \ \isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline -\isacommand{qed}% +\ \ \ \ \isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isachardot}assoc{\isacharparenright}\isanewline +\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% +% \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}% -\isacommand{end}\end{isabellebody}% +\isamarkuptrue% +\isacommand{end}\isamarkupfalse% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/NatClass.tex --- a/doc-src/AxClass/generated/NatClass.tex Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/NatClass.tex Sat Oct 27 23:13:42 2001 +0200 @@ -4,7 +4,9 @@ % \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}% } -\isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}% +\isamarkuptrue% +\isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip\noindent Axiomatic type classes abstract over exactly one type argument. Thus, any \emph{axiomatic} theory extension where each @@ -15,11 +17,13 @@ Isabelle/FOL.\footnote{See also \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{consts}\isanewline \ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymzero}{\isachardoublequote}{\isacharparenright}\isanewline \ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline \ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline \isanewline +\isamarkupfalse% \isacommand{axclass}\ nat\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline \ \ induct{\isacharcolon}\ {\isachardoublequote}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequote}\isanewline \ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequote}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline @@ -27,9 +31,11 @@ \ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequote}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequote}\isanewline \ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequote}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline \isanewline +\isamarkupfalse% \isacommand{constdefs}\isanewline \ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline -\ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}% +\ \ {\isachardoublequote}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% This is an abstract version of the plain \isa{Nat} theory in FOL.\footnote{See @@ -55,7 +61,9 @@ re-used with some trivial changes only (mostly adding some type constraints).% \end{isamarkuptext}% -\isacommand{end}\end{isabellebody}% +\isamarkuptrue% +\isacommand{end}\isamarkupfalse% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/Product.tex --- a/doc-src/AxClass/generated/Product.tex Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/Product.tex Sat Oct 27 23:13:42 2001 +0200 @@ -4,7 +4,9 @@ % \isamarkupheader{Syntactic classes% } -\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}% +\isamarkuptrue% +\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip\noindent There is still a feature of Isabelle's type system left that we have not yet discussed. When declaring polymorphic @@ -17,10 +19,13 @@ The \isa{product} class below provides a less degenerate example of syntactic type classes.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{axclass}\isanewline \ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline +\isamarkupfalse% \isacommand{consts}\isanewline -\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}% +\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% +% \begin{isamarkuptext}% Here class \isa{product} is defined as subclass of \isa{term} without any additional axioms. This effects in logical equivalence @@ -49,9 +54,13 @@ This is done for class \isa{product} and type \isa{bool} as follows.% \end{isamarkuptext}% -\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isacommand{{\isachardot}{\isachardot}}\isanewline +\isamarkuptrue% +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\isamarkupfalse% \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline -\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}% +\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made @@ -75,7 +84,9 @@ Isabelle's meta-logic, because there is no internal notion of ``providing operations'' or even ``names of functions''.% \end{isamarkuptext}% -\isacommand{end}\end{isabellebody}% +\isamarkuptrue% +\isacommand{end}\isamarkupfalse% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/Semigroups.tex --- a/doc-src/AxClass/generated/Semigroups.tex Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/Semigroups.tex Sat Oct 27 23:13:42 2001 +0200 @@ -4,7 +4,9 @@ % \isamarkupheader{Semigroups% } -\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}% +\isamarkuptrue% +\isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}\isamarkupfalse% +% \begin{isamarkuptext}% \medskip\noindent An axiomatic type class is simply a class of types that all meet certain properties, which are also called \emph{class @@ -17,10 +19,13 @@ We illustrate these basic concepts by the following formulation of semigroups.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{consts}\isanewline \ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline +\isamarkupfalse% \isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline -\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}% +\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% \noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an @@ -36,15 +41,20 @@ \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.% \end{isamarkuptext}% +\isamarkuptrue% \isacommand{consts}\isanewline \ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline +\isamarkupfalse% \isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline -\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}% +\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse% +% \begin{isamarkuptext}% \noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly not quite the same.% \end{isamarkuptext}% -\isacommand{end}\end{isabellebody}% +\isamarkuptrue% +\isacommand{end}\isamarkupfalse% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/isabelle.sty --- a/doc-src/AxClass/generated/isabelle.sty Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/isabelle.sty Sat Oct 27 23:13:42 2001 +0200 @@ -24,11 +24,12 @@ \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} \newdimen\isa@parindent\newdimen\isa@parskip \newenvironment{isabellebody}{% -\par% +\isamarkuptrue\par% \isa@parindent\parindent\parindent0pt% \isa@parskip\parskip\parskip0pt% \isastyle}{\par} @@ -94,7 +95,8 @@ \newcommand{\isamarkupsubsect}[1]{\subsection{#1}} \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} -\newcommand{\isabeginpar}{\par\medskip} +\newif\ifisamarkup +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} \newcommand{\isaendpar}{\par\medskip} \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}} diff -r a6608d44a46b -r 828ea309dc21 doc-src/AxClass/generated/isabellesym.sty --- a/doc-src/AxClass/generated/isabellesym.sty Sat Oct 27 00:09:59 2001 +0200 +++ b/doc-src/AxClass/generated/isabellesym.sty Sat Oct 27 23:13:42 2001 +0200 @@ -5,16 +5,6 @@ %% definitions of standard Isabelle symbols %% -% Required packages for unusual symbols -- see below for details. -%\usepackage{latexsym} -%\usepackage{amssymb} -%\usepackage[english]{babel} -%\usepackage[latin1]{inputenc} -%\usepackage[only,bigsqcap]{stmaryrd} -%\usepackage{wasysym} -%\usepackage{eufrak} - - % symbol definitions \newcommand{\isasymA}{\isamath{\mathcal{A}}} @@ -219,6 +209,8 @@ \newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires latexsym \newcommand{\isasymturnstile}{\isamath{\vdash}} \newcommand{\isasymTurnstile}{\isamath{\models}} +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} \newcommand{\isasymstileturn}{\isamath{\dashv}} \newcommand{\isasymsurd}{\isamath{\surd}} \newcommand{\isasymle}{\isamath{\le}} @@ -273,10 +265,10 @@ \newcommand{\isasymdiv}{\isamath{\div}} \newcommand{\isasymcdot}{\isamath{\cdot}} \newcommand{\isasymstar}{\isamath{\star}} +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}} +\newcommand{\isasymcirc}{\isamath{\circ}} \newcommand{\isasymdagger}{\isamath{\dagger}} \newcommand{\isasymddagger}{\isamath{\ddagger}} -\newcommand{\isasymcirc}{\isamath{\circ}} -\newcommand{\isasymbullet}{\isamath{\bullet}} \newcommand{\isasymlhd}{\isamath{\lhd}} \newcommand{\isasymrhd}{\isamath{\rhd}} \newcommand{\isasymunlhd}{\isamath{\unlhd}} @@ -347,4 +339,3 @@ \newcommand{\isasymdieresis}{\isatext{\"\relax}} \newcommand{\isasymcedilla}{\isatext{\c\relax}} \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} -