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