--- a/doc-src/AxClass/Group/ROOT.ML Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Group/ROOT.ML Mon May 22 10:31:44 2000 +0200
@@ -1,5 +1,4 @@
-use_thy "Semigroup";
use_thy "Semigroups";
use_thy "Group";
use_thy "Product";
--- a/doc-src/AxClass/Group/Semigroup.thy Mon May 22 10:02:58 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-theory Semigroup = Main:;
-
-consts
- times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 70);
-axclass
- semigroup < "term"
- assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
-
-end;
\ No newline at end of file
--- a/doc-src/AxClass/Group/Semigroups.thy Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Group/Semigroups.thy Mon May 22 10:31:44 2000 +0200
@@ -1,19 +1,54 @@
+
+header {* Semigroups *};
+
theory Semigroups = Main:;
-constdefs
- is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
- "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)";
+text {*
+ \medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain \emph{axioms}. Thus, type classes may be also
+ understood as type predicates --- i.e.\ abstractions over a single
+ type argument $\alpha$. Class axioms typically contain polymorphic
+ constants that depend on this type $\alpha$. These
+ \emph{characteristic constants} behave like operations associated
+ with the ``carrier'' type $\alpha$.
+
+ We illustrate these basic concepts by the following formulation of
+ semigroups.
+*};
consts
- plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 65);
+ times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 70);
+axclass
+ semigroup < "term"
+ assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+
+text {*
+ \noindent Above we have first declared a polymorphic constant $\TIMES
+ :: \alpha \To \alpha \To \alpha$ and then defined the class
+ $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
+ \To \tau$ is indeed an associative operator. The $assoc$ axiom
+ contains exactly one type variable, which is invisible in the above
+ presentation, though. Also note that free term variables (like $x$,
+ $y$, $z$) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
+
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{signature}. Different signatures require different classes.
+ Subsequently, class $plus_semigroup$ represents semigroups of the
+ form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ to semigroups $(\tau, \TIMES^\tau)$.
+*};
+
+consts
+ plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 70);
axclass
plus_semigroup < "term"
- assoc: "is_assoc (op \<Oplus>)";
+ assoc: "(x \<Oplus> y) \<Oplus> z = x \<Oplus> (y \<Oplus> z)";
-consts
- times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 65);
-axclass
- times_semigroup < "term"
- assoc: "is_assoc (op \<Otimes>)";
+text {*
+ \noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
+ represent semigroups in a sense, they are certainly not the same!
+*};
end;
\ No newline at end of file
--- a/doc-src/AxClass/IsaMakefile Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/IsaMakefile Mon May 22 10:31:44 2000 +0200
@@ -24,8 +24,9 @@
@cd $(SRC)/HOL; $(ISATOOL) make HOL
$(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/document/root.tex \
- Group/Group.thy Group/Product.thy Group/Semigroup.thy Group/Semigroups.thy
+ Group/Group.thy Group/Product.thy Group/Semigroups.thy
@$(USEDIR) $(OUT)/HOL Group
+ @rm -f generated/pdfsetup.sty generated/session.tex
## Nat
@@ -38,6 +39,7 @@
$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/document/root.tex \
Nat/NatClass.ML Nat/NatClass.thy
@$(USEDIR) $(OUT)/FOL Nat
+ @rm -f generated/pdfsetup.sty generated/session.tex
## clean
--- a/doc-src/AxClass/Makefile Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Makefile Mon May 22 10:31:44 2000 +0200
@@ -15,8 +15,7 @@
FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
../pdfsetup.sty generated/Group.tex generated/NatClass.tex \
- generated/Product.tex generated/Semigroup.tex generated/Semigroups.tex \
- generated/session.tex
+ generated/Product.tex generated/Semigroups.tex
dvi: $(NAME).dvi
--- a/doc-src/AxClass/Nat/NatClass.thy Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/Nat/NatClass.thy Mon May 22 10:31:44 2000 +0200
@@ -1,5 +1,19 @@
+
+header {* Defining natural numbers in FOL \label{sec:ex-natclass} *};
+
theory NatClass = FOL:;
+text {*
+ \medskip\noindent Axiomatic type classes abstract over exactly one
+ type argument. Thus, any \emph{axiomatic} theory extension where each
+ axiom refers to at most one type variable, may be trivially turned
+ into a \emph{definitional} one.
+
+ We illustrate this with the natural numbers in
+ Isabelle/FOL.\footnote{See also
+ \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}
+*};
+
consts
zero :: 'a ("0")
Suc :: "'a \\<Rightarrow> 'a"
@@ -17,4 +31,30 @@
add :: "'a::nat \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "+" 60)
"m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))";
+text {*
+ This is an abstract version of the plain $Nat$ theory in
+ FOL.\footnote{See
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+
+ Basically, we have just replaced all occurrences of type $nat$ by
+ $\alpha$ and used the natural number axioms to define class $nat$.
+ There is only a minor snag, that the original recursion operator
+ $rec$ had to be made monomorphic, in a sense. Thus class $nat$
+ contains exactly those types $\tau$ that are isomorphic to ``the''
+ natural numbers (with signature $0$, $Suc$, $rec$).
+
+ \medskip What we have done here can be also viewed as \emph{type
+ specification}. Of course, it still remains open if there is some
+ type at all that meets the class axioms. Now a very nice property of
+ axiomatic type classes is, that abstract reasoning is always possible
+ --- independent of satisfiability. The meta-logic won't break, even
+ if some classes (or general sorts) turns out to be empty
+ (``inconsistent'') later.
+
+ Theorems of the abstract natural numbers may be derived in the same
+ way as for the concrete version. The original proof scripts may be
+ used with some trivial changes only (mostly adding some type
+ constraints).
+*};
+
end;
\ No newline at end of file
--- a/doc-src/AxClass/body.tex Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/body.tex Mon May 22 10:31:44 2000 +0200
@@ -46,84 +46,13 @@
formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
FOL.
-\section{Semigroups}
-
-An axiomatic type class is simply a class of types that all meet certain
-\emph{axioms}. Thus, type classes may be also understood as type predicates
---- i.e.\ abstractions over a single type argument $\alpha$. Class axioms
-typically contain polymorphic constants that depend on this type $\alpha$.
-These \emph{characteristic constants} behave like operations associated with
-the ``carrier'' type $\alpha$.
-
-We illustrate these basic concepts by the following theory of semigroups.
-
-\bigskip
-\input{generated/Semigroup}
-\bigskip
-
-\noindent
-Above we have first declared a polymorphic constant $\TIMES :: \alpha \To
-\alpha \To \alpha$ and then defined the class $semigroup$ of all types $\tau$
-such that $\TIMES :: \tau \To \tau \To \tau$ is indeed an associative
-operator. The $assoc$ axiom contains exactly one type variable, which is
-invisible in the above presentation, though. Also note that free term
-variables (like $x$, $y$, $z$) are allowed for user convenience ---
-conceptually all of these are bound by outermost universal quantifiers.
-
-\medskip
-
-In general, type classes may be used to describe \emph{structures} with
-exactly one carrier $\alpha$ and a fixed \emph{signature}. Different
-signatures require different classes. In the following theory, class
-$plus_semigroup$ represents semigroups of the form $(\tau, \PLUS^\tau)$ while
-$times_semigroup$ represents semigroups $(\tau, \TIMES^\tau)$.
-
-\bigskip
\input{generated/Semigroups}
-\bigskip
-
-\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both represent
-semigroups in a sense, they are not the same!
-
\input{generated/Group}
\input{generated/Product}
-
-\section{Defining natural numbers in FOL}\label{sec:ex-natclass}
-
-Axiomatic type classes abstract over exactly one type argument. Thus, any
-\emph{axiomatic} theory extension where each axiom refers to at most one type
-variable, may be trivially turned into a \emph{definitional} one.
-
-We illustrate this with the natural numbers in Isabelle/FOL.
-
-\bigskip
\input{generated/NatClass}
-\bigskip
-
-This is an abstract version of the plain $Nat$ theory in
-FOL.\footnote{See \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
-
-Basically, we have just replaced all occurrences of type $nat$ by $\alpha$ and
-used the natural number axioms to define class $nat$. There is only a minor
-snag, that the original recursion operator $rec$ had to be made monomorphic,
-in a sense. Thus class $nat$ contains exactly those types $\tau$ that are
-isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, $rec$).
-
-\medskip
-
-What we have done here can be also viewed as \emph{type specification}. Of
-course, it still remains open if there is some type at all that meets the
-class axioms. Now a very nice property of axiomatic type classes is, that
-abstract reasoning is always possible --- independent of satisfiability. The
-meta-logic won't break, even if some classes (or general sorts) turns out to
-be empty (``inconsistent'') later.
-
-Theorems of the abstract natural numbers may be derived in the same way as for
-the concrete version. The original proof scripts may be used with some
-trivial changes only (mostly adding some type constraints).
%% FIXME move some parts to ref or isar-ref manual (!?);
@@ -151,7 +80,7 @@
% \emphnd{matharray}
% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
-% $string$) and $axm@1, \ldots, axm@m$ (with $m \ge
+% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
% 0$) are formulas (category $string$).
% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
--- a/doc-src/AxClass/generated/NatClass.tex Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/generated/NatClass.tex Mon May 22 10:31:44 2000 +0200
@@ -1,6 +1,17 @@
\begin{isabelle}%
-\isacommand{theory}~NatClass~=~FOL:\isanewline
-\isanewline
+%
+\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
+\isacommand{theory}~NatClass~=~FOL:%
+\begin{isamarkuptext}%
+\medskip\noindent Axiomatic type classes abstract over exactly one
+ type argument. Thus, any \emph{axiomatic} theory extension where each
+ axiom refers to at most one type variable, may be trivially turned
+ into a \emph{definitional} one.
+
+ We illustrate this with the natural numbers in
+ Isabelle/FOL.\footnote{See also
+ \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
+\end{isamarkuptext}%
\isacommand{consts}\isanewline
~~zero~::~'a~~~~({"}0{"})\isanewline
~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
@@ -16,6 +27,30 @@
\isanewline
\isacommand{constdefs}\isanewline
~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline
-~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}\isanewline
-\isanewline
+~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}%
+\begin{isamarkuptext}%
+This is an abstract version of the plain $Nat$ theory in
+ FOL.\footnote{See
+ \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}}
+
+ Basically, we have just replaced all occurrences of type $nat$ by
+ $\alpha$ and used the natural number axioms to define class $nat$.
+ There is only a minor snag, that the original recursion operator
+ $rec$ had to be made monomorphic, in a sense. Thus class $nat$
+ contains exactly those types $\tau$ that are isomorphic to ``the''
+ natural numbers (with signature $0$, $Suc$, $rec$).
+
+ \medskip What we have done here can be also viewed as \emph{type
+ specification}. Of course, it still remains open if there is some
+ type at all that meets the class axioms. Now a very nice property of
+ axiomatic type classes is, that abstract reasoning is always possible
+ --- independent of satisfiability. The meta-logic won't break, even
+ if some classes (or general sorts) turns out to be empty
+ (``inconsistent'') later.
+
+ Theorems of the abstract natural numbers may be derived in the same
+ way as for the concrete version. The original proof scripts may be
+ used with some trivial changes only (mostly adding some type
+ constraints).%
+\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%
--- a/doc-src/AxClass/generated/Semigroup.tex Mon May 22 10:02:58 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-\begin{isabelle}%
-\isacommand{theory}~Semigroup~=~Main:\isanewline
-\isanewline
-\isacommand{consts}\isanewline
-~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
-\isacommand{axclass}\isanewline
-~~semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
-\isanewline
-\isacommand{end}\end{isabelle}%
--- a/doc-src/AxClass/generated/Semigroups.tex Mon May 22 10:02:58 2000 +0200
+++ b/doc-src/AxClass/generated/Semigroups.tex Mon May 22 10:31:44 2000 +0200
@@ -1,20 +1,48 @@
\begin{isabelle}%
-\isacommand{theory}~Semigroups~=~Main:\isanewline
-\isanewline
-\isacommand{constdefs}\isanewline
-~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
-~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline
-\isanewline
+%
+\isamarkupheader{Semigroups}
+\isacommand{theory}~Semigroups~=~Main:%
+\begin{isamarkuptext}%
+\medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain \emph{axioms}. Thus, type classes may be also
+ understood as type predicates --- i.e.\ abstractions over a single
+ type argument $\alpha$. Class axioms typically contain polymorphic
+ constants that depend on this type $\alpha$. These
+ \emph{characteristic constants} behave like operations associated
+ with the ``carrier'' type $\alpha$.
+
+ We illustrate these basic concepts by the following formulation of
+ semigroups.%
+\end{isamarkuptext}%
\isacommand{consts}\isanewline
-~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
+~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
+\isacommand{axclass}\isanewline
+~~semigroup~<~{"}term{"}\isanewline
+~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}%
+\begin{isamarkuptext}%
+\noindent Above we have first declared a polymorphic constant $\TIMES
+ :: \alpha \To \alpha \To \alpha$ and then defined the class
+ $semigroup$ of all types $\tau$ such that $\TIMES :: \tau \To \tau
+ \To \tau$ is indeed an associative operator. The $assoc$ axiom
+ contains exactly one type variable, which is invisible in the above
+ presentation, though. Also note that free term variables (like $x$,
+ $y$, $z$) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
+
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier $\alpha$ and a fixed
+ \emph{signature}. Different signatures require different classes.
+ Subsequently, class $plus_semigroup$ represents semigroups of the
+ form $(\tau, \PLUS^\tau)$, while $semigroup$ above would correspond
+ to semigroups $(\tau, \TIMES^\tau)$.%
+\end{isamarkuptext}%
+\isacommand{consts}\isanewline
+~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline
\isacommand{axclass}\isanewline
~~plus\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline
-\isanewline
-\isacommand{consts}\isanewline
-~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline
-\isacommand{axclass}\isanewline
-~~times\_semigroup~<~{"}term{"}\isanewline
-~~assoc:~{"}is\_assoc~(op~{\isasymOtimes}){"}\isanewline
-\isanewline
+~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}%
+\begin{isamarkuptext}%
+\noindent Even if classes $plus_semigroup$ and $times_semigroup$ both
+ represent semigroups in a sense, they are certainly not the same!%
+\end{isamarkuptext}%
\isacommand{end}\end{isabelle}%
--- a/doc-src/AxClass/generated/pdfsetup.sty Mon May 22 10:02:58 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-%%
-%% $Id$
-%%
-%% conditional url/hyperref setup
-%%
-
-\@ifundefined{pdfoutput}{\usepackage{url}}
-{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
- \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
--- a/doc-src/AxClass/generated/session.tex Mon May 22 10:02:58 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\input{NatClass.tex}