diff -r b094999e1d33 -r 37f47ea6fed1 doc-src/AxClass/Group/Group.thy
--- a/doc-src/AxClass/Group/Group.thy	Thu Feb 26 06:39:06 2009 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-
-header {* Basic group theory *}
-
-theory Group imports Main begin
-
-text {*
-  \medskip\noindent The meta-level type system of Isabelle supports
-  \emph{intersections} and \emph{inclusions} of type classes. These
-  directly correspond to intersections and inclusions of type
-  predicates in a purely set theoretic sense. This is sufficient as a
-  means to describe simple hierarchies of structures.  As an
-  illustration, we use the well-known example of semigroups, monoids,
-  general groups and Abelian groups.
-*}
-
-subsection {* Monoids and Groups *}
-
-text {*
-  First we declare some polymorphic constants required later for the
-  signature parts of our structures.
-*}
-
-consts
-  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
-  invers :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
-  one :: 'a    ("\<one>")
-
-text {*
-  \noindent Next we define class @{text monoid} of monoids with
-  operations @{text \<odot>} and @{text \<one>}.  Note that multiple class
-  axioms are allowed for user convenience --- they simply represent
-  the conjunction of their respective universal closures.
-*}
-
-axclass monoid \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-  left_unit: "\<one> \<odot> x = x"
-  right_unit: "x \<odot> \<one> = x"
-
-text {*
-  \noindent So class @{text monoid} contains exactly those types
-  @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"}
-  are specified appropriately, such that @{text \<odot>} is associative and
-  @{text \<one>} is a left and right unit element for the @{text \<odot>}
-  operation.
-*}
-
-text {*
-  \medskip Independently of @{text monoid}, we now define a linear
-  hierarchy of semigroups, general groups and Abelian groups.  Note
-  that the names of class axioms are automatically qualified with each
-  class name, so we may re-use common names such as @{text assoc}.
-*}
-
-axclass semigroup \<subseteq> type
-  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-axclass group \<subseteq> semigroup
-  left_unit: "\<one> \<odot> x = x"
-  left_inverse: "x\<inv> \<odot> x = \<one>"
-
-axclass agroup \<subseteq> group
-  commute: "x \<odot> y = y \<odot> x"
-
-text {*
-  \noindent Class @{text group} inherits associativity of @{text \<odot>}
-  from @{text semigroup} and adds two further group axioms. Similarly,
-  @{text agroup} is defined as the subset of @{text group} such that
-  for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
-  \<tau>"} is even commutative.
-*}
-
-
-subsection {* Abstract reasoning *}
-
-text {*
-  In a sense, axiomatic type classes may be viewed as \emph{abstract
-  theories}.  Above class definitions gives rise to abstract axioms
-  @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
-  commute}, where any of these contain a type variable @{text "'a \<Colon>
-  c"} that is restricted to types of the corresponding class @{text
-  c}.  \emph{Sort constraints} like this express a logical
-  precondition for the whole formula.  For example, @{text assoc}
-  states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
-  semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
-
-  \medskip From a technical point of view, abstract axioms are just
-  ordinary Isabelle theorems, which may be used in proofs without
-  special treatment.  Such ``abstract proofs'' usually yield new
-  ``abstract theorems''.  For example, we may now derive the following
-  well-known laws of general groups.
-*}
-
-theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
-proof -
-  have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
-    by (simp only: group_class.left_unit)
-  also have "... = \<one> \<odot> x \<odot> x\<inv>"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
-    by (simp only: group_class.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
-    by (simp only: group_class.left_inverse)
-  also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
-    by (simp only: semigroup_class.assoc)
-  also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
-    by (simp only: group_class.left_unit)
-  also have "... = \<one>"
-    by (simp only: group_class.left_inverse)
-  finally show ?thesis .
-qed
-
-text {*
-  \noindent With @{text group_right_inverse} already available, @{text
-  group_right_unit}\label{thm:group-right-unit} is now established
-  much easier.
-*}
-
-theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
-proof -
-  have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
-    by (simp only: group_class.left_inverse)
-  also have "... = x \<odot> x\<inv> \<odot> x"
-    by (simp only: semigroup_class.assoc)
-  also have "... = \<one> \<odot> x"
-    by (simp only: group_right_inverse)
-  also have "... = x"
-    by (simp only: group_class.left_unit)
-  finally show ?thesis .
-qed
-
-text {*
-  \medskip Abstract theorems may be instantiated to only those types
-  @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
-  known at Isabelle's type signature level.  Since we have @{text
-  "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
-  semigroup} and @{text group} are automatically inherited by @{text
-  group} and @{text agroup}.
-*}
-
-
-subsection {* Abstract instantiation *}
-
-text {*
-  From the definition, the @{text monoid} and @{text group} classes
-  have been independent.  Note that for monoids, @{text right_unit}
-  had to be included as an axiom, but for groups both @{text
-  right_unit} and @{text right_inverse} are derivable from the other
-  axioms.  With @{text group_right_unit} derived as a theorem of group
-  theory (see page~\pageref{thm:group-right-unit}), we may now
-  instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
-  monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
-
- \begin{figure}[htbp]
-   \begin{center}
-     \small
-     \unitlength 0.6mm
-     \begin{picture}(65,90)(0,-10)
-       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
-       \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
-       \put(15,5){\makebox(0,0){@{text agroup}}}
-       \put(15,25){\makebox(0,0){@{text group}}}
-       \put(15,45){\makebox(0,0){@{text semigroup}}}
-       \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
-     \end{picture}
-     \hspace{4em}
-     \begin{picture}(30,90)(0,0)
-       \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
-       \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
-       \put(15,5){\makebox(0,0){@{text agroup}}}
-       \put(15,25){\makebox(0,0){@{text group}}}
-       \put(15,45){\makebox(0,0){@{text monoid}}}
-       \put(15,65){\makebox(0,0){@{text semigroup}}}
-       \put(15,85){\makebox(0,0){@{text type}}}
-     \end{picture}
-     \caption{Monoids and groups: according to definition, and by proof}
-     \label{fig:monoid-group}
-   \end{center}
- \end{figure}
-*}
-
-instance monoid \<subseteq> semigroup
-proof
-  fix x y z :: "'a\<Colon>monoid"
-  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
-    by (rule monoid_class.assoc)
-qed
-
-instance group \<subseteq> monoid
-proof
-  fix x y z :: "'a\<Colon>group"
-  show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
-    by (rule semigroup_class.assoc)
-  show "\<one> \<odot> x = x"
-    by (rule group_class.left_unit)
-  show "x \<odot> \<one> = x"
-    by (rule group_right_unit)
-qed
-
-text {*
-  \medskip The \isakeyword{instance} command sets up an appropriate
-  goal that represents the class inclusion (or type arity, see
-  \secref{sec:inst-arity}) to be proven (see also
-  \cite{isabelle-isar-ref}).  The initial proof step causes
-  back-chaining of class membership statements wrt.\ the hierarchy of
-  any classes defined in the current theory; the effect is to reduce
-  to the initial statement to a number of goals that directly
-  correspond to any class axioms encountered on the path upwards
-  through the class hierarchy.
-*}
-
-
-subsection {* Concrete instantiation \label{sec:inst-arity} *}
-
-text {*
-  So far we have covered the case of the form
-  \isakeyword{instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely
-  \emph{abstract instantiation} --- $c@1$ is more special than @{text
-  "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}.  Even more
-  interesting for practical applications are \emph{concrete
-  instantiations} of axiomatic type classes.  That is, certain simple
-  schemes @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class
-  membership may be established at the logical level and then
-  transferred to Isabelle's type signature level.
-
-  \medskip As a typical example, we show that type @{typ bool} with
-  exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
-  @{term False} as @{text \<one>} forms an Abelian group.
-*}
-
-defs (overloaded)
-  times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
-  inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
-  unit_bool_def: "\<one> \<equiv> False"
-
-text {*
-  \medskip It is important to note that above \isakeyword{defs} are
-  just overloaded meta-level constant definitions, where type classes
-  are not yet involved at all.  This form of constant definition with
-  overloading (and optional recursion over the syntactic structure of
-  simple types) are admissible as definitional extensions of plain HOL
-  \cite{Wenzel:1997:TPHOL}.  The Haskell-style type system is not
-  required for overloading.  Nevertheless, overloaded definitions are
-  best applied in the context of type classes.
-
-  \medskip Since we have chosen above \isakeyword{defs} of the generic
-  group operations on type @{typ bool} appropriately, the class
-  membership @{text "bool \<Colon> agroup"} may be now derived as follows.
-*}
-
-instance bool :: agroup
-proof (intro_classes,
-    unfold times_bool_def inverse_bool_def unit_bool_def)
-  fix x y z
-  show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast
-  show "(False \<noteq> x) = x" by blast
-  show "(x \<noteq> x) = False" by blast
-  show "(x \<noteq> y) = (y \<noteq> x)" by blast
-qed
-
-text {*
-  The result of an \isakeyword{instance} statement is both expressed
-  as a theorem of Isabelle's meta-logic, and as a type arity of the
-  type signature.  The latter enables type-inference system to take
-  care of this new instance automatically.
-
-  \medskip We could now also instantiate our group theory classes to
-  many other concrete types.  For example, @{text "int \<Colon> agroup"}
-  (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
-  and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"}
-  (e.g.\ if @{text \<odot>} is defined as list append).  Thus, the
-  characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<one>}
-  really become overloaded, i.e.\ have different meanings on different
-  types.
-*}
-
-
-subsection {* Lifting and Functors *}
-
-text {*
-  As already mentioned above, overloading in the simply-typed HOL
-  systems may include recursion over the syntactic structure of types.
-  That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
-  contain constants of name @{text c} on the right-hand side --- if
-  these have types that are structurally simpler than @{text \<tau>}.
-
-  This feature enables us to \emph{lift operations}, say to Cartesian
-  products, direct sums or function spaces.  Subsequently we lift
-  @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
-*}
-
-defs (overloaded)
-  times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
-
-text {*
-  It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
-  and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
-  'b"}.  Hence the binary type constructor @{text \<odot>} maps semigroups
-  to semigroups.  This may be established formally as follows.
-*}
-
-instance * :: (semigroup, semigroup) semigroup
-proof (intro_classes, unfold times_prod_def)
-  fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
-  show
-    "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r,
-      snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
-       (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
-        snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
-    by (simp add: semigroup_class.assoc)
-qed
-
-text {*
-  Thus, if we view class instances as ``structures'', then overloaded
-  constant definitions with recursion over types indirectly provide
-  some kind of ``functors'' --- i.e.\ mappings between abstract
-  theories.
-*}
-
-end