# HG changeset patch # User wenzelm # Date 981401630 -3600 # Node ID 4e542a09b5825e9120d962cf8182068fb1160b33 # Parent cc421547e744d2eef2e6135af8b0768350c33a30 tuned; diff -r cc421547e744 -r 4e542a09b582 doc-src/AxClass/Group/Group.thy --- a/doc-src/AxClass/Group/Group.thy Mon Feb 05 20:14:15 2001 +0100 +++ b/doc-src/AxClass/Group/Group.thy Mon Feb 05 20:33:50 2001 +0100 @@ -22,7 +22,7 @@ consts times :: "'a \ 'a \ 'a" (infixl "\" 70) - inverse :: "'a \ 'a" ("(_\)" [1000] 999) + invers :: "'a \ 'a" ("(_\)" [1000] 999) one :: 'a ("\") text {* @@ -66,8 +66,8 @@ \noindent Class @{text group} inherits associativity of @{text \} from @{text semigroup} and adds two further group axioms. Similarly, @{text agroup} is defined as the subset of @{text group} such that - for all of its elements @{text \}, the operation @{text "\ \ \ \ \ \ \"} - is even commutative. + for all of its elements @{text \}, the operation @{text "\ \ \ \ \ \ + \"} is even commutative. *} @@ -220,10 +220,10 @@ $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}. Even more interesting for practical applications are \emph{concrete instantiations} of axiomatic type - classes. That is, certain simple schemes - @{text "(\\<^sub>1, \, \\<^sub>n) t \ c"} of class membership may be - established at the logical level and then transferred to Isabelle's - type signature level. + classes. That is, certain simple schemes @{text "(\\<^sub>1, \, + \\<^sub>n) t \ 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 @{typ bool} with exclusive-or as @{text \} operation, identity as @{text \}, and @@ -296,8 +296,8 @@ text {* It is very easy to see that associativity of @{text \} on @{typ 'a} - and @{text \} on @{typ 'b} transfers to @{text \} on @{typ "'a \ 'b"}. - Hence the binary type constructor @{text \} maps semigroups to + and @{text \} on @{typ 'b} transfers to @{text \} on @{typ "'a \ + 'b"}. Hence the binary type constructor @{text \} maps semigroups to semigroups. This may be established formally as follows. *} diff -r cc421547e744 -r 4e542a09b582 doc-src/AxClass/Group/Product.thy --- a/doc-src/AxClass/Group/Product.thy Mon Feb 05 20:14:15 2001 +0100 +++ b/doc-src/AxClass/Group/Product.thy Mon Feb 05 20:33:50 2001 +0100 @@ -9,9 +9,9 @@ constants @{text "c \ \"}, the type variables occurring in @{text \} may be constrained by type classes (or even general sorts) in an arbitrary way. Note that by default, in Isabelle/HOL the declaration - @{text "\ \ 'a \ 'a \ 'a"} is actually an abbreviation for - @{text "\ \ 'a\term \ 'a \ 'a"} Since class @{text "term"} is the - universal class of HOL, this is not really a constraint at all. + @{text "\ \ 'a \ 'a \ 'a"} is actually an abbreviation for @{text "\ + \ 'a\term \ 'a \ 'a"} Since class @{text "term"} is the universal + class of HOL, this is not really a constraint at all. The @{text product} class below provides a less degenerate example of syntactic type classes. @@ -28,14 +28,13 @@ of @{text product} and @{text term}, as is reflected by the trivial introduction rule generated for this definition. - \medskip So what is the difference of declaring - @{text "\ \ 'a\product \ 'a \ 'a"} vs.\ declaring - @{text "\ \ 'a\term \ 'a \ 'a"} anyway? In this particular case - where @{text "product \ term"}, it should be obvious that both - declarations are the same from the logic's point of view. It even - makes the most sense to remove sort constraints from constant - declarations, as far as the purely logical meaning is concerned - \cite{Wenzel:1997:TPHOL}. + \medskip So what is the difference of declaring @{text "\ \ + 'a\product \ 'a \ 'a"} vs.\ declaring @{text "\ \ 'a\term \ 'a \ 'a"} + anyway? In this particular case where @{text "product \ term"}, it + should be obvious that both declarations are the same from the + logic's point of view. It even makes the most sense to remove sort + constraints from constant declarations, as far as the purely logical + meaning is concerned \cite{Wenzel:1997:TPHOL}. On the other hand there are syntactic differences, of course. Constants @{text \} on some type @{text \} are rejected by the diff -r cc421547e744 -r 4e542a09b582 doc-src/AxClass/generated/Group.tex --- a/doc-src/AxClass/generated/Group.tex Mon Feb 05 20:14:15 2001 +0100 +++ b/doc-src/AxClass/generated/Group.tex Mon Feb 05 20:33:50 2001 +0100 @@ -24,7 +24,7 @@ \end{isamarkuptext}% \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 -\ \ inverse\ {\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 +\ \ 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}% \begin{isamarkuptext}% \noindent Next we define class \isa{monoid} of monoids with @@ -62,8 +62,7 @@ \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.% + for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.% \end{isamarkuptext}% % \isamarkupsubsection{Abstract reasoning% @@ -203,10 +202,9 @@ $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. + 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 @@ -273,8 +271,7 @@ \ \ 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}% \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 + 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}% \isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline diff -r cc421547e744 -r 4e542a09b582 doc-src/AxClass/generated/Product.tex --- a/doc-src/AxClass/generated/Product.tex Mon Feb 05 20:14:15 2001 +0100 +++ b/doc-src/AxClass/generated/Product.tex Mon Feb 05 20:33:50 2001 +0100 @@ -11,9 +11,8 @@ constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}} may be constrained by type classes (or even general sorts) in an arbitrary way. Note that by default, in Isabelle/HOL the declaration - \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for - \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the - universal class of HOL, this is not really a constraint at all. + \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the universal + class of HOL, this is not really a constraint at all. The \isa{product} class below provides a less degenerate example of syntactic type classes.% @@ -28,14 +27,12 @@ of \isa{product} and \isa{term}, as is reflected by the trivial introduction rule generated for this definition. - \medskip So what is the difference of declaring - \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring - \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway? In this particular case - where \isa{product\ {\isasymequiv}\ term}, it should be obvious that both - declarations are the same from the logic's point of view. It even - makes the most sense to remove sort constraints from constant - declarations, as far as the purely logical meaning is concerned - \cite{Wenzel:1997:TPHOL}. + \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} + anyway? In this particular case where \isa{product\ {\isasymequiv}\ term}, it + should be obvious that both declarations are the same from the + logic's point of view. It even makes the most sense to remove sort + constraints from constant declarations, as far as the purely logical + meaning is concerned \cite{Wenzel:1997:TPHOL}. On the other hand there are syntactic differences, of course. Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the