# HG changeset patch # User wenzelm # Date 958864320 -7200 # Node ID 9a44d8d98731f04bec9a7388ef2764f547325996 # Parent 2ec6371fde543e579bc1b65a0713a743ce27afd5 snapshot of new Isar'ized version; diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/Group.thy --- /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 "\" 70) + inverse :: "'a => 'a" ("(_\)" [1000] 999) + one :: 'a ("\"); + + +axclass + monoid < "term" + assoc: "(x \ y) \ z = x \ (y \ z)" + left_unit: "\ \ x = x" + right_unit: "x \ \ = x"; + + +axclass + semigroup < "term" + assoc: "(x \ y) \ z = x \ (y \ z)"; + +axclass + group < semigroup + left_unit: "\ \ x = x" + left_inverse: "inverse x \ x = \"; + + +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 \ x\ = (\::'a::group)"; +proof -; + have "x \ x\ = \ \ (x \ x\)"; + by (simp only: group.left_unit); + also; have "... = (\ \ x) \ x\"; + by (simp only: semigroup.assoc); + also; have "... = (x\)\ \ x\ \ x \ x\"; + by (simp only: group.left_inverse); + also; have "... = (x\)\ \ (x\ \ x) \ x\"; + by (simp only: semigroup.assoc); + also; have "... = (x\)\ \ \ \ x\"; + by (simp only: group.left_inverse); + also; have "... = (x\)\ \ (\ \ x\)"; + by (simp only: semigroup.assoc); + also; have "... = (x\)\ \ x\"; + by (simp only: group.left_unit); + also; have "... = \"; + 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 \ \ = (x::'a::group)"; +proof -; + have "x \ \ = x \ (x\ \ x)"; + by (simp only: group.left_inverse); + also; have "... = x \ x\ \ x"; + by (simp only: semigroup.assoc); + also; have "... = \ \ 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 \ y = y \ x"; + + + +instance monoid < semigroup; +proof intro_classes; + fix x y z :: "'a::monoid"; + show "x \ y \ z = x \ (y \ z)"; + by (rule monoid.assoc); +qed; + + +instance group < monoid; +proof intro_classes; + fix x y z :: "'a::group"; + show "x \ y \ z = x \ (y \ z)"; + by (rule semigroup.assoc); + show "\ \ x = x"; + by (rule group.left_unit); + show "x \ \ = x"; + by (rule group_right_unit); +qed; + + + +defs + times_bool_def: "x \ y \\ x \\ (y\\bool)" + inverse_bool_def: "x\ \\ x\\bool" + unit_bool_def: "\ \\ False"; + +instance bool :: agroup; +proof (intro_classes, + unfold times_bool_def inverse_bool_def unit_bool_def); + fix x y z :: bool; + show "((x \\ y) \\ z) = (x \\ (y \\ z))"; by blast; + show "(False \\ x) = x"; by blast; + show "(x \\ x) = False"; by blast; + show "(x \\ y) = (y \\ x)"; by blast; +qed; + + +defs + prod_prod_def: "p \ q \\ (fst p \ fst q, snd p \ 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 \ fst q, snd p \ snd q) \ fst r, + snd (fst p \ fst q, snd p \ snd q) \ snd r) = + (fst p \ fst (fst q \ fst r, snd q \ snd r), + snd p \ snd (fst q \ fst r, snd q \ snd r))"; + by (simp add: semigroup.assoc); +qed; + +end; \ No newline at end of file diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/Product.thy --- /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 \\ 'a \\ 'a" (infixl "\\" 70); + +instance bool :: product; + by intro_classes; +defs + product_bool_def: "x \\ y \\ x \\ y"; + +end; \ No newline at end of file diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/ROOT.ML --- /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"; diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/Semigroup.thy --- /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 \\ 'a \\ 'a" (infixl "\" 70); +axclass + semigroup < "term" + assoc: "(x \ y) \ z = x \ (y \ z)"; + +end; \ No newline at end of file diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/Semigroups.thy --- /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 \\ 'a \\ 'a) \\ bool" + "is_assoc f == \\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 \"; +*}; + +consts + plus :: "'a \\ 'a \\ 'a" (infixl "\" 65); +axclass + plus_semigroup < "term" + assoc: "is_assoc (op \)"; + +text {* + \medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}: + %term (latex xsymbols symbols) "op \"; +*}; + +consts + times :: "'a \\ 'a \\ 'a" (infixl "\" 65); +axclass + times_semigroup < "term" + assoc: "is_assoc (op \)"; + +end; \ No newline at end of file diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Group/document/root.tex --- /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} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/IsaMakefile --- /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 diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Makefile --- 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) diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Nat/NatClass.ML --- /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 ""; + diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Nat/NatClass.thy --- /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 \\ 'a" + rec :: "'a \\ 'a \\ ('a \\ 'a \\ 'a) \\ 'a"; + +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))"; + +constdefs + add :: "'a::nat \\ 'a \\ 'a" (infixl "+" 60) + "m + n \\ rec(m, n, \\x y. Suc(y))"; + +end; \ No newline at end of file diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Nat/ROOT.ML --- /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"; diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/Nat/document/root.tex --- /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} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/axclass.tex --- 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 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 diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/bbb.sty --- 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}}} - diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/body.tex --- /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 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 diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Group.aux --- /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} +} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Group.tex --- /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}% diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/NatClass.aux --- /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} +} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/NatClass.tex --- /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}% diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Product.aux --- /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} +} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Product.tex --- /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}% diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Semigroup.aux --- /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} +} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Semigroup.tex --- /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}% diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Semigroups.aux --- /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} +} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/Semigroups.tex --- /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 \";% +\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 \";% +\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}% diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/isabelle.sty --- /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}} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/isabellesym.sty --- /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$}} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/pdfsetup.sty --- /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}}{}} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/generated/session.tex --- /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} diff -r 2ec6371fde54 -r 9a44d8d98731 doc-src/AxClass/style.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: