removed obsolete axclass manual and examples;
authorwenzelm
Mon Feb 16 12:27:30 2009 +0100 (2009-02-16)
changeset 297482ff24d87fad1
parent 29747 bab2371e0348
child 29749 5a576282c935
removed obsolete axclass manual and examples;
doc-src/AxClass/Group/Group.thy
doc-src/AxClass/Group/Product.thy
doc-src/AxClass/Group/ROOT.ML
doc-src/AxClass/Group/Semigroups.thy
doc-src/AxClass/Group/document/Group.tex
doc-src/AxClass/Group/document/Product.tex
doc-src/AxClass/Group/document/Semigroups.tex
doc-src/AxClass/IsaMakefile
doc-src/AxClass/Makefile
doc-src/AxClass/Nat/NatClass.thy
doc-src/AxClass/Nat/ROOT.ML
doc-src/AxClass/Nat/document/NatClass.tex
doc-src/AxClass/axclass.tex
doc-src/AxClass/body.tex
src/HOL/AxClasses/Group.thy
src/HOL/AxClasses/Lattice/OrdInsts.thy
src/HOL/AxClasses/Product.thy
src/HOL/AxClasses/README.html
src/HOL/AxClasses/ROOT.ML
src/HOL/AxClasses/Semigroups.thy
src/HOL/IsaMakefile
     1.1 --- a/doc-src/AxClass/Group/Group.thy	Sun Feb 15 21:26:25 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,322 +0,0 @@
     1.4 -
     1.5 -header {* Basic group theory *}
     1.6 -
     1.7 -theory Group imports Main begin
     1.8 -
     1.9 -text {*
    1.10 -  \medskip\noindent The meta-level type system of Isabelle supports
    1.11 -  \emph{intersections} and \emph{inclusions} of type classes. These
    1.12 -  directly correspond to intersections and inclusions of type
    1.13 -  predicates in a purely set theoretic sense. This is sufficient as a
    1.14 -  means to describe simple hierarchies of structures.  As an
    1.15 -  illustration, we use the well-known example of semigroups, monoids,
    1.16 -  general groups and Abelian groups.
    1.17 -*}
    1.18 -
    1.19 -subsection {* Monoids and Groups *}
    1.20 -
    1.21 -text {*
    1.22 -  First we declare some polymorphic constants required later for the
    1.23 -  signature parts of our structures.
    1.24 -*}
    1.25 -
    1.26 -consts
    1.27 -  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
    1.28 -  invers :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
    1.29 -  one :: 'a    ("\<one>")
    1.30 -
    1.31 -text {*
    1.32 -  \noindent Next we define class @{text monoid} of monoids with
    1.33 -  operations @{text \<odot>} and @{text \<one>}.  Note that multiple class
    1.34 -  axioms are allowed for user convenience --- they simply represent
    1.35 -  the conjunction of their respective universal closures.
    1.36 -*}
    1.37 -
    1.38 -axclass monoid \<subseteq> type
    1.39 -  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    1.40 -  left_unit: "\<one> \<odot> x = x"
    1.41 -  right_unit: "x \<odot> \<one> = x"
    1.42 -
    1.43 -text {*
    1.44 -  \noindent So class @{text monoid} contains exactly those types
    1.45 -  @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"}
    1.46 -  are specified appropriately, such that @{text \<odot>} is associative and
    1.47 -  @{text \<one>} is a left and right unit element for the @{text \<odot>}
    1.48 -  operation.
    1.49 -*}
    1.50 -
    1.51 -text {*
    1.52 -  \medskip Independently of @{text monoid}, we now define a linear
    1.53 -  hierarchy of semigroups, general groups and Abelian groups.  Note
    1.54 -  that the names of class axioms are automatically qualified with each
    1.55 -  class name, so we may re-use common names such as @{text assoc}.
    1.56 -*}
    1.57 -
    1.58 -axclass semigroup \<subseteq> type
    1.59 -  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    1.60 -
    1.61 -axclass group \<subseteq> semigroup
    1.62 -  left_unit: "\<one> \<odot> x = x"
    1.63 -  left_inverse: "x\<inv> \<odot> x = \<one>"
    1.64 -
    1.65 -axclass agroup \<subseteq> group
    1.66 -  commute: "x \<odot> y = y \<odot> x"
    1.67 -
    1.68 -text {*
    1.69 -  \noindent Class @{text group} inherits associativity of @{text \<odot>}
    1.70 -  from @{text semigroup} and adds two further group axioms. Similarly,
    1.71 -  @{text agroup} is defined as the subset of @{text group} such that
    1.72 -  for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
    1.73 -  \<tau>"} is even commutative.
    1.74 -*}
    1.75 -
    1.76 -
    1.77 -subsection {* Abstract reasoning *}
    1.78 -
    1.79 -text {*
    1.80 -  In a sense, axiomatic type classes may be viewed as \emph{abstract
    1.81 -  theories}.  Above class definitions gives rise to abstract axioms
    1.82 -  @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
    1.83 -  commute}, where any of these contain a type variable @{text "'a \<Colon>
    1.84 -  c"} that is restricted to types of the corresponding class @{text
    1.85 -  c}.  \emph{Sort constraints} like this express a logical
    1.86 -  precondition for the whole formula.  For example, @{text assoc}
    1.87 -  states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
    1.88 -  semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
    1.89 -
    1.90 -  \medskip From a technical point of view, abstract axioms are just
    1.91 -  ordinary Isabelle theorems, which may be used in proofs without
    1.92 -  special treatment.  Such ``abstract proofs'' usually yield new
    1.93 -  ``abstract theorems''.  For example, we may now derive the following
    1.94 -  well-known laws of general groups.
    1.95 -*}
    1.96 -
    1.97 -theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
    1.98 -proof -
    1.99 -  have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
   1.100 -    by (simp only: group_class.left_unit)
   1.101 -  also have "... = \<one> \<odot> x \<odot> x\<inv>"
   1.102 -    by (simp only: semigroup_class.assoc)
   1.103 -  also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
   1.104 -    by (simp only: group_class.left_inverse)
   1.105 -  also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
   1.106 -    by (simp only: semigroup_class.assoc)
   1.107 -  also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
   1.108 -    by (simp only: group_class.left_inverse)
   1.109 -  also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
   1.110 -    by (simp only: semigroup_class.assoc)
   1.111 -  also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
   1.112 -    by (simp only: group_class.left_unit)
   1.113 -  also have "... = \<one>"
   1.114 -    by (simp only: group_class.left_inverse)
   1.115 -  finally show ?thesis .
   1.116 -qed
   1.117 -
   1.118 -text {*
   1.119 -  \noindent With @{text group_right_inverse} already available, @{text
   1.120 -  group_right_unit}\label{thm:group-right-unit} is now established
   1.121 -  much easier.
   1.122 -*}
   1.123 -
   1.124 -theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
   1.125 -proof -
   1.126 -  have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
   1.127 -    by (simp only: group_class.left_inverse)
   1.128 -  also have "... = x \<odot> x\<inv> \<odot> x"
   1.129 -    by (simp only: semigroup_class.assoc)
   1.130 -  also have "... = \<one> \<odot> x"
   1.131 -    by (simp only: group_right_inverse)
   1.132 -  also have "... = x"
   1.133 -    by (simp only: group_class.left_unit)
   1.134 -  finally show ?thesis .
   1.135 -qed
   1.136 -
   1.137 -text {*
   1.138 -  \medskip Abstract theorems may be instantiated to only those types
   1.139 -  @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
   1.140 -  known at Isabelle's type signature level.  Since we have @{text
   1.141 -  "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
   1.142 -  semigroup} and @{text group} are automatically inherited by @{text
   1.143 -  group} and @{text agroup}.
   1.144 -*}
   1.145 -
   1.146 -
   1.147 -subsection {* Abstract instantiation *}
   1.148 -
   1.149 -text {*
   1.150 -  From the definition, the @{text monoid} and @{text group} classes
   1.151 -  have been independent.  Note that for monoids, @{text right_unit}
   1.152 -  had to be included as an axiom, but for groups both @{text
   1.153 -  right_unit} and @{text right_inverse} are derivable from the other
   1.154 -  axioms.  With @{text group_right_unit} derived as a theorem of group
   1.155 -  theory (see page~\pageref{thm:group-right-unit}), we may now
   1.156 -  instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
   1.157 -  monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
   1.158 -
   1.159 - \begin{figure}[htbp]
   1.160 -   \begin{center}
   1.161 -     \small
   1.162 -     \unitlength 0.6mm
   1.163 -     \begin{picture}(65,90)(0,-10)
   1.164 -       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
   1.165 -       \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
   1.166 -       \put(15,5){\makebox(0,0){@{text agroup}}}
   1.167 -       \put(15,25){\makebox(0,0){@{text group}}}
   1.168 -       \put(15,45){\makebox(0,0){@{text semigroup}}}
   1.169 -       \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
   1.170 -     \end{picture}
   1.171 -     \hspace{4em}
   1.172 -     \begin{picture}(30,90)(0,0)
   1.173 -       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
   1.174 -       \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
   1.175 -       \put(15,5){\makebox(0,0){@{text agroup}}}
   1.176 -       \put(15,25){\makebox(0,0){@{text group}}}
   1.177 -       \put(15,45){\makebox(0,0){@{text monoid}}}
   1.178 -       \put(15,65){\makebox(0,0){@{text semigroup}}}
   1.179 -       \put(15,85){\makebox(0,0){@{text type}}}
   1.180 -     \end{picture}
   1.181 -     \caption{Monoids and groups: according to definition, and by proof}
   1.182 -     \label{fig:monoid-group}
   1.183 -   \end{center}
   1.184 - \end{figure}
   1.185 -*}
   1.186 -
   1.187 -instance monoid \<subseteq> semigroup
   1.188 -proof
   1.189 -  fix x y z :: "'a\<Colon>monoid"
   1.190 -  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
   1.191 -    by (rule monoid_class.assoc)
   1.192 -qed
   1.193 -
   1.194 -instance group \<subseteq> monoid
   1.195 -proof
   1.196 -  fix x y z :: "'a\<Colon>group"
   1.197 -  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
   1.198 -    by (rule semigroup_class.assoc)
   1.199 -  show "\<one> \<odot> x = x"
   1.200 -    by (rule group_class.left_unit)
   1.201 -  show "x \<odot> \<one> = x"
   1.202 -    by (rule group_right_unit)
   1.203 -qed
   1.204 -
   1.205 -text {*
   1.206 -  \medskip The \isakeyword{instance} command sets up an appropriate
   1.207 -  goal that represents the class inclusion (or type arity, see
   1.208 -  \secref{sec:inst-arity}) to be proven (see also
   1.209 -  \cite{isabelle-isar-ref}).  The initial proof step causes
   1.210 -  back-chaining of class membership statements wrt.\ the hierarchy of
   1.211 -  any classes defined in the current theory; the effect is to reduce
   1.212 -  to the initial statement to a number of goals that directly
   1.213 -  correspond to any class axioms encountered on the path upwards
   1.214 -  through the class hierarchy.
   1.215 -*}
   1.216 -
   1.217 -
   1.218 -subsection {* Concrete instantiation \label{sec:inst-arity} *}
   1.219 -
   1.220 -text {*
   1.221 -  So far we have covered the case of the form
   1.222 -  \isakeyword{instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely
   1.223 -  \emph{abstract instantiation} --- $c@1$ is more special than @{text
   1.224 -  "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}.  Even more
   1.225 -  interesting for practical applications are \emph{concrete
   1.226 -  instantiations} of axiomatic type classes.  That is, certain simple
   1.227 -  schemes @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class
   1.228 -  membership may be established at the logical level and then
   1.229 -  transferred to Isabelle's type signature level.
   1.230 -
   1.231 -  \medskip As a typical example, we show that type @{typ bool} with
   1.232 -  exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
   1.233 -  @{term False} as @{text \<one>} forms an Abelian group.
   1.234 -*}
   1.235 -
   1.236 -defs (overloaded)
   1.237 -  times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
   1.238 -  inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
   1.239 -  unit_bool_def: "\<one> \<equiv> False"
   1.240 -
   1.241 -text {*
   1.242 -  \medskip It is important to note that above \isakeyword{defs} are
   1.243 -  just overloaded meta-level constant definitions, where type classes
   1.244 -  are not yet involved at all.  This form of constant definition with
   1.245 -  overloading (and optional recursion over the syntactic structure of
   1.246 -  simple types) are admissible as definitional extensions of plain HOL
   1.247 -  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   1.248 -  required for overloading.  Nevertheless, overloaded definitions are
   1.249 -  best applied in the context of type classes.
   1.250 -
   1.251 -  \medskip Since we have chosen above \isakeyword{defs} of the generic
   1.252 -  group operations on type @{typ bool} appropriately, the class
   1.253 -  membership @{text "bool \<Colon> agroup"} may be now derived as follows.
   1.254 -*}
   1.255 -
   1.256 -instance bool :: agroup
   1.257 -proof (intro_classes,
   1.258 -    unfold times_bool_def inverse_bool_def unit_bool_def)
   1.259 -  fix x y z
   1.260 -  show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast
   1.261 -  show "(False \<noteq> x) = x" by blast
   1.262 -  show "(x \<noteq> x) = False" by blast
   1.263 -  show "(x \<noteq> y) = (y \<noteq> x)" by blast
   1.264 -qed
   1.265 -
   1.266 -text {*
   1.267 -  The result of an \isakeyword{instance} statement is both expressed
   1.268 -  as a theorem of Isabelle's meta-logic, and as a type arity of the
   1.269 -  type signature.  The latter enables type-inference system to take
   1.270 -  care of this new instance automatically.
   1.271 -
   1.272 -  \medskip We could now also instantiate our group theory classes to
   1.273 -  many other concrete types.  For example, @{text "int \<Colon> agroup"}
   1.274 -  (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
   1.275 -  and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"}
   1.276 -  (e.g.\ if @{text \<odot>} is defined as list append).  Thus, the
   1.277 -  characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<one>}
   1.278 -  really become overloaded, i.e.\ have different meanings on different
   1.279 -  types.
   1.280 -*}
   1.281 -
   1.282 -
   1.283 -subsection {* Lifting and Functors *}
   1.284 -
   1.285 -text {*
   1.286 -  As already mentioned above, overloading in the simply-typed HOL
   1.287 -  systems may include recursion over the syntactic structure of types.
   1.288 -  That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
   1.289 -  contain constants of name @{text c} on the right-hand side --- if
   1.290 -  these have types that are structurally simpler than @{text \<tau>}.
   1.291 -
   1.292 -  This feature enables us to \emph{lift operations}, say to Cartesian
   1.293 -  products, direct sums or function spaces.  Subsequently we lift
   1.294 -  @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
   1.295 -*}
   1.296 -
   1.297 -defs (overloaded)
   1.298 -  times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
   1.299 -
   1.300 -text {*
   1.301 -  It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
   1.302 -  and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
   1.303 -  'b"}.  Hence the binary type constructor @{text \<odot>} maps semigroups
   1.304 -  to semigroups.  This may be established formally as follows.
   1.305 -*}
   1.306 -
   1.307 -instance * :: (semigroup, semigroup) semigroup
   1.308 -proof (intro_classes, unfold times_prod_def)
   1.309 -  fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
   1.310 -  show
   1.311 -    "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r,
   1.312 -      snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
   1.313 -       (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
   1.314 -        snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
   1.315 -    by (simp add: semigroup_class.assoc)
   1.316 -qed
   1.317 -
   1.318 -text {*
   1.319 -  Thus, if we view class instances as ``structures'', then overloaded
   1.320 -  constant definitions with recursion over types indirectly provide
   1.321 -  some kind of ``functors'' --- i.e.\ mappings between abstract
   1.322 -  theories.
   1.323 -*}
   1.324 -
   1.325 -end
     2.1 --- a/doc-src/AxClass/Group/Product.thy	Sun Feb 15 21:26:25 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,85 +0,0 @@
     2.4 -
     2.5 -header {* Syntactic classes *}
     2.6 -
     2.7 -theory Product imports Main begin
     2.8 -
     2.9 -text {*
    2.10 -  \medskip\noindent There is still a feature of Isabelle's type system
    2.11 -  left that we have not yet discussed.  When declaring polymorphic
    2.12 -  constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
    2.13 -  may be constrained by type classes (or even general sorts) in an
    2.14 -  arbitrary way.  Note that by default, in Isabelle/HOL the
    2.15 -  declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
    2.16 -  for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
    2.17 -  universal class of HOL, this is not really a constraint at all.
    2.18 -
    2.19 - The @{text product} class below provides a less degenerate example of
    2.20 - syntactic type classes.
    2.21 -*}
    2.22 -
    2.23 -axclass
    2.24 -  product \<subseteq> type
    2.25 -consts
    2.26 -  product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
    2.27 -
    2.28 -text {*
    2.29 -  Here class @{text product} is defined as subclass of @{text type}
    2.30 -  without any additional axioms.  This effects in logical equivalence
    2.31 -  of @{text product} and @{text type}, as is reflected by the trivial
    2.32 -  introduction rule generated for this definition.
    2.33 -
    2.34 -  \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
    2.35 -  'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
    2.36 -  'a"} anyway?  In this particular case where @{text "product \<equiv>
    2.37 -  type"}, it should be obvious that both declarations are the same
    2.38 -  from the logic's point of view.  It even makes the most sense to
    2.39 -  remove sort constraints from constant declarations, as far as the
    2.40 -  purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
    2.41 -
    2.42 -  On the other hand there are syntactic differences, of course.
    2.43 - Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
    2.44 - type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
    2.45 - type signature.  In our example, this arity may be always added when
    2.46 - required by means of an \isakeyword{instance} with the default proof
    2.47 - (double-dot).
    2.48 -
    2.49 -  \medskip Thus, we may observe the following discipline of using
    2.50 -  syntactic classes.  Overloaded polymorphic constants have their type
    2.51 -  arguments restricted to an associated (logically trivial) class
    2.52 -  @{text c}.  Only immediately before \emph{specifying} these
    2.53 -  constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
    2.54 -  c"}.
    2.55 -
    2.56 -  This is done for class @{text product} and type @{typ bool} as
    2.57 -  follows.
    2.58 -*}
    2.59 -
    2.60 -instance bool :: product ..
    2.61 -defs (overloaded)
    2.62 -  product_bool_def: "x \<odot> y \<equiv> x \<and> y"
    2.63 -
    2.64 -text {*
    2.65 - The definition @{text prod_bool_def} becomes syntactically
    2.66 - well-formed only after the arity @{text "bool \<Colon> product"} is made
    2.67 - known to the type checker.
    2.68 -
    2.69 - \medskip It is very important to see that above \isakeyword{defs} are
    2.70 - not directly connected with \isakeyword{instance} at all!  We were
    2.71 - just following our convention to specify @{text \<odot>} on @{typ bool}
    2.72 - after having instantiated @{text "bool \<Colon> product"}.  Isabelle does
    2.73 - not require these definitions, which is in contrast to programming
    2.74 - languages like Haskell \cite{haskell-report}.
    2.75 -
    2.76 - \medskip While Isabelle type classes and those of Haskell are almost
    2.77 - the same as far as type-checking and type inference are concerned,
    2.78 - there are important semantic differences.  Haskell classes require
    2.79 - their instances to \emph{provide operations} of certain \emph{names}.
    2.80 - Therefore, its \texttt{instance} has a \texttt{where} part that tells
    2.81 - the system what these ``member functions'' should be.
    2.82 -
    2.83 - This style of \texttt{instance} would not make much sense in
    2.84 - Isabelle's meta-logic, because there is no internal notion of
    2.85 - ``providing operations'' or even ``names of functions''.
    2.86 -*}
    2.87 -
    2.88 -end
     3.1 --- a/doc-src/AxClass/Group/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,4 +0,0 @@
     3.4 -
     3.5 -use_thy "Semigroups";
     3.6 -use_thy "Group";
     3.7 -use_thy "Product";
     4.1 --- a/doc-src/AxClass/Group/Semigroups.thy	Sun Feb 15 21:26:25 2009 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,54 +0,0 @@
     4.4 -
     4.5 -header {* Semigroups *}
     4.6 -
     4.7 -theory Semigroups imports Main begin
     4.8 -
     4.9 -text {*
    4.10 -  \medskip\noindent An axiomatic type class is simply a class of types
    4.11 -  that all meet certain properties, which are also called \emph{class
    4.12 -  axioms}. Thus, type classes may be also understood as type
    4.13 -  predicates --- i.e.\ abstractions over a single type argument @{typ
    4.14 -  'a}.  Class axioms typically contain polymorphic constants that
    4.15 -  depend on this type @{typ 'a}.  These \emph{characteristic
    4.16 -  constants} behave like operations associated with the ``carrier''
    4.17 -  type @{typ 'a}.
    4.18 -
    4.19 -  We illustrate these basic concepts by the following formulation of
    4.20 -  semigroups.
    4.21 -*}
    4.22 -
    4.23 -consts
    4.24 -  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
    4.25 -axclass semigroup \<subseteq> type
    4.26 -  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
    4.27 -
    4.28 -text {*
    4.29 -  \noindent Above we have first declared a polymorphic constant @{text
    4.30 -  "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
    4.31 -  all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
    4.32 -  associative operator.  The @{text assoc} axiom contains exactly one
    4.33 -  type variable, which is invisible in the above presentation, though.
    4.34 -  Also note that free term variables (like @{term x}, @{term y},
    4.35 -  @{term z}) are allowed for user convenience --- conceptually all of
    4.36 -  these are bound by outermost universal quantifiers.
    4.37 -
    4.38 -  \medskip In general, type classes may be used to describe
    4.39 -  \emph{structures} with exactly one carrier @{typ 'a} and a fixed
    4.40 -  \emph{signature}.  Different signatures require different classes.
    4.41 -  Below, class @{text plus_semigroup} represents semigroups @{text
    4.42 -  "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
    4.43 -  correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
    4.44 -*}
    4.45 -
    4.46 -consts
    4.47 -  plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
    4.48 -axclass plus_semigroup \<subseteq> type
    4.49 -  assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
    4.50 -
    4.51 -text {*
    4.52 -  \noindent Even if classes @{text plus_semigroup} and @{text
    4.53 -  semigroup} both represent semigroups in a sense, they are certainly
    4.54 -  not quite the same.
    4.55 -*}
    4.56 -
    4.57 -end
     5.1 --- a/doc-src/AxClass/Group/document/Group.tex	Sun Feb 15 21:26:25 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,512 +0,0 @@
     5.4 -%
     5.5 -\begin{isabellebody}%
     5.6 -\def\isabellecontext{Group}%
     5.7 -%
     5.8 -\isamarkupheader{Basic group theory%
     5.9 -}
    5.10 -\isamarkuptrue%
    5.11 -%
    5.12 -\isadelimtheory
    5.13 -%
    5.14 -\endisadelimtheory
    5.15 -%
    5.16 -\isatagtheory
    5.17 -\isacommand{theory}\isamarkupfalse%
    5.18 -\ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
    5.19 -\endisatagtheory
    5.20 -{\isafoldtheory}%
    5.21 -%
    5.22 -\isadelimtheory
    5.23 -%
    5.24 -\endisadelimtheory
    5.25 -%
    5.26 -\begin{isamarkuptext}%
    5.27 -\medskip\noindent The meta-level type system of Isabelle supports
    5.28 -  \emph{intersections} and \emph{inclusions} of type classes. These
    5.29 -  directly correspond to intersections and inclusions of type
    5.30 -  predicates in a purely set theoretic sense. This is sufficient as a
    5.31 -  means to describe simple hierarchies of structures.  As an
    5.32 -  illustration, we use the well-known example of semigroups, monoids,
    5.33 -  general groups and Abelian groups.%
    5.34 -\end{isamarkuptext}%
    5.35 -\isamarkuptrue%
    5.36 -%
    5.37 -\isamarkupsubsection{Monoids and Groups%
    5.38 -}
    5.39 -\isamarkuptrue%
    5.40 -%
    5.41 -\begin{isamarkuptext}%
    5.42 -First we declare some polymorphic constants required later for the
    5.43 -  signature parts of our structures.%
    5.44 -\end{isamarkuptext}%
    5.45 -\isamarkuptrue%
    5.46 -\isacommand{consts}\isamarkupfalse%
    5.47 -\isanewline
    5.48 -\ \ 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
    5.49 -\ \ 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
    5.50 -\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}%
    5.51 -\begin{isamarkuptext}%
    5.52 -\noindent Next we define class \isa{monoid} of monoids with
    5.53 -  operations \isa{{\isasymodot}} and \isa{{\isasymone}}.  Note that multiple class
    5.54 -  axioms are allowed for user convenience --- they simply represent
    5.55 -  the conjunction of their respective universal closures.%
    5.56 -\end{isamarkuptext}%
    5.57 -\isamarkuptrue%
    5.58 -\isacommand{axclass}\isamarkupfalse%
    5.59 -\ monoid\ {\isasymsubseteq}\ type\isanewline
    5.60 -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
    5.61 -\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
    5.62 -\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
    5.63 -\begin{isamarkuptext}%
    5.64 -\noindent So class \isa{monoid} contains exactly those types
    5.65 -  \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}}
    5.66 -  are specified appropriately, such that \isa{{\isasymodot}} is associative and
    5.67 -  \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}}
    5.68 -  operation.%
    5.69 -\end{isamarkuptext}%
    5.70 -\isamarkuptrue%
    5.71 -%
    5.72 -\begin{isamarkuptext}%
    5.73 -\medskip Independently of \isa{monoid}, we now define a linear
    5.74 -  hierarchy of semigroups, general groups and Abelian groups.  Note
    5.75 -  that the names of class axioms are automatically qualified with each
    5.76 -  class name, so we may re-use common names such as \isa{assoc}.%
    5.77 -\end{isamarkuptext}%
    5.78 -\isamarkuptrue%
    5.79 -\isacommand{axclass}\isamarkupfalse%
    5.80 -\ semigroup\ {\isasymsubseteq}\ type\isanewline
    5.81 -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
    5.82 -\isanewline
    5.83 -\isacommand{axclass}\isamarkupfalse%
    5.84 -\ group\ {\isasymsubseteq}\ semigroup\isanewline
    5.85 -\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
    5.86 -\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
    5.87 -\isanewline
    5.88 -\isacommand{axclass}\isamarkupfalse%
    5.89 -\ agroup\ {\isasymsubseteq}\ group\isanewline
    5.90 -\ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}%
    5.91 -\begin{isamarkuptext}%
    5.92 -\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
    5.93 -  from \isa{semigroup} and adds two further group axioms. Similarly,
    5.94 -  \isa{agroup} is defined as the subset of \isa{group} such that
    5.95 -  for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
    5.96 -\end{isamarkuptext}%
    5.97 -\isamarkuptrue%
    5.98 -%
    5.99 -\isamarkupsubsection{Abstract reasoning%
   5.100 -}
   5.101 -\isamarkuptrue%
   5.102 -%
   5.103 -\begin{isamarkuptext}%
   5.104 -In a sense, axiomatic type classes may be viewed as \emph{abstract
   5.105 -  theories}.  Above class definitions gives rise to abstract axioms
   5.106 -  \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
   5.107 -  precondition for the whole formula.  For example, \isa{assoc}
   5.108 -  states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
   5.109 -
   5.110 -  \medskip From a technical point of view, abstract axioms are just
   5.111 -  ordinary Isabelle theorems, which may be used in proofs without
   5.112 -  special treatment.  Such ``abstract proofs'' usually yield new
   5.113 -  ``abstract theorems''.  For example, we may now derive the following
   5.114 -  well-known laws of general groups.%
   5.115 -\end{isamarkuptext}%
   5.116 -\isamarkuptrue%
   5.117 -\isacommand{theorem}\isamarkupfalse%
   5.118 -\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.119 -%
   5.120 -\isadelimproof
   5.121 -%
   5.122 -\endisadelimproof
   5.123 -%
   5.124 -\isatagproof
   5.125 -\isacommand{proof}\isamarkupfalse%
   5.126 -\ {\isacharminus}\isanewline
   5.127 -\ \ \isacommand{have}\isamarkupfalse%
   5.128 -\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.129 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.130 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
   5.131 -\ \ \isacommand{also}\isamarkupfalse%
   5.132 -\ \isacommand{have}\isamarkupfalse%
   5.133 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
   5.134 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.135 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.136 -\ \ \isacommand{also}\isamarkupfalse%
   5.137 -\ \isacommand{have}\isamarkupfalse%
   5.138 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
   5.139 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.140 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
   5.141 -\ \ \isacommand{also}\isamarkupfalse%
   5.142 -\ \isacommand{have}\isamarkupfalse%
   5.143 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
   5.144 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.145 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.146 -\ \ \isacommand{also}\isamarkupfalse%
   5.147 -\ \isacommand{have}\isamarkupfalse%
   5.148 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
   5.149 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.150 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
   5.151 -\ \ \isacommand{also}\isamarkupfalse%
   5.152 -\ \isacommand{have}\isamarkupfalse%
   5.153 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.154 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.155 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.156 -\ \ \isacommand{also}\isamarkupfalse%
   5.157 -\ \isacommand{have}\isamarkupfalse%
   5.158 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
   5.159 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.160 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
   5.161 -\ \ \isacommand{also}\isamarkupfalse%
   5.162 -\ \isacommand{have}\isamarkupfalse%
   5.163 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
   5.164 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.165 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
   5.166 -\ \ \isacommand{finally}\isamarkupfalse%
   5.167 -\ \isacommand{show}\isamarkupfalse%
   5.168 -\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
   5.169 -\isanewline
   5.170 -\isacommand{qed}\isamarkupfalse%
   5.171 -%
   5.172 -\endisatagproof
   5.173 -{\isafoldproof}%
   5.174 -%
   5.175 -\isadelimproof
   5.176 -%
   5.177 -\endisadelimproof
   5.178 -%
   5.179 -\begin{isamarkuptext}%
   5.180 -\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
   5.181 -  much easier.%
   5.182 -\end{isamarkuptext}%
   5.183 -\isamarkuptrue%
   5.184 -\isacommand{theorem}\isamarkupfalse%
   5.185 -\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.186 -%
   5.187 -\isadelimproof
   5.188 -%
   5.189 -\endisadelimproof
   5.190 -%
   5.191 -\isatagproof
   5.192 -\isacommand{proof}\isamarkupfalse%
   5.193 -\ {\isacharminus}\isanewline
   5.194 -\ \ \isacommand{have}\isamarkupfalse%
   5.195 -\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.196 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.197 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
   5.198 -\ \ \isacommand{also}\isamarkupfalse%
   5.199 -\ \isacommand{have}\isamarkupfalse%
   5.200 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
   5.201 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.202 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.203 -\ \ \isacommand{also}\isamarkupfalse%
   5.204 -\ \isacommand{have}\isamarkupfalse%
   5.205 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
   5.206 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.207 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
   5.208 -\ \ \isacommand{also}\isamarkupfalse%
   5.209 -\ \isacommand{have}\isamarkupfalse%
   5.210 -\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
   5.211 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.212 -\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
   5.213 -\ \ \isacommand{finally}\isamarkupfalse%
   5.214 -\ \isacommand{show}\isamarkupfalse%
   5.215 -\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
   5.216 -\isanewline
   5.217 -\isacommand{qed}\isamarkupfalse%
   5.218 -%
   5.219 -\endisatagproof
   5.220 -{\isafoldproof}%
   5.221 -%
   5.222 -\isadelimproof
   5.223 -%
   5.224 -\endisadelimproof
   5.225 -%
   5.226 -\begin{isamarkuptext}%
   5.227 -\medskip Abstract theorems may be instantiated to only those types
   5.228 -  \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
   5.229 -  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}.%
   5.230 -\end{isamarkuptext}%
   5.231 -\isamarkuptrue%
   5.232 -%
   5.233 -\isamarkupsubsection{Abstract instantiation%
   5.234 -}
   5.235 -\isamarkuptrue%
   5.236 -%
   5.237 -\begin{isamarkuptext}%
   5.238 -From the definition, the \isa{monoid} and \isa{group} classes
   5.239 -  have been independent.  Note that for monoids, \isa{right{\isacharunderscore}unit}
   5.240 -  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
   5.241 -  axioms.  With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group
   5.242 -  theory (see page~\pageref{thm:group-right-unit}), we may now
   5.243 -  instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}).
   5.244 -
   5.245 - \begin{figure}[htbp]
   5.246 -   \begin{center}
   5.247 -     \small
   5.248 -     \unitlength 0.6mm
   5.249 -     \begin{picture}(65,90)(0,-10)
   5.250 -       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
   5.251 -       \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
   5.252 -       \put(15,5){\makebox(0,0){\isa{agroup}}}
   5.253 -       \put(15,25){\makebox(0,0){\isa{group}}}
   5.254 -       \put(15,45){\makebox(0,0){\isa{semigroup}}}
   5.255 -       \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
   5.256 -     \end{picture}
   5.257 -     \hspace{4em}
   5.258 -     \begin{picture}(30,90)(0,0)
   5.259 -       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
   5.260 -       \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
   5.261 -       \put(15,5){\makebox(0,0){\isa{agroup}}}
   5.262 -       \put(15,25){\makebox(0,0){\isa{group}}}
   5.263 -       \put(15,45){\makebox(0,0){\isa{monoid}}}
   5.264 -       \put(15,65){\makebox(0,0){\isa{semigroup}}}
   5.265 -       \put(15,85){\makebox(0,0){\isa{type}}}
   5.266 -     \end{picture}
   5.267 -     \caption{Monoids and groups: according to definition, and by proof}
   5.268 -     \label{fig:monoid-group}
   5.269 -   \end{center}
   5.270 - \end{figure}%
   5.271 -\end{isamarkuptext}%
   5.272 -\isamarkuptrue%
   5.273 -\isacommand{instance}\isamarkupfalse%
   5.274 -\ monoid\ {\isasymsubseteq}\ semigroup\isanewline
   5.275 -%
   5.276 -\isadelimproof
   5.277 -%
   5.278 -\endisadelimproof
   5.279 -%
   5.280 -\isatagproof
   5.281 -\isacommand{proof}\isamarkupfalse%
   5.282 -\isanewline
   5.283 -\ \ \isacommand{fix}\isamarkupfalse%
   5.284 -\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
   5.285 -\ \ \isacommand{show}\isamarkupfalse%
   5.286 -\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.287 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.288 -\ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.289 -\isacommand{qed}\isamarkupfalse%
   5.290 -%
   5.291 -\endisatagproof
   5.292 -{\isafoldproof}%
   5.293 -%
   5.294 -\isadelimproof
   5.295 -\isanewline
   5.296 -%
   5.297 -\endisadelimproof
   5.298 -\isanewline
   5.299 -\isacommand{instance}\isamarkupfalse%
   5.300 -\ group\ {\isasymsubseteq}\ monoid\isanewline
   5.301 -%
   5.302 -\isadelimproof
   5.303 -%
   5.304 -\endisadelimproof
   5.305 -%
   5.306 -\isatagproof
   5.307 -\isacommand{proof}\isamarkupfalse%
   5.308 -\isanewline
   5.309 -\ \ \isacommand{fix}\isamarkupfalse%
   5.310 -\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
   5.311 -\ \ \isacommand{show}\isamarkupfalse%
   5.312 -\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.313 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.314 -\ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.315 -\ \ \isacommand{show}\isamarkupfalse%
   5.316 -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
   5.317 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.318 -\ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
   5.319 -\ \ \isacommand{show}\isamarkupfalse%
   5.320 -\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
   5.321 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.322 -\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
   5.323 -\isacommand{qed}\isamarkupfalse%
   5.324 -%
   5.325 -\endisatagproof
   5.326 -{\isafoldproof}%
   5.327 -%
   5.328 -\isadelimproof
   5.329 -%
   5.330 -\endisadelimproof
   5.331 -%
   5.332 -\begin{isamarkuptext}%
   5.333 -\medskip The \isakeyword{instance} command sets up an appropriate
   5.334 -  goal that represents the class inclusion (or type arity, see
   5.335 -  \secref{sec:inst-arity}) to be proven (see also
   5.336 -  \cite{isabelle-isar-ref}).  The initial proof step causes
   5.337 -  back-chaining of class membership statements wrt.\ the hierarchy of
   5.338 -  any classes defined in the current theory; the effect is to reduce
   5.339 -  to the initial statement to a number of goals that directly
   5.340 -  correspond to any class axioms encountered on the path upwards
   5.341 -  through the class hierarchy.%
   5.342 -\end{isamarkuptext}%
   5.343 -\isamarkuptrue%
   5.344 -%
   5.345 -\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}%
   5.346 -}
   5.347 -\isamarkuptrue%
   5.348 -%
   5.349 -\begin{isamarkuptext}%
   5.350 -So far we have covered the case of the form
   5.351 -  \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely
   5.352 -  \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
   5.353 -  interesting for practical applications are \emph{concrete
   5.354 -  instantiations} of axiomatic type classes.  That is, certain simple
   5.355 -  schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class
   5.356 -  membership may be established at the logical level and then
   5.357 -  transferred to Isabelle's type signature level.
   5.358 -
   5.359 -  \medskip As a typical example, we show that type \isa{bool} with
   5.360 -  exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
   5.361 -  \isa{False} as \isa{{\isasymone}} forms an Abelian group.%
   5.362 -\end{isamarkuptext}%
   5.363 -\isamarkuptrue%
   5.364 -\isacommand{defs}\isamarkupfalse%
   5.365 -\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   5.366 -\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.367 -\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline
   5.368 -\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}%
   5.369 -\begin{isamarkuptext}%
   5.370 -\medskip It is important to note that above \isakeyword{defs} are
   5.371 -  just overloaded meta-level constant definitions, where type classes
   5.372 -  are not yet involved at all.  This form of constant definition with
   5.373 -  overloading (and optional recursion over the syntactic structure of
   5.374 -  simple types) are admissible as definitional extensions of plain HOL
   5.375 -  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
   5.376 -  required for overloading.  Nevertheless, overloaded definitions are
   5.377 -  best applied in the context of type classes.
   5.378 -
   5.379 -  \medskip Since we have chosen above \isakeyword{defs} of the generic
   5.380 -  group operations on type \isa{bool} appropriately, the class
   5.381 -  membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
   5.382 -\end{isamarkuptext}%
   5.383 -\isamarkuptrue%
   5.384 -\isacommand{instance}\isamarkupfalse%
   5.385 -\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
   5.386 -%
   5.387 -\isadelimproof
   5.388 -%
   5.389 -\endisadelimproof
   5.390 -%
   5.391 -\isatagproof
   5.392 -\isacommand{proof}\isamarkupfalse%
   5.393 -\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
   5.394 -\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
   5.395 -\ \ \isacommand{fix}\isamarkupfalse%
   5.396 -\ x\ y\ z\isanewline
   5.397 -\ \ \isacommand{show}\isamarkupfalse%
   5.398 -\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   5.399 -\ blast\isanewline
   5.400 -\ \ \isacommand{show}\isamarkupfalse%
   5.401 -\ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   5.402 -\ blast\isanewline
   5.403 -\ \ \isacommand{show}\isamarkupfalse%
   5.404 -\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   5.405 -\ blast\isanewline
   5.406 -\ \ \isacommand{show}\isamarkupfalse%
   5.407 -\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   5.408 -\ blast\isanewline
   5.409 -\isacommand{qed}\isamarkupfalse%
   5.410 -%
   5.411 -\endisatagproof
   5.412 -{\isafoldproof}%
   5.413 -%
   5.414 -\isadelimproof
   5.415 -%
   5.416 -\endisadelimproof
   5.417 -%
   5.418 -\begin{isamarkuptext}%
   5.419 -The result of an \isakeyword{instance} statement is both expressed
   5.420 -  as a theorem of Isabelle's meta-logic, and as a type arity of the
   5.421 -  type signature.  The latter enables type-inference system to take
   5.422 -  care of this new instance automatically.
   5.423 -
   5.424 -  \medskip We could now also instantiate our group theory classes to
   5.425 -  many other concrete types.  For example, \isa{int\ {\isasymColon}\ agroup}
   5.426 -  (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
   5.427 -  and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
   5.428 -  (e.g.\ if \isa{{\isasymodot}} is defined as list append).  Thus, the
   5.429 -  characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}}
   5.430 -  really become overloaded, i.e.\ have different meanings on different
   5.431 -  types.%
   5.432 -\end{isamarkuptext}%
   5.433 -\isamarkuptrue%
   5.434 -%
   5.435 -\isamarkupsubsection{Lifting and Functors%
   5.436 -}
   5.437 -\isamarkuptrue%
   5.438 -%
   5.439 -\begin{isamarkuptext}%
   5.440 -As already mentioned above, overloading in the simply-typed HOL
   5.441 -  systems may include recursion over the syntactic structure of types.
   5.442 -  That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
   5.443 -  contain constants of name \isa{c} on the right-hand side --- if
   5.444 -  these have types that are structurally simpler than \isa{{\isasymtau}}.
   5.445 -
   5.446 -  This feature enables us to \emph{lift operations}, say to Cartesian
   5.447 -  products, direct sums or function spaces.  Subsequently we lift
   5.448 -  \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
   5.449 -\end{isamarkuptext}%
   5.450 -\isamarkuptrue%
   5.451 -\isacommand{defs}\isamarkupfalse%
   5.452 -\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
   5.453 -\ \ 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}%
   5.454 -\begin{isamarkuptext}%
   5.455 -It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
   5.456 -  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
   5.457 -  to semigroups.  This may be established formally as follows.%
   5.458 -\end{isamarkuptext}%
   5.459 -\isamarkuptrue%
   5.460 -\isacommand{instance}\isamarkupfalse%
   5.461 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   5.462 -%
   5.463 -\isadelimproof
   5.464 -%
   5.465 -\endisadelimproof
   5.466 -%
   5.467 -\isatagproof
   5.468 -\isacommand{proof}\isamarkupfalse%
   5.469 -\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
   5.470 -\ \ \isacommand{fix}\isamarkupfalse%
   5.471 -\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
   5.472 -\ \ \isacommand{show}\isamarkupfalse%
   5.473 -\isanewline
   5.474 -\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline
   5.475 -\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
   5.476 -\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
   5.477 -\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   5.478 -\ \ \ \ \isacommand{by}\isamarkupfalse%
   5.479 -\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
   5.480 -\isacommand{qed}\isamarkupfalse%
   5.481 -%
   5.482 -\endisatagproof
   5.483 -{\isafoldproof}%
   5.484 -%
   5.485 -\isadelimproof
   5.486 -%
   5.487 -\endisadelimproof
   5.488 -%
   5.489 -\begin{isamarkuptext}%
   5.490 -Thus, if we view class instances as ``structures'', then overloaded
   5.491 -  constant definitions with recursion over types indirectly provide
   5.492 -  some kind of ``functors'' --- i.e.\ mappings between abstract
   5.493 -  theories.%
   5.494 -\end{isamarkuptext}%
   5.495 -\isamarkuptrue%
   5.496 -%
   5.497 -\isadelimtheory
   5.498 -%
   5.499 -\endisadelimtheory
   5.500 -%
   5.501 -\isatagtheory
   5.502 -\isacommand{end}\isamarkupfalse%
   5.503 -%
   5.504 -\endisatagtheory
   5.505 -{\isafoldtheory}%
   5.506 -%
   5.507 -\isadelimtheory
   5.508 -%
   5.509 -\endisadelimtheory
   5.510 -\isanewline
   5.511 -\end{isabellebody}%
   5.512 -%%% Local Variables:
   5.513 -%%% mode: latex
   5.514 -%%% TeX-master: "root"
   5.515 -%%% End:
     6.1 --- a/doc-src/AxClass/Group/document/Product.tex	Sun Feb 15 21:26:25 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,133 +0,0 @@
     6.4 -%
     6.5 -\begin{isabellebody}%
     6.6 -\def\isabellecontext{Product}%
     6.7 -%
     6.8 -\isamarkupheader{Syntactic classes%
     6.9 -}
    6.10 -\isamarkuptrue%
    6.11 -%
    6.12 -\isadelimtheory
    6.13 -%
    6.14 -\endisadelimtheory
    6.15 -%
    6.16 -\isatagtheory
    6.17 -\isacommand{theory}\isamarkupfalse%
    6.18 -\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
    6.19 -\endisatagtheory
    6.20 -{\isafoldtheory}%
    6.21 -%
    6.22 -\isadelimtheory
    6.23 -%
    6.24 -\endisadelimtheory
    6.25 -%
    6.26 -\begin{isamarkuptext}%
    6.27 -\medskip\noindent There is still a feature of Isabelle's type system
    6.28 -  left that we have not yet discussed.  When declaring polymorphic
    6.29 -  constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
    6.30 -  may be constrained by type classes (or even general sorts) in an
    6.31 -  arbitrary way.  Note that by default, in Isabelle/HOL the
    6.32 -  declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
    6.33 -  for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
    6.34 -  universal class of HOL, this is not really a constraint at all.
    6.35 -
    6.36 - The \isa{product} class below provides a less degenerate example of
    6.37 - syntactic type classes.%
    6.38 -\end{isamarkuptext}%
    6.39 -\isamarkuptrue%
    6.40 -\isacommand{axclass}\isamarkupfalse%
    6.41 -\isanewline
    6.42 -\ \ product\ {\isasymsubseteq}\ type\isanewline
    6.43 -\isacommand{consts}\isamarkupfalse%
    6.44 -\isanewline
    6.45 -\ \ 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}%
    6.46 -\begin{isamarkuptext}%
    6.47 -Here class \isa{product} is defined as subclass of \isa{type}
    6.48 -  without any additional axioms.  This effects in logical equivalence
    6.49 -  of \isa{product} and \isa{type}, as is reflected by the trivial
    6.50 -  introduction rule generated for this definition.
    6.51 -
    6.52 -  \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
    6.53 -  from the logic's point of view.  It even makes the most sense to
    6.54 -  remove sort constraints from constant declarations, as far as the
    6.55 -  purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
    6.56 -
    6.57 -  On the other hand there are syntactic differences, of course.
    6.58 - Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
    6.59 - type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
    6.60 - type signature.  In our example, this arity may be always added when
    6.61 - required by means of an \isakeyword{instance} with the default proof
    6.62 - (double-dot).
    6.63 -
    6.64 -  \medskip Thus, we may observe the following discipline of using
    6.65 -  syntactic classes.  Overloaded polymorphic constants have their type
    6.66 -  arguments restricted to an associated (logically trivial) class
    6.67 -  \isa{c}.  Only immediately before \emph{specifying} these
    6.68 -  constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
    6.69 -
    6.70 -  This is done for class \isa{product} and type \isa{bool} as
    6.71 -  follows.%
    6.72 -\end{isamarkuptext}%
    6.73 -\isamarkuptrue%
    6.74 -\isacommand{instance}\isamarkupfalse%
    6.75 -\ bool\ {\isacharcolon}{\isacharcolon}\ product%
    6.76 -\isadelimproof
    6.77 -\ %
    6.78 -\endisadelimproof
    6.79 -%
    6.80 -\isatagproof
    6.81 -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
    6.82 -%
    6.83 -\endisatagproof
    6.84 -{\isafoldproof}%
    6.85 -%
    6.86 -\isadelimproof
    6.87 -%
    6.88 -\endisadelimproof
    6.89 -\isanewline
    6.90 -\isacommand{defs}\isamarkupfalse%
    6.91 -\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
    6.92 -\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}%
    6.93 -\begin{isamarkuptext}%
    6.94 -The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
    6.95 - well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
    6.96 - known to the type checker.
    6.97 -
    6.98 - \medskip It is very important to see that above \isakeyword{defs} are
    6.99 - not directly connected with \isakeyword{instance} at all!  We were
   6.100 - just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
   6.101 - after having instantiated \isa{bool\ {\isasymColon}\ product}.  Isabelle does
   6.102 - not require these definitions, which is in contrast to programming
   6.103 - languages like Haskell \cite{haskell-report}.
   6.104 -
   6.105 - \medskip While Isabelle type classes and those of Haskell are almost
   6.106 - the same as far as type-checking and type inference are concerned,
   6.107 - there are important semantic differences.  Haskell classes require
   6.108 - their instances to \emph{provide operations} of certain \emph{names}.
   6.109 - Therefore, its \texttt{instance} has a \texttt{where} part that tells
   6.110 - the system what these ``member functions'' should be.
   6.111 -
   6.112 - This style of \texttt{instance} would not make much sense in
   6.113 - Isabelle's meta-logic, because there is no internal notion of
   6.114 - ``providing operations'' or even ``names of functions''.%
   6.115 -\end{isamarkuptext}%
   6.116 -\isamarkuptrue%
   6.117 -%
   6.118 -\isadelimtheory
   6.119 -%
   6.120 -\endisadelimtheory
   6.121 -%
   6.122 -\isatagtheory
   6.123 -\isacommand{end}\isamarkupfalse%
   6.124 -%
   6.125 -\endisatagtheory
   6.126 -{\isafoldtheory}%
   6.127 -%
   6.128 -\isadelimtheory
   6.129 -%
   6.130 -\endisadelimtheory
   6.131 -\isanewline
   6.132 -\end{isabellebody}%
   6.133 -%%% Local Variables:
   6.134 -%%% mode: latex
   6.135 -%%% TeX-master: "root"
   6.136 -%%% End:
     7.1 --- a/doc-src/AxClass/Group/document/Semigroups.tex	Sun Feb 15 21:26:25 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,88 +0,0 @@
     7.4 -%
     7.5 -\begin{isabellebody}%
     7.6 -\def\isabellecontext{Semigroups}%
     7.7 -%
     7.8 -\isamarkupheader{Semigroups%
     7.9 -}
    7.10 -\isamarkuptrue%
    7.11 -%
    7.12 -\isadelimtheory
    7.13 -%
    7.14 -\endisadelimtheory
    7.15 -%
    7.16 -\isatagtheory
    7.17 -\isacommand{theory}\isamarkupfalse%
    7.18 -\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
    7.19 -\endisatagtheory
    7.20 -{\isafoldtheory}%
    7.21 -%
    7.22 -\isadelimtheory
    7.23 -%
    7.24 -\endisadelimtheory
    7.25 -%
    7.26 -\begin{isamarkuptext}%
    7.27 -\medskip\noindent An axiomatic type class is simply a class of types
    7.28 -  that all meet certain properties, which are also called \emph{class
    7.29 -  axioms}. Thus, type classes may be also understood as type
    7.30 -  predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}.  Class axioms typically contain polymorphic constants that
    7.31 -  depend on this type \isa{{\isacharprime}a}.  These \emph{characteristic
    7.32 -  constants} behave like operations associated with the ``carrier''
    7.33 -  type \isa{{\isacharprime}a}.
    7.34 -
    7.35 -  We illustrate these basic concepts by the following formulation of
    7.36 -  semigroups.%
    7.37 -\end{isamarkuptext}%
    7.38 -\isamarkuptrue%
    7.39 -\isacommand{consts}\isamarkupfalse%
    7.40 -\isanewline
    7.41 -\ \ 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
    7.42 -\isacommand{axclass}\isamarkupfalse%
    7.43 -\ semigroup\ {\isasymsubseteq}\ type\isanewline
    7.44 -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}%
    7.45 -\begin{isamarkuptext}%
    7.46 -\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
    7.47 -  all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
    7.48 -  associative operator.  The \isa{assoc} axiom contains exactly one
    7.49 -  type variable, which is invisible in the above presentation, though.
    7.50 -  Also note that free term variables (like \isa{x}, \isa{y},
    7.51 -  \isa{z}) are allowed for user convenience --- conceptually all of
    7.52 -  these are bound by outermost universal quantifiers.
    7.53 -
    7.54 -  \medskip In general, type classes may be used to describe
    7.55 -  \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
    7.56 -  \emph{signature}.  Different signatures require different classes.
    7.57 -  Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
    7.58 -  correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
    7.59 -\end{isamarkuptext}%
    7.60 -\isamarkuptrue%
    7.61 -\isacommand{consts}\isamarkupfalse%
    7.62 -\isanewline
    7.63 -\ \ 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
    7.64 -\isacommand{axclass}\isamarkupfalse%
    7.65 -\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
    7.66 -\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
    7.67 -\begin{isamarkuptext}%
    7.68 -\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
    7.69 -  not quite the same.%
    7.70 -\end{isamarkuptext}%
    7.71 -\isamarkuptrue%
    7.72 -%
    7.73 -\isadelimtheory
    7.74 -%
    7.75 -\endisadelimtheory
    7.76 -%
    7.77 -\isatagtheory
    7.78 -\isacommand{end}\isamarkupfalse%
    7.79 -%
    7.80 -\endisatagtheory
    7.81 -{\isafoldtheory}%
    7.82 -%
    7.83 -\isadelimtheory
    7.84 -%
    7.85 -\endisadelimtheory
    7.86 -\isanewline
    7.87 -\end{isabellebody}%
    7.88 -%%% Local Variables:
    7.89 -%%% mode: latex
    7.90 -%%% TeX-master: "root"
    7.91 -%%% End:
     8.1 --- a/doc-src/AxClass/IsaMakefile	Sun Feb 15 21:26:25 2009 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,47 +0,0 @@
     8.4 -
     8.5 -## targets
     8.6 -
     8.7 -default: Group Nat
     8.8 -images: 
     8.9 -test: Group Nat
    8.10 -
    8.11 -all: images test
    8.12 -
    8.13 -
    8.14 -## global settings
    8.15 -
    8.16 -SRC = $(ISABELLE_HOME)/src
    8.17 -OUT = $(ISABELLE_OUTPUT)
    8.18 -LOG = $(OUT)/log
    8.19 -USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
    8.20 -
    8.21 -
    8.22 -## Group
    8.23 -
    8.24 -Group: HOL $(LOG)/HOL-Group.gz
    8.25 -
    8.26 -HOL:
    8.27 -	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
    8.28 -
    8.29 -$(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/Group.thy \
    8.30 -  Group/Product.thy Group/Semigroups.thy
    8.31 -	@$(USEDIR) $(OUT)/HOL Group
    8.32 -	@rm -f Group/document/pdfsetup.sty Group/document/session.tex
    8.33 -
    8.34 -
    8.35 -## Nat
    8.36 -
    8.37 -Nat: FOL $(LOG)/FOL-Nat.gz
    8.38 -
    8.39 -FOL:
    8.40 -	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
    8.41 -
    8.42 -$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
    8.43 -	@$(USEDIR) $(OUT)/FOL Nat
    8.44 -	@rm -f Nat/document/*.sty Nat/document/session.tex
    8.45 -
    8.46 -
    8.47 -## clean
    8.48 -
    8.49 -clean:
    8.50 -	@rm -f $(LOG)/HOL-Group.gz $(LOG)/FOL-Nat.gz
     9.1 --- a/doc-src/AxClass/Makefile	Sun Feb 15 21:26:25 2009 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,36 +0,0 @@
     9.4 -#
     9.5 -# $Id$
     9.6 -#
     9.7 -
     9.8 -## targets
     9.9 -
    9.10 -default: dvi
    9.11 -
    9.12 -
    9.13 -## dependencies
    9.14 -
    9.15 -include ../Makefile.in
    9.16 -
    9.17 -NAME = axclass
    9.18 -
    9.19 -FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty	\
    9.20 -  ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty			\
    9.21 -  Group/document/Group.tex Nat/document/NatClass.tex			\
    9.22 -  Group/document/Product.tex Group/document/Semigroups.tex
    9.23 -
    9.24 -dvi: $(NAME).dvi
    9.25 -
    9.26 -$(NAME).dvi: $(FILES) isabelle_isar.eps
    9.27 -	$(LATEX) $(NAME)
    9.28 -	$(BIBTEX) $(NAME)
    9.29 -	$(LATEX) $(NAME)
    9.30 -	$(LATEX) $(NAME)
    9.31 -
    9.32 -pdf: $(NAME).pdf
    9.33 -
    9.34 -$(NAME).pdf: $(FILES) isabelle_isar.pdf
    9.35 -	$(PDFLATEX) $(NAME)
    9.36 -	$(FIXBOOKMARKS) $(NAME).out
    9.37 -	$(BIBTEX) $(NAME)
    9.38 -	$(PDFLATEX) $(NAME)
    9.39 -	$(PDFLATEX) $(NAME)
    10.1 --- a/doc-src/AxClass/Nat/NatClass.thy	Sun Feb 15 21:26:25 2009 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,117 +0,0 @@
    10.4 -
    10.5 -header {* Defining natural numbers in FOL \label{sec:ex-natclass} *}
    10.6 -
    10.7 -theory NatClass imports FOL begin
    10.8 -
    10.9 -text {*
   10.10 - \medskip\noindent Axiomatic type classes abstract over exactly one
   10.11 - type argument. Thus, any \emph{axiomatic} theory extension where each
   10.12 - axiom refers to at most one type variable, may be trivially turned
   10.13 - into a \emph{definitional} one.
   10.14 -
   10.15 - We illustrate this with the natural numbers in
   10.16 - Isabelle/FOL.\footnote{See also
   10.17 - \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}
   10.18 -*}
   10.19 -
   10.20 -consts
   10.21 -  zero :: 'a    ("\<zero>")
   10.22 -  Suc :: "'a \<Rightarrow> 'a"
   10.23 -  rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
   10.24 -
   10.25 -axclass nat \<subseteq> "term"
   10.26 -  induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
   10.27 -  Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
   10.28 -  Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
   10.29 -  rec_0: "rec(\<zero>, a, f) = a"
   10.30 -  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
   10.31 -
   10.32 -constdefs
   10.33 -  add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "+" 60)
   10.34 -  "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))"
   10.35 -
   10.36 -text {*
   10.37 - This is an abstract version of the plain @{text Nat} theory in
   10.38 - FOL.\footnote{See
   10.39 - \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
   10.40 - we have just replaced all occurrences of type @{text nat} by @{typ
   10.41 - 'a} and used the natural number axioms to define class @{text nat}.
   10.42 - There is only a minor snag, that the original recursion operator
   10.43 - @{term rec} had to be made monomorphic.
   10.44 -
   10.45 - Thus class @{text nat} contains exactly those types @{text \<tau>} that
   10.46 - are isomorphic to ``the'' natural numbers (with signature @{term
   10.47 - \<zero>}, @{term Suc}, @{term rec}).
   10.48 -
   10.49 - \medskip What we have done here can be also viewed as \emph{type
   10.50 - specification}.  Of course, it still remains open if there is some
   10.51 - type at all that meets the class axioms.  Now a very nice property of
   10.52 - axiomatic type classes is that abstract reasoning is always possible
   10.53 - --- independent of satisfiability.  The meta-logic won't break, even
   10.54 - if some classes (or general sorts) turns out to be empty later ---
   10.55 - ``inconsistent'' class definitions may be useless, but do not cause
   10.56 - any harm.
   10.57 -
   10.58 - Theorems of the abstract natural numbers may be derived in the same
   10.59 - way as for the concrete version.  The original proof scripts may be
   10.60 - re-used with some trivial changes only (mostly adding some type
   10.61 - constraints).
   10.62 -*}
   10.63 -
   10.64 -(*<*)
   10.65 -lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
   10.66 -apply (rule_tac n = k in induct)
   10.67 -apply (rule notI)
   10.68 -apply (erule Suc_neq_0)
   10.69 -apply (rule notI)
   10.70 -apply (erule notE)
   10.71 -apply (erule Suc_inject)
   10.72 -done
   10.73 -
   10.74 -lemma "(k+m)+n = k+(m+n)"
   10.75 -apply (rule induct)
   10.76 -back
   10.77 -back
   10.78 -back
   10.79 -back
   10.80 -back
   10.81 -back
   10.82 -oops
   10.83 -
   10.84 -lemma add_0 [simp]: "\<zero>+n = n"
   10.85 -apply (unfold add_def)
   10.86 -apply (rule rec_0)
   10.87 -done
   10.88 -
   10.89 -lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
   10.90 -apply (unfold add_def)
   10.91 -apply (rule rec_Suc)
   10.92 -done
   10.93 -
   10.94 -lemma add_assoc: "(k+m)+n = k+(m+n)"
   10.95 -apply (rule_tac n = k in induct)
   10.96 -apply simp
   10.97 -apply simp
   10.98 -done
   10.99 -
  10.100 -lemma add_0_right: "m+\<zero> = m"
  10.101 -apply (rule_tac n = m in induct)
  10.102 -apply simp
  10.103 -apply simp
  10.104 -done
  10.105 -
  10.106 -lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
  10.107 -apply (rule_tac n = m in induct)
  10.108 -apply simp_all
  10.109 -done
  10.110 -
  10.111 -lemma
  10.112 -  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
  10.113 -  shows "f(i+j) = i+f(j)"
  10.114 -apply (rule_tac n = i in induct)
  10.115 -apply simp
  10.116 -apply (simp add: prem)
  10.117 -done
  10.118 -(*>*)
  10.119 -
  10.120 -end
  10.121 \ No newline at end of file
    11.1 --- a/doc-src/AxClass/Nat/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,2 +0,0 @@
    11.4 -
    11.5 -use_thy "NatClass";
    12.1 --- a/doc-src/AxClass/Nat/document/NatClass.tex	Sun Feb 15 21:26:25 2009 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,201 +0,0 @@
    12.4 -%
    12.5 -\begin{isabellebody}%
    12.6 -\def\isabellecontext{NatClass}%
    12.7 -%
    12.8 -\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
    12.9 -}
   12.10 -\isamarkuptrue%
   12.11 -%
   12.12 -\isadelimtheory
   12.13 -%
   12.14 -\endisadelimtheory
   12.15 -%
   12.16 -\isatagtheory
   12.17 -\isacommand{theory}\isamarkupfalse%
   12.18 -\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}%
   12.19 -\endisatagtheory
   12.20 -{\isafoldtheory}%
   12.21 -%
   12.22 -\isadelimtheory
   12.23 -%
   12.24 -\endisadelimtheory
   12.25 -%
   12.26 -\begin{isamarkuptext}%
   12.27 -\medskip\noindent Axiomatic type classes abstract over exactly one
   12.28 - type argument. Thus, any \emph{axiomatic} theory extension where each
   12.29 - axiom refers to at most one type variable, may be trivially turned
   12.30 - into a \emph{definitional} one.
   12.31 -
   12.32 - We illustrate this with the natural numbers in
   12.33 - Isabelle/FOL.\footnote{See also
   12.34 - \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
   12.35 -\end{isamarkuptext}%
   12.36 -\isamarkuptrue%
   12.37 -\isacommand{consts}\isamarkupfalse%
   12.38 -\isanewline
   12.39 -\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   12.40 -\ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
   12.41 -\ \ 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
   12.42 -\isanewline
   12.43 -\isacommand{axclass}\isamarkupfalse%
   12.44 -\ nat\ {\isasymsubseteq}\ {\isachardoublequoteopen}term{\isachardoublequoteclose}\isanewline
   12.45 -\ \ 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
   12.46 -\ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   12.47 -\ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequoteclose}\isanewline
   12.48 -\ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
   12.49 -\ \ 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
   12.50 -\isanewline
   12.51 -\isacommand{constdefs}\isamarkupfalse%
   12.52 -\isanewline
   12.53 -\ \ 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
   12.54 -\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
   12.55 -\begin{isamarkuptext}%
   12.56 -This is an abstract version of the plain \isa{Nat} theory in
   12.57 - FOL.\footnote{See
   12.58 - \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
   12.59 - 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}.
   12.60 - There is only a minor snag, that the original recursion operator
   12.61 - \isa{rec} had to be made monomorphic.
   12.62 -
   12.63 - Thus class \isa{nat} contains exactly those types \isa{{\isasymtau}} that
   12.64 - are isomorphic to ``the'' natural numbers (with signature \isa{{\isasymzero}}, \isa{Suc}, \isa{rec}).
   12.65 -
   12.66 - \medskip What we have done here can be also viewed as \emph{type
   12.67 - specification}.  Of course, it still remains open if there is some
   12.68 - type at all that meets the class axioms.  Now a very nice property of
   12.69 - axiomatic type classes is that abstract reasoning is always possible
   12.70 - --- independent of satisfiability.  The meta-logic won't break, even
   12.71 - if some classes (or general sorts) turns out to be empty later ---
   12.72 - ``inconsistent'' class definitions may be useless, but do not cause
   12.73 - any harm.
   12.74 -
   12.75 - Theorems of the abstract natural numbers may be derived in the same
   12.76 - way as for the concrete version.  The original proof scripts may be
   12.77 - re-used with some trivial changes only (mostly adding some type
   12.78 - constraints).%
   12.79 -\end{isamarkuptext}%
   12.80 -\isamarkuptrue%
   12.81 -%
   12.82 -\isadelimproof
   12.83 -%
   12.84 -\endisadelimproof
   12.85 -%
   12.86 -\isatagproof
   12.87 -%
   12.88 -\endisatagproof
   12.89 -{\isafoldproof}%
   12.90 -%
   12.91 -\isadelimproof
   12.92 -%
   12.93 -\endisadelimproof
   12.94 -%
   12.95 -\isadelimproof
   12.96 -%
   12.97 -\endisadelimproof
   12.98 -%
   12.99 -\isatagproof
  12.100 -%
  12.101 -\endisatagproof
  12.102 -{\isafoldproof}%
  12.103 -%
  12.104 -\isadelimproof
  12.105 -%
  12.106 -\endisadelimproof
  12.107 -%
  12.108 -\isadelimproof
  12.109 -%
  12.110 -\endisadelimproof
  12.111 -%
  12.112 -\isatagproof
  12.113 -%
  12.114 -\endisatagproof
  12.115 -{\isafoldproof}%
  12.116 -%
  12.117 -\isadelimproof
  12.118 -%
  12.119 -\endisadelimproof
  12.120 -%
  12.121 -\isadelimproof
  12.122 -%
  12.123 -\endisadelimproof
  12.124 -%
  12.125 -\isatagproof
  12.126 -%
  12.127 -\endisatagproof
  12.128 -{\isafoldproof}%
  12.129 -%
  12.130 -\isadelimproof
  12.131 -%
  12.132 -\endisadelimproof
  12.133 -%
  12.134 -\isadelimproof
  12.135 -%
  12.136 -\endisadelimproof
  12.137 -%
  12.138 -\isatagproof
  12.139 -%
  12.140 -\endisatagproof
  12.141 -{\isafoldproof}%
  12.142 -%
  12.143 -\isadelimproof
  12.144 -%
  12.145 -\endisadelimproof
  12.146 -%
  12.147 -\isadelimproof
  12.148 -%
  12.149 -\endisadelimproof
  12.150 -%
  12.151 -\isatagproof
  12.152 -%
  12.153 -\endisatagproof
  12.154 -{\isafoldproof}%
  12.155 -%
  12.156 -\isadelimproof
  12.157 -%
  12.158 -\endisadelimproof
  12.159 -%
  12.160 -\isadelimproof
  12.161 -%
  12.162 -\endisadelimproof
  12.163 -%
  12.164 -\isatagproof
  12.165 -%
  12.166 -\endisatagproof
  12.167 -{\isafoldproof}%
  12.168 -%
  12.169 -\isadelimproof
  12.170 -%
  12.171 -\endisadelimproof
  12.172 -%
  12.173 -\isadelimproof
  12.174 -%
  12.175 -\endisadelimproof
  12.176 -%
  12.177 -\isatagproof
  12.178 -%
  12.179 -\endisatagproof
  12.180 -{\isafoldproof}%
  12.181 -%
  12.182 -\isadelimproof
  12.183 -\isanewline
  12.184 -%
  12.185 -\endisadelimproof
  12.186 -%
  12.187 -\isadelimtheory
  12.188 -%
  12.189 -\endisadelimtheory
  12.190 -%
  12.191 -\isatagtheory
  12.192 -\isacommand{end}\isamarkupfalse%
  12.193 -%
  12.194 -\endisatagtheory
  12.195 -{\isafoldtheory}%
  12.196 -%
  12.197 -\isadelimtheory
  12.198 -%
  12.199 -\endisadelimtheory
  12.200 -\end{isabellebody}%
  12.201 -%%% Local Variables:
  12.202 -%%% mode: latex
  12.203 -%%% TeX-master: "root"
  12.204 -%%% End:
    13.1 --- a/doc-src/AxClass/axclass.tex	Sun Feb 15 21:26:25 2009 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,80 +0,0 @@
    13.4 -
    13.5 -\documentclass[12pt,a4paper,fleqn]{report}
    13.6 -\usepackage{graphicx,../iman,../extra,../isar}
    13.7 -\usepackage{../isabelle,../isabellesym}
    13.8 -\usepackage{../pdfsetup}  % last one!
    13.9 -
   13.10 -\isabellestyle{it}
   13.11 -\newcommand{\isasyminv}{\isamath{{}^{-1}}}
   13.12 -\renewcommand{\isasymzero}{\isamath{0}}
   13.13 -\renewcommand{\isasymone}{\isamath{1}}
   13.14 -
   13.15 -\newcommand{\secref}[1]{\S\ref{#1}}
   13.16 -\newcommand{\figref}[1]{figure~\ref{#1}}
   13.17 -
   13.18 -\hyphenation{Isabelle}
   13.19 -\hyphenation{Isar}
   13.20 -\hyphenation{Haskell}
   13.21 -
   13.22 -\title{\includegraphics[scale=0.5]{isabelle_isar}
   13.23 -  \\[4ex] Using Axiomatic Type Classes in Isabelle}
   13.24 -\author{\emph{Markus Wenzel} \\ TU M\"unchen}
   13.25 -
   13.26 -
   13.27 -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
   13.28 -
   13.29 -\pagestyle{headings}
   13.30 -\sloppy
   13.31 -\binperiod     %%%treat . like a binary operator
   13.32 -
   13.33 -
   13.34 -\begin{document}
   13.35 -
   13.36 -\underscoreoff
   13.37 -
   13.38 -\maketitle 
   13.39 -
   13.40 -\begin{abstract}
   13.41 -  Isabelle offers order-sorted type classes on top of the simple types of
   13.42 -  plain Higher-Order Logic.  The resulting type system is similar to that of
   13.43 -  the programming language Haskell.  Its interpretation within the logic
   13.44 -  enables further application, though, apart from restricting polymorphism
   13.45 -  syntactically.  In particular, the concept of \emph{Axiomatic Type Classes}
   13.46 -  provides a useful light-weight mechanism for hierarchically-structured
   13.47 -  abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
   13.48 -  axiomatic type classes to model basic algebraic structures.
   13.49 -  
   13.50 -  This document describes axiomatic type classes using Isabelle/Isar theories,
   13.51 -  with proofs expressed via Isar proof language elements.  The new theory
   13.52 -  format greatly simplifies the arrangement of the overall development, since
   13.53 -  definitions and proofs may be freely intermixed.  Users who prefer tactic
   13.54 -  scripts over structured proofs do not need to fall back on separate ML
   13.55 -  scripts, though, but may refer to Isar's tactic emulation commands.
   13.56 -\end{abstract}
   13.57 -
   13.58 -
   13.59 -\pagenumbering{roman} \tableofcontents \clearfirst
   13.60 -
   13.61 -\include{body}
   13.62 -
   13.63 -%FIXME
   13.64 -\nocite{nipkow-types93}
   13.65 -\nocite{nipkow-sorts93}
   13.66 -\nocite{Wenzel:1997:TPHOL}
   13.67 -\nocite{paulson-isa-book}
   13.68 -\nocite{isabelle-isar-ref}
   13.69 -\nocite{Wenzel:1999:TPHOL}
   13.70 -
   13.71 -\begingroup
   13.72 -  \bibliographystyle{plain} \small\raggedright\frenchspacing
   13.73 -  \bibliography{../manual}
   13.74 -\endgroup
   13.75 -
   13.76 -\end{document}
   13.77 -
   13.78 -
   13.79 -%%% Local Variables: 
   13.80 -%%% mode: latex
   13.81 -%%% TeX-master: t
   13.82 -%%% End: 
   13.83 -% LocalWords:  Isabelle FIXME
    14.1 --- a/doc-src/AxClass/body.tex	Sun Feb 15 21:26:25 2009 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,166 +0,0 @@
    14.4 -
    14.5 -\chapter{Introduction}
    14.6 -
    14.7 -A Haskell-style type-system \cite{haskell-report} with ordered type-classes
    14.8 -has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
    14.9 -Initially, classes have mainly served as a \emph{purely syntactic} tool to
   14.10 -formulate polymorphic object-logics in a clean way, such as the standard
   14.11 -Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
   14.12 -
   14.13 -Applying classes at the \emph{logical level} to provide a simple notion of
   14.14 -abstract theories and instantiations to concrete ones, has been long proposed
   14.15 -as well \cite{nipkow-types93,nipkow-sorts93}.  At that time, Isabelle still
   14.16 -lacked built-in support for these \emph{axiomatic type classes}. More
   14.17 -importantly, their semantics was not yet fully fleshed out (and unnecessarily
   14.18 -complicated, too).
   14.19 -
   14.20 -Since Isabelle94, actual axiomatic type classes have been an integral part of
   14.21 -Isabelle's meta-logic.  This very simple implementation is based on a
   14.22 -straight-forward extension of traditional simply-typed Higher-Order Logic, by
   14.23 -including types qualified by logical predicates and overloaded constant
   14.24 -definitions (see \cite{Wenzel:1997:TPHOL} for further details).
   14.25 -
   14.26 -Yet even until Isabelle99, there used to be still a fundamental methodological
   14.27 -problem in using axiomatic type classes conveniently, due to the traditional
   14.28 -distinction of Isabelle theory files vs.\ ML proof scripts.  This has been
   14.29 -finally overcome with the advent of Isabelle/Isar theories
   14.30 -\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
   14.31 -This nicely accommodates the usual procedure of defining axiomatic type
   14.32 -classes, proving abstract properties, defining operations on concrete types,
   14.33 -proving concrete properties for instantiation of classes etc.
   14.34 -
   14.35 -\medskip
   14.36 -
   14.37 -So to cut a long story short, the present version of axiomatic type classes
   14.38 -now provides an even more useful and convenient mechanism for light-weight
   14.39 -abstract theories, without any special technical provisions to be observed by
   14.40 -the user.
   14.41 -
   14.42 -
   14.43 -\chapter{Examples}\label{sec:ex}
   14.44 -
   14.45 -Axiomatic type classes are a concept of Isabelle's meta-logic
   14.46 -\cite{paulson-isa-book,Wenzel:1997:TPHOL}.  They may be applied to any
   14.47 -object-logic that directly uses the meta type system, such as Isabelle/HOL
   14.48 -\cite{isabelle-HOL}.  Subsequently, we present various examples that are all
   14.49 -formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
   14.50 -FOL.  See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
   14.51 -\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
   14.52 -
   14.53 -\input{Group/document/Semigroups}
   14.54 -
   14.55 -\input{Group/document/Group}
   14.56 -
   14.57 -\input{Group/document/Product}
   14.58 -
   14.59 -\input{Nat/document/NatClass}
   14.60 -
   14.61 -
   14.62 -%% FIXME move some parts to ref or isar-ref manual (!?);
   14.63 -
   14.64 -% \chapter{The user interface of Isabelle's axclass package}
   14.65 -
   14.66 -% The actual axiomatic type class package of Isabelle/Pure mainly consists
   14.67 -% of two new theory sections: \texttt{axclass} and \texttt{instance}.  Some
   14.68 -% typical applications of these have already been demonstrated in
   14.69 -% \secref{sec:ex}, below their syntax and semantics are presented more
   14.70 -% completely.
   14.71 -
   14.72 -
   14.73 -% \section{The axclass section}
   14.74 -
   14.75 -% Within theory files, \texttt{axclass} introduces an axiomatic type class
   14.76 -% definition. Its concrete syntax is:
   14.77 -
   14.78 -% \begin{matharray}{l}
   14.79 -%   \texttt{axclass} \\
   14.80 -%   \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
   14.81 -%   \ \ id@1\ axm@1 \\
   14.82 -%   \ \ \vdots \\
   14.83 -%   \ \ id@m\ axm@m
   14.84 -% \emphnd{matharray}
   14.85 -
   14.86 -% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
   14.87 -% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
   14.88 -% 0$) are formulas (category $string$).
   14.89 -
   14.90 -% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
   14.91 -% \texttt{logic}. Each class axiom $axm@j$ may contain any term
   14.92 -% variables, but at most one type variable (which need not be the same
   14.93 -% for all axioms). The sort of this type variable has to be a supersort
   14.94 -% of $\{c@1, \ldots, c@n\}$.
   14.95 -
   14.96 -% \medskip
   14.97 -
   14.98 -% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
   14.99 -% c@n$ to the type signature.
  14.100 -
  14.101 -% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
  14.102 -% ``abstract axioms'' of $c$ with names $id@1, \ldots,
  14.103 -% id@m$.  This is done by replacing all occurring type variables
  14.104 -% by $\alpha :: c$. Original axioms that do not contain any type
  14.105 -% variable will be prefixed by the logical precondition
  14.106 -% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
  14.107 -
  14.108 -% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
  14.109 -% rule'' --- is built from the respective universal closures of
  14.110 -% $axm@1, \ldots, axm@m$ appropriately.
  14.111 -
  14.112 -
  14.113 -% \section{The instance section}
  14.114 -
  14.115 -% Section \texttt{instance} proves class inclusions or type arities at the
  14.116 -% logical level and then transfers these into the type signature.
  14.117 -
  14.118 -% Its concrete syntax is:
  14.119 -
  14.120 -% \begin{matharray}{l}
  14.121 -%   \texttt{instance} \\
  14.122 -%   \ \ [\ c@1 \texttt{ < } c@2 \ |\
  14.123 -%       t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
  14.124 -%   \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
  14.125 -%   \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
  14.126 -% \emphnd{matharray}
  14.127 -
  14.128 -% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
  14.129 -% (all of category $id$ or $string)$. Furthermore,
  14.130 -% $sort@i$ are sorts in the usual Isabelle-syntax.
  14.131 -
  14.132 -% \medskip
  14.133 -
  14.134 -% Internally, \texttt{instance} first sets up an appropriate goal that
  14.135 -% expresses the class inclusion or type arity as a meta-proposition.
  14.136 -% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
  14.137 -% meta-definitions of the current theory file and the user-supplied
  14.138 -% witnesses. The latter are $name@1, \ldots, name@m$, where
  14.139 -% $id$ refers to an \ML-name of a theorem, and $string$ to an
  14.140 -% axiom of the current theory node\footnote{Thus, the user may reference
  14.141 -%   axioms from above this \texttt{instance} in the theory file. Note
  14.142 -%   that new axioms appear at the \ML-toplevel only after the file is
  14.143 -%   processed completely.}.
  14.144 -
  14.145 -% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
  14.146 -% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
  14.147 -% according to their form: Meta-definitions are unfolded, all other
  14.148 -% formulas are repeatedly resolved\footnote{This is done in a way that
  14.149 -%   enables proper object-\emph{rules} to be used as witnesses for
  14.150 -%   corresponding class axioms.} with.
  14.151 -
  14.152 -% The final optional argument $text$ is \ML-code of an arbitrary
  14.153 -% user tactic which is applied last to any remaining goals.
  14.154 -
  14.155 -% \medskip
  14.156 -
  14.157 -% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
  14.158 -% new users of the axclass package are advised to only use the simple
  14.159 -% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
  14.160 -% the identifiers refer to theorems that are appropriate type instances
  14.161 -% of the class axioms. This typically requires an auxiliary theory,
  14.162 -% though, which defines some constants and then proves these witnesses.
  14.163 -
  14.164 -
  14.165 -%%% Local Variables: 
  14.166 -%%% mode: latex
  14.167 -%%% TeX-master: "axclass"
  14.168 -%%% End: 
  14.169 -% LocalWords:  Isabelle FOL
    15.1 --- a/src/HOL/AxClasses/Group.thy	Sun Feb 15 21:26:25 2009 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,124 +0,0 @@
    15.4 -(*  Title:      HOL/AxClasses/Group.thy
    15.5 -    ID:         $Id$
    15.6 -    Author:     Markus Wenzel, TU Muenchen
    15.7 -*)
    15.8 -
    15.9 -theory Group imports Main begin
   15.10 -
   15.11 -subsection {* Monoids and Groups *}
   15.12 -
   15.13 -consts
   15.14 -  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
   15.15 -  invers :: "'a => 'a"
   15.16 -  one :: 'a
   15.17 -
   15.18 -
   15.19 -axclass monoid < type
   15.20 -  assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
   15.21 -  left_unit:  "one [*] x = x"
   15.22 -  right_unit: "x [*] one = x"
   15.23 -
   15.24 -axclass semigroup < type
   15.25 -  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
   15.26 -
   15.27 -axclass group < semigroup
   15.28 -  left_unit:    "one [*] x = x"
   15.29 -  left_inverse: "invers x [*] x = one"
   15.30 -
   15.31 -axclass agroup < group
   15.32 -  commute: "x [*] y = y [*] x"
   15.33 -
   15.34 -
   15.35 -subsection {* Abstract reasoning *}
   15.36 -
   15.37 -theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
   15.38 -proof -
   15.39 -  have "x [*] invers x = one [*] (x [*] invers x)"
   15.40 -    by (simp only: group_class.left_unit)
   15.41 -  also have "... = one [*] x [*] invers x"
   15.42 -    by (simp only: semigroup_class.assoc)
   15.43 -  also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
   15.44 -    by (simp only: group_class.left_inverse)
   15.45 -  also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
   15.46 -    by (simp only: semigroup_class.assoc)
   15.47 -  also have "... = invers (invers x) [*] one [*] invers x"
   15.48 -    by (simp only: group_class.left_inverse)
   15.49 -  also have "... = invers (invers x) [*] (one [*] invers x)"
   15.50 -    by (simp only: semigroup_class.assoc)
   15.51 -  also have "... = invers (invers x) [*] invers x"
   15.52 -    by (simp only: group_class.left_unit)
   15.53 -  also have "... = one"
   15.54 -    by (simp only: group_class.left_inverse)
   15.55 -  finally show ?thesis .
   15.56 -qed
   15.57 -
   15.58 -theorem group_right_unit: "x [*] one = (x::'a::group)"
   15.59 -proof -
   15.60 -  have "x [*] one = x [*] (invers x [*] x)"
   15.61 -    by (simp only: group_class.left_inverse)
   15.62 -  also have "... = x [*] invers x [*] x"
   15.63 -    by (simp only: semigroup_class.assoc)
   15.64 -  also have "... = one [*] x"
   15.65 -    by (simp only: group_right_inverse)
   15.66 -  also have "... = x"
   15.67 -    by (simp only: group_class.left_unit)
   15.68 -  finally show ?thesis .
   15.69 -qed
   15.70 -
   15.71 -
   15.72 -subsection {* Abstract instantiation *}
   15.73 -
   15.74 -instance monoid < semigroup
   15.75 -proof intro_classes
   15.76 -  fix x y z :: "'a::monoid"
   15.77 -  show "x [*] y [*] z = x [*] (y [*] z)"
   15.78 -    by (rule monoid_class.assoc)
   15.79 -qed
   15.80 -
   15.81 -instance group < monoid
   15.82 -proof intro_classes
   15.83 -  fix x y z :: "'a::group"
   15.84 -  show "x [*] y [*] z = x [*] (y [*] z)"
   15.85 -    by (rule semigroup_class.assoc)
   15.86 -  show "one [*] x = x"
   15.87 -    by (rule group_class.left_unit)
   15.88 -  show "x [*] one = x"
   15.89 -    by (rule group_right_unit)
   15.90 -qed
   15.91 -
   15.92 -
   15.93 -subsection {* Concrete instantiation *}
   15.94 -
   15.95 -defs (overloaded)
   15.96 -  times_bool_def:   "x [*] y == x ~= (y::bool)"
   15.97 -  inverse_bool_def: "invers x == x::bool"
   15.98 -  unit_bool_def:    "one == False"
   15.99 -
  15.100 -instance bool :: agroup
  15.101 -proof (intro_classes,
  15.102 -    unfold times_bool_def inverse_bool_def unit_bool_def)
  15.103 -  fix x y z
  15.104 -  show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast
  15.105 -  show "(False ~= x) = x" by blast
  15.106 -  show "(x ~= x) = False" by blast
  15.107 -  show "(x ~= y) = (y ~= x)" by blast
  15.108 -qed
  15.109 -
  15.110 -
  15.111 -subsection {* Lifting and Functors *}
  15.112 -
  15.113 -defs (overloaded)
  15.114 -  times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"
  15.115 -
  15.116 -instance * :: (semigroup, semigroup) semigroup
  15.117 -proof (intro_classes, unfold times_prod_def)
  15.118 -  fix p q r :: "'a::semigroup * 'b::semigroup"
  15.119 -  show
  15.120 -    "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r,
  15.121 -      snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
  15.122 -       (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
  15.123 -        snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"
  15.124 -    by (simp add: semigroup_class.assoc)
  15.125 -qed
  15.126 -
  15.127 -end
    16.1 --- a/src/HOL/AxClasses/Lattice/OrdInsts.thy	Sun Feb 15 21:26:25 2009 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,43 +0,0 @@
    16.4 -(*  Title:      OrdInsts.thy
    16.5 -    ID:         $Id$
    16.6 -    Author:     Markus Wenzel, TU Muenchen
    16.7 -
    16.8 -Some order instantiations.
    16.9 -*)
   16.10 -
   16.11 -OrdInsts = OrdDefs +
   16.12 -
   16.13 -
   16.14 -(* binary / general products of quasi_orders / orders *)
   16.15 -
   16.16 -instance
   16.17 -  "*" :: (quasi_order, quasi_order) quasi_order         (le_prod_refl, le_prod_trans)
   16.18 -
   16.19 -instance
   16.20 -  "*" :: (partial_order, partial_order) partial_order   (le_prod_antisym)
   16.21 -  
   16.22 -
   16.23 -instance
   16.24 -  fun :: (term, quasi_order) quasi_order                (le_fun_refl, le_fun_trans)
   16.25 -
   16.26 -instance
   16.27 -  fun :: (term, partial_order) partial_order            (le_fun_antisym)
   16.28 -
   16.29 -
   16.30 -(* duals of quasi orders / partial orders / linear orders *)
   16.31 -
   16.32 -instance
   16.33 -  dual :: (quasi_order) quasi_order                     (le_dual_refl, le_dual_trans)
   16.34 -
   16.35 -instance
   16.36 -  dual :: (partial_order) partial_order                 (le_dual_antisym)
   16.37 -
   16.38 -
   16.39 -(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
   16.40 -  'feature' in Pure/type.ML
   16.41 -
   16.42 -instance
   16.43 -  dual :: (linear_order) linear_order                   (le_dual_lin)
   16.44 -*)
   16.45 -
   16.46 -end
    17.1 --- a/src/HOL/AxClasses/Product.thy	Sun Feb 15 21:26:25 2009 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,20 +0,0 @@
    17.4 -(*  Title:      HOL/AxClasses/Product.thy
    17.5 -    ID:         $Id$
    17.6 -    Author:     Markus Wenzel, TU Muenchen
    17.7 -*)
    17.8 -
    17.9 -theory Product imports Main begin
   17.10 -
   17.11 -axclass product < type
   17.12 -
   17.13 -consts
   17.14 -  product :: "'a::product => 'a => 'a"    (infixl "[*]" 70)
   17.15 -
   17.16 -
   17.17 -instance bool :: product
   17.18 -  by intro_classes
   17.19 -
   17.20 -defs (overloaded)
   17.21 -  product_bool_def: "x [*] y == x & y"
   17.22 -
   17.23 -end
    18.1 --- a/src/HOL/AxClasses/README.html	Sun Feb 15 21:26:25 2009 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,20 +0,0 @@
    18.4 -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    18.5 -
    18.6 -<!-- $Id$ -->
    18.7 -
    18.8 -<html>
    18.9 -
   18.10 -<head>
   18.11 -  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
   18.12 -  <title>HOL/AxClasses</title>
   18.13 -</head>
   18.14 -
   18.15 -<body>
   18.16 -<h1>HOL/AxClasses</h1>
   18.17 -
   18.18 -These are the HOL examples of the tutorial <a
   18.19 -href="http://isabelle.in.tum.de/dist/Isabelle/doc/axclass.pdf">Using Axiomatic Type
   18.20 -Classes in Isabelle</a>.  See also FOL/ex/NatClass for the natural
   18.21 -number example.
   18.22 -</body>
   18.23 -</html>
    19.1 --- a/src/HOL/AxClasses/ROOT.ML	Sun Feb 15 21:26:25 2009 +0100
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,3 +0,0 @@
    19.4 -(* $Id$ *)
    19.5 -
    19.6 -use_thys ["Semigroups", "Group", "Product"];
    20.1 --- a/src/HOL/AxClasses/Semigroups.thy	Sun Feb 15 21:26:25 2009 +0100
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,21 +0,0 @@
    20.4 -(*  Title:      HOL/AxClasses/Semigroups.thy
    20.5 -    ID:         $Id$
    20.6 -    Author:     Markus Wenzel, TU Muenchen
    20.7 -*)
    20.8 -
    20.9 -theory Semigroups imports Main begin
   20.10 -
   20.11 -consts
   20.12 -  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
   20.13 -
   20.14 -axclass semigroup < type
   20.15 -  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
   20.16 -
   20.17 -
   20.18 -consts
   20.19 -  plus :: "'a => 'a => 'a"    (infixl "[+]" 70)
   20.20 -
   20.21 -axclass plus_semigroup < type
   20.22 -  assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
   20.23 -
   20.24 -end
    21.1 --- a/src/HOL/IsaMakefile	Sun Feb 15 21:26:25 2009 +0100
    21.2 +++ b/src/HOL/IsaMakefile	Mon Feb 16 12:27:30 2009 +0100
    21.3 @@ -13,7 +13,6 @@
    21.4    HOL-Library \
    21.5    HOL-ex \
    21.6    HOL-Auth \
    21.7 -  HOL-AxClasses \
    21.8    HOL-Bali \
    21.9    HOL-Extraction \
   21.10    HOL-HahnBanach \
   21.11 @@ -770,15 +769,6 @@
   21.12  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
   21.13  
   21.14  
   21.15 -## HOL-AxClasses
   21.16 -
   21.17 -HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
   21.18 -
   21.19 -$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
   21.20 -  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
   21.21 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
   21.22 -
   21.23 -
   21.24  ## HOL-Lattice
   21.25  
   21.26  HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
   21.27 @@ -1045,22 +1035,22 @@
   21.28  ## clean
   21.29  
   21.30  clean:
   21.31 -	@rm -f  $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
   21.32 -		$(LOG)/HOL.gz $(LOG)/TLA.gz \
   21.33 -		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
   21.34 -		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
   21.35 -		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
   21.36 -		$(LOG)/HOL-HoareParallel.gz \
   21.37 -		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
   21.38 -		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
   21.39 -		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
   21.40 -                $(LOG)/HOL-Bali.gz \
   21.41 -		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
   21.42 -                $(LOG)/HOL-Nominal-Examples.gz \
   21.43 -		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
   21.44 -		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
   21.45 -		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
   21.46 -                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
   21.47 -		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
   21.48 -                $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
   21.49 -                $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
   21.50 +	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
   21.51 +		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
   21.52 +		$(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz		\
   21.53 +		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
   21.54 +		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
   21.55 +		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
   21.56 +		$(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz		\
   21.57 +		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
   21.58 +		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
   21.59 +		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
   21.60 +		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
   21.61 +		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
   21.62 +		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
   21.63 +		$(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz	\
   21.64 +		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
   21.65 +		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
   21.66 +		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
   21.67 +		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
   21.68 +		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz