summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 21 May 2000 21:48:39 +0200 | |

changeset 8903 | 78d6e47469e4 |

parent 8902 | a705822f4e2a |

child 8904 | 0bb77c5b86cc |

new Isar version;

--- a/doc-src/AxClass/Group/Group.thy Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/Group/Group.thy Sun May 21 21:48:39 2000 +0200 @@ -1,12 +1,36 @@ + +header {* Basic group theory *}; theory Group = Main:; +text {* + \medskip\noindent 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 *}; + +text {* + First we declare some polymorphic constants required later for the + signature parts of our structures. +*}; consts times :: "'a => 'a => 'a" (infixl "\<Otimes>" 70) inverse :: "'a => 'a" ("(_\<inv>)" [1000] 999) one :: 'a ("\<unit>"); +text {* + \noindent Next we define class $monoid$ of monoids with operations + $\TIMES$ and $1$. Note that multiple class axioms are allowed for + user convenience --- they simply represent the conjunction of their + respective universal closures. +*}; axclass monoid < "term" @@ -14,6 +38,19 @@ left_unit: "\<unit> \<Otimes> x = x" right_unit: "x \<Otimes> \<unit> = x"; +text {* + \noindent 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 element for $\TIMES$. +*}; + +text {* + \medskip 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$. +*}; axclass semigroup < "term" @@ -24,13 +61,40 @@ left_unit: "\<unit> \<Otimes> x = x" left_inverse: "inverse x \<Otimes> x = \<unit>"; +axclass + agroup < group + commute: "x \<Otimes> y = y \<Otimes> x"; + +text {* + \noindent 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 *}; text {* - The group axioms only state the properties of left unit and inverse, - the right versions may be derived as follows. + In a sense, axiomatic type classes may be viewed as \emph{abstract + theories}. Above class definitions gives rise to abstract axioms + $assoc$, $left_unit$, $left_inverse$, $commute$, where all of these + contain type a variable $\alpha :: c$ that is restricted to types of + the corresponding class $c$. \emph{Sort constraints} like this + 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 technical point of view, abstract axioms are just + ordinary Isabelle theorems, which may be used in proofs without + special treatment. Such ``abstract proofs'' usually yield new + ``abstract theorems''. For example, we may now derive the following + laws of general groups. *}; -theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>::'a::group)"; +theorem group_right_inverse: "x \<Otimes> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"; proof -; have "x \<Otimes> x\<inv> = \<unit> \<Otimes> (x \<Otimes> x\<inv>)"; by (simp only: group.left_unit); @@ -52,12 +116,12 @@ qed; text {* - With $group_right_inverse$ already available, + \noindent With $group_right_inverse$ already available, $group_right_unit$\label{thm:group-right-unit} is now established much easier. *}; -theorem group_right_unit: "x \<Otimes> \<unit> = (x::'a::group)"; +theorem group_right_unit: "x \<Otimes> \<unit> = (x\<Colon>'a\<Colon>group)"; proof -; have "x \<Otimes> \<unit> = x \<Otimes> (x\<inv> \<Otimes> x)"; by (simp only: group.left_inverse); @@ -70,24 +134,70 @@ finally; show ?thesis; .; qed; - -axclass - agroup < group - commute: "x \<Otimes> y = y \<Otimes> x"; +text {* + \medskip 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 *}; + +text {* + 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 \subseteq monoid$ properly as follows + (cf.\ \figref{fig:monoid-group}). + + \begin{figure}[htbp] + \begin{center} + \small + \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} + + 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. +*}; instance monoid < semigroup; proof intro_classes; - fix x y z :: "'a::monoid"; + fix x y z :: "'a\<Colon>monoid"; show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)"; by (rule monoid.assoc); qed; - instance group < monoid; proof intro_classes; - fix x y z :: "'a::group"; + fix x y z :: "'a\<Colon>group"; show "x \<Otimes> y \<Otimes> z = x \<Otimes> (y \<Otimes> z)"; by (rule semigroup.assoc); show "\<unit> \<Otimes> x = x"; @@ -96,13 +206,55 @@ by (rule group_right_unit); qed; +text {* + \medskip The $\isakeyword{instance}$ command sets up an appropriate + goal that represents the class inclusion (or type arity) to be proven + (see also \cite{isabelle-isar-ref}). The $intro_classes$ proof + method does back-chaining of class membership statements wrt.\ the + hierarchy of any classes defined in the current theory; the effect is + to reduce to any logical class axioms as subgoals. +*}; +subsection {* Concrete instantiation *}; + +text {* + So far we have covered the case of the form + $\isakeyword{instance}~c@1 < c@2$, namely \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 established at the logical level and then + transferred to Isabelle's type signature level. + + \medskip + + As an typical example, we show that type $bool$ with exclusive-or as + operation $\TIMES$, identity as $\isasyminv$, and $False$ as $1$ + forms an Abelian group. +*}; + defs times_bool_def: "x \<Otimes> y \\<equiv> x \\<noteq> (y\\<Colon>bool)" inverse_bool_def: "x\<inv> \\<equiv> x\\<Colon>bool" unit_bool_def: "\<unit> \\<equiv> False"; +text {* + \medskip It is important to note that above $\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 recursion over the + syntactic structure of simple types) are admissible of proper + definitional extensions in any version of HOL + \cite{Wenzel:1997:TPHOL}. Nevertheless, overloaded definitions are + best applied in the context of type classes. + + \medskip Since we have chosen above $\DEFS$ of the generic group + operations on type $bool$ appropriately, the class membership $bool + :: agroup$ may be now derived as follows. +*}; + instance bool :: agroup; proof (intro_classes, unfold times_bool_def inverse_bool_def unit_bool_def); @@ -113,13 +265,50 @@ show "(x \\<noteq> y) = (y \\<noteq> x)"; by blast; qed; +text {* + The result of $\isakeyword{instance}$ is both expressed as a theorem + of Isabelle's meta-logic, and a type arity statement of the type + signature. The latter enables the type-inference system to take care + of this new instance automatically. + + \medskip In a similarly fashion, we could also instantiate our group + theory classes to many other concrete types. For example, $int :: + agroup$ (e.g.\ by defining $\TIMES$ as addition, $\isasyminv$ as + negation and $1$ as zero) or $list :: (term)semigroup$ (e.g.\ if + $\TIMES$ is defined as list append). Thus, the characteristic + constants $\TIMES$, $\isasyminv$, $1$ really become overloaded, i.e.\ + have different meanings on different types. +*}; + + +subsection {* Lifting and Functors *}; + +text {* + As already mentioned above, overloading in the simply-typed HOL + systems may include recursion over the syntactic structure of types. + That is, definitional equations $c^\tau \equiv t$ may also contain + constants of name $c$ on the right-hand side --- if these have types + that are structurally simpler than $\tau$. + + This feature enables us to \emph{lift operations}, say to Cartesian + products, direct sums or function spaces. Subsequently we lift + $\TIMES$ component-wise to binary Cartesian products $\alpha \times + \beta$. +*}; defs prod_prod_def: "p \<Otimes> q \\<equiv> (fst p \<Otimes> fst q, snd p \<Otimes> snd q)"; +text {* + It is very easy to see that associativity of $\TIMES^\alpha$, + $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence + the binary type constructor $\times$ maps semigroups to semigroups. + This may be established formally as follows. +*}; + instance * :: (semigroup, semigroup) semigroup; proof (intro_classes, unfold prod_prod_def); - fix p q r :: "'a::semigroup * 'b::semigroup"; + fix p q r :: "'a\<Colon>semigroup * 'b\<Colon>semigroup"; show "(fst (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> fst r, snd (fst p \<Otimes> fst q, snd p \<Otimes> snd q) \<Otimes> snd r) = @@ -128,4 +317,11 @@ by (simp add: semigroup.assoc); qed; +text {* + Thus, if we view class instances as ``structures'', then overloaded + constant definitions with primitive recursion over types indirectly + provide some kind of ``functors'' --- i.e.\ mappings between abstract + theories. +*}; + end; \ No newline at end of file

--- a/doc-src/AxClass/Group/Product.thy Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/Group/Product.thy Sun May 21 21:48:39 2000 +0200 @@ -1,22 +1,83 @@ -(* 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! -*) +header {* Syntactic classes *}; theory Product = Main:; +text {* + \medskip\noindent 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 $\TIMES + :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for + $\TIMES :: (\alpha::term) \To \alpha \To \alpha$. Since class $term$ + is the universal class of HOL, this is not really a restriction at + all. + + The $product$ class below provides a less degenerate example of + syntactic type classes. +*}; + axclass product < "term"; consts product :: "'a::product \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\\<otimes>" 70); +text {* + Here class $product$ is defined as subclass of $term$ without any + additional axioms. This effects in logical equivalence of $product$ + and $term$, as is reflected by the trivial introduction rule + generated for this definition. + + \medskip So what is the difference of declaring $\TIMES :: (\alpha :: + product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha :: + term) \To \alpha \To \alpha$ anyway? In this particular case where + $product \equiv term$, it should be obvious that both declarations + are the same from the logic's point of view. It even makes the most + sense to remove sort constraints from constant declarations, as far + as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}. + + On the other hand there are syntactic differences, of course. + Constants $\TIMES^\tau$ are rejected by the type-checker, unless the + arity $\tau :: product$ is part of the type signature. In our + example, this arity may be always added when required by means of an + $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$. + + \medskip Thus, we may observe the following discipline of using + syntactic classes. 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 $product$ and type $bool$ as follows. +*}; + instance bool :: product; by intro_classes; defs product_bool_def: "x \\<otimes> y \\<equiv> x \\<and> y"; +text {* + The definition $prod_bool_def$ becomes syntactically well-formed only + after the arity $bool :: product$ is made known to the type checker. + + \medskip It is very important to see that above $\DEFS$ are not + directly connected with $\isarkeyword{instance}$ at all! We were + just following our convention to specify $\TIMES$ on $bool$ after + having instantiated $bool :: product$. Isabelle does not require + these definitions, which is in contrast to programming languages like + Haskell \cite{haskell-report}. + + \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''. +*}; + end; \ No newline at end of file

--- a/doc-src/AxClass/Group/Semigroups.thy Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/Group/Semigroups.thy Sun May 21 21:48:39 2000 +0200 @@ -1,16 +1,8 @@ theory Semigroups = Main:; -text {* - \noindent Associativity of binary operations: -*}; constdefs is_assoc :: "('a \\<Rightarrow> 'a \\<Rightarrow> 'a) \\<Rightarrow> bool" - "is_assoc f == \\<forall>x y z. f (f x y) z = f x (f y z)"; - -text {* - \medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}: - %term (latex xsymbols symbols) "op \<Oplus>"; -*}; + "is_assoc f \\<equiv> \\<forall>x y z. f (f x y) z = f x (f y z)"; consts plus :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Oplus>" 65); @@ -18,11 +10,6 @@ plus_semigroup < "term" assoc: "is_assoc (op \<Oplus>)"; -text {* - \medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}: - %term (latex xsymbols symbols) "op \<Otimes>"; -*}; - consts times :: "'a \\<Rightarrow> 'a \\<Rightarrow> 'a" (infixl "\<Otimes>" 65); axclass

--- a/doc-src/AxClass/Makefile Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/Makefile Sun May 21 21:48:39 2000 +0200 @@ -13,7 +13,10 @@ NAME = axclass -FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../pdfsetup.sty +FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \ + ../pdfsetup.sty generated/Group.tex generated/NatClass.tex \ + generated/Product.tex generated/Semigroup.tex generated/Semigroups.tex \ + generated/session.tex dvi: $(NAME).dvi

--- a/doc-src/AxClass/Nat/NatClass.thy Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/Nat/NatClass.thy Sun May 21 21:48:39 2000 +0200 @@ -1,15 +1,3 @@ -(* 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

--- a/doc-src/AxClass/axclass.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/axclass.tex Sun May 21 21:48:39 2000 +0200 @@ -1,6 +1,6 @@ \documentclass[12pt,a4paper,fleqn]{report} -\usepackage{graphicx,../iman,../extra,../pdfsetup} +\usepackage{graphicx,../iman,../extra,../isar,../pdfsetup} \usepackage{generated/isabelle,generated/isabellesym} \newcommand{\isasymOtimes}{\emph{$\odot$}}

--- a/doc-src/AxClass/body.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/body.tex Sun May 21 21:48:39 2000 +0200 @@ -55,7 +55,7 @@ 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. +We illustrate these basic concepts by the following theory of semigroups. \bigskip \input{generated/Semigroup} @@ -86,496 +86,44 @@ 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$. +\input{generated/Product} -\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} +\section{Defining natural numbers in FOL}\label{sec:ex-natclass} - -\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). +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. -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} +We illustrate this with the natural numbers in Isabelle/FOL. -So far we have covered the case of \texttt{instance $c@1$ < $c@2$} that -could be described as \emph{abstract instantiation} --- $c@1$ is more -special than $c@2$ and thus an instance of $c@2$. Even more -interesting for practical applications are \emph{concrete instantiations} -of axiomatic type classes. That is, certain simple schemes $(\alpha@1, -\ldots, \alpha@n)t :: c$ of class membership may be transferred to -Isabelle's type signature level. This form of \texttt{instance} is a ``safe'' -variant of the old-style \texttt{arities} theory section. - -As an example, we show that type \texttt{bool} with exclusive-or as -operation $\TIMES$, identity as \texttt{inverse}, and \texttt{False} as \texttt{1} -forms an abelian group. We first define theory \texttt{Xor}: - -\begin{ascbox} -Xor = Group +\medskip -defs - prod@bool@def "x <*> y == x ~= (y::bool)" - inverse@bool@def "inverse x == x::bool" - unit@bool@def "1 == False"\medskip -end -\emphnd{ascbox} - -It is important to note that above \texttt{defs} are just overloaded -meta-level constant definitions. In particular, type classes are not -yet involved at all! This form of constant definition with overloading -(and optional primitive recursion over types) would be also possible -in traditional versions of \HOL\ that lack type classes. -% (see FIXME <foundation> for more details) -Nonetheless, such definitions are best applied in the context of -classes. - -\medskip - -Since we chose the \texttt{defs} of theory \texttt{Xor} suitably, the class -membership $\texttt{bool} :: \texttt{agroup}$ is now derivable as follows: +\bigskip +\input{generated/NatClass} +\bigskip -\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: +This is an abstract version of the plain $Nat$ theory in +FOL.\footnote{See \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} -\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. +Basically, we have just replaced all occurrences of type $nat$ by $\alpha$ and +used the natural number axioms to define class $nat$. There is only a minor +snag, that the original recursion operator $rec$ had to be made monomorphic, +in a sense. Thus class $nat$ contains exactly those types $\tau$ that are +isomorphic to ``the'' natural numbers (with signature $0$, $Suc$, $rec$). \medskip -What we have done here 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: +What we have done here can be also viewed as \emph{type specification}. Of +course, it still remains open if there is some type at all that meets the +class axioms. Now a very nice property of axiomatic type classes is, that +abstract reasoning is always possible --- independent of satisfiability. The +meta-logic won't break, even if some classes (or general sorts) turns out to +be empty (``inconsistent'') later. -\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}. +Theorems of the abstract natural numbers may be derived in the same way as for +the concrete version. The original proof scripts may be used with some +trivial changes only (mostly adding some type constraints). %% FIXME move some parts to ref or isar-ref manual (!?);

--- a/doc-src/AxClass/generated/Group.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/generated/Group.tex Sun May 21 21:48:39 2000 +0200 @@ -1,21 +1,51 @@ \begin{isabelle}% -\isanewline -\isacommand{theory}~Group~=~Main:\isanewline -\isanewline -\isanewline +% +\isamarkupheader{Basic group theory} +\isacommand{theory}~Group~=~Main:% +\begin{isamarkuptext}% +\medskip\noindent 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.% +\end{isamarkuptext}% +% +\isamarkupsubsection{Monoids and Groups} +% +\begin{isamarkuptext}% +First we declare some polymorphic constants required later for the + signature parts of our structures.% +\end{isamarkuptext}% \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 +~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})% +\begin{isamarkuptext}% +\noindent Next we define class $monoid$ of monoids with operations + $\TIMES$ and $1$. Note that multiple class axioms are allowed for + user convenience --- they simply represent the conjunction of their + respective universal closures.% +\end{isamarkuptext}% \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 +~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}% +\begin{isamarkuptext}% +\noindent 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 element for $\TIMES$.% +\end{isamarkuptext}% +% +\begin{isamarkuptext}% +\medskip 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$.% +\end{isamarkuptext}% \isacommand{axclass}\isanewline ~~semigroup~<~{"}term{"}\isanewline ~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline @@ -23,12 +53,39 @@ \isacommand{axclass}\isanewline ~~group~<~semigroup\isanewline ~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline -~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}% +~~left\_inverse:~{"}inverse~x~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline +\isanewline +\isacommand{axclass}\isanewline +~~agroup~<~group\isanewline +~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}% +\begin{isamarkuptext}% +\noindent 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.% +\end{isamarkuptext}% +% +\isamarkupsubsection{Abstract reasoning} +% \begin{isamarkuptext}% -The group axioms only state the properties of left unit and inverse, - the right versions may be derived as follows.% +In a sense, axiomatic type classes may be viewed as \emph{abstract + theories}. Above class definitions gives rise to abstract axioms + $assoc$, $left_unit$, $left_inverse$, $commute$, where all of these + contain type a variable $\alpha :: c$ that is restricted to types of + the corresponding class $c$. \emph{Sort constraints} like this + 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 technical point of view, abstract axioms are just + ordinary Isabelle theorems, which may be used in proofs without + special treatment. Such ``abstract proofs'' usually yield new + ``abstract theorems''. For example, we may now derive the following + laws of general groups.% \end{isamarkuptext}% -\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}::'a::group){"}\isanewline +\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}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 @@ -49,11 +106,11 @@ ~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline \isacommand{qed}% \begin{isamarkuptext}% -With $group_right_inverse$ already available, +\noindent 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{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}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 @@ -64,41 +121,121 @@ ~~\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{qed}% +\begin{isamarkuptext}% +\medskip 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$.% +\end{isamarkuptext}% +% +\isamarkupsubsection{Abstract instantiation} +% +\begin{isamarkuptext}% +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 \subseteq monoid$ properly as follows + (cf.\ \figref{fig:monoid-group}). + + \begin{figure}[htbp] + \begin{center} + \small + \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} + + 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.% +\end{isamarkuptext}% \isacommand{instance}~monoid~<~semigroup\isanewline \isacommand{proof}~intro\_classes\isanewline -~~\isacommand{fix}~x~y~z~::~{"}'a::monoid{"}\isanewline +~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}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{fix}~x~y~z~::~{"}'a{\isasymColon}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{qed}% +\begin{isamarkuptext}% +\medskip The $\isakeyword{instance}$ command sets up an appropriate + goal that represents the class inclusion (or type arity) to be proven + (see also \cite{isabelle-isar-ref}). The $intro_classes$ proof + method does back-chaining of class membership statements wrt.\ the + hierarchy of any classes defined in the current theory; the effect is + to reduce to any logical class axioms as subgoals.% +\end{isamarkuptext}% +% +\isamarkupsubsection{Concrete instantiation} +% +\begin{isamarkuptext}% +So far we have covered the case of the form + $\isakeyword{instance}~c@1 < c@2$, namely \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 established at the logical level and then + transferred to Isabelle's type signature level. + + \medskip + + As an typical example, we show that type $bool$ with exclusive-or as + operation $\TIMES$, identity as $\isasyminv$, and $False$ as $1$ + forms an Abelian group.% +\end{isamarkuptext}% \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 +~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}% +\begin{isamarkuptext}% +\medskip It is important to note that above $\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 recursion over the + syntactic structure of simple types) are admissible of proper + definitional extensions in any version of HOL + \cite{Wenzel:1997:TPHOL}. Nevertheless, overloaded definitions are + best applied in the context of type classes. + + \medskip Since we have chosen above $\DEFS$ of the generic group + operations on type $bool$ appropriately, the class membership $bool + :: agroup$ may be now derived as follows.% +\end{isamarkuptext}% \isacommand{instance}~bool~::~agroup\isanewline \isacommand{proof}~(intro\_classes,\isanewline ~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline @@ -107,21 +244,58 @@ ~~\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{qed}% +\begin{isamarkuptext}% +The result of $\isakeyword{instance}$ is both expressed as a theorem + of Isabelle's meta-logic, and a type arity statement of the type + signature. The latter enables the type-inference system to take care + of this new instance automatically. + + \medskip In a similarly fashion, we could also instantiate our group + theory classes to many other concrete types. For example, $int :: + agroup$ (e.g.\ by defining $\TIMES$ as addition, $\isasyminv$ as + negation and $1$ as zero) or $list :: (term)semigroup$ (e.g.\ if + $\TIMES$ is defined as list append). Thus, the characteristic + constants $\TIMES$, $\isasyminv$, $1$ really become overloaded, i.e.\ + have different meanings on different types.% +\end{isamarkuptext}% +% +\isamarkupsubsection{Lifting and Functors} +% +\begin{isamarkuptext}% +As already mentioned above, overloading in the simply-typed HOL + systems may include recursion over the syntactic structure of types. + That is, definitional equations $c^\tau \equiv t$ may also contain + constants of name $c$ on the right-hand side --- if these have types + that are structurally simpler than $\tau$. + + This feature enables us to \emph{lift operations}, say to Cartesian + products, direct sums or function spaces. Subsequently we lift + $\TIMES$ component-wise to binary Cartesian products $\alpha \times + \beta$.% +\end{isamarkuptext}% \isacommand{defs}\isanewline -~~prod\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}\isanewline -\isanewline +~~prod\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}% +\begin{isamarkuptext}% +It is very easy to see that associativity of $\TIMES^\alpha$, + $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence + the binary type constructor $\times$ maps semigroups to semigroups. + This may be established formally as follows.% +\end{isamarkuptext}% \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{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~*~'b{\isasymColon}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{qed}% +\begin{isamarkuptext}% +Thus, if we view class instances as ``structures'', then overloaded + constant definitions with primitive recursion over types indirectly + provide some kind of ``functors'' --- i.e.\ mappings between abstract + theories.% +\end{isamarkuptext}% \isacommand{end}\end{isabelle}%

--- a/doc-src/AxClass/generated/NatClass.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/generated/NatClass.tex Sun May 21 21:48:39 2000 +0200 @@ -1,6 +1,4 @@ \begin{isabelle}% -\isanewline -\isanewline \isacommand{theory}~NatClass~=~FOL:\isanewline \isanewline \isacommand{consts}\isanewline

--- a/doc-src/AxClass/generated/Product.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/generated/Product.tex Sun May 21 21:48:39 2000 +0200 @@ -1,16 +1,77 @@ \begin{isabelle}% -\isanewline -\isanewline -\isacommand{theory}~Product~=~Main:\isanewline -\isanewline +% +\isamarkupheader{Syntactic classes} +\isacommand{theory}~Product~=~Main:% +\begin{isamarkuptext}% +\medskip\noindent 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 $\TIMES + :: \alpha \To \alpha \To \alpha$ is actually an abbreviation for + $\TIMES :: (\alpha::term) \To \alpha \To \alpha$. Since class $term$ + is the universal class of HOL, this is not really a restriction at + all. + + The $product$ class below provides a less degenerate example of + syntactic type classes.% +\end{isamarkuptext}% \isacommand{axclass}\isanewline ~~product~<~{"}term{"}\isanewline \isacommand{consts}\isanewline -~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)\isanewline -\isanewline +~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymotimes}{"}~70)% +\begin{isamarkuptext}% +Here class $product$ is defined as subclass of $term$ without any + additional axioms. This effects in logical equivalence of $product$ + and $term$, as is reflected by the trivial introduction rule + generated for this definition. + + \medskip So what is the difference of declaring $\TIMES :: (\alpha :: + product) \To \alpha \To \alpha$ vs.\ declaring $\TIMES :: (\alpha :: + term) \To \alpha \To \alpha$ anyway? In this particular case where + $product \equiv term$, it should be obvious that both declarations + are the same from the logic's point of view. It even makes the most + sense to remove sort constraints from constant declarations, as far + as the purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}. + + On the other hand there are syntactic differences, of course. + Constants $\TIMES^\tau$ are rejected by the type-checker, unless the + arity $\tau :: product$ is part of the type signature. In our + example, this arity may be always added when required by means of an + $\isarkeyword{instance}$ with the trivial proof $\BY{intro_classes}$. + + \medskip Thus, we may observe the following discipline of using + syntactic classes. 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 $product$ and type $bool$ as follows.% +\end{isamarkuptext}% \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 +~~product\_bool\_def:~{"}x~{\isasymotimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}% +\begin{isamarkuptext}% +The definition $prod_bool_def$ becomes syntactically well-formed only + after the arity $bool :: product$ is made known to the type checker. + + \medskip It is very important to see that above $\DEFS$ are not + directly connected with $\isarkeyword{instance}$ at all! We were + just following our convention to specify $\TIMES$ on $bool$ after + having instantiated $bool :: product$. Isabelle does not require + these definitions, which is in contrast to programming languages like + Haskell \cite{haskell-report}. + + \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''.% +\end{isamarkuptext}% \isacommand{end}\end{isabelle}%

--- a/doc-src/AxClass/generated/Semigroups.tex Sun May 21 14:49:28 2000 +0200 +++ b/doc-src/AxClass/generated/Semigroups.tex Sun May 21 21:48:39 2000 +0200 @@ -1,24 +1,16 @@ \begin{isabelle}% -\isacommand{theory}~Semigroups~=~Main:% -\begin{isamarkuptext}% -\noindent Associativity of binary operations:% -\end{isamarkuptext}% +\isacommand{theory}~Semigroups~=~Main:\isanewline +\isanewline \isacommand{constdefs}\isanewline ~~is\_assoc~::~{"}('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~bool{"}\isanewline -~~{"}is\_assoc~f~==~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}% -\begin{isamarkuptext}% -\medskip\noindent Semigroups over \isa{(op~{\isasymOplus})}: - %term (latex xsymbols symbols) "op \<Oplus>";% -\end{isamarkuptext}% +~~{"}is\_assoc~f~{\isasymequiv}~{\isasymforall}x~y~z.~f~(f~x~y)~z~=~f~x~(f~y~z){"}\isanewline +\isanewline \isacommand{consts}\isanewline ~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~65)\isanewline \isacommand{axclass}\isanewline ~~plus\_semigroup~<~{"}term{"}\isanewline -~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}% -\begin{isamarkuptext}% -\medskip\noindent Semigroups over \isa{(op~{\isasymOtimes})}: - %term (latex xsymbols symbols) "op \<Otimes>";% -\end{isamarkuptext}% +~~assoc:~{"}is\_assoc~(op~{\isasymOplus}){"}\isanewline +\isanewline \isacommand{consts}\isanewline ~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~65)\isanewline \isacommand{axclass}\isanewline