doc-src/AxClass/Group/Semigroups.thy

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

header {* Semigroups *}

theory Semigroups = Main:

text {*
  \medskip\noindent An axiomatic type class is simply a class of types
  that all meet certain properties, which are also called \emph{class
  axioms}. Thus, type classes may be also understood as type
  predicates --- i.e.\ abstractions over a single type argument @{typ
  'a}.  Class axioms typically contain polymorphic constants that
  depend on this type @{typ 'a}.  These \emph{characteristic
  constants} behave like operations associated with the ``carrier''
  type @{typ 'a}.

  We illustrate these basic concepts by the following formulation of
  semigroups.
*}

consts
  times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<odot>" 70)
axclass semigroup \<subseteq> type
  assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"

text {*
  \noindent Above we have first declared a polymorphic constant @{text
  "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
  all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
  associative operator.  The @{text assoc} axiom contains exactly one
  type variable, which is invisible in the above presentation, though.
  Also note that free term variables (like @{term x}, @{term y},
  @{term z}) are allowed for user convenience --- conceptually all of
  these are bound by outermost universal quantifiers.

  \medskip In general, type classes may be used to describe
  \emph{structures} with exactly one carrier @{typ 'a} and a fixed
  \emph{signature}.  Different signatures require different classes.
  Below, class @{text plus_semigroup} represents semigroups @{text
  "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
  correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
*}

consts
  plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>" 70)
axclass plus_semigroup \<subseteq> type
  assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"

text {*
  \noindent Even if classes @{text plus_semigroup} and @{text
  semigroup} both represent semigroups in a sense, they are certainly
  not quite the same.
*}

end