# HG changeset patch
# User wenzelm
# Date 1234783650 -3600
# Node ID 2ff24d87fad12d2ad530dc413953dc4ee84723c9
# Parent  bab2371e03484ef4b5f0eee5f7f8ab40f187b25a
removed obsolete axclass manual and examples;

diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-
-header {* Basic group theory *}
-
-theory Group imports Main begin
-
-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.
-*}
-
-subsection {* Monoids and Groups *}
-
-text {*
-  First we declare some polymorphic constants required later for the
-  signature parts of our structures.
-*}
-
-consts
-  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-  invers :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
-  one :: 'a    ("\<one>")
-
-text {*
-  \noindent Next we define class @{text monoid} of monoids with
-  operations @{text \<odot>} and @{text \<one>}.  Note that multiple class
-  axioms are allowed for user convenience --- they simply represent
-  the conjunction of their respective universal closures.
-*}
-
-axclass monoid \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-  left_unit: "\<one> \<odot> x = x"
-  right_unit: "x \<odot> \<one> = x"
-
-text {*
-  \noindent So class @{text monoid} contains exactly those types
-  @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"}
-  are specified appropriately, such that @{text \<odot>} is associative and
-  @{text \<one>} 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}.
-*}
-
-axclass semigroup \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-axclass group \<subseteq> semigroup
-  left_unit: "\<one> \<odot> x = x"
-  left_inverse: "x\<inv> \<odot> x = \<one>"
-
-axclass agroup \<subseteq> group
-  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.
-*}
-
-
-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.
-
-  \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> = (\<one>\<Colon>'a\<Colon>group)"
-proof -
-  have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
-    by (simp only: group_class.left_unit)
-  also have "... = \<one> \<odot> x \<odot> x\<inv>"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
-    by (simp only: group_class.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
-    by (simp only: group_class.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
-    by (simp only: group_class.left_unit)
-  also have "... = \<one>"
-    by (simp only: group_class.left_inverse)
-  finally show ?thesis .
-qed
-
-text {*
-  \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> \<one> = (x\<Colon>'a\<Colon>group)"
-proof -
-  have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
-    by (simp only: group_class.left_inverse)
-  also have "... = x \<odot> x\<inv> \<odot> x"
-    by (simp only: semigroup_class.assoc)
-  also have "... = \<one> \<odot> x"
-    by (simp only: group_right_inverse)
-  also have "... = x"
-    by (simp only: group_class.left_unit)
-  finally show ?thesis .
-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}.
-*}
-
-
-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}).
-
- \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){@{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 type}}} \put(50,45){\makebox(0,0){@{text 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){@{text agroup}}}
-       \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 type}}}
-     \end{picture}
-     \caption{Monoids and groups: according to definition, and by proof}
-     \label{fig:monoid-group}
-   \end{center}
- \end{figure}
-*}
-
-instance monoid \<subseteq> semigroup
-proof
-  fix x y z :: "'a\<Colon>monoid"
-  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
-    by (rule monoid_class.assoc)
-qed
-
-instance group \<subseteq> monoid
-proof
-  fix x y z :: "'a\<Colon>group"
-  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
-    by (rule semigroup_class.assoc)
-  show "\<one> \<odot> x = x"
-    by (rule group_class.left_unit)
-  show "x \<odot> \<one> = x"
-    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, 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
-  \isakeyword{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 \<one>} forms an Abelian group.
-*}
-
-defs (overloaded)
-  times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
-  inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
-  unit_bool_def: "\<one> \<equiv> False"
-
-text {*
-  \medskip It is important to note that above \isakeyword{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 \isakeyword{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
-proof (intro_classes,
-    unfold times_bool_def inverse_bool_def unit_bool_def)
-  fix x y z
-  show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast
-  show "(False \<noteq> x) = x" by blast
-  show "(x \<noteq> x) = False" by blast
-  show "(x \<noteq> y) = (y \<noteq> x)" by blast
-qed
-
-text {*
-  The result of an \isakeyword{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 \<one>} 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 \<one>}
-  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>}.
-
-  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.
-*}
-
-instance * :: (semigroup, semigroup) semigroup
-proof (intro_classes, unfold times_prod_def)
-  fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
-  show
-    "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r,
-      snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
-       (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
-        snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
-    by (simp add: semigroup_class.assoc)
-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.
-*}
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/Product.thy
--- a/doc-src/AxClass/Group/Product.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-
-header {* Syntactic classes *}
-
-theory Product imports Main begin
-
-text {*
-  \medskip\noindent There is still a feature of Isabelle's type system
-  left that we have not yet discussed.  When declaring polymorphic
-  constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
-  may be constrained by type classes (or even general sorts) in an
-  arbitrary way.  Note that by default, in Isabelle/HOL the
-  declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
-  for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
-  universal class of HOL, this is not really a constraint at all.
-
- The @{text product} class below provides a less degenerate example of
- syntactic type classes.
-*}
-
-axclass
-  product \<subseteq> type
-consts
-  product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-
-text {*
-  Here class @{text product} is defined as subclass of @{text type}
-  without any additional axioms.  This effects in logical equivalence
-  of @{text product} and @{text type}, as is reflected by the trivial
-  introduction rule generated for this definition.
-
-  \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
-  'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
-  'a"} anyway?  In this particular case where @{text "product \<equiv>
-  type"}, 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 @{text \<odot>} on some type @{text \<tau>} are rejected by the
- type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
- type signature.  In our example, this arity may be always added when
- required by means of an \isakeyword{instance} with the default proof
- (double-dot).
-
-  \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
-  @{text c}.  Only immediately before \emph{specifying} these
-  constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
-  c"}.
-
-  This is done for class @{text product} and type @{typ bool} as
-  follows.
-*}
-
-instance bool :: product ..
-defs (overloaded)
-  product_bool_def: "x \<odot> y \<equiv> x \<and> y"
-
-text {*
- The definition @{text prod_bool_def} becomes syntactically
- well-formed only after the arity @{text "bool \<Colon> product"} is made
- known to the type checker.
-
- \medskip It is very important to see that above \isakeyword{defs} are
- not directly connected with \isakeyword{instance} at all!  We were
- just following our convention to specify @{text \<odot>} on @{typ bool}
- after having instantiated @{text "bool \<Colon> 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 important 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} would not make much sense in
- Isabelle's meta-logic, because there is no internal notion of
- ``providing operations'' or even ``names of functions''.
-*}
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/ROOT.ML
--- a/doc-src/AxClass/Group/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-
-use_thy "Semigroups";
-use_thy "Group";
-use_thy "Product";
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/Semigroups.thy
--- a/doc-src/AxClass/Group/Semigroups.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-
-header {* Semigroups *}
-
-theory Semigroups imports Main begin
-
-text {*
-  \medskip\noindent An axiomatic type class is simply a class of types
-  that all meet certain properties, which are also called \emph{class
-  axioms}. Thus, type classes may be also understood as type
-  predicates --- i.e.\ abstractions over a single type argument @{typ
-  'a}.  Class axioms typically contain polymorphic constants that
-  depend on this type @{typ 'a}.  These \emph{characteristic
-  constants} behave like operations associated with the ``carrier''
-  type @{typ 'a}.
-
-  We illustrate these basic concepts by the following formulation of
-  semigroups.
-*}
-
-consts
-  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-axclass semigroup \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-text {*
-  \noindent Above we have first declared a polymorphic constant @{text
-  "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
-  all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
-  associative operator.  The @{text assoc} axiom contains exactly one
-  type variable, which is invisible in the above presentation, though.
-  Also note that free term variables (like @{term x}, @{term y},
-  @{term 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 @{typ 'a} and a fixed
-  \emph{signature}.  Different signatures require different classes.
-  Below, class @{text plus_semigroup} represents semigroups @{text
-  "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
-  correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
-*}
-
-consts
-  plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
-axclass plus_semigroup \<subseteq> type
-  assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-
-text {*
-  \noindent Even if classes @{text plus_semigroup} and @{text
-  semigroup} both represent semigroups in a sense, they are certainly
-  not quite the same.
-*}
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/document/Group.tex
--- a/doc-src/AxClass/Group/document/Group.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,512 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Group}%
-%
-\isamarkupheader{Basic group theory%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Monoids and Groups%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-First we declare some polymorphic constants required later for the
-  signature parts of our structures.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent Next we define class \isa{monoid} of monoids with
-  operations \isa{{\isasymodot}} and \isa{{\isasymone}}.  Note that multiple class
-  axioms are allowed for user convenience --- they simply represent
-  the conjunction of their respective universal closures.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ monoid\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent So class \isa{monoid} contains exactly those types
-  \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}}
-  are specified appropriately, such that \isa{{\isasymodot}} is associative and
-  \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}}
-  operation.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\medskip Independently of \isa{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 \isa{assoc}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ group\ {\isasymsubseteq}\ semigroup\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ agroup\ {\isasymsubseteq}\ group\isanewline
-\ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
-  from \isa{semigroup} and adds two further group axioms. Similarly,
-  \isa{agroup} is defined as the subset of \isa{group} such that
-  for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Abstract reasoning%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In a sense, axiomatic type classes may be viewed as \emph{abstract
-  theories}.  Above class definitions gives rise to abstract axioms
-  \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}.  \emph{Sort constraints} like this express a logical
-  precondition for the whole formula.  For example, \isa{assoc}
-  states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
-  much easier.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\medskip Abstract theorems may be instantiated to only those types
-  \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
-  known at Isabelle's type signature level.  Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Abstract instantiation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-From the definition, the \isa{monoid} and \isa{group} classes
-  have been independent.  Note that for monoids, \isa{right{\isacharunderscore}unit}
-  had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other
-  axioms.  With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group
-  theory (see page~\pageref{thm:group-right-unit}), we may now
-  instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ 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){\isa{agroup}}}
-       \put(15,25){\makebox(0,0){\isa{group}}}
-       \put(15,45){\makebox(0,0){\isa{semigroup}}}
-       \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{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){\isa{agroup}}}
-       \put(15,25){\makebox(0,0){\isa{group}}}
-       \put(15,45){\makebox(0,0){\isa{monoid}}}
-       \put(15,65){\makebox(0,0){\isa{semigroup}}}
-       \put(15,85){\makebox(0,0){\isa{type}}}
-     \end{picture}
-     \caption{Monoids and groups: according to definition, and by proof}
-     \label{fig:monoid-group}
-   \end{center}
- \end{figure}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ monoid\ {\isasymsubseteq}\ semigroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ group\ {\isasymsubseteq}\ monoid\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\medskip The \isakeyword{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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-So far we have covered the case of the form
-  \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely
-  \emph{abstract instantiation} --- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance of \isa{c\isactrlsub {\isadigit{2}}}.  Even more
-  interesting for practical applications are \emph{concrete
-  instantiations} of axiomatic type classes.  That is, certain simple
-  schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ 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 \isa{bool} with
-  exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
-  \isa{False} as \isa{{\isasymone}} forms an Abelian group.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline
-\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\medskip It is important to note that above \isakeyword{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 \isakeyword{defs} of the generic
-  group operations on type \isa{bool} appropriately, the class
-  membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
-\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The result of an \isakeyword{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, \isa{int\ {\isasymColon}\ agroup}
-  (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
-  and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
-  (e.g.\ if \isa{{\isasymodot}} is defined as list append).  Thus, the
-  characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}}
-  really become overloaded, i.e.\ have different meanings on different
-  types.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lifting and Functors%
-}
-\isamarkuptrue%
-%
-\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 \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
-  contain constants of name \isa{c} on the right-hand side --- if
-  these have types that are structurally simpler than \isa{{\isasymtau}}.
-
-  This feature enables us to \emph{lift operations}, say to Cartesian
-  products, direct sums or function spaces.  Subsequently we lift
-  \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
-  and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.  Hence the binary type constructor \isa{{\isasymodot}} maps semigroups
-  to semigroups.  This may be established formally as follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\isanewline
-\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline
-\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
-\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-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{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/document/Product.tex
--- a/doc-src/AxClass/Group/document/Product.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Product}%
-%
-\isamarkupheader{Syntactic classes%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent There is still a feature of Isabelle's type system
-  left that we have not yet discussed.  When declaring polymorphic
-  constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
-  may be constrained by type classes (or even general sorts) in an
-  arbitrary way.  Note that by default, in Isabelle/HOL the
-  declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
-  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
-  universal class of HOL, this is not really a constraint at all.
-
- The \isa{product} class below provides a less degenerate example of
- syntactic type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isasymsubseteq}\ type\isanewline
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-Here class \isa{product} is defined as subclass of \isa{type}
-  without any additional axioms.  This effects in logical equivalence
-  of \isa{product} and \isa{type}, as is reflected by the trivial
-  introduction rule generated for this definition.
-
-  \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway?  In this particular case where \isa{product\ {\isasymequiv}\ type}, 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 \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
- type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
- type signature.  In our example, this arity may be always added when
- required by means of an \isakeyword{instance} with the default proof
- (double-dot).
-
-  \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
-  \isa{c}.  Only immediately before \emph{specifying} these
-  constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
-
-  This is done for class \isa{product} and type \isa{bool} as
-  follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ product%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
- well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
- known to the type checker.
-
- \medskip It is very important to see that above \isakeyword{defs} are
- not directly connected with \isakeyword{instance} at all!  We were
- just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
- after having instantiated \isa{bool\ {\isasymColon}\ 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 important 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} would not make much sense in
- Isabelle's meta-logic, because there is no internal notion of
- ``providing operations'' or even ``names of functions''.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Group/document/Semigroups.tex
--- a/doc-src/AxClass/Group/document/Semigroups.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Semigroups}%
-%
-\isamarkupheader{Semigroups%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent An axiomatic type class is simply a class of types
-  that all meet certain properties, which are also called \emph{class
-  axioms}. Thus, type classes may be also understood as type
-  predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
-  depend on this type \isa{{\isacharprime}a}.  These \emph{characteristic
-  constants} behave like operations associated with the ``carrier''
-  type \isa{{\isacharprime}a}.
-
-  We illustrate these basic concepts by the following formulation of
-  semigroups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
-  all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
-  associative operator.  The \isa{assoc} axiom contains exactly one
-  type variable, which is invisible in the above presentation, though.
-  Also note that free term variables (like \isa{x}, \isa{y},
-  \isa{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 \isa{{\isacharprime}a} and a fixed
-  \emph{signature}.  Different signatures require different classes.
-  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
-  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
-  not quite the same.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/IsaMakefile
--- a/doc-src/AxClass/IsaMakefile	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-
-## targets
-
-default: Group Nat
-images: 
-test: Group Nat
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
-
-
-## Group
-
-Group: HOL $(LOG)/HOL-Group.gz
-
-HOL:
-	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-$(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/Group.thy \
-  Group/Product.thy Group/Semigroups.thy
-	@$(USEDIR) $(OUT)/HOL Group
-	@rm -f Group/document/pdfsetup.sty Group/document/session.tex
-
-
-## Nat
-
-Nat: FOL $(LOG)/FOL-Nat.gz
-
-FOL:
-	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
-
-$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
-	@$(USEDIR) $(OUT)/FOL Nat
-	@rm -f Nat/document/*.sty Nat/document/session.tex
-
-
-## clean
-
-clean:
-	@rm -f $(LOG)/HOL-Group.gz $(LOG)/FOL-Nat.gz
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Makefile
--- a/doc-src/AxClass/Makefile	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-#
-# $Id$
-#
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = axclass
-
-FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty	\
-  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty			\
-  Group/document/Group.tex Nat/document/NatClass.tex			\
-  Group/document/Product.tex Group/document/Semigroups.tex
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle_isar.eps
-	$(LATEX) $(NAME)
-	$(BIBTEX) $(NAME)
-	$(LATEX) $(NAME)
-	$(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle_isar.pdf
-	$(PDFLATEX) $(NAME)
-	$(FIXBOOKMARKS) $(NAME).out
-	$(BIBTEX) $(NAME)
-	$(PDFLATEX) $(NAME)
-	$(PDFLATEX) $(NAME)
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-
-header {* Defining natural numbers in FOL \label{sec:ex-natclass} *}
-
-theory NatClass imports FOL begin
-
-text {*
- \medskip\noindent Axiomatic type classes abstract over exactly one
- type argument. Thus, any \emph{axiomatic} theory extension where each
- axiom refers to at most one type variable, may be trivially turned
- into a \emph{definitional} one.
-
- We illustrate this with the natural numbers in
- Isabelle/FOL.\footnote{See also
- \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}
-*}
-
-consts
-  zero :: 'a    ("\<zero>")
-  Suc :: "'a \<Rightarrow> 'a"
-  rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
-
-axclass nat \<subseteq> "term"
-  induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
-  Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
-  Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
-  rec_0: "rec(\<zero>, a, f) = a"
-  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
-
-constdefs
-  add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "+" 60)
-  "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))"
-
-text {*
- This is an abstract version of the plain @{text Nat} theory in
- FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type @{text nat} by @{typ
- 'a} and used the natural number axioms to define class @{text nat}.
- There is only a minor snag, that the original recursion operator
- @{term rec} had to be made monomorphic.
-
- Thus class @{text nat} contains exactly those types @{text \<tau>} that
- are isomorphic to ``the'' natural numbers (with signature @{term
- \<zero>}, @{term Suc}, @{term rec}).
-
- \medskip What we have done here can be also viewed as \emph{type
- specification}.  Of course, it still remains open if there is some
- type at all that meets the class axioms.  Now a very nice property of
- axiomatic type classes is that abstract reasoning is always possible
- --- independent of satisfiability.  The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty later ---
- ``inconsistent'' class definitions may be useless, but do not cause
- any harm.
-
- Theorems of the abstract natural numbers may be derived in the same
- way as for the concrete version.  The original proof scripts may be
- re-used with some trivial changes only (mostly adding some type
- constraints).
-*}
-
-(*<*)
-lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
-apply (rule_tac n = k in induct)
-apply (rule notI)
-apply (erule Suc_neq_0)
-apply (rule notI)
-apply (erule notE)
-apply (erule Suc_inject)
-done
-
-lemma "(k+m)+n = k+(m+n)"
-apply (rule induct)
-back
-back
-back
-back
-back
-back
-oops
-
-lemma add_0 [simp]: "\<zero>+n = n"
-apply (unfold add_def)
-apply (rule rec_0)
-done
-
-lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
-apply (unfold add_def)
-apply (rule rec_Suc)
-done
-
-lemma add_assoc: "(k+m)+n = k+(m+n)"
-apply (rule_tac n = k in induct)
-apply simp
-apply simp
-done
-
-lemma add_0_right: "m+\<zero> = m"
-apply (rule_tac n = m in induct)
-apply simp
-apply simp
-done
-
-lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
-apply (rule_tac n = m in induct)
-apply simp_all
-done
-
-lemma
-  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
-  shows "f(i+j) = i+f(j)"
-apply (rule_tac n = i in induct)
-apply simp
-apply (simp add: prem)
-done
-(*>*)
-
-end
\ No newline at end of file
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Nat/ROOT.ML
--- a/doc-src/AxClass/Nat/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-use_thy "NatClass";
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/Nat/document/NatClass.tex
--- a/doc-src/AxClass/Nat/document/NatClass.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{NatClass}%
-%
-\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent Axiomatic type classes abstract over exactly one
- type argument. Thus, any \emph{axiomatic} theory extension where each
- axiom refers to at most one type variable, may be trivially turned
- into a \emph{definitional} one.
-
- We illustrate this with the natural numbers in
- Isabelle/FOL.\footnote{See also
- \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ nat\ {\isasymsubseteq}\ {\isachardoublequoteopen}term{\isachardoublequoteclose}\isanewline
-\ \ induct{\isacharcolon}\ {\isachardoublequoteopen}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequoteclose}\isanewline
-\ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
-\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-This is an abstract version of the plain \isa{Nat} theory in
- FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type \isa{nat} by \isa{{\isacharprime}a} and used the natural number axioms to define class \isa{nat}.
- There is only a minor snag, that the original recursion operator
- \isa{rec} had to be made monomorphic.
-
- Thus class \isa{nat} contains exactly those types \isa{{\isasymtau}} that
- are isomorphic to ``the'' natural numbers (with signature \isa{{\isasymzero}}, \isa{Suc}, \isa{rec}).
-
- \medskip What we have done here can be also viewed as \emph{type
- specification}.  Of course, it still remains open if there is some
- type at all that meets the class axioms.  Now a very nice property of
- axiomatic type classes is that abstract reasoning is always possible
- --- independent of satisfiability.  The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty later ---
- ``inconsistent'' class definitions may be useless, but do not cause
- any harm.
-
- Theorems of the abstract natural numbers may be derived in the same
- way as for the concrete version.  The original proof scripts may be
- re-used with some trivial changes only (mostly adding some type
- constraints).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/axclass.tex
--- a/doc-src/AxClass/axclass.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{graphicx,../iman,../extra,../isar}
-\usepackage{../isabelle,../isabellesym}
-\usepackage{../pdfsetup}  % last one!
-
-\isabellestyle{it}
-\newcommand{\isasyminv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymzero}{\isamath{0}}
-\renewcommand{\isasymone}{\isamath{1}}
-
-\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}
-
-\underscoreoff
-
-\maketitle 
-
-\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.
-  
-  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, though, but may refer to Isar's tactic emulation commands.
-\end{abstract}
-
-
-\pagenumbering{roman} \tableofcontents \clearfirst
-
-\include{body}
-
-%FIXME
-\nocite{nipkow-types93}
-\nocite{nipkow-sorts93}
-\nocite{Wenzel:1997:TPHOL}
-\nocite{paulson-isa-book}
-\nocite{isabelle-isar-ref}
-\nocite{Wenzel:1999:TPHOL}
-
-\begingroup
-  \bibliographystyle{plain} \small\raggedright\frenchspacing
-  \bibliography{../manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
-% LocalWords:  Isabelle FIXME
diff -r bab2371e0348 -r 2ff24d87fad1 doc-src/AxClass/body.tex
--- a/doc-src/AxClass/body.tex	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,166 +0,0 @@
-
-\chapter{Introduction}
-
-A Haskell-style type-system \cite{haskell-report} with ordered type-classes
-has been present in Isabelle since 1991 already \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 Isabelle94, 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 simply-typed Higher-Order Logic, by
-including types qualified by logical predicates and overloaded constant
-definitions (see \cite{Wenzel:1997:TPHOL} for further details).
-
-Yet even 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
-now provides an even more useful and convenient mechanism for light-weight
-abstract theories, without any special technical 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.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
-\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
-
-\input{Group/document/Semigroups}
-
-\input{Group/document/Group}
-
-\input{Group/document/Product}
-
-\input{Nat/document/NatClass}
-
-
-%% 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 \geq
-% 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 bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/Group.thy
--- a/src/HOL/AxClasses/Group.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-(*  Title:      HOL/AxClasses/Group.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-theory Group imports Main begin
-
-subsection {* Monoids and Groups *}
-
-consts
-  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
-  invers :: "'a => 'a"
-  one :: 'a
-
-
-axclass monoid < type
-  assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
-  left_unit:  "one [*] x = x"
-  right_unit: "x [*] one = x"
-
-axclass semigroup < type
-  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
-
-axclass group < semigroup
-  left_unit:    "one [*] x = x"
-  left_inverse: "invers x [*] x = one"
-
-axclass agroup < group
-  commute: "x [*] y = y [*] x"
-
-
-subsection {* Abstract reasoning *}
-
-theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
-proof -
-  have "x [*] invers x = one [*] (x [*] invers x)"
-    by (simp only: group_class.left_unit)
-  also have "... = one [*] x [*] invers x"
-    by (simp only: semigroup_class.assoc)
-  also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
-    by (simp only: group_class.left_inverse)
-  also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
-    by (simp only: semigroup_class.assoc)
-  also have "... = invers (invers x) [*] one [*] invers x"
-    by (simp only: group_class.left_inverse)
-  also have "... = invers (invers x) [*] (one [*] invers x)"
-    by (simp only: semigroup_class.assoc)
-  also have "... = invers (invers x) [*] invers x"
-    by (simp only: group_class.left_unit)
-  also have "... = one"
-    by (simp only: group_class.left_inverse)
-  finally show ?thesis .
-qed
-
-theorem group_right_unit: "x [*] one = (x::'a::group)"
-proof -
-  have "x [*] one = x [*] (invers x [*] x)"
-    by (simp only: group_class.left_inverse)
-  also have "... = x [*] invers x [*] x"
-    by (simp only: semigroup_class.assoc)
-  also have "... = one [*] x"
-    by (simp only: group_right_inverse)
-  also have "... = x"
-    by (simp only: group_class.left_unit)
-  finally show ?thesis .
-qed
-
-
-subsection {* Abstract instantiation *}
-
-instance monoid < semigroup
-proof intro_classes
-  fix x y z :: "'a::monoid"
-  show "x [*] y [*] z = x [*] (y [*] z)"
-    by (rule monoid_class.assoc)
-qed
-
-instance group < monoid
-proof intro_classes
-  fix x y z :: "'a::group"
-  show "x [*] y [*] z = x [*] (y [*] z)"
-    by (rule semigroup_class.assoc)
-  show "one [*] x = x"
-    by (rule group_class.left_unit)
-  show "x [*] one = x"
-    by (rule group_right_unit)
-qed
-
-
-subsection {* Concrete instantiation *}
-
-defs (overloaded)
-  times_bool_def:   "x [*] y == x ~= (y::bool)"
-  inverse_bool_def: "invers x == x::bool"
-  unit_bool_def:    "one == False"
-
-instance bool :: agroup
-proof (intro_classes,
-    unfold times_bool_def inverse_bool_def unit_bool_def)
-  fix x y z
-  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
-
-
-subsection {* Lifting and Functors *}
-
-defs (overloaded)
-  times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"
-
-instance * :: (semigroup, semigroup) semigroup
-proof (intro_classes, unfold times_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_class.assoc)
-qed
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/Lattice/OrdInsts.thy
--- a/src/HOL/AxClasses/Lattice/OrdInsts.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      OrdInsts.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Some order instantiations.
-*)
-
-OrdInsts = OrdDefs +
-
-
-(* binary / general products of quasi_orders / orders *)
-
-instance
-  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
-
-instance
-  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
-  
-
-instance
-  fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
-
-instance
-  fun :: (term, partial_order) partial_order            (le_fun_antisym)
-
-
-(* duals of quasi orders / partial orders / linear orders *)
-
-instance
-  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
-
-instance
-  dual :: (partial_order) partial_order                 (le_dual_antisym)
-
-
-(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
-  'feature' in Pure/type.ML
-
-instance
-  dual :: (linear_order) linear_order                   (le_dual_lin)
-*)
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/Product.thy
--- a/src/HOL/AxClasses/Product.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      HOL/AxClasses/Product.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-theory Product imports Main begin
-
-axclass product < type
-
-consts
-  product :: "'a::product => 'a => 'a"    (infixl "[*]" 70)
-
-
-instance bool :: product
-  by intro_classes
-
-defs (overloaded)
-  product_bool_def: "x [*] y == x & y"
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/README.html
--- a/src/HOL/AxClasses/README.html	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<html>
-
-<head>
-  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
-  <title>HOL/AxClasses</title>
-</head>
-
-<body>
-<h1>HOL/AxClasses</h1>
-
-These are the HOL examples of the tutorial <a
-href="http://isabelle.in.tum.de/dist/Isabelle/doc/axclass.pdf">Using Axiomatic Type
-Classes in Isabelle</a>.  See also FOL/ex/NatClass for the natural
-number example.
-</body>
-</html>
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/ROOT.ML
--- a/src/HOL/AxClasses/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(* $Id$ *)
-
-use_thys ["Semigroups", "Group", "Product"];
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/AxClasses/Semigroups.thy
--- a/src/HOL/AxClasses/Semigroups.thy	Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title:      HOL/AxClasses/Semigroups.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-theory Semigroups imports Main begin
-
-consts
-  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
-
-axclass semigroup < type
-  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
-
-
-consts
-  plus :: "'a => 'a => 'a"    (infixl "[+]" 70)
-
-axclass plus_semigroup < type
-  assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
-
-end
diff -r bab2371e0348 -r 2ff24d87fad1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Feb 15 21:26:25 2009 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 16 12:27:30 2009 +0100
@@ -13,7 +13,6 @@
   HOL-Library \
   HOL-ex \
   HOL-Auth \
-  HOL-AxClasses \
   HOL-Bali \
   HOL-Extraction \
   HOL-HahnBanach \
@@ -770,15 +769,6 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
 
 
-## HOL-AxClasses
-
-HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
-
-$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
-  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
-
-
 ## HOL-Lattice
 
 HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
@@ -1045,22 +1035,22 @@
 ## clean
 
 clean:
-	@rm -f  $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
-		$(LOG)/HOL.gz $(LOG)/TLA.gz \
-		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
-		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
-		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
-		$(LOG)/HOL-HoareParallel.gz \
-		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
-		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
-		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-                $(LOG)/HOL-Bali.gz \
-		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
-                $(LOG)/HOL-Nominal-Examples.gz \
-		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
-		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
-		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
-                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
-		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
-                $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
-                $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
+	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
+		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
+		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
+		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
+		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
+		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
+		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
+		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
+		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
+		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
+		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
+		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
+		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
+		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
+		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
+		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
+		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
+		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
+		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz