--- a/doc-src/AxClass/Group/Group.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Group.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,20 +4,20 @@
theory Group = Main:
text {*
- \medskip\noindent The meta-level 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.
+ \medskip\noindent The meta-level 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.
+ First we declare some polymorphic constants required later for the
+ signature parts of our structures.
*}
consts
@@ -26,33 +26,33 @@
one :: 'a ("\<unit>")
text {*
- \noindent Next we define class @{text monoid} of monoids with
- operations @{text \<odot>} and @{text \<unit>}. Note that multiple class
- axioms are allowed for user convenience --- they simply represent the
- conjunction of their respective universal closures.
+ \noindent Next we define class @{text monoid} of monoids with
+ operations @{text \<odot>} and @{text \<unit>}. Note that multiple class
+ axioms are allowed for user convenience --- they simply represent
+ the conjunction of their respective universal closures.
*}
-axclass monoid \<subseteq> "term"
+axclass monoid \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
left_unit: "\<unit> \<odot> x = x"
right_unit: "x \<odot> \<unit> = x"
text {*
- \noindent So class @{text monoid} contains exactly those types @{text
- \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"} are
- specified appropriately, such that @{text \<odot>} is associative and
- @{text \<unit>} is a left and right unit element for the @{text \<odot>}
- operation.
+ \noindent So class @{text monoid} contains exactly those types
+ @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"}
+ are specified appropriately, such that @{text \<odot>} is associative and
+ @{text \<unit>} is a left and right unit element for the @{text \<odot>}
+ operation.
*}
text {*
- \medskip Independently of @{text 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 each
- class name, so we may re-use common names such as @{text assoc}.
+ \medskip Independently of @{text 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 each
+ class name, so we may re-use common names such as @{text assoc}.
*}
-axclass semigroup \<subseteq> "term"
+axclass semigroup \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
axclass group \<subseteq> semigroup
@@ -63,32 +63,32 @@
commute: "x \<odot> y = y \<odot> x"
text {*
- \noindent Class @{text group} inherits associativity of @{text \<odot>}
- from @{text semigroup} and adds two further group axioms. Similarly,
- @{text agroup} is defined as the subset of @{text group} such that
- for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
- \<tau>"} is even commutative.
+ \noindent Class @{text group} inherits associativity of @{text \<odot>}
+ from @{text semigroup} and adds two further group axioms. Similarly,
+ @{text agroup} is defined as the subset of @{text group} such that
+ for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
+ \<tau>"} is even commutative.
*}
subsection {* Abstract reasoning *}
text {*
- In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}. Above class definitions gives rise to abstract axioms
- @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
- commute}, where any of these contain a type variable @{text "'a \<Colon> c"}
- that is restricted to types of the corresponding class @{text c}.
- \emph{Sort constraints} like this express a logical precondition for
- the whole formula. For example, @{text assoc} states that for all
- @{text \<tau>}, provided that @{text "\<tau> \<Colon> semigroup"}, the operation
- @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
+ In a sense, axiomatic type classes may be viewed as \emph{abstract
+ theories}. Above class definitions gives rise to abstract axioms
+ @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
+ commute}, where any of these contain a type variable @{text "'a \<Colon>
+ c"} that is restricted to types of the corresponding class @{text
+ c}. \emph{Sort constraints} like this express a logical
+ precondition for the whole formula. For example, @{text assoc}
+ states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
+ semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<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
- well-known laws of general groups.
+ \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
+ well-known laws of general groups.
*}
theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
@@ -113,9 +113,9 @@
qed
text {*
- \noindent With @{text group_right_inverse} already available, @{text
- group_right_unit}\label{thm:group-right-unit} is now established much
- easier.
+ \noindent With @{text group_right_inverse} already available, @{text
+ group_right_unit}\label{thm:group-right-unit} is now established
+ much easier.
*}
theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
@@ -132,26 +132,26 @@
qed
text {*
- \medskip Abstract theorems may be instantiated to only those types
- @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
- known at Isabelle's type signature level. Since we have @{text
- "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
- semigroup} and @{text group} are automatically inherited by @{text
- group} and @{text agroup}.
+ \medskip Abstract theorems may be instantiated to only those types
+ @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
+ known at Isabelle's type signature level. Since we have @{text
+ "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
+ semigroup} and @{text group} are automatically inherited by @{text
+ group} and @{text agroup}.
*}
subsection {* Abstract instantiation *}
text {*
- From the definition, the @{text monoid} and @{text group} classes
- have been independent. Note that for monoids, @{text right_unit} had
- to be included as an axiom, but for groups both @{text right_unit}
- and @{text right_inverse} are derivable from the other axioms. With
- @{text group_right_unit} derived as a theorem of group theory (see
- page~\pageref{thm:group-right-unit}), we may now instantiate @{text
- "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> monoid"} properly as
- follows (cf.\ \figref{fig:monoid-group}).
+ From the definition, the @{text monoid} and @{text group} classes
+ have been independent. Note that for monoids, @{text right_unit}
+ had to be included as an axiom, but for groups both @{text
+ right_unit} and @{text right_inverse} are derivable from the other
+ axioms. With @{text group_right_unit} derived as a theorem of group
+ theory (see page~\pageref{thm:group-right-unit}), we may now
+ instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
+ monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
\begin{figure}[htbp]
\begin{center}
@@ -163,7 +163,7 @@
\put(15,5){\makebox(0,0){@{text agroup}}}
\put(15,25){\makebox(0,0){@{text group}}}
\put(15,45){\makebox(0,0){@{text semigroup}}}
- \put(30,65){\makebox(0,0){@{text "term"}}} \put(50,45){\makebox(0,0){@{text monoid}}}
+ \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
\end{picture}
\hspace{4em}
\begin{picture}(30,90)(0,0)
@@ -173,7 +173,7 @@
\put(15,25){\makebox(0,0){@{text group}}}
\put(15,45){\makebox(0,0){@{text monoid}}}
\put(15,65){\makebox(0,0){@{text semigroup}}}
- \put(15,85){\makebox(0,0){@{text term}}}
+ \put(15,85){\makebox(0,0){@{text type}}}
\end{picture}
\caption{Monoids and groups: according to definition, and by proof}
\label{fig:monoid-group}
@@ -200,34 +200,34 @@
qed
text {*
- \medskip The $\INSTANCE$ command sets up an appropriate goal that
- represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}). The initial proof step causes
- back-chaining of class membership statements wrt.\ the hierarchy of
- any classes defined in the current theory; the effect is to reduce to
- the initial statement to a number of goals that directly correspond
- to any class axioms encountered on the path upwards through the class
- hierarchy.
+ \medskip The $\INSTANCE$ command sets up an appropriate goal that
+ represents the class inclusion (or type arity, see
+ \secref{sec:inst-arity}) to be proven (see also
+ \cite{isabelle-isar-ref}). The initial proof step causes
+ back-chaining of class membership statements wrt.\ the hierarchy of
+ any classes defined in the current theory; the effect is to reduce
+ to the initial statement to a number of goals that directly
+ correspond to any class axioms encountered on the path upwards
+ through the class hierarchy.
*}
subsection {* Concrete instantiation \label{sec:inst-arity} *}
text {*
- So far we have covered the case of the form $\INSTANCE$~@{text
- "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
- $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
- of @{text "c\<^sub>2"}. Even more interesting for practical
- applications are \emph{concrete instantiations} of axiomatic type
- classes. That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
- \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
- logical level and then transferred to Isabelle's type signature
- level.
+ So far we have covered the case of the form $\INSTANCE$~@{text
+ "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
+ $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
+ of @{text "c\<^sub>2"}. Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes. That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
+ \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
+ logical level and then transferred to Isabelle's type signature
+ level.
- \medskip As a typical example, we show that type @{typ bool} with
- exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
- @{term False} as @{text \<unit>} forms an Abelian group.
+ \medskip As a typical example, we show that type @{typ bool} with
+ exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
+ @{term False} as @{text \<unit>} forms an Abelian group.
*}
defs (overloaded)
@@ -236,18 +236,18 @@
unit_bool_def: "\<unit> \<equiv> False"
text {*
- \medskip It is important to note that above $\DEFS$ are just
- overloaded meta-level constant definitions, where 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 as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
- required for overloading. Nevertheless, overloaded definitions are
- best applied in the context of type classes.
+ \medskip It is important to note that above $\DEFS$ are just
+ overloaded meta-level constant definitions, where 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 as definitional extensions of plain HOL
+ \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
+ required for overloading. 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 @{typ bool} appropriately, the class membership
- @{text "bool \<Colon> agroup"} may be now derived as follows.
+ \medskip Since we have chosen above $\DEFS$ of the generic group
+ operations on type @{typ bool} appropriately, the class membership
+ @{text "bool \<Colon> agroup"} may be now derived as follows.
*}
instance bool :: agroup
@@ -261,44 +261,44 @@
qed
text {*
- The result of an $\INSTANCE$ statement is both expressed as a theorem
- of Isabelle's meta-logic, and as a type arity of the type signature.
- The latter enables type-inference system to take care of this new
- instance automatically.
+ The result of an $\INSTANCE$ statement is both expressed as a
+ theorem of Isabelle's meta-logic, and as a type arity of the type
+ signature. The latter enables type-inference system to take care of
+ this new instance automatically.
- \medskip We could now also instantiate our group theory classes to
- many other concrete types. For example, @{text "int \<Colon> agroup"}
- (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
- and @{text \<unit>} as zero) or @{text "list \<Colon> (term) semigroup"}
- (e.g.\ if @{text \<odot>} is defined as list append). Thus, the
- characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
- really become overloaded, i.e.\ have different meanings on different
- types.
+ \medskip We could now also instantiate our group theory classes to
+ many other concrete types. For example, @{text "int \<Colon> agroup"}
+ (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
+ and @{text \<unit>} as zero) or @{text "list \<Colon> (type) semigroup"}
+ (e.g.\ if @{text \<odot>} is defined as list append). Thus, the
+ characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
+ 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 @{text "c\<^sup>\<tau> \<equiv> t"} may also
- contain constants of name @{text c} on the right-hand side --- if
- these have types that are structurally simpler than @{text \<tau>}.
+ As already mentioned above, overloading in the simply-typed HOL
+ systems may include recursion over the syntactic structure of types.
+ That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
+ contain constants of name @{text c} on the right-hand side --- if
+ these have types that are structurally simpler than @{text \<tau>}.
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces. Subsequently we lift
- @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
+ This feature enables us to \emph{lift operations}, say to Cartesian
+ products, direct sums or function spaces. Subsequently we lift
+ @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
*}
defs (overloaded)
times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
text {*
- It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
- and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
- 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups to
- semigroups. This may be established formally as follows.
+ It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
+ and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
+ 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups
+ to semigroups. This may be established formally as follows.
*}
instance * :: (semigroup, semigroup) semigroup
@@ -313,10 +313,10 @@
qed
text {*
- Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.
+ Thus, if we view class instances as ``structures'', then overloaded
+ constant definitions with recursion over types indirectly provide
+ some kind of ``functors'' --- i.e.\ mappings between abstract
+ theories.
*}
-end
\ No newline at end of file
+end