--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/Group.thy Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,131 @@
+
+theory Group = Main:;
+
+
+consts
+ times :: "'a => 'a => 'a" (infixl "\<Otimes>" 70)
+ inverse :: "'a => 'a" ("(_\<inv>)" [1000] 999)
+ one :: 'a ("\<unit>");
+
+
+axclass
+ monoid < "term"
+ assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)"
+ left_unit: "\<unit> \<Otimes> x = x"
+ right_unit: "x \<Otimes> \<unit> = x";
+
+
+axclass
+ semigroup < "term"
+ assoc: "(x \<Otimes> y) \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+
+axclass
+ group < semigroup
+ left_unit: "\<unit> \<Otimes> x = x"
+ left_inverse: "inverse x \<Otimes> x = \<unit>";
+
+
+text {*
+ The group axioms only state the properties of left unit and inverse,
+ the right versions may be derived as follows.
+*};
+
+theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>::'a::group)";
+proof -;
+ have "x \<Otimes> x\<inv> = \<unit> \<Otimes> (x \<Otimes> x\<inv>)";
+ by (simp only: group.left_unit);
+ also; have "... = (\<unit> \<Otimes> x) \<Otimes> x\<inv>";
+ by (simp only: semigroup.assoc);
+ also; have "... = (x\<inv>)\<inv> \<Otimes> x\<inv> \<Otimes> x \<Otimes> x\<inv>";
+ by (simp only: group.left_inverse);
+ also; have "... = (x\<inv>)\<inv> \<Otimes> (x\<inv> \<Otimes> x) \<Otimes> x\<inv>";
+ by (simp only: semigroup.assoc);
+ also; have "... = (x\<inv>)\<inv> \<Otimes> \<unit> \<Otimes> x\<inv>";
+ by (simp only: group.left_inverse);
+ also; have "... = (x\<inv>)\<inv> \<Otimes> (\<unit> \<Otimes> x\<inv>)";
+ by (simp only: semigroup.assoc);
+ also; have "... = (x\<inv>)\<inv> \<Otimes> x\<inv>";
+ by (simp only: group.left_unit);
+ also; have "... = \<unit>";
+ by (simp only: group.left_inverse);
+ finally; show ?thesis; .;
+qed;
+
+text {*
+ With $group_right_inverse$ already available,
+ $group_right_unit$\label{thm:group-right-unit} is now established
+ much easier.
+*};
+
+theorem group_right_unit: "x \<Otimes> \<unit> = (x::'a::group)";
+proof -;
+ have "x \<Otimes> \<unit> = x \<Otimes> (x\<inv> \<Otimes> x)";
+ by (simp only: group.left_inverse);
+ also; have "... = x \<Otimes> x\<inv> \<Otimes> x";
+ by (simp only: semigroup.assoc);
+ also; have "... = \<unit> \<Otimes> x";
+ by (simp only: group_right_inverse);
+ also; have "... = x";
+ by (simp only: group.left_unit);
+ finally; show ?thesis; .;
+qed;
+
+
+axclass
+ agroup < group
+ commute: "x \<Otimes> y = y \<Otimes> x";
+
+
+
+instance monoid < semigroup;
+proof intro_classes;
+ fix x y z :: "'a::monoid";
+ show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+ by (rule monoid.assoc);
+qed;
+
+
+instance group < monoid;
+proof intro_classes;
+ fix x y z :: "'a::group";
+ show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)";
+ by (rule semigroup.assoc);
+ show "\<unit> \<Otimes> x = x";
+ by (rule group.left_unit);
+ show "x \<Otimes> \<unit> = x";
+ by (rule group_right_unit);
+qed;
+
+
+
+defs
+ times_bool_def: "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)"
+ inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool"
+ unit_bool_def: "\<unit> \\<equiv> False";
+
+instance bool :: agroup;
+proof (intro_classes,
+ unfold times_bool_def inverse_bool_def unit_bool_def);
+ fix x y z :: bool;
+ show "((x \\<noteq> y) \\<noteq> z) = (x \\<noteq> (y \\<noteq> z))"; by blast;
+ show "(False \\<noteq> x) = x"; by blast;
+ show "(x \\<noteq> x) = False"; by blast;
+ show "(x \\<noteq> y) = (y \\<noteq> x)"; by blast;
+qed;
+
+
+defs
+ prod_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)";
+
+instance * :: (semigroup, semigroup) semigroup;
+proof (intro_classes, unfold prod_prod_def);
+ fix p q r :: "'a::semigroup * 'b::semigroup";
+ show
+ "(fst (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> fst r,
+ snd (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> snd r) =
+ (fst p \<Otimes> fst (fst q \<Otimes> fst r, snd q \<Otimes> snd r),
+ snd p \<Otimes> snd (fst q \<Otimes> fst r, snd q \<Otimes> snd r))";
+ by (simp add: semigroup.assoc);
+qed;
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/Product.thy Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,22 @@
+(* Title: HOL/AxClasses/Tutorial/Product.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Example 'syntactic' class "product", instantiated on type "bool". At
+first sight this may look like instance in Haskell, but is not quite
+the same!
+*)
+
+theory Product = Main:;
+
+axclass
+ product < "term";
+consts
+ product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\\<otimes>" 70);
+
+instance bool :: product;
+ by intro_classes;
+defs
+ product_bool_def: "x \\<otimes> y \\<equiv> x \\<and> y";
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/ROOT.ML Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,5 @@
+
+use_thy "Semigroup";
+use_thy "Semigroups";
+use_thy "Group";
+use_thy "Product";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/Semigroup.thy Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,9 @@
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/Semigroups.thy Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,32 @@
+theory Semigroups = Main:;
+
+text {*
+ \noindent Associativity of binary operations:
+*};
+constdefs
+ is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool"
+ "is_assoc f == \\<forall>x y z. f (f x y) z = f x (f y z)";
+
+text {*
+ \medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
+ %term (latex xsymbols symbols) "op \<Oplus>";
+*};
+
+consts
+ plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 65);
+axclass
+ plus_semigroup < "term"
+ assoc: "is_assoc (op \<Oplus>)";
+
+text {*
+ \medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
+ %term (latex xsymbols symbols) "op \<Otimes>";
+*};
+
+consts
+ times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 65);
+axclass
+ times_semigroup < "term"
+ assoc: "is_assoc (op \<Otimes>)";
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Group/document/root.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,6 @@
+
+\documentclass{article}
+
+\begin{document}
+--- dummy ---
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/IsaMakefile Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,46 @@
+
+## targets
+
+default: Group Nat
+images:
+test: Group Nat
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+USEDIR = $(ISATOOL) usedir -i true -d dvi -D ../generated
+
+
+## Group
+
+Group: HOL $(LOG)/HOL-Group.gz
+
+HOL:
+ @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
+ @$(USEDIR) $(OUT)/HOL Group
+
+
+## Nat
+
+Nat: FOL $(LOG)/FOL-Nat.gz
+
+FOL:
+ @cd $(SRC)/FOL; $(ISATOOL) make FOL
+
+$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/document/root.tex \
+ Nat/NatClass.ML Nat/NatClass.thy
+ @$(USEDIR) $(OUT)/FOL Nat
+
+
+## clean
+
+clean:
+ @rm -f $(LOG)/HOL-Group.gz $(LOG)/FOL-Nat.gz
--- a/doc-src/AxClass/Makefile Sat May 20 18:37:21 2000 +0200
+++ b/doc-src/AxClass/Makefile Sun May 21 01:12:00 2000 +0200
@@ -12,17 +12,22 @@
include ../Makefile.in
NAME = axclass
-FILES = axclass.tex style.tex
+
+FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../pdfsetup.sty
dvi: $(NAME).dvi
-$(NAME).dvi: $(FILES)
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+ $(LATEX) $(NAME)
+ $(BIBTEX) $(NAME)
$(LATEX) $(NAME)
$(LATEX) $(NAME)
pdf: $(NAME).pdf
-$(NAME).pdf: $(FILES)
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
$(PDFLATEX) $(NAME)
$(FIXBOOKMARKS) $(NAME).out
+ $(BIBTEX) $(NAME)
$(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Nat/NatClass.ML Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,69 @@
+(* Title: FOL/ex/NatClass.ML
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+This is Nat.ML with some trivial modifications in order to make it
+work with NatClass.thy.
+*)
+
+val induct = thm "induct";
+val Suc_inject = thm "Suc_inject";
+val Suc_neq_0 = thm "Suc_neq_0";
+val rec_0 = thm "rec_0";
+val rec_Suc = thm "rec_Suc";
+val add_def = thm "add_def";
+
+
+Goal "Suc(k) ~= (k::'a::nat)";
+by (res_inst_tac [("n","k")] induct 1);
+by (rtac notI 1);
+by (etac Suc_neq_0 1);
+by (rtac notI 1);
+by (etac notE 1);
+by (etac Suc_inject 1);
+qed "Suc_n_not_n";
+
+
+Goal "(k+m)+n = k+(m+n)";
+prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
+by (rtac induct 1);
+back();
+back();
+back();
+back();
+back();
+back();
+
+Goalw [add_def] "0+n = n";
+by (rtac rec_0 1);
+qed "add_0";
+
+Goalw [add_def] "Suc(m)+n = Suc(m+n)";
+by (rtac rec_Suc 1);
+qed "add_Suc";
+
+Addsimps [add_0, add_Suc];
+
+Goal "(k+m)+n = k+(m+n)";
+by (res_inst_tac [("n","k")] induct 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_assoc";
+
+Goal "m+0 = m";
+by (res_inst_tac [("n","m")] induct 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_0_right";
+
+Goal "m+Suc(n) = Suc(m+n)";
+by (res_inst_tac [("n","m")] induct 1);
+by (ALLGOALS (Asm_simp_tac));
+qed "add_Suc_right";
+
+val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
+by (res_inst_tac [("n","i")] induct 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [prem]) 1);
+qed "";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Nat/NatClass.thy Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,32 @@
+(* Title: FOL/ex/NatClass.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+This is an abstract version of Nat.thy. Instead of axiomatizing a
+single type "nat" we define the class of all these types (up to
+isomorphism).
+
+Note: The "rec" operator had to be made 'monomorphic', because class
+axioms may not contain more than one type variable.
+*)
+
+theory NatClass = FOL:;
+
+consts
+ zero :: 'a ("0")
+ Suc :: "'a \\<Rightarrow> 'a"
+ rec :: "'a \\<Rightarrow> 'a \\<Rightarrow> ('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> 'a";
+
+axclass
+ nat < "term"
+ induct: "P(0) \\<Longrightarrow> (\\<And>x. P(x) \\<Longrightarrow> P(Suc(x))) \\<Longrightarrow> P(n)"
+ Suc_inject: "Suc(m) = Suc(n) \\<Longrightarrow> m = n"
+ Suc_neq_0: "Suc(m) = 0 \\<Longrightarrow> R"
+ rec_0: "rec(0, a, f) = a"
+ rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))";
+
+constdefs
+ add :: "'a::nat \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "+" 60)
+ "m + n \\<equiv> rec(m, n, \\<lambda>x y. Suc(y))";
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Nat/ROOT.ML Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,2 @@
+
+use_thy "NatClass";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/Nat/document/root.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,6 @@
+
+\documentclass{article}
+
+\begin{document}
+--- dummy ---
+\end{document}
--- a/doc-src/AxClass/axclass.tex Sat May 20 18:37:21 2000 +0200
+++ b/doc-src/AxClass/axclass.tex Sun May 21 01:12:00 2000 +0200
@@ -1,747 +1,82 @@
-\input{style}
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{graphicx,../iman,../extra,../pdfsetup}
+\usepackage{generated/isabelle,generated/isabellesym}
+
+\newcommand{\isasymOtimes}{\emph{$\odot$}}
+\newcommand{\isasymOplus}{\emph{$\oplus$}}
+\newcommand{\isasyminv}{\emph{${}^{-1}$}}
+\newcommand{\isasymunit}{\emph{$1$}}
+\newcommand{\TIMES}{\odot}
+\newcommand{\PLUS}{\oplus}
+
+
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+\hyphenation{Haskell}
+
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+ \\[4ex] Using Axiomatic Type Classes in Isabelle}
+\author{\emph{Markus Wenzel} \\ TU M\"unchen}
+
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod %%%treat . like a binary operator
+
\begin{document}
-\title{Using Axiomatic Type Classes in Isabelle \\ a tutorial}
-\author{Markus Wenzel}
-%\date{29 August 1995}
-\maketitle
-
-\Isa\ features a \Haskell-like type system with ordered type classes
-already since 1991 (see \cite{Nipkow93}). Initially, classes mainly
-served as a \E{syntactic tool} to formulate polymorphic object logics
-in a clean way (like many-sorted \FOL, see
-\cite[\S1.1.2--1.1.3]{Paulson94}).
-
-Applying classes at the \E{logical level} to provide a simple notion
-of abstract theories and instantiations to concrete ones, has also
-been long proposed (see \cite{Nipkow-slides} and
-\cite[\S4]{Nipkow93}). At that time, \Isa\ still lacked built-in
-support for these \E{axiomatic type classes}. More importantly, their
-semantics was not yet fully fleshed out and unnecessarily complicated.
-
-How simple things really are has been shown in \cite[esp.\
-\S4]{Wenzel94} which also provided an implementation of the axclass
-package that was eventually released with \Isa94. Unfortunately there
-was a snag: That version of \Isa\ still contained an old conceptual
-bug in the core machinery which caused theories to become inconsistent
-after introducing empty sorts. Note that empty intersections of
-axiomatic type classes easily occur, unless all basic classes are very
-trivial.
-
-These problems prevented the axclass package to be used seriously ---
-they have been fixed in \Isa94-2.
-
-
-\section{Some simple examples} \label{sec:ex}
-
-Axiomatic type classes are a concept of \Isa's meta-logic. They may
-be applied to any object-logic that directly uses the meta type
-system. Subsequently, we present various examples that are formulated
-within \Isa/\HOL\footnote{See also directory
- \TT{HOL/AxClasses/Tutorial}.}, except the one of
-\secref{sec:ex-natclass} which is in \Isa/\FOL\footnote{See also files
- \TT{FOL/ex/NatClass.thy} and \TT{FOL/ex/NatClass.ML}.}.
-
-
-\subsection{Semigroups}
-
-An axiomatic type class is simply a class of types that all meet
-certain \E{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 \E{characteristic constants}
-behave like operations associated with the ``carrier'' $\alpha$.
-
-We illustrate these basic concepts with the following theory
-\TT{Semigroup}:
-
-\begin{ascbox}
-Semigroup = HOL +\medskip
-consts
- "<*>" :: "['a, 'a] => 'a" (infixl 70)\medskip
-axclass
- semigroup < term
- assoc "(x <*> y) <*> z = x <*> (y <*> z)"\medskip
-end
-\end{ascbox}
+\underscoreoff
-\TT{Semigroup} first declares a polymorphic constant $\TIMES ::
-[\alpha, \alpha] \To \alpha$ and then defines the class \TT{semigroup}
-of all those types $\tau$ such that $\TIMES :: [\tau, \tau] \To \tau$
-is an associative operator\footnote{Note that $\TIMES$ is used here
- instead of $*$, because the latter is already declared in theory
- \TT{HOL} in a slightly different way.}. The axiom \TT{assoc}
-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 \E{structures} with
-exactly one carrier $\alpha$ and a fixed \E{signature}. Different
-signatures require different classes. In the following theory
-\TT{Semigroups}, class \TT{plus\_sg} represents semigroups of the form
-$(\tau, \PLUS^\tau)$ while \TT{times\_sg} represents semigroups
-$(\tau, \TIMES^\tau)$:
-
-\begin{ascbox}
-Semigroups = HOL +\medskip
-consts
- "<+>" :: "['a, 'a] => 'a" (infixl 65)
- "<*>" :: "['a, 'a] => 'a" (infixl 70)
- assoc :: "(['a, 'a] => 'a) => bool"\medskip
-defs
- assoc_def "assoc f == ALL x y z. f (f x y) z = f x (f y z)"\medskip
-axclass
- plus_sg < term
- plus_assoc "assoc (op <+>)"\medskip
-axclass
- times_sg < term
- times_assoc "assoc (op <*>)"\medskip
-end
-\end{ascbox}
-
-Even if both classes \TT{plus\_sg} and \TT{times\_sg} represent
-semigroups in a sense, they are not the same!
-
-
-\subsection{Basic group theory}
-
-The meta type system of \Isa\ supports \E{intersections} and
-\E{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.
-
-
-\subsubsection{Monoids and Groups}
-
-First a small theory that provides some polymorphic constants to be
-used later for the signature parts:
-
-\begin{ascbox}
-Sigs = HOL +\medskip
-consts
- "<*>" :: "['a, 'a] => 'a" (infixl 70)
- inverse :: "'a => 'a"
- "1" :: "'a" ("1")\medskip
-end
-\end{ascbox}
-
-Next comes the theory \TT{Monoid} which defines class
-\TT{monoid}\footnote{Note that multiple class axioms are allowed for
- user convenience --- they simply represent the conjunction of their
- respective universal closures.}:
-
-\begin{ascbox}
-Monoid = Sigs +\medskip
-axclass
- monoid < term
- assoc "(x <*> y) <*> z = x <*> (y <*> z)"
- left_unit "1 <*> x = x"
- right_unit "x <*> 1 = x"\medskip
-end
-\end{ascbox}
-
-So class \TT{monoid} contains exactly those types $\tau$ where $\TIMES
-:: [\tau, \tau] \To \tau$ and $\TT{1} :: \tau$ are specified
-appropriately, such that $\TIMES$ is associative and $\TT{1}$ is a
-left and right unit for $\TIMES$.
+\maketitle
-\medskip
-
-Independently of \TT{Monoid}, we now define theory \TT{Group} which
-introduces a linear hierarchy of semigroups, general groups and
-abelian groups:
-
-\begin{ascbox}
-Group = Sigs +\medskip
-axclass
- semigroup < term
- assoc "(x <*> y) <*> z = x <*> (y <*> z)"\brk
-axclass
- group < semigroup
- left_unit "1 <*> x = x"
- left_inverse "inverse x <*> x = 1"\medskip
-axclass
- agroup < group
- commut "x <*> y = y <*> x"\medskip
-end
-\end{ascbox}
-
-Class \TT{group} inherits associativity of $\TIMES$ from
-\TT{semigroup} and adds the other two group axioms. Similarly,
-\TT{agroup} is defined as the subset of \TT{group} such that for all
-of its elements $\tau$, the operation $\TIMES :: [\tau, \tau] \To
-\tau$ is even commutative.
-
-
-\subsubsection{Abstract reasoning}
-
-In a sense, axiomatic type classes may be viewed as \E{abstract
- theories}. Above class definitions internally generate the
-following abstract axioms:
-
-\begin{ascbox}
-assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup)
- <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip
-left_unit: 1 <*> (?x::?'a::group) = ?x
-left_inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip
-commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x
-\end{ascbox}
-
-All of these contain type variables $\alpha :: c$ that are restricted
-to types of some class $c$. These \E{sort constraints} express a
-logical precondition for the whole formula. For example, \TT{assoc}
-states that for all $\tau$, provided that $\tau :: \TT{semigroup}$,
-the operation $\TIMES :: [\tau, \tau] \To \tau$ is associative.
-
-\medskip
-
-From a purely technical point of view, abstract axioms are just
-ordinary \Isa-theorems (of \ML-type \TT{thm}). They may be used for
-\Isa-proofs without special treatment. Such ``abstract proofs''
-usually yield new abstract theorems. For example, in theory \TT{Group}
-we may derive:
-
-\begin{ascbox}
-right_unit: (?x::?'a::group) <*> 1 = ?x
-right_inverse: (?x::?'a::group) <*> inverse ?x = 1
-inverse_product: inverse ((?x::?'a::group) <*> (?y::?'a::group)) =
- inverse ?y <*> inverse ?x
-inverse_inv: inverse (inverse (?x::?'a::group)) = ?x
-ex1_inverse: ALL x::?'a::group. EX! y::?'a::group. y <*> x = 1
-\end{ascbox}
-
-Abstract theorems (which include abstract axioms, of course) may be
-instantiated to only those types $\tau$ where the appropriate class
-membership $\tau :: c$ is known at \Isa's type signature level. Since
-we have $\TT{agroup} \subseteq \TT{group} \subseteq \TT{semigroup}$ by
-definition, all theorems of \TT{semigroup} and \TT{group} are
-automatically inherited by \TT{group} and \TT{agroup}.
-
-
-\subsubsection{Abstract instantiation}
-
-Until now, theories \TT{Monoid} and \TT{Group} were independent.
-Forming their union $\TT{Monoid} + \TT{Group}$ we get the following
-class hierarchy at the type signature level (left hand side):
-
-\begin{center}
- \small
- \unitlength 0.75mm
- \begin{picture}(65,90)(0,-10)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
- \put(15,5){\makebox(0,0){\tt agroup}}
- \put(15,25){\makebox(0,0){\tt group}}
- \put(15,45){\makebox(0,0){\tt semigroup}}
- \put(30,65){\makebox(0,0){\tt term}} \put(50,45){\makebox(0,0){\tt
- monoid}}
- \end{picture}
- \hspace{4em}
- \begin{picture}(30,90)(0,0)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
- \put(15,5){\makebox(0,0){\tt agroup}}
- \put(15,25){\makebox(0,0){\tt group}}
- \put(15,45){\makebox(0,0){\tt monoid}}
- \put(15,65){\makebox(0,0){\tt semigroup}}
- \put(15,85){\makebox(0,0){\tt term}}
- \end{picture}
-\end{center}
-
-We know by definition that $\TIMES$ is associative for monoids, i.e.\
-$\TT{monoid} \subseteq \TT{semigroup}$. Furthermore we have
-\TT{assoc}, \TT{left\_unit} and \TT{right\_unit} for groups (where
-\TT{right\_unit} is derivable from the group axioms), that is
-$\TT{group} \subseteq \TT{monoid}$. This way we get the refined class
-hierarchy shown above at the right hand side.
-
-The additional inclusions $\TT{monoid} \subseteq \TT{semigroup}$ and
-$\TT{group} \subseteq \TT{monoid}$ are established by logical means
-and have to be explicitly made known at the type signature level. This
-is what the theory section \TT{instance} does. So we define
-\TT{MonoidGroupInsts} as follows:
-
-\begin{ascbox}
-MonoidGroupInsts = Monoid + Group +\medskip
-instance
- monoid < semigroup (Monoid.assoc)\medskip
-instance
- group < monoid (assoc, left_unit, right_unit)\medskip
-end
-\end{ascbox}
-
-The \TT{instance} section does really check that the class inclusions
-(or type arities) to be added are derivable. To this end, it sets up a
-suitable goal and attempts a proof with the help of some internal
-axioms and user supplied theorems. These latter \E{witnesses} usually
-should be appropriate type instances of the class axioms (as are
-\TT{Monoid.assoc} and \TT{assoc}, \TT{left\_unit}, \TT{right\_unit}
-above).
-
-The most important internal tool for instantiation proofs is the class
-introduction rule that is automatically generated by \TT{axclass}. For
-class \TT{group} this is axiom \TT{groupI}:
-
-\begin{ascbox}
-groupI: [| OFCLASS(?'a::term, semigroup_class);
- !!x::?'a::term. 1 <*> x = x;
- !!x::?'a::term. inverse x <*> x = 1 |]
- ==> OFCLASS(?'a::term, group_class)
-\end{ascbox}
-
-There are also axioms \TT{monoidI}, \TT{semigroupI} and \TT{agroupI}
-of a similar form. Note that $\TT{OFCLASS}(\tau, c \TT{\_class})$
-expresses class membership $\tau :: c$ as a proposition of the
-meta-logic.
+\begin{abstract}
+ Isabelle offers order-sorted type classes on top of the simple types of
+ plain Higher-Order Logic. The resulting type system is similar to that of
+ the programming language Haskell. Its interpretation within the logic
+ enables further application, though, apart from restricting polymorphism
+ syntactically. In particular, the concept of \emph{Axiomatic Type Classes}
+ provides a useful light-weight mechanism for hierarchically-structured
+ abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
+ axiomatic type classes to model basic algebraic structures.
+
+ Note that this document describes axiomatic type classes using Isabelle/Isar
+ theories, with proofs expressed via Isar proof language elements. The new
+ theory format greatly simplifies the arrangement of the overall development,
+ since definitions and proofs may be freely intermixed. Users who prefer
+ tactic scripts over structured proofs do not need to fall back on separate
+ ML scripts, but may refer to Isar's tactic emulation commands.
+\end{abstract}
-\subsubsection{Concrete instantiation}
-
-So far we have covered the case of \TT{instance $c_1$ < $c_2$} that
-could be described as \E{abstract instantiation} --- $c_1$ is more
-special than $c_2$ and thus an instance of $c_2$. Even more
-interesting for practical applications are \E{concrete instantiations}
-of axiomatic type classes. That is, certain simple schemes $(\alpha_1,
-\ldots, \alpha_n)t :: c$ of class membership may be transferred to
-\Isa's type signature level. This form of \TT{instance} is a ``safe''
-variant of the old-style \TT{arities} theory section.
-
-As an example, we show that type \TT{bool} with exclusive-or as
-operation $\TIMES$, identity as \TT{inverse}, and \TT{False} as \TT{1}
-forms an abelian group. We first define theory \TT{Xor}:
-
-\begin{ascbox}
-Xor = Group +\medskip
-defs
- prod_bool_def "x <*> y == x ~= (y::bool)"
- inverse_bool_def "inverse x == x::bool"
- unit_bool_def "1 == False"\medskip
-end
-\end{ascbox}
-
-It is important to note that above \TT{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 primitive recursion over types) would be also possible
-in traditional versions of \HOL\ that lack type classes.
-% (see FIXME <foundation> for more details)
-Nonetheless, such definitions are best applied in the context of
-classes.
-
-\medskip
-
-Since we chose the \TT{defs} of theory \TT{Xor} suitably, the class
-membership $\TT{bool} :: \TT{agroup}$ is now derivable as follows:
+\pagenumbering{roman} \tableofcontents \clearfirst
-\begin{ascbox}
-open AxClass;
-goal_arity Xor.thy ("bool", [], "agroup");
-\out{Level 0}
-\out{OFCLASS(bool, agroup_class)}
-\out{ 1. OFCLASS(bool, agroup_class)}\brk
-by (axclass_tac []);
-\out{Level 1}
-\out{OFCLASS(bool, agroup_class)}
-\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}
-\out{ 2. !!x::bool. 1 <*> x = x}
-\out{ 3. !!x::bool. inverse x <*> x = 1}
-\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}
-\end{ascbox}
-
-The tactic \TT{axclass\_tac} has applied \TT{agroupI} internally to
-expand the class definition. It now remains to be shown that the
-\TT{agroup} axioms hold for bool. To this end, we expand the
-definitions of \TT{Xor} and solve the new subgoals by \TT{fast\_tac}
-of \HOL:
-
-\begin{ascbox}
-by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inverse_bool_def,
- Xor.unit_bool_def]);
-\out{Level 2}
-\out{OFCLASS(bool, agroup_class)}
-\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}
-\out{ 2. !!x::bool. False ~= x = x}
-\out{ 3. !!x::bool. x ~= x = False}
-\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}
-by (ALLGOALS (fast_tac HOL_cs));
-\out{Level 3}
-\out{OFCLASS(bool, agroup_class)}
-\out{No subgoals!}
-qed "bool_in_agroup";
-\out{val bool_in_agroup = "OFCLASS(bool, agroup_class)"}
-\end{ascbox}
+\include{body}
-The result is theorem $\TT{OFCLASS}(\TT{bool}, \TT{agroup\_class})$
-which expresses $\TT{bool} :: \TT{agroup}$ as a meta-proposition. This
-is not yet known at the type signature level, though.
-
-\medskip
-
-What we have done here by hand, can be also performed via
-\TT{instance} in a similar way behind the scenes. This may look as
-follows\footnote{Subsequently, theory \TT{Xor} is no longer
- required.}:
-
-\begin{ascbox}
-BoolGroupInsts = Group +\medskip
-defs
- prod_bool_def "x <*> y == x ~= (y::bool)"
- inverse_bool_def "inverse x == x::bool"
- unit_bool_def "1 == False"\medskip
-instance
- bool :: agroup \{| ALLGOALS (fast_tac HOL_cs) |\}\medskip
-end
-\end{ascbox}
-
-This way, we have $\TT{bool} :: \TT{agroup}$ in the type signature of
-\TT{BoolGroupInsts}, and all abstract group theorems are transferred
-to \TT{bool} for free.
-
-Similarly, we could now also instantiate our group theory classes to
-many other concrete types. For example, $\TT{int} :: \TT{agroup}$ (by
-defining $\TIMES$ as addition, \TT{inverse} as negation and \TT{1} as
-zero, say) or $\TT{list} :: (\TT{term})\TT{semigroup}$ (e.g.\ if
-$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
-\TT{inverse}, \TT{1} really become overloaded, i.e.\ have different
-meanings on different types.
-
-
-\subsubsection{Lifting and Functors}
+%FIXME
+\nocite{nipkow-types93}
+\nocite{nipkow-sorts93}
+\nocite{Wenzel:1997:TPHOL}
+\nocite{paulson-isa-book}
+\nocite{isabelle-isar-ref}
+\nocite{Wenzel:1999:TPHOL}
-As already mentioned above, \HOL-like systems not only support
-overloaded definitions of polymorphic constants (without requiring
-type classes), but even primitive recursion over types. That is,
-definitional equations $c^\tau \Eq t$ may also contain constants of
-name $c$ on the RHS --- provided that these have types that are
-strictly simpler (structurally) than $\tau$.
-
-This feature enables us to \E{lift operations}, e.g.\ to Cartesian
-products, direct sums or function spaces. Below, theory
-\TT{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place
-Cartesian products $\alpha \times \beta$:
+\begingroup
+ \bibliographystyle{plain} \small\raggedright\frenchspacing
+ \bibliography{../manual}
+\endgroup
-\begin{ascbox}
-ProdGroupInsts = Prod + Group +\medskip
-defs
- prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip
-instance
- "*" :: (semigroup, semigroup) semigroup
- \{| simp_tac (prod_ss addsimps [assoc]) 1 |\}
-end
-\end{ascbox}
-
-Note that \TT{prod\_prod\_def} basically has the form $\edrv
-{\TIMES}^{\alpha \times \beta} \Eq \ldots {\TIMES}^\alpha \ldots
-{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences
-$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.
-
-It is very easy to see that associativity of $\TIMES^\alpha$,
-$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
-the two-place type constructor $\times$ maps semigroups into
-semigroups. This fact is proven and put into \Isa's type signature by
-above \TT{instance} section.
-
-\medskip
-
-Thus, if we view class instances as ``structures'', overloaded
-constant definitions with primitive recursion over types indirectly
-provide some kind of ``functors'' (mappings between abstract theories,
-that is).
+\end{document}
-\subsection{Syntactic classes}
-
-There is still a feature of \Isa's type system left that we have not
-yet used: When declaring polymorphic constants $c :: \tau$, the type
-variables occurring in $\tau$ may be constrained by type classes (or
-even general sorts). Note that by default, in \Isa/\HOL\ the
-declaration:
-
-\begin{ascbox}
- <*> :: ['a, 'a] => 'a
-\end{ascbox}
-
-is actually an abbreviation for:
-
-\begin{ascbox}
- <*> :: ['a::term, 'a::term] => 'a::term
-\end{ascbox}
-
-Since class \TT{term} is the universal class of \HOL, this is not
-really a restriction at all. A less trivial example is the following
-theory \TT{Product}:
-
-\begin{ascbox}
-Product = HOL +\medskip
-axclass
- product < term\medskip
-consts
- "<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip
-end
-\end{ascbox}
-
-Here class \TT{product} is defined as subclass of \TT{term}, but
-without any additional axioms. This effects in logical equivalence of
-\TT{product} and \TT{term}, since \TT{productI} is as follows:
-
-\begin{ascbox}
-productI: OFCLASS(?'a::logic, term_class) ==>
- OFCLASS(?'a::logic, product_class)
-\end{ascbox}
-
-I.e.\ $\TT{term} \subseteq \TT{product}$. The converse inclusion is
-already contained in the type signature of theory \TT{Product}.
-
-Now, what is the difference of declaring $\TIMES :: [\alpha ::
-\TT{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
-\TT{term}, \alpha] \To \alpha$? In this special case (where
-$\TT{product} \Eq \TT{term}$), it should be obvious that both
-declarations are the same from the logic's point of view. It is even
-most sensible in the general case not to attach any \E{logical}
-meaning to sort constraints occurring in constant \E{declarations}
-(see \cite[page 79]{Wenzel94} for more details).
-
-On the other hand there are syntactic differences, of course.
-Constants $\TIMES^\tau$ are rejected by the type-checker, unless $\tau
-:: \TT{product}$ is part of the type signature. In our example, this
-arity may be always added when required by means of a trivial
-\TT{instance}.
-
-Thus, we can follow this discipline: Overloaded polymorphic constants
-have their type arguments restricted to an associated (logically
-trivial) class $c$. Only immediately before \E{specifying} these
-constants on a certain type $\tau$ do we instantiate $\tau :: c$.
-
-This is done for class \TT{product} and type \TT{bool} in theory
-\TT{ProductInsts} below:
-
-\begin{ascbox}
-ProductInsts = Product +\medskip
-instance
- bool :: product\medskip
-defs
- prod_bool_def "x <*> y == x & y::bool"\medskip
-end
-\end{ascbox}
-
-Note that \TT{instance bool ::\ product} does not require any
-witnesses, since this statement is logically trivial. Nonetheless,
-\TT{instance} really performs a proof.
-
-Only after $\TT{bool} :: \TT{product}$ is made known to the type
-checker, does \TT{prod\_bool\_def} become syntactically well-formed.
-
-\medskip
-
-It is very important to see that above \TT{defs} are not directly
-connected with \TT{instance} at all! We were just following our
-convention to specify $\TIMES$ on \TT{bool} after having instantiated
-$\TT{bool} :: \TT{product}$. \Isa\ does not require these definitions,
-which is in contrast to programming languages like \Haskell.
-
-\medskip
-
-While \Isa\ type classes and those of \Haskell\ are almost the same as
-far as type-checking and type inference are concerned, there are major
-semantic differences. \Haskell\ classes require their instances to
-\E{provide operations} of certain \E{names}. Therefore, its
-\TT{instance} has a \TT{where} part that tells the system what these
-``member functions'' should be.
-
-This style of \TT{instance} won't make much sense in \Isa, because its
-meta-logic has no corresponding notion of ``providing operations'' or
-``names''.
-
-
-\subsection{Defining natural numbers in FOL}
-\label{sec:ex-natclass}
-
-Axiomatic type classes abstract over exactly one type argument. Thus,
-any \E{axiomatic} theory extension where each axiom refers to at most
-one type variable, may be trivially turned into a \E{definitional}
-one.
-
-We illustrate this with the natural numbers in \Isa/\FOL:
-
-\begin{ascbox}
-NatClass = FOL +\medskip
-consts
- "0" :: "'a" ("0")
- Suc :: "'a => 'a"
- rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip
-axclass
- nat < term
- induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
- Suc_inject "Suc(m) = Suc(n) ==> m = n"
- Suc_neq_0 "Suc(m) = 0 ==> R"
- rec_0 "rec(0, a, f) = a"
- rec_Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip
-consts
- "+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip
-defs
- add_def "m + n == rec(m, n, %x y. Suc(y))"\medskip
-end
-\end{ascbox}
-
-\TT{NatClass} is an abstract version of \TT{Nat}\footnote{See
- directory \TT{FOL/ex}.}. Basically, we have just replaced all
-occurrences of \E{type} \TT{nat} by $\alpha$ and used the natural
-number axioms to define \E{class} \TT{nat}\footnote{There's a snag:
- The original recursion operator \TT{rec} had to be made monomorphic,
- in a sense.}. Thus class \TT{nat} contains exactly those types
-$\tau$ that are isomorphic to ``the'' natural numbers (with signature
-\TT{0}, \TT{Suc}, \TT{rec}).
-
-Furthermore, theory \TT{NatClass} defines an ``abstract constant'' $+$
-based on class \TT{nat}.
-
-\medskip
-
-What we have done here can be also viewed as \E{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 class (or
-general sort) turns out to be empty (``inconsistent'')
-later\footnote{As a consequence of an old bug, this is \E{not} true
- for pre-\Isa94-2 versions.}.
-
-For example, we may derive the following abstract natural numbers
-theorems:
-
-\begin{ascbox}
-add_0: 0 + (?n::?'a::nat) = ?n
-add_Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)
-\end{ascbox}
-
-See also file \TT{FOL/ex/NatClass.ML}. Note that this required only
-some trivial modifications of the original \TT{Nat.ML}.
-
-
-\section{The user interface of Isabelle's axclass package}
-
-The actual axiomatic type class package of \Isa/\Pure\ mainly consists
-of two new theory sections: \TT{axclass} and \TT{instance}. Some
-typical applications of these have already been demonstrated in
-\secref{sec:ex}, below their syntax and semantics are presented more
-completely.
-
-
-\subsection{The axclass section}
-
-Within theory files, \TT{axclass} introduces an axiomatic type class
-definition. Its concrete syntax is:
-
-\begin{matharray}{l}
- \TT{axclass} \\
- \ \ c \TT{ < } c_1\TT, \ldots\TT, c_n \\
- \ \ \idt{id}_1\ \idt{axm}_1 \\
- \ \ \vdots \\
- \ \ \idt{id}_m\ \idt{axm}_m
-\end{matharray}
-
-Where $c, c_1, \ldots, c_n$ are classes (category $\idt{id}$ or
-$\idt{string}$) and $\idt{axm}_1, \ldots, \idt{axm}_m$ (with $m \ge
-0$) are formulas (category $\idt{string}$).
-
-Class $c$ has to be new, and sort $\{c_1, \ldots, c_n\}$ a subsort of
-\TT{logic}. Each class axiom $\idt{axm}_j$ may contain any term
-variables, but at most one type variable (which need not be the same
-for all axioms). The sort of this type variable has to be a supersort
-of $\{c_1, \ldots, c_n\}$.
-
-\medskip
-
-The \TT{axclass} section declares $c$ as subclass of $c_1, \ldots,
-c_n$ to the type signature.
-
-Furthermore, $\idt{axm}_1, \ldots, \idt{axm}_m$ are turned into the
-``abstract axioms'' of $c$ with names $\idt{id}_1, \ldots,
-\idt{id}_m$. This is done by replacing all occurring type variables
-by $\alpha :: c$. Original axioms that do not contain any type
-variable will be prefixed by the logical precondition
-$\TT{OFCLASS}(\alpha :: \TT{logic}, c\TT{\_class})$.
-
-Another axiom of name $c\TT{I}$ --- the ``class $c$ introduction
-rule'' --- is built from the respective universal closures of
-$\idt{axm}_1, \ldots, \idt{axm}_m$ appropriately.
-
-
-\subsection{The instance section}
-
-Section \TT{instance} proves class inclusions or type arities at the
-logical level and then transfers these into the type signature.
-
-Its concrete syntax is:
-
-\begin{matharray}{l}
- \TT{instance} \\
- \ \ [\ c_1 \TT{ < } c_2 \ |\
- t \TT{ ::\ (}\idt{sort}_1\TT, \ldots \TT, \idt{sort}_n\TT) \idt{sort}\ ] \\
- \ \ [\ \TT(\idt{name}_1 \TT, \ldots\TT, \idt{name}_m\TT)\ ] \\
- \ \ [\ \TT{\{|} \idt{text} \TT{|\}}\ ]
-\end{matharray}
-
-Where $c_1, c_2$ are classes and $t$ is an $n$-place type constructor
-(all of category $\idt{id}$ or $\idt{string})$. Furthermore,
-$\idt{sort}_i$ are sorts in the usual \Isa-syntax.
-
-\medskip
-
-Internally, \TT{instance} first sets up an appropriate goal that
-expresses the class inclusion or type arity as a meta-proposition.
-Then tactic \TT{AxClass.axclass\_tac} is applied with all preceding
-meta-definitions of the current theory file and the user-supplied
-witnesses. The latter are $\idt{name}_1, \ldots, \idt{name}_m$, where
-$\idt{id}$ refers to an \ML-name of a theorem, and $\idt{string}$ to an
-axiom of the current theory node\footnote{Thus, the user may reference
- axioms from above this \TT{instance} in the theory file. Note
- that new axioms appear at the \ML-toplevel only after the file is
- processed completely.}.
-
-Tactic \TT{AxClass.axclass\_tac} first unfolds the class definition by
-resolving with rule $c\TT{I}$, and then applies the witnesses
-according to their form: Meta-definitions are unfolded, all other
-formulas are repeatedly resolved\footnote{This is done in a way that
- enables proper object-\E{rules} to be used as witnesses for
- corresponding class axioms.} with.
-
-The final optional argument $\idt{text}$ is \ML-code of an arbitrary
-user tactic which is applied last to any remaining goals.
-
-\medskip
-
-Because of the complexity of \TT{instance}'s witnessing mechanisms,
-new users of the axclass package are advised to only use the simple
-form $\TT{instance}\ \ldots\ (\idt{id}_1, \ldots, \idt{id}_m)$, where
-the identifiers refer to theorems that are appropriate type instances
-of the class axioms. This typically requires an auxiliary theory,
-though, which defines some constants and then proves these witnesses.
-
-
-\begin{thebibliography}{}
-
-\bibitem[Nipkow, 1993a]{Nipkow-slides} T. Nipkow. Axiomatic Type
- Classes (in Isabelle). Presentation at the workshop \E{Types for
- Proof and Programs}, Nijmegen, 1993.
-
-\bibitem[Nipkow, 1993b]{Nipkow93} T. Nipkow. Order-Sorted Polymorphism
- in Isabelle. In G. Huet, G. Plotkin, editors, \E{Logical
- Environments}, pp.\ 164--188, Cambridge University Press, 1993.
-
-\bibitem[Paulson, 1994]{Paulson94} L.C. Paulson. \E{Isabelle --- A
- Generic Theorem Prover}. LNCS 828, 1994.
-
-\bibitem[Wenzel, 1994]{Wenzel94} M. Wenzel. \E{Axiomatische
- Typ-Klassen in Isabelle}. Diplom\-arbeit, TU München, 1994.
-
-\end{thebibliography}
-
-\end{document}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+% LocalWords: Isabelle FIXME
--- a/doc-src/AxClass/bbb.sty Sat May 20 18:37:21 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-% bbb.sty 10-Nov-1991, 27-Mar-1994
-%
-% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
-%
-
-\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
-\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
-\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
-\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
-\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
-\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
-\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
-\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
-\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
-\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
-\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
-\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/body.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,688 @@
+
+\chapter{Introduction}
+
+A Haskell-style type-system \cite{haskell-report} with ordered type-classes
+has been present in Isabelle since 1991 \cite{nipkow-sorts93}. Initially,
+classes have mainly served as a \emph{purely syntactic} tool to formulate
+polymorphic object-logics in a clean way, such as the standard Isabelle
+formulation of many-sorted FOL \cite{paulson-isa-book}.
+
+Applying classes at the \emph{logical level} to provide a simple notion of
+abstract theories and instantiations to concrete ones, has been long proposed
+as well \cite{nipkow-types93,nipkow-sorts93}). At that time, Isabelle still
+lacked built-in support for these \emph{axiomatic type classes}. More
+importantly, their semantics was not yet fully fleshed out (and unnecessarily
+complicated, too).
+
+Since the Isabelle94 releases, actual axiomatic type classes have been an
+integral part of Isabelle's meta-logic. This very simple implementation is
+based on a straight-forward extension of traditional simple-typed Higher-Order
+Logic, including types qualified by logical predicates and overloaded constant
+definitions; see \cite{Wenzel:1997:TPHOL} for further details.
+
+Yet until Isabelle99, there used to be still a fundamental methodological
+problem in using axiomatic type classes conveniently, due to the traditional
+distinction of Isabelle theory files vs.\ ML proof scripts. This has been
+finally overcome with the advent of Isabelle/Isar theories
+\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
+This nicely accommodates the usual procedure of defining axiomatic type
+classes, proving abstract properties, defining operations on concrete types,
+proving concrete properties for instantiation of classes etc.
+
+\medskip
+
+So to cut a long story short, the present version of axiomatic type classes
+(Isabelle99 or later) now provides an even more useful and convenient
+mechanism for light-weight abstract theories, without any special provisions
+to be observed by the user.
+
+
+\chapter{Examples}\label{sec:ex}
+
+Axiomatic type classes are a concept of Isabelle's meta-logic
+\cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any
+object-logic that directly uses the meta type system, such as Isabelle/HOL
+\cite{isabelle-HOL}. Subsequently, we present various examples that are all
+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 semi-groups.
+
+\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!
+
+
+\section{Basic group theory}
+
+\input{generated/Group}
+
+
+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.
+
+
+\subsection{Monoids and Groups}
+
+First we declare some polymorphic constants required later for the signature
+parts of our structures.
+
+
+Next we define class $monoid$ of monoids of the form $(\alpha,
+{\TIMES}^\alpha)$. Note that multiple class axioms are allowed for user
+convenience --- they simply represent the conjunction of their respective
+universal closures.
+
+
+So class $monoid$ contains exactly those types $\tau$ where $\TIMES :: \tau
+\To \tau \To \tau$ and $1 :: \tau$ are specified appropriately, such that
+$\TIMES$ is associative and $1$ is a left and right unit for $\TIMES$.
+
+
+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$.
+
+
+Class $group$ inherits associativity of $\TIMES$ from $semigroup$ and adds the
+other two 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.
+
+
+\subsection{Abstract reasoning}
+
+In a sense, axiomatic type classes may be viewed as \emph{abstract theories}.
+Above class definitions internally generate the following abstract axioms:
+
+%FIXME
+% \begin{ascbox}
+% assoc: (?x::?'a::semigroup) <*> (?y::?'a::semigroup)
+% <*> (?z::?'a::semigroup) = ?x <*> (?y <*> ?z)\medskip
+% left@unit: 1 <*> (?x::?'a::group) = ?x
+% left@inverse: inverse (?x::?'a::group) <*> ?x = 1\medskip
+% commut: (?x::?'a::agroup) <*> (?y::?'a::agroup) = ?y <*> ?x
+% \emphnd{ascbox}
+
+All of these contain type variables $\alpha :: c$ that are restricted to types
+of some class $c$. These \emph{sort constraints} express a logical
+precondition for the whole formula. For example, $assoc$ states that for all
+$\tau$, provided that $\tau :: semigroup$, the operation $\TIMES :: \tau \To
+\tau \To \tau$ is associative.
+
+\medskip
+
+From a purely technical point of view, abstract axioms are just ordinary
+Isabelle theorems; they may be used for proofs without special treatment.
+Such ``abstract proofs'' usually yield new abstract theorems. For example, we
+may now derive the following laws of general groups.
+
+
+
+Abstract theorems may be instantiated to only those types $\tau$ where the
+appropriate class membership $\tau :: c$ is known at Isabelle's type signature
+level. Since we have $agroup \subseteq group \subseteq semigroup$ by
+definition, all theorems of $semigroup$ and $group$ are automatically
+inherited by $group$ and $agroup$.
+
+
+\subsection{Abstract instantiation}
+
+From the definition, the $monoid$ and $group$ classes have been independent.
+Note that for monoids, $right_unit$ had to be included 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 \subset
+monoid$ properly as follows (cf.\ \figref{fig:monoid-group}).
+
+\begin{figure}[htbp]
+ \begin{center}
+ \small
+% \unitlength 0.75mm
+ \unitlength 0.6mm
+ \begin{picture}(65,90)(0,-10)
+ \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
+ \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
+ \put(15,5){\makebox(0,0){$agroup$}}
+ \put(15,25){\makebox(0,0){$group$}}
+ \put(15,45){\makebox(0,0){$semigroup$}}
+ \put(30,65){\makebox(0,0){$term$}} \put(50,45){\makebox(0,0){$monoid$}}
+ \end{picture}
+ \hspace{4em}
+ \begin{picture}(30,90)(0,0)
+ \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
+ \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
+ \put(15,5){\makebox(0,0){$agroup$}}
+ \put(15,25){\makebox(0,0){$group$}}
+ \put(15,45){\makebox(0,0){$monoid$}}
+ \put(15,65){\makebox(0,0){$semigroup$}}
+ \put(15,85){\makebox(0,0){$term$}}
+ \end{picture}
+ \caption{Monoids and groups: according to definition, and by proof}
+ \label{fig:monoid-group}
+ \end{center}
+\end{figure}
+
+
+\endinput
+
+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.
+
+\endinput
+
+The \texttt{instance} section does really check that the class inclusions
+(or type arities) to be added are derivable. To this end, it sets up a
+suitable goal and attempts a proof with the help of some internal
+axioms and user supplied theorems. These latter \emph{witnesses} usually
+should be appropriate type instances of the class axioms (as are
+\texttt{Monoid.assoc} and \texttt{assoc}, \texttt{left_unit}, \texttt{right_unit}
+above).
+
+The most important internal tool for instantiation proofs is the class
+introduction rule that is automatically generated by \texttt{axclass}. For
+class \texttt{group} this is axiom \texttt{groupI}:
+
+\begin{ascbox}
+groupI: [| OFCLASS(?'a::term, semigroup@class);
+ !!x::?'a::term. 1 <*> x = x;
+ !!x::?'a::term. inverse x <*> x = 1 |]
+ ==> OFCLASS(?'a::term, group@class)
+\emphnd{ascbox}
+
+There are also axioms \texttt{monoidI}, \texttt{semigroupI} and \texttt{agroupI}
+of a similar form. Note that $\texttt{OFCLASS}(\tau, c \texttt{_class})$
+expresses class membership $\tau :: c$ as a proposition of the
+meta-logic.
+
+
+\subsection{Concrete instantiation}
+
+So far we have covered the case of \texttt{instance $c@1$ < $c@2$} that
+could be described as \emph{abstract instantiation} --- $c@1$ is more
+special than $c@2$ and thus an instance of $c@2$. Even more
+interesting for practical applications are \emph{concrete instantiations}
+of axiomatic type classes. That is, certain simple schemes $(\alpha@1,
+\ldots, \alpha@n)t :: c$ of class membership may be transferred to
+Isabelle's type signature level. This form of \texttt{instance} is a ``safe''
+variant of the old-style \texttt{arities} theory section.
+
+As an example, we show that type \texttt{bool} with exclusive-or as
+operation $\TIMES$, identity as \texttt{inverse}, and \texttt{False} as \texttt{1}
+forms an abelian group. We first define theory \texttt{Xor}:
+
+\begin{ascbox}
+Xor = Group +\medskip
+defs
+ prod@bool@def "x <*> y == x ~= (y::bool)"
+ inverse@bool@def "inverse x == x::bool"
+ unit@bool@def "1 == False"\medskip
+end
+\emphnd{ascbox}
+
+It is important to note that above \texttt{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 primitive recursion over types) would be also possible
+in traditional versions of \HOL\ that lack type classes.
+% (see FIXME <foundation> for more details)
+Nonetheless, such definitions are best applied in the context of
+classes.
+
+\medskip
+
+Since we chose the \texttt{defs} of theory \texttt{Xor} suitably, the class
+membership $\texttt{bool} :: \texttt{agroup}$ is now derivable as follows:
+
+\begin{ascbox}
+open AxClass;
+goal@arity Xor.thy ("bool", [], "agroup");
+\out{Level 0}
+\out{OFCLASS(bool, agroup@class)}
+\out{ 1. OFCLASS(bool, agroup@class)}\brk
+by (axclass@tac []);
+\out{Level 1}
+\out{OFCLASS(bool, agroup@class)}
+\out{ 1. !!(x::bool) (y::bool) z::bool. x <*> y <*> z = x <*> (y <*> z)}
+\out{ 2. !!x::bool. 1 <*> x = x}
+\out{ 3. !!x::bool. inverse x <*> x = 1}
+\out{ 4. !!(x::bool) y::bool. x <*> y = y <*> x}
+\emphnd{ascbox}
+
+The tactic \texttt{axclass_tac} has applied \texttt{agroupI} internally to
+expand the class definition. It now remains to be shown that the
+\texttt{agroup} axioms hold for bool. To this end, we expand the
+definitions of \texttt{Xor} and solve the new subgoals by \texttt{fast_tac}
+of \HOL:
+
+\begin{ascbox}
+by (rewrite@goals@tac [Xor.prod@bool@def, Xor.inverse@bool@def,
+ Xor.unit@bool@def]);
+\out{Level 2}
+\out{OFCLASS(bool, agroup@class)}
+\out{ 1. !!(x::bool) (y::bool) z::bool. x ~= y ~= z = (x ~= (y ~= z))}
+\out{ 2. !!x::bool. False ~= x = x}
+\out{ 3. !!x::bool. x ~= x = False}
+\out{ 4. !!(x::bool) y::bool. x ~= y = (y ~= x)}
+by (ALLGOALS (fast@tac HOL@cs));
+\out{Level 3}
+\out{OFCLASS(bool, agroup@class)}
+\out{No subgoals!}
+qed "bool@in@agroup";
+\out{val bool@in@agroup = "OFCLASS(bool, agroup@class)"}
+\emphnd{ascbox}
+
+The result is theorem $\texttt{OFCLASS}(\texttt{bool}, \texttt{agroup_class})$
+which expresses $\texttt{bool} :: \texttt{agroup}$ as a meta-proposition. This
+is not yet known at the type signature level, though.
+
+\medskip
+
+What we have done here by hand, can be also performed via
+\texttt{instance} in a similar way behind the scenes. This may look as
+follows\footnote{Subsequently, theory \texttt{Xor} is no longer
+ required.}:
+
+\begin{ascbox}
+BoolGroupInsts = Group +\medskip
+defs
+ prod@bool@def "x <*> y == x ~= (y::bool)"
+ inverse@bool@def "inverse x == x::bool"
+ unit@bool@def "1 == False"\medskip
+instance
+ bool :: agroup \{| ALLGOALS (fast@tac HOL@cs) |\}\medskip
+end
+\emphnd{ascbox}
+
+This way, we have $\texttt{bool} :: \texttt{agroup}$ in the type signature of
+\texttt{BoolGroupInsts}, and all abstract group theorems are transferred
+to \texttt{bool} for free.
+
+Similarly, we could now also instantiate our group theory classes to
+many other concrete types. For example, $\texttt{int} :: \texttt{agroup}$ (by
+defining $\TIMES$ as addition, \texttt{inverse} as negation and \texttt{1} as
+zero, say) or $\texttt{list} :: (\texttt{term})\texttt{semigroup}$ (e.g.\ if
+$\TIMES$ is list append). Thus, the characteristic constants $\TIMES$,
+\texttt{inverse}, \texttt{1} really become overloaded, i.e.\ have different
+meanings on different types.
+
+
+\subsection{Lifting and Functors}
+
+As already mentioned above, \HOL-like systems not only support
+overloaded definitions of polymorphic constants (without requiring
+type classes), but even primitive recursion over types. That is,
+definitional equations $c^\tau \emphq t$ may also contain constants of
+name $c$ on the RHS --- provided that these have types that are
+strictly simpler (structurally) than $\tau$.
+
+This feature enables us to \emph{lift operations}, e.g.\ to Cartesian
+products, direct sums or function spaces. Below, theory
+\texttt{ProdGroupInsts} lifts $\TIMES$ componentwise to two-place
+Cartesian products $\alpha \times \beta$:
+
+\begin{ascbox}
+ProdGroupInsts = Prod + Group +\medskip
+defs
+ prod@prod@def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"\medskip
+instance
+ "*" :: (semigroup, semigroup) semigroup
+ \{| simp@tac (prod@ss addsimps [assoc]) 1 |\}
+end
+\emphnd{ascbox}
+
+Note that \texttt{prod_prod_def} basically has the form $\emphdrv
+{\TIMES}^{\alpha \times \beta} \emphq \ldots {\TIMES}^\alpha \ldots
+{\TIMES}^\beta \ldots$, i.e.\ the recursive occurrences
+$\TIMES^\alpha$ and $\TIMES^\beta$ are really at ``simpler'' types.
+
+It is very easy to see that associativity of $\TIMES^\alpha$,
+$\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence
+the two-place type constructor $\times$ maps semigroups into
+semigroups. This fact is proven and put into Isabelle's type signature by
+above \texttt{instance} section.
+
+\medskip
+
+Thus, if we view class instances as ``structures'', overloaded
+constant definitions with primitive recursion over types indirectly
+provide some kind of ``functors'' (mappings between abstract theories,
+that is).
+
+
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "axclass"
+%%% End:
+
+
+\section{Syntactic classes}
+
+There is still a feature of Isabelle's type system left that we have not yet
+used: when declaring polymorphic constants $c :: \sigma$, the type variables
+occurring in $\sigma$ may be constrained by type classes (or even general
+sorts) in an arbitrary way. Note that by default, in Isabelle/HOL the
+declaration: FIXME
+
+\input{generated/Product}
+\input{generated/NatClass}
+
+
+
+\endinput
+
+
+%\section
+
+\begin{ascbox}
+ <*> :: ['a, 'a] => 'a
+\emphnd{ascbox}
+
+is actually an abbreviation for:
+
+\begin{ascbox}
+ <*> :: ['a::term, 'a::term] => 'a::term
+\emphnd{ascbox}
+
+Since class \texttt{term} is the universal class of \HOL, this is not
+really a restriction at all. A less trivial example is the following
+theory \texttt{Product}:
+
+\begin{ascbox}
+Product = HOL +\medskip
+axclass
+ product < term\medskip
+consts
+ "<*>" :: "['a::product, 'a] => 'a" (infixl 70)\medskip
+end
+\emphnd{ascbox}
+
+Here class \texttt{product} is defined as subclass of \texttt{term}, but
+without any additional axioms. This effects in logical equivalence of
+\texttt{product} and \texttt{term}, since \texttt{productI} is as follows:
+
+\begin{ascbox}
+productI: OFCLASS(?'a::logic, term@class) ==>
+ OFCLASS(?'a::logic, product@class)
+\emphnd{ascbox}
+
+I.e.\ $\texttt{term} \subseteq \texttt{product}$. The converse inclusion is
+already contained in the type signature of theory \texttt{Product}.
+
+Now, what is the difference of declaring $\TIMES :: [\alpha ::
+\texttt{product}, \alpha] \To \alpha$ vs.\ declaring $\TIMES :: [\alpha ::
+\texttt{term}, \alpha] \To \alpha$? In this special case (where
+$\texttt{product} \emphq \texttt{term}$), it should be obvious that both
+declarations are the same from the logic's point of view. It is even
+most sensible in the general case not to attach any \emph{logical}
+meaning to sort constraints occurring in constant \emph{declarations}
+(see \cite[page 79]{Wenzel94} for more details).
+
+On the other hand there are syntactic differences, of course.
+Constants $\TIMES^\tau$ are rejected by the type-checker, unless $\tau
+:: \texttt{product}$ is part of the type signature. In our example, this
+arity may be always added when required by means of a trivial
+\texttt{instance}.
+
+Thus, we can follow this discipline: Overloaded polymorphic constants
+have their type arguments restricted to an associated (logically
+trivial) class $c$. Only immediately before \emph{specifying} these
+constants on a certain type $\tau$ do we instantiate $\tau :: c$.
+
+This is done for class \texttt{product} and type \texttt{bool} in theory
+\texttt{ProductInsts} below:
+
+\begin{ascbox}
+ProductInsts = Product +\medskip
+instance
+ bool :: product\medskip
+defs
+ prod@bool@def "x <*> y == x & y::bool"\medskip
+end
+\emphnd{ascbox}
+
+Note that \texttt{instance bool ::\ product} does not require any
+witnesses, since this statement is logically trivial. Nonetheless,
+\texttt{instance} really performs a proof.
+
+Only after $\texttt{bool} :: \texttt{product}$ is made known to the type
+checker, does \texttt{prod_bool_def} become syntactically well-formed.
+
+\medskip
+
+It is very important to see that above \texttt{defs} are not directly
+connected with \texttt{instance} at all! We were just following our
+convention to specify $\TIMES$ on \texttt{bool} after having instantiated
+$\texttt{bool} :: \texttt{product}$. Isabelle does not require these definitions,
+which is in contrast to programming languages like Haskell.
+
+\medskip
+
+While Isabelle type classes and those of Haskell are almost the same as
+far as type-checking and type inference are concerned, there are major
+semantic differences. Haskell classes require their instances to
+\emph{provide operations} of certain \emph{names}. Therefore, its
+\texttt{instance} has a \texttt{where} part that tells the system what these
+``member functions'' should be.
+
+This style of \texttt{instance} won't make much sense in Isabelle, because its
+meta-logic has no corresponding notion of ``providing operations'' or
+``names''.
+
+
+\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:
+
+\begin{ascbox}
+NatClass = FOL +\medskip
+consts
+ "0" :: "'a" ("0")
+ Suc :: "'a => 'a"
+ rec :: "['a, 'a, ['a, 'a] => 'a] => 'a"\medskip
+axclass
+ nat < term
+ induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
+ Suc@inject "Suc(m) = Suc(n) ==> m = n"
+ Suc@neq@0 "Suc(m) = 0 ==> R"
+ rec@0 "rec(0, a, f) = a"
+ rec@Suc "rec(Suc(m), a, f) = f(m, rec(m, a, f))"\medskip
+consts
+ "+" :: "['a::nat, 'a] => 'a" (infixl 60)\medskip
+defs
+ add@def "m + n == rec(m, n, %x y. Suc(y))"\medskip
+end
+\emphnd{ascbox}
+
+\texttt{NatClass} is an abstract version of \texttt{Nat}\footnote{See
+ directory \texttt{FOL/ex}.}. Basically, we have just replaced all
+occurrences of \emph{type} \texttt{nat} by $\alpha$ and used the natural
+number axioms to define \emph{class} \texttt{nat}\footnote{There's a snag:
+ The original recursion operator \texttt{rec} had to be made monomorphic,
+ in a sense.}. Thus class \texttt{nat} contains exactly those types
+$\tau$ that are isomorphic to ``the'' natural numbers (with signature
+\texttt{0}, \texttt{Suc}, \texttt{rec}).
+
+Furthermore, theory \texttt{NatClass} defines an ``abstract constant'' $+$
+based on class \texttt{nat}.
+
+\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 class (or
+general sort) turns out to be empty (``inconsistent'')
+later\footnote{As a consequence of an old bug, this is \emph{not} true
+ for pre-Isabelle94-2 versions.}.
+
+For example, we may derive the following abstract natural numbers
+theorems:
+
+\begin{ascbox}
+add@0: 0 + (?n::?'a::nat) = ?n
+add@Suc: Suc(?m::?'a::nat) + (?n::?'a::nat) = Suc(?m + ?n)
+\emphnd{ascbox}
+
+See also file \texttt{FOL/ex/NatClass.ML}. Note that this required only
+some trivial modifications of the original \texttt{Nat.ML}.
+
+
+%% FIXME move some parts to ref or isar-ref manual (!?);
+
+% \chapter{The user interface of Isabelle's axclass package}
+
+% The actual axiomatic type class package of Isabelle/Pure mainly consists
+% of two new theory sections: \texttt{axclass} and \texttt{instance}. Some
+% typical applications of these have already been demonstrated in
+% \secref{sec:ex}, below their syntax and semantics are presented more
+% completely.
+
+
+% \section{The axclass section}
+
+% Within theory files, \texttt{axclass} introduces an axiomatic type class
+% definition. Its concrete syntax is:
+
+% \begin{matharray}{l}
+% \texttt{axclass} \\
+% \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
+% \ \ id@1\ axm@1 \\
+% \ \ \vdots \\
+% \ \ id@m\ axm@m
+% \emphnd{matharray}
+
+% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
+% $string$) and $axm@1, \ldots, axm@m$ (with $m \ge
+% 0$) are formulas (category $string$).
+
+% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
+% \texttt{logic}. Each class axiom $axm@j$ may contain any term
+% variables, but at most one type variable (which need not be the same
+% for all axioms). The sort of this type variable has to be a supersort
+% of $\{c@1, \ldots, c@n\}$.
+
+% \medskip
+
+% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
+% c@n$ to the type signature.
+
+% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
+% ``abstract axioms'' of $c$ with names $id@1, \ldots,
+% id@m$. This is done by replacing all occurring type variables
+% by $\alpha :: c$. Original axioms that do not contain any type
+% variable will be prefixed by the logical precondition
+% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
+
+% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
+% rule'' --- is built from the respective universal closures of
+% $axm@1, \ldots, axm@m$ appropriately.
+
+
+% \section{The instance section}
+
+% Section \texttt{instance} proves class inclusions or type arities at the
+% logical level and then transfers these into the type signature.
+
+% Its concrete syntax is:
+
+% \begin{matharray}{l}
+% \texttt{instance} \\
+% \ \ [\ c@1 \texttt{ < } c@2 \ |\
+% t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
+% \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
+% \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
+% \emphnd{matharray}
+
+% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
+% (all of category $id$ or $string)$. Furthermore,
+% $sort@i$ are sorts in the usual Isabelle-syntax.
+
+% \medskip
+
+% Internally, \texttt{instance} first sets up an appropriate goal that
+% expresses the class inclusion or type arity as a meta-proposition.
+% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
+% meta-definitions of the current theory file and the user-supplied
+% witnesses. The latter are $name@1, \ldots, name@m$, where
+% $id$ refers to an \ML-name of a theorem, and $string$ to an
+% axiom of the current theory node\footnote{Thus, the user may reference
+% axioms from above this \texttt{instance} in the theory file. Note
+% that new axioms appear at the \ML-toplevel only after the file is
+% processed completely.}.
+
+% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
+% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
+% according to their form: Meta-definitions are unfolded, all other
+% formulas are repeatedly resolved\footnote{This is done in a way that
+% enables proper object-\emph{rules} to be used as witnesses for
+% corresponding class axioms.} with.
+
+% The final optional argument $text$ is \ML-code of an arbitrary
+% user tactic which is applied last to any remaining goals.
+
+% \medskip
+
+% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
+% new users of the axclass package are advised to only use the simple
+% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
+% the identifiers refer to theorems that are appropriate type instances
+% of the class axioms. This typically requires an auxiliary theory,
+% though, which defines some constants and then proves these witnesses.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "axclass"
+%%% End:
+% LocalWords: Isabelle FOL
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Group.aux Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,20 @@
+\relax
+\@setckpt{generated/Group}{
+\setcounter{page}{4}
+\setcounter{equation}{0}
+\setcounter{enumi}{0}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Group.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,127 @@
+\begin{isabelle}%
+\isanewline
+\isacommand{theory}~Group~=~Main:\isanewline
+\isanewline
+\isanewline
+\isacommand{consts}\isanewline
+~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline
+~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline
+~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})\isanewline
+\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~monoid~<~{"}term{"}\isanewline
+~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
+~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
+\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~semigroup~<~{"}term{"}\isanewline
+~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~group~<~semigroup\isanewline
+~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
+~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}%
+\begin{isamarkuptext}%
+The group axioms only state the properties of left unit and inverse,
+ the right versions may be derived as follows.%
+\end{isamarkuptext}%
+\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}::'a::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{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
+~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline
+~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
+~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{qed}%
+\begin{isamarkuptext}%
+With $group_right_inverse$ already available,
+ $group_right_unit$\label{thm:group-right-unit} is now established
+ much easier.%
+\end{isamarkuptext}%
+\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x::'a::group){"}\isanewline
+\isacommand{proof}~-\isanewline
+~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline
+~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline
+~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline
+~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline
+\isacommand{qed}\isanewline
+\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~agroup~<~group\isanewline
+~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}\isanewline
+\isanewline
+\isanewline
+\isanewline
+\isacommand{instance}~monoid~<~semigroup\isanewline
+\isacommand{proof}~intro\_classes\isanewline
+~~\isacommand{fix}~x~y~z~::~{"}'a::monoid{"}\isanewline
+~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline
+\isacommand{qed}\isanewline
+\isanewline
+\isanewline
+\isacommand{instance}~group~<~monoid\isanewline
+\isacommand{proof}~intro\_classes\isanewline
+~~\isacommand{fix}~x~y~z~::~{"}'a::group{"}\isanewline
+~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline
+~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline
+~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline
+~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline
+~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline
+~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline
+\isacommand{qed}\isanewline
+\isanewline
+\isanewline
+\isanewline
+\isacommand{defs}\isanewline
+~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline
+~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline
+~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}\isanewline
+\isanewline
+\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{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}\isanewline
+\isanewline
+\isanewline
+\isacommand{defs}\isanewline
+~~prod\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}\isanewline
+\isanewline
+\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline
+\isacommand{proof}~(intro\_classes,~unfold~prod\_prod\_def)\isanewline
+~~\isacommand{fix}~p~q~r~::~{"}'a::semigroup~*~'b::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
+~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline
+~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline
+~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline
+\isacommand{qed}\isanewline
+\isanewline
+\isacommand{end}\end{isabelle}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/NatClass.aux Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,20 @@
+\relax
+\@setckpt{generated/NatClass}{
+\setcounter{page}{6}
+\setcounter{equation}{0}
+\setcounter{enumi}{0}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/NatClass.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,23 @@
+\begin{isabelle}%
+\isanewline
+\isanewline
+\isacommand{theory}~NatClass~=~FOL:\isanewline
+\isanewline
+\isacommand{consts}\isanewline
+~~zero~::~'a~~~~({"}0{"})\isanewline
+~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline
+~~rec~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~'a{"}\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~nat~<~{"}term{"}\isanewline
+~~induct:~~~~~{"}P(0)~{\isasymLongrightarrow}~({\isasymAnd}x.~P(x)~{\isasymLongrightarrow}~P(Suc(x)))~{\isasymLongrightarrow}~P(n){"}\isanewline
+~~Suc\_inject:~{"}Suc(m)~=~Suc(n)~{\isasymLongrightarrow}~m~=~n{"}\isanewline
+~~Suc\_neq\_0:~~{"}Suc(m)~=~0~{\isasymLongrightarrow}~R{"}\isanewline
+~~rec\_0:~~~~~~{"}rec(0,~a,~f)~=~a{"}\isanewline
+~~rec\_Suc:~~~~{"}rec(Suc(m),~a,~f)~=~f(m,~rec(m,~a,~f)){"}\isanewline
+\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
+\isacommand{end}\end{isabelle}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Product.aux Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,20 @@
+\relax
+\@setckpt{generated/Product}{
+\setcounter{page}{5}
+\setcounter{equation}{0}
+\setcounter{enumi}{0}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Product.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,16 @@
+\begin{isabelle}%
+\isanewline
+\isanewline
+\isacommand{theory}~Product~=~Main:\isanewline
+\isanewline
+\isacommand{axclass}\isanewline
+~~product~<~{"}term{"}\isanewline
+\isacommand{consts}\isanewline
+~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)\isanewline
+\isanewline
+\isacommand{instance}~bool~::~product\isanewline
+~~\isacommand{by}~intro\_classes\isanewline
+\isacommand{defs}\isanewline
+~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}\isanewline
+\isanewline
+\isacommand{end}\end{isabelle}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Semigroup.aux Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,20 @@
+\relax
+\@setckpt{generated/Semigroup}{
+\setcounter{page}{2}
+\setcounter{equation}{0}
+\setcounter{enumi}{0}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Semigroup.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,10 @@
+\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}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Semigroups.aux Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,20 @@
+\relax
+\@setckpt{generated/Semigroups}{
+\setcounter{page}{3}
+\setcounter{equation}{0}
+\setcounter{enumi}{0}
+\setcounter{enumii}{0}
+\setcounter{enumiii}{0}
+\setcounter{enumiv}{0}
+\setcounter{footnote}{0}
+\setcounter{mpfootnote}{0}
+\setcounter{part}{0}
+\setcounter{chapter}{0}
+\setcounter{section}{0}
+\setcounter{subsection}{0}
+\setcounter{subsubsection}{0}
+\setcounter{paragraph}{0}
+\setcounter{subparagraph}{0}
+\setcounter{figure}{0}
+\setcounter{table}{0}
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/Semigroups.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,28 @@
+\begin{isabelle}%
+\isacommand{theory}~Semigroups~=~Main:%
+\begin{isamarkuptext}%
+\noindent Associativity of binary operations:%
+\end{isamarkuptext}%
+\isacommand{constdefs}\isanewline
+~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline
+~~{"}is\_assoc~f~==~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}%
+\begin{isamarkuptext}%
+\medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}:
+ %term (latex xsymbols symbols) "op \<Oplus>";%
+\end{isamarkuptext}%
+\isacommand{consts}\isanewline
+~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline
+\isacommand{axclass}\isanewline
+~~plus\_semigroup~<~{"}term{"}\isanewline
+~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}%
+\begin{isamarkuptext}%
+\medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}:
+ %term (latex xsymbols symbols) "op \<Otimes>";%
+\end{isamarkuptext}%
+\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
+\isacommand{end}\end{isabelle}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/isabelle.sty Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,52 @@
+%%
+%% $Id$
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language)
+
+% isabelle environments
+
+\newcommand{\isabellestyle}{\small\tt\slshape}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+\newenvironment{isabelle}{%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isabellestyle}{}
+
+\newcommand{\isa}[1]{\emph{\isabellestyle #1}}
+
+\newenvironment{isabellequote}%
+{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
+
+\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+
+\chardef\isabraceleft=`\{
+\chardef\isabraceright=`\}
+\chardef\isatilde=`\~
+\chardef\isacircum=`\^
+\chardef\isabackslash=`\\
+
+
+% keyword and section markup
+
+\newcommand{\isacommand}[1]{\emph{\bf #1}}
+\newcommand{\isakeyword}[1]{\emph{\bf #1}}
+\newcommand{\isabeginblock}{\isakeyword{\{}}
+\newcommand{\isaendblock}{\isakeyword{\}}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
+\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/isabellesym.sty Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,152 @@
+%%
+%% $Id$
+%%
+%% definitions of many Isabelle symbols
+%%
+
+\usepackage{latexsym}
+%\usepackage[latin1]{inputenc}
+
+\newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack
+%\def\textbrokenbar??? etc
+
+\newcommand{\isasymspacespace}{~~}
+\newcommand{\isasymGamma}{$\Gamma$}
+\newcommand{\isasymDelta}{$\Delta$}
+\newcommand{\isasymTheta}{$\Theta$}
+\newcommand{\isasymLambda}{$\Lambda$}
+\newcommand{\isasymPi}{$\Pi$}
+\newcommand{\isasymSigma}{$\Sigma$}
+\newcommand{\isasymPhi}{$\Phi$}
+\newcommand{\isasymPsi}{$\Psi$}
+\newcommand{\isasymOmega}{$\Omega$}
+\newcommand{\isasymalpha}{$\alpha$}
+\newcommand{\isasymbeta}{$\beta$}
+\newcommand{\isasymgamma}{$\gamma$}
+\newcommand{\isasymdelta}{$\delta$}
+\newcommand{\isasymepsilon}{$\varepsilon$}
+\newcommand{\isasymzeta}{$\zeta$}
+\newcommand{\isasymeta}{$\eta$}
+\newcommand{\isasymtheta}{$\vartheta$}
+\newcommand{\isasymkappa}{$\kappa$}
+\newcommand{\isasymlambda}{$\lambda$}
+\newcommand{\isasymmu}{$\mu$}
+\newcommand{\isasymnu}{$\nu$}
+\newcommand{\isasymxi}{$\xi$}
+\newcommand{\isasympi}{$\pi$}
+\newcommand{\isasymrho}{$\rho$}
+\newcommand{\isasymsigma}{$\sigma$}
+\newcommand{\isasymtau}{$\tau$}
+\newcommand{\isasymphi}{$\varphi$}
+\newcommand{\isasymchi}{$\chi$}
+\newcommand{\isasympsi}{$\psi$}
+\newcommand{\isasymomega}{$\omega$}
+\newcommand{\isasymnot}{\emph{$\neg$}}
+\newcommand{\isasymand}{\emph{$\wedge$}}
+\newcommand{\isasymor}{\emph{$\vee$}}
+\newcommand{\isasymforall}{\emph{$\forall\,$}}
+\newcommand{\isasymexists}{\emph{$\exists\,$}}
+\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
+\newcommand{\isasymlceil}{\emph{$\lceil$}}
+\newcommand{\isasymrceil}{\emph{$\rceil$}}
+\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
+\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
+\newcommand{\isasymturnstile}{\emph{$\vdash$}}
+\newcommand{\isasymTurnstile}{\emph{$\models$}}
+\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
+\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
+\newcommand{\isasymcdot}{\emph{$\cdot$}}
+\newcommand{\isasymin}{\emph{$\in$}}
+\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
+\newcommand{\isasyminter}{\emph{$\cap$}}
+\newcommand{\isasymunion}{\emph{$\cup$}}
+\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
+\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
+\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
+\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
+\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}
+\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
+\newcommand{\isasymbottom}{\emph{$\bot$}}
+\newcommand{\isasymdoteq}{\emph{$\doteq$}}
+\newcommand{\isasymequiv}{\emph{$\equiv$}}
+\newcommand{\isasymnoteq}{\emph{$\not=$}}
+\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
+\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
+\newcommand{\isasymprec}{\emph{$\prec$}}
+\newcommand{\isasympreceq}{\emph{$\preceq$}}
+\newcommand{\isasymsucc}{\emph{$\succ$}}
+\newcommand{\isasymapprox}{\emph{$\approx$}}
+\newcommand{\isasymsim}{\emph{$\sim$}}
+\newcommand{\isasymsimeq}{\emph{$\simeq$}}
+\newcommand{\isasymle}{\emph{$\le$}}
+\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
+\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
+\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated
+\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
+\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
+\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
+\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
+\newcommand{\isasymbow}{\emph{$\frown$}}
+\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
+\newcommand{\isasymleadsto}{\emph{$\leadsto$}}
+\newcommand{\isasymup}{\emph{$\uparrow$}}
+\newcommand{\isasymdown}{\emph{$\downarrow$}}
+\newcommand{\isasymnotin}{\emph{$\notin$}}
+\newcommand{\isasymtimes}{\emph{$\times$}}
+\newcommand{\isasymoplus}{\emph{$\oplus$}}
+\newcommand{\isasymominus}{\emph{$\ominus$}}
+\newcommand{\isasymotimes}{\emph{$\otimes$}}
+\newcommand{\isasymoslash}{\emph{$\oslash$}}
+\newcommand{\isasymsubset}{\emph{$\subset$}}
+\newcommand{\isasyminfinity}{\emph{$\infty$}}
+\newcommand{\isasymbox}{\emph{$\Box$}}
+\newcommand{\isasymdiamond}{\emph{$\Diamond$}}
+\newcommand{\isasymcirc}{\emph{$\circ$}}
+\newcommand{\isasymbullet}{\emph{$\bullet$}}
+\newcommand{\isasymparallel}{\emph{$\parallel$}}
+\newcommand{\isasymsurd}{\emph{$\surd$}}
+\newcommand{\isasymcopyright}{\emph{\copyright}}
+
+\newcommand{\isasymplusminus}{\emph{$\pm$}}
+\newcommand{\isasymdiv}{\emph{$\div$}}
+\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
+\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
+\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
+\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
+\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
+\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
+%requires OT1 encoding:
+\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}}
+\newcommand{\isasymhyphen}{-}
+\newcommand{\isasymmacron}{\={}}
+\newcommand{\isasymexclamdown}{\emph{\textexclamdown}}
+\newcommand{\isasymquestiondown}{\emph{\textquestiondown}}
+%requires OT1 encoding:
+\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}}
+%requires OT1 encoding:
+\newcommand{\isasymguillemotright}{\emph{\guillemotright}}
+%should be available (?):
+\newcommand{\isasymdegree}{\emph{\textdegree}}
+\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}
+\newcommand{\isasymonequarter}{\emph{\textonequarter}}
+\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}
+\newcommand{\isasymonehalf}{\emph{\textonehalf}}
+\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}
+\newcommand{\isasymthreequarters}{\emph{\textthreequarters}}
+\newcommand{\isasymparagraph}{\emph{\P}}
+\newcommand{\isasymregistered}{\emph{\textregistered}}
+%should be available (?):
+\newcommand{\isasymordfeminine}{\emph{\textordfeminine}}
+%should be available (?):
+\newcommand{\isasymordmasculine}{\emph{\textordmasculine}}
+\newcommand{\isasymsection}{\S}
+\newcommand{\isasympounds}{\emph{$\pounds$}}
+%requires OT1 encoding:
+\newcommand{\isasymyen}{\emph{\textyen}}
+%requires OT1 encoding:
+\newcommand{\isasymcent}{\emph{\textcent}}
+%requires OT1 encoding:
+\newcommand{\isasymcurrency}{\emph{\textcurrency}}
+\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
+\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
+\newcommand{\isasymtop}{\emph{$\top$}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/pdfsetup.sty Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,9 @@
+%%
+%% $Id$
+%%
+%% conditional url/hyperref setup
+%%
+
+\@ifundefined{pdfoutput}{\usepackage{url}}
+{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
+ \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/AxClass/generated/session.tex Sun May 21 01:12:00 2000 +0200
@@ -0,0 +1,4 @@
+\input{Semigroup.tex}
+\input{Semigroups.tex}
+\input{Group.tex}
+\input{Product.tex}
--- a/doc-src/AxClass/style.tex Sat May 20 18:37:21 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,362 +0,0 @@
-
-\documentclass[11pt,a4paper,fleqn]{article}
-\usepackage{bbb,../pdfsetup}
-
-\makeatletter
-
-
-%%% layout
-
-\sloppy
-
-\parindent 0pt
-\parskip 0.5ex
-
-
-%%% text mode
-
-\newcommand{\B}[1]{\textbf{#1}}
-\newcommand{\TT}[1]{\ifmmode\mbox{\texttt{#1}}\else\texttt{#1}\fi}
-\newcommand{\E}[1]{\emph{#1}}
-\renewcommand{\P}[1]{\textsc{#1}}
-
-
-\renewcommand{\labelenumi}{(\theenumi)}
-\newcommand{\dfn}[1]{{\bf #1}}
-
-\newcommand{\thy}[1]{\mbox{\sc #1}}
-%\newcommand{\thy}[1]{\mbox{\textsc{#1}}}
-\newcommand{\IHOL}{\thy{ihol}}
-\newcommand{\SIHOL}{\thy{sihol}}
-\newcommand{\HOL}{\thy{hol}}
-\newcommand{\HOLBB}{\thy{hol88}}
-\newcommand{\FOL}{\thy{fol}}
-\newcommand{\SET}{\thy{set}}
-\newcommand{\Pure}{\thy{Pure}}
-
-
-\newcommand{\secref}[1]{\S\ref{#1}}
-
-\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
-
-
-%from alltt.sty
-\def\docspecials{\do\ \do\$\do\&%
- \do\#\do\^\do\^^K\do\_\do\^^A\do\%\do\~}
-
-\newenvironment{asc}{\small\trivlist \item[]\if@minipage\else\vskip\parskip\fi
-\leftskip\@totalleftmargin\rightskip\z@
-\parindent\z@\parfillskip\@flushglue\parskip\z@
-\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
-\obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \docspecials
-\frenchspacing\@vobeyspaces}{\endtrivlist}
-
-\newenvironment{ascbox}{\vbox\bgroup\begin{asc}}{\end{asc}\egroup}
-\newcommand{\brk}{\end{ascbox}\vskip-20pt\begin{ascbox}}
-
-\newcommand{\out}[1]{{\fontfamily{cmtt}\fontseries{m}\fontshape{sl}\selectfont\ \ #1}}
-
-
-% warning environment
-\newcommand{\dbend}{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
-\newenvironment{warning}{\medskip\medbreak\begingroup \clubpenalty=10000
- \noindent \hangindent1.5em \hangafter=-2
- \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
- {\par\endgroup\medbreak}
-
-\newcommand{\Isa}{{\sc Isabelle}}
-\newcommand{\ML}{{\sc ml}}
-\newcommand{\Haskell}{{\rm Haskell}}
-
-\newcommand{\IMP}{"`$\Longrightarrow$"'}
-\newcommand{\PMI}{"`$\Longleftarrow$"'}
-
-
-
-%%% math mode
-
-%% generic defs
-
-\newcommand{\nquad}{\hskip-1em}
-
-\newcommand{\fct}[1]{\mathop{\rm #1}\nolimits}
-\newcommand{\idt}[1]{{\mathord{\it #1}}}
-\newcommand{\syn}[1]{{\mathord{\it #1}}}
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\rmtext}[1]{\mbox{\rm #1}}
-%\newcommand{\mtt}[1]{\mbox{\tt #1}}
-
-\newcommand{\falls}{\text{falls }}
-\newcommand{\sonst}{\text{sonst}}
-
-\newcommand{\Bool}{\bbbB}
-\newcommand{\Nat}{\bbbN}
-\newcommand{\Natz}{{\bbbN_0}}
-\newcommand{\Rat}{\bbbQ}
-\newcommand{\Real}{\bbbR}
-
-\newcommand{\dt}{{\mathpunct.}}
-
-\newcommand{\Gam}{\Gamma}
-\renewcommand{\epsilon}{\varepsilon}
-\renewcommand{\phi}{\varphi}
-\renewcommand{\rho}{\varrho}
-\newcommand{\eset}{{\{\}}}
-\newcommand{\etuple}{{\langle\rangle}}
-
-\newcommand{\dfneq}{\mathbin{\mathord:\mathord=}}
-\newcommand{\impl}{\Longrightarrow}
-\renewcommand{\iff}{{\;\;\mathord{\Longleftrightarrow}\;\;}}
-\newcommand{\dfniff}{{\;\;\mathord:\mathord{\Longleftrightarrow}\;\;}}
-\renewcommand{\land}{\mathrel{\,\wedge\,}}
-\renewcommand{\lor}{\mathrel{\,\vee\,}}
-\newcommand{\iso}{\cong}
-
-\newcommand{\union}{\cup}
-\newcommand{\sunion}{\mathbin{\;\cup\;}}
-\newcommand{\dunion}{\mathbin{\dot\union}}
-\newcommand{\Union}{\bigcup}
-\newcommand{\inter}{\cap}
-\newcommand{\where}{\mathrel|}
-\newcommand{\pto}{\rightharpoonup}
-\newcommand{\comp}{\circ}
-\newcommand{\aaast}{{\mathord*\mathord*\mathord*}}
-
-\newcommand{\all}[1]{\forall #1\dt\;}
-\newcommand{\ex}[1]{\exists #1\dt\;}
-\newcommand{\lam}[1]{\mathop{\lambda} #1\dt}
-
-\newcommand\lbrakk{\mathopen{[\![}}
-\newcommand\rbrakk{\mathclose{]\!]}}
-
-\newcommand{\unif}{\mathrel{=^?}}
-\newcommand{\notunif}{\mathrel{{\not=}^?}}
-\newcommand{\incompat}{\mathrel{\#}}
-
-
-%% specific defs
-
-\newcommand{\PLUS}{\mathord{\langle{+}\rangle}}
-\newcommand{\TIMES}{\mathord{\langle{*}\rangle}}
-
-
-% IHOL
-
-\newcommand{\TV}{\fct{TV}}
-\newcommand{\FV}{\fct{FV}}
-\newcommand{\BV}{\fct{BV}}
-\newcommand{\VN}{\fct{VN}}
-\newcommand{\AT}{\fct{AT}}
-\newcommand{\STV}{\fct{STV}}
-
-\newcommand{\TyVars}{\syn{TyVars}}
-\newcommand{\TyNames}{\syn{TyNames}}
-\newcommand{\TyCons}{\syn{TyCons}}
-\newcommand{\TyConsSg}{\TyCons_\Sigma}
-\newcommand{\Types}{\syn{Types}}
-\newcommand{\TypesSg}{\Types_\Sigma}
-\newcommand{\GrTypes}{\syn{GrTypes}}
-\newcommand{\GrTypesSg}{\GrTypes_\Sigma}
-\newcommand{\VarNames}{\syn{VarNames}}
-\newcommand{\Vars}{\syn{Vars}}
-\newcommand{\VarsSg}{\Vars_\Sigma}
-\newcommand{\GrVars}{\syn{GrVars}}
-\newcommand{\GrVarsSg}{\GrVars_\Sigma}
-\newcommand{\ConstNames}{\syn{ConstNames}}
-\newcommand{\Consts}{\syn{Consts}}
-\newcommand{\ConstsSg}{\Consts_\Sigma}
-\newcommand{\GrConsts}{\syn{GrConsts}}
-\newcommand{\GrConstsSg}{\GrConsts_\Sigma}
-\newcommand{\Terms}{\syn{Terms}}
-\newcommand{\TermsSg}{\Terms_\Sigma}
-\newcommand{\GrTerms}{\syn{GrTerms}}
-\newcommand{\GrTermsSg}{\GrTerms_\Sigma}
-\newcommand{\Forms}{\syn{Forms}}
-\newcommand{\FormsTh}{\Forms_\Theta}
-\newcommand{\Seqs}{\syn{Seqs}}
-\newcommand{\SeqsTh}{\Seqs_\Theta}
-\newcommand{\Axms}{\syn{Axms}}
-\newcommand{\AxmsTh}{\Axms_\Theta}
-\newcommand{\Thms}{\syn{Thms}}
-\newcommand{\ThmsTh}{\Thms_\Theta}
-
-
-\newcommand{\U}{{\cal U}}
-\newcommand{\UU}{\bbbU}
-
-\newcommand{\ty}{{\mathbin{\,:\,}}}
-\newcommand{\typ}[1]{{\mathord{\sl #1}}}
-\newcommand{\tap}{\mathord{\,}}
-\newcommand{\prop}{\typ{prop}}
-\newcommand{\itself}{\typ{itself}}
-
-\newcommand{\cnst}[1]{{\mathord{\sl #1}}}
-\newcommand{\ap}{\mathbin{}}
-\newcommand{\To}{\Rightarrow}
-\newcommand{\Eq}{\equiv}
-\newcommand{\Impl}{\Rightarrow}
-\newcommand{\Forall}{\mathop{\textstyle\bigwedge}}
-\newcommand{\All}[1]{\Forall #1\dt}
-\newcommand{\True}{\top}
-\newcommand{\False}{\bot}
-\newcommand{\Univ}{{\top\!\!\!\!\top}}
-\newcommand{\Conj}{\wedge}
-\newcommand{\TYPE}{\cnst{TYPE}}
-
-
-% rules
-
-\newcommand{\Axm}{\rmtext{Axm}}
-\newcommand{\Assm}{\rmtext{Assm}}
-\newcommand{\Mon}{\rmtext{Mon}}
-\newcommand{\ImplI}{\mathord{\Impl}\rmtext{I}}
-\newcommand{\ImplE}{\mathord{\Impl}\rmtext{E}}
-\newcommand{\ImplMP}{\rmtext{MP}}
-\newcommand{\ImplRefl}{\mathord{\Impl}\rmtext{Refl}}
-\newcommand{\ImplTrans}{\mathord{\Impl}\rmtext{Trans}}
-\newcommand{\EqRefl}{\mathord{\Eq}\rmtext{Refl}}
-\newcommand{\EqTrans}{\mathord{\Eq}\rmtext{Trans}}
-\newcommand{\EqSym}{\mathord{\Eq}\rmtext{Sym}}
-\newcommand{\EqApp}{\mathord{\Eq}\rmtext{App}}
-\newcommand{\EqAbs}{\mathord{\Eq}\rmtext{Abs}}
-\newcommand{\Eqa}{\mathord{\Eq}\alpha}
-\newcommand{\Eqb}{\mathord{\Eq}\beta}
-\newcommand{\Eqe}{\mathord{\Eq}\eta}
-\newcommand{\Ext}{\rmtext{Ext}}
-\newcommand{\EqI}{\mathord{\Eq}\rmtext{I}}
-\newcommand{\EqMP}{\mathord{\Eq}\rmtext{MP}}
-\newcommand{\EqUnfold}{\mathord{\Eq}\rmtext{Unfold}}
-\newcommand{\EqFold}{\mathord{\Eq}\rmtext{Fold}}
-\newcommand{\AllI}{\mathord{\Forall}\rmtext{I}}
-\newcommand{\AllE}{\mathord{\Forall}\rmtext{E}}
-\newcommand{\TypInst}{\rmtext{TypInst}}
-\newcommand{\Inst}{\rmtext{Inst}}
-\newcommand{\TrueI}{\True\rmtext{I}}
-\newcommand{\FalseE}{\False\rmtext{E}}
-\newcommand{\UnivI}{\Univ\rmtext{I}}
-\newcommand{\ConjI}{\mathord{\Conj}\rmtext{I}}
-\newcommand{\ConjE}{\mathord{\Conj}\rmtext{E}}
-\newcommand{\ConjProj}{\mathord{\Conj}\rmtext{Proj}}
-\newcommand{\ImplCurry}{\mathord{\Impl}\rmtext{Curry}}
-\newcommand{\ImplUncurry}{\mathord{\Impl}\rmtext{Uncurry}}
-\newcommand{\CImplI}{\mathord{\Conj}\mathord{\Impl}\rmtext{I}}
-\newcommand{\CImplE}{\mathord{\Conj}\mathord{\Impl}\rmtext{E}}
-\newcommand{\Subclass}{\rmtext{Subclass}}
-\newcommand{\Subsort}{\rmtext{Subsort}}
-\newcommand{\VarSort}{\rmtext{VarSort}}
-\newcommand{\Arity}{\rmtext{Arity}}
-\newcommand{\SortMP}{\rmtext{SortMP}}
-\newcommand{\TopSort}{\rmtext{TopSort}}
-\newcommand{\OfSort}{\rmtext{OfSort}}
-
-\newcommand{\infr}{{\mathrel/}}
-\newcommand{\einfr}{{}{\mathrel/}}
-
-\newcommand{\drv}{\mathrel{\vdash}}
-\newcommand{\Drv}[1]{\mathrel{\mathord{\drv}_{#1}}}
-\newcommand{\Gdrv}{\Gam\drv}
-\newcommand{\edrv}{\mathop{\drv}\nolimits}
-\newcommand{\Edrv}[1]{\mathop{\drv}\nolimits_{#1}}
-\newcommand{\notEdrv}[1]{\mathop{\not\drv}\nolimits_{#1}}
-
-\newcommand{\lsem}{\lbrakk}
-\newcommand{\rsem}{\rbrakk}
-\newcommand{\sem}[1]{{\lsem #1\rsem}}
-
-\newcommand{\vld}{\mathrel{\models}}
-\newcommand{\Vld}[1]{\mathrel{\mathord{\models}_#1}}
-\newcommand{\Evld}[1]{\mathop{\vld}\nolimits_{#1}}
-\newcommand{\notEvld}[1]{\mathop{\not\vld}\nolimits_{#1}}
-
-\newcommand{\EQ}{\fct{EQ}}
-\newcommand{\IMPL}{\fct{IMPL}}
-\newcommand{\ALL}{\fct{ALL}}
-
-\newcommand{\extcv}{\mathrel{\unlhd}}
-\newcommand{\weakth}{\preceq}
-\newcommand{\eqvth}{\approx}
-\newcommand{\extdcli}{\mathrel{<_{\rm dcl}^1}}
-\newcommand{\extdcl}{\mathrel{\le_{\rm dcl}}}
-\newcommand{\extdfni}{\mathrel{<_{\rm dfn}^1}}
-\newcommand{\extdfn}{\mathrel{\le_{\rm dfn}}}
-\newcommand{\extsdfn}{\mathrel{\le_{\rm sdfn}}}
-\newcommand{\extqdfn}{\mathrel{\le_{\rm qdfn}}}
-
-\newcommand{\lvarbl}{\langle}
-\newcommand{\rvarbl}{\rangle}
-\newcommand{\varbl}[1]{{\lvarbl #1\rvarbl}}
-\newcommand{\up}{{\scriptstyle\mathord\uparrow}}
-\newcommand{\down}{{\scriptstyle\mathord\downarrow}}
-\newcommand{\Down}{{\mathord\downarrow}}
-
-
-\newcommand{\Sle}{{\mathrel{\le_S}}}
-\newcommand{\Classes}{\syn{Classes}}
-\newcommand{\ClassNames}{\syn{ClassNames}}
-\newcommand{\Sorts}{\syn{Sorts}}
-\newcommand{\TyVarNames}{\syn{TyVarNames}}
-\newcommand{\STyVars}{\syn{STyVars}}
-\newcommand{\STyArities}{\syn{STyArities}}
-\newcommand{\STypes}{\syn{STypes}}
-\newcommand{\SVars}{\syn{SVars}}
-\newcommand{\SConsts}{\syn{SConsts}}
-\newcommand{\STerms}{\syn{STerms}}
-\newcommand{\SForms}{\syn{SForms}}
-\newcommand{\SAxms}{\syn{SAxms}}
-\newcommand{\T}{{\cal T}}
-
-\newcommand{\cls}[1]{{\mathord{\sl #1}}}
-\newcommand{\intsrt}{\sqcap}
-\newcommand{\Intsrt}{{\mathop\sqcap}}
-\newcommand{\subcls}{\preceq}
-\newcommand{\Subcls}[1]{\mathrel{\subcls_{#1}}}
-\newcommand{\subsrt}{\sqsubseteq}
-\newcommand{\Subsrt}[1]{\mathrel{\subsrt_{#1}}}
-\newcommand{\subsrtp}{\sqsubset}
-\newcommand{\eqvsrt}{\approx}
-\newcommand{\topsrt}{\top}
-\newcommand{\srt}{\ty}
-
-\newcommand{\sct}[1]{{\bf #1}}
-\newcommand{\CLASSES}{\sct{classes}}
-\newcommand{\CLASSREL}{\sct{classrel}}
-\newcommand{\TYPES}{\sct{types}}
-\newcommand{\ARITIES}{\sct{arities}}
-\newcommand{\CONSTS}{\sct{consts}}
-\newcommand{\AXIOMS}{\sct{axioms}}
-\newcommand{\DEFNS}{\sct{defns}}
-\newcommand{\AXCLASS}{\sct{axclass}}
-\newcommand{\INSTANCE}{\sct{instance}}
-
-\newcommand{\Srt}{{\mathbin{\,:\,}}}
-\newcommand{\insrt}[2]{{\mathopen{(\!|} #1 \Srt #2 \mathclose{|\!)}}}
-\newcommand{\ofsrt}[2]{{\mathopen{\langle\!|} #1 \Srt #2 \mathclose{|\!\rangle}}}
-
-\newcommand{\injV}{{\iota_V}}
-\newcommand{\inj}{\iota}
-\newcommand{\injC}{{\iota_C}}
-\newcommand{\I}{{\cal I}}
-\newcommand{\C}{{\cal C}}
-
-\newcommand{\Sdrv}{\mathrel{\vdash\!\!\!\vdash}}
-\newcommand{\SDrv}[1]{\mathrel{\mathord{\Sdrv}_{#1}}}
-\newcommand{\SGdrv}{\Gam\Sdrv}
-\newcommand{\Sedrv}{\mathop{\Sdrv}\nolimits}
-\newcommand{\SEdrv}[1]{\mathop{\Sdrv}\nolimits_{#1}}
-
-\newcommand{\SSubclass}{\rmtext{S-Subclass}}
-\newcommand{\SSubsort}{\rmtext{S-Subsort}}
-\newcommand{\SVarSort}{\rmtext{S-VarSort}}
-\newcommand{\SArity}{\rmtext{S-Arity}}
-\newcommand{\SSortMP}{\rmtext{S-SortMP}}
-\newcommand{\STopSort}{\rmtext{S-TopSort}}
-\newcommand{\SOfSort}{\rmtext{S-OfSort}}
-
-
-\makeatother
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: