--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
- inverse :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
+ invers :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
one :: 'a ("\<unit>")
text {*
@@ -66,8 +66,8 @@
\noindent Class @{text group} inherits associativity of @{text \<odot>}
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 \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"}
- is even commutative.
+ for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
+ \<tau>"} 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 "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> 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 "(\<alpha>\<^sub>1, \<dots>,
+ \<alpha>\<^sub>n) t \<Colon> 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 \<odot>} operation, identity as @{text \<inv>}, and
@@ -296,8 +296,8 @@
text {*
It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
- and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times> 'b"}.
- Hence the binary type constructor @{text \<odot>} maps semigroups to
+ and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
+ 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups to
semigroups. This may be established formally as follows.
*}
--- 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 \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
may be constrained by type classes (or even general sorts) in an
arbitrary way. Note that by default, in Isabelle/HOL the declaration
- @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for
- @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the
- universal class of HOL, this is not really a constraint at all.
+ @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for @{text "\<odot>
+ \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> '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 "\<odot> \<Colon> 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring
- @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} anyway? In this particular case
- where @{text "product \<equiv> 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 "\<odot> \<Colon>
+ 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"}
+ anyway? In this particular case where @{text "product \<equiv> 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 \<odot>} on some type @{text \<tau>} are rejected by the
--- 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
--- 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