--- a/doc-src/AxClass/Group/Group.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-
-header {* Basic group theory *}
-
-theory Group imports Main begin
-
-text {*
- \medskip\noindent The meta-level type system of Isabelle supports
- \emph{intersections} and \emph{inclusions} of type classes. These
- directly correspond to intersections and inclusions of type
- predicates in a purely set theoretic sense. This is sufficient as a
- means to describe simple hierarchies of structures. As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.
-*}
-
-subsection {* Monoids and Groups *}
-
-text {*
- First we declare some polymorphic constants required later for the
- signature parts of our structures.
-*}
-
-consts
- times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
- invers :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
- one :: 'a ("\<one>")
-
-text {*
- \noindent Next we define class @{text monoid} of monoids with
- operations @{text \<odot>} and @{text \<one>}. Note that multiple class
- axioms are allowed for user convenience --- they simply represent
- the conjunction of their respective universal closures.
-*}
-
-axclass monoid \<subseteq> type
- assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
- left_unit: "\<one> \<odot> x = x"
- right_unit: "x \<odot> \<one> = x"
-
-text {*
- \noindent So class @{text monoid} contains exactly those types
- @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<one> \<Colon> \<tau>"}
- are specified appropriately, such that @{text \<odot>} is associative and
- @{text \<one>} is a left and right unit element for the @{text \<odot>}
- operation.
-*}
-
-text {*
- \medskip Independently of @{text monoid}, we now define a linear
- hierarchy of semigroups, general groups and Abelian groups. Note
- that the names of class axioms are automatically qualified with each
- class name, so we may re-use common names such as @{text assoc}.
-*}
-
-axclass semigroup \<subseteq> type
- assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-axclass group \<subseteq> semigroup
- left_unit: "\<one> \<odot> x = x"
- left_inverse: "x\<inv> \<odot> x = \<one>"
-
-axclass agroup \<subseteq> group
- commute: "x \<odot> y = y \<odot> x"
-
-text {*
- \noindent Class @{text group} inherits associativity of @{text \<odot>}
- from @{text semigroup} and adds two further group axioms. Similarly,
- @{text agroup} is defined as the subset of @{text group} such that
- for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
- \<tau>"} is even commutative.
-*}
-
-
-subsection {* Abstract reasoning *}
-
-text {*
- In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}. Above class definitions gives rise to abstract axioms
- @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
- commute}, where any of these contain a type variable @{text "'a \<Colon>
- c"} that is restricted to types of the corresponding class @{text
- c}. \emph{Sort constraints} like this express a logical
- precondition for the whole formula. For example, @{text assoc}
- states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
- semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
-
- \medskip From a technical point of view, abstract axioms are just
- ordinary Isabelle theorems, which may be used in proofs without
- special treatment. Such ``abstract proofs'' usually yield new
- ``abstract theorems''. For example, we may now derive the following
- well-known laws of general groups.
-*}
-
-theorem group_right_inverse: "x \<odot> x\<inv> = (\<one>\<Colon>'a\<Colon>group)"
-proof -
- have "x \<odot> x\<inv> = \<one> \<odot> (x \<odot> x\<inv>)"
- by (simp only: group_class.left_unit)
- also have "... = \<one> \<odot> x \<odot> x\<inv>"
- by (simp only: semigroup_class.assoc)
- also have "... = (x\<inv>)\<inv> \<odot> x\<inv> \<odot> x \<odot> x\<inv>"
- by (simp only: group_class.left_inverse)
- also have "... = (x\<inv>)\<inv> \<odot> (x\<inv> \<odot> x) \<odot> x\<inv>"
- by (simp only: semigroup_class.assoc)
- also have "... = (x\<inv>)\<inv> \<odot> \<one> \<odot> x\<inv>"
- by (simp only: group_class.left_inverse)
- also have "... = (x\<inv>)\<inv> \<odot> (\<one> \<odot> x\<inv>)"
- by (simp only: semigroup_class.assoc)
- also have "... = (x\<inv>)\<inv> \<odot> x\<inv>"
- by (simp only: group_class.left_unit)
- also have "... = \<one>"
- by (simp only: group_class.left_inverse)
- finally show ?thesis .
-qed
-
-text {*
- \noindent With @{text group_right_inverse} already available, @{text
- group_right_unit}\label{thm:group-right-unit} is now established
- much easier.
-*}
-
-theorem group_right_unit: "x \<odot> \<one> = (x\<Colon>'a\<Colon>group)"
-proof -
- have "x \<odot> \<one> = x \<odot> (x\<inv> \<odot> x)"
- by (simp only: group_class.left_inverse)
- also have "... = x \<odot> x\<inv> \<odot> x"
- by (simp only: semigroup_class.assoc)
- also have "... = \<one> \<odot> x"
- by (simp only: group_right_inverse)
- also have "... = x"
- by (simp only: group_class.left_unit)
- finally show ?thesis .
-qed
-
-text {*
- \medskip Abstract theorems may be instantiated to only those types
- @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
- known at Isabelle's type signature level. Since we have @{text
- "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
- semigroup} and @{text group} are automatically inherited by @{text
- group} and @{text agroup}.
-*}
-
-
-subsection {* Abstract instantiation *}
-
-text {*
- From the definition, the @{text monoid} and @{text group} classes
- have been independent. Note that for monoids, @{text right_unit}
- had to be included as an axiom, but for groups both @{text
- right_unit} and @{text right_inverse} are derivable from the other
- axioms. With @{text group_right_unit} derived as a theorem of group
- theory (see page~\pageref{thm:group-right-unit}), we may now
- instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
- monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
-
- \begin{figure}[htbp]
- \begin{center}
- \small
- \unitlength 0.6mm
- \begin{picture}(65,90)(0,-10)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
- \put(15,5){\makebox(0,0){@{text agroup}}}
- \put(15,25){\makebox(0,0){@{text group}}}
- \put(15,45){\makebox(0,0){@{text semigroup}}}
- \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
- \end{picture}
- \hspace{4em}
- \begin{picture}(30,90)(0,0)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
- \put(15,5){\makebox(0,0){@{text agroup}}}
- \put(15,25){\makebox(0,0){@{text group}}}
- \put(15,45){\makebox(0,0){@{text monoid}}}
- \put(15,65){\makebox(0,0){@{text semigroup}}}
- \put(15,85){\makebox(0,0){@{text type}}}
- \end{picture}
- \caption{Monoids and groups: according to definition, and by proof}
- \label{fig:monoid-group}
- \end{center}
- \end{figure}
-*}
-
-instance monoid \<subseteq> semigroup
-proof
- fix x y z :: "'a\<Colon>monoid"
- show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
- by (rule monoid_class.assoc)
-qed
-
-instance group \<subseteq> monoid
-proof
- fix x y z :: "'a\<Colon>group"
- show "x \<odot> y \<odot> z = x \<odot> (y \<odot> z)"
- by (rule semigroup_class.assoc)
- show "\<one> \<odot> x = x"
- by (rule group_class.left_unit)
- show "x \<odot> \<one> = x"
- by (rule group_right_unit)
-qed
-
-text {*
- \medskip The \isakeyword{instance} command sets up an appropriate
- goal that represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}). The initial proof step causes
- back-chaining of class membership statements wrt.\ the hierarchy of
- any classes defined in the current theory; the effect is to reduce
- to the initial statement to a number of goals that directly
- correspond to any class axioms encountered on the path upwards
- through the class hierarchy.
-*}
-
-
-subsection {* Concrete instantiation \label{sec:inst-arity} *}
-
-text {*
- So far we have covered the case of the form
- \isakeyword{instance}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely
- \emph{abstract instantiation} --- $c@1$ is more special than @{text
- "c\<^sub>1"} and thus an instance of @{text "c\<^sub>2"}. Even more
- interesting for practical applications are \emph{concrete
- instantiations} of axiomatic type classes. That is, certain simple
- schemes @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Colon> c"} of class
- membership may be established at the logical level and then
- transferred to Isabelle's type signature level.
-
- \medskip As a typical example, we show that type @{typ bool} with
- exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
- @{term False} as @{text \<one>} forms an Abelian group.
-*}
-
-defs (overloaded)
- times_bool_def: "x \<odot> y \<equiv> x \<noteq> (y\<Colon>bool)"
- inverse_bool_def: "x\<inv> \<equiv> x\<Colon>bool"
- unit_bool_def: "\<one> \<equiv> False"
-
-text {*
- \medskip It is important to note that above \isakeyword{defs} are
- just overloaded meta-level constant definitions, where type classes
- are not yet involved at all. This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
- required for overloading. Nevertheless, overloaded definitions are
- best applied in the context of type classes.
-
- \medskip Since we have chosen above \isakeyword{defs} of the generic
- group operations on type @{typ bool} appropriately, the class
- membership @{text "bool \<Colon> agroup"} may be now derived as follows.
-*}
-
-instance bool :: agroup
-proof (intro_classes,
- unfold times_bool_def inverse_bool_def unit_bool_def)
- fix x y z
- show "((x \<noteq> y) \<noteq> z) = (x \<noteq> (y \<noteq> z))" by blast
- show "(False \<noteq> x) = x" by blast
- show "(x \<noteq> x) = False" by blast
- show "(x \<noteq> y) = (y \<noteq> x)" by blast
-qed
-
-text {*
- The result of an \isakeyword{instance} statement is both expressed
- as a theorem of Isabelle's meta-logic, and as a type arity of the
- type signature. The latter enables type-inference system to take
- care of this new instance automatically.
-
- \medskip We could now also instantiate our group theory classes to
- many other concrete types. For example, @{text "int \<Colon> agroup"}
- (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
- and @{text \<one>} as zero) or @{text "list \<Colon> (type) semigroup"}
- (e.g.\ if @{text \<odot>} is defined as list append). Thus, the
- characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<one>}
- really become overloaded, i.e.\ have different meanings on different
- types.
-*}
-
-
-subsection {* Lifting and Functors *}
-
-text {*
- As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
- contain constants of name @{text c} on the right-hand side --- if
- these have types that are structurally simpler than @{text \<tau>}.
-
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces. Subsequently we lift
- @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
-*}
-
-defs (overloaded)
- times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
-
-text {*
- It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
- and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
- 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups
- to semigroups. This may be established formally as follows.
-*}
-
-instance * :: (semigroup, semigroup) semigroup
-proof (intro_classes, unfold times_prod_def)
- fix p q r :: "'a\<Colon>semigroup \<times> 'b\<Colon>semigroup"
- show
- "(fst (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> fst r,
- snd (fst p \<odot> fst q, snd p \<odot> snd q) \<odot> snd r) =
- (fst p \<odot> fst (fst q \<odot> fst r, snd q \<odot> snd r),
- snd p \<odot> snd (fst q \<odot> fst r, snd q \<odot> snd r))"
- by (simp add: semigroup_class.assoc)
-qed
-
-text {*
- Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.
-*}
-
-end
--- a/doc-src/AxClass/Group/Product.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-
-header {* Syntactic classes *}
-
-theory Product imports Main begin
-
-text {*
- \medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet discussed. When declaring polymorphic
- constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
- may be constrained by type classes (or even general sorts) in an
- arbitrary way. Note that by default, in Isabelle/HOL the
- declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
- for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
- universal class of HOL, this is not really a constraint at all.
-
- The @{text product} class below provides a less degenerate example of
- syntactic type classes.
-*}
-
-axclass
- product \<subseteq> type
-consts
- product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
-
-text {*
- Here class @{text product} is defined as subclass of @{text type}
- without any additional axioms. This effects in logical equivalence
- of @{text product} and @{text type}, as is reflected by the trivial
- introduction rule generated for this definition.
-
- \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
- 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
- 'a"} anyway? In this particular case where @{text "product \<equiv>
- type"}, it should be obvious that both declarations are the same
- from the logic's point of view. It even makes the most sense to
- remove sort constraints from constant declarations, as far as the
- purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
-
- On the other hand there are syntactic differences, of course.
- Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
- type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
- type signature. In our example, this arity may be always added when
- required by means of an \isakeyword{instance} with the default proof
- (double-dot).
-
- \medskip Thus, we may observe the following discipline of using
- syntactic classes. Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class
- @{text c}. Only immediately before \emph{specifying} these
- constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
- c"}.
-
- This is done for class @{text product} and type @{typ bool} as
- follows.
-*}
-
-instance bool :: product ..
-defs (overloaded)
- product_bool_def: "x \<odot> y \<equiv> x \<and> y"
-
-text {*
- The definition @{text prod_bool_def} becomes syntactically
- well-formed only after the arity @{text "bool \<Colon> product"} is made
- known to the type checker.
-
- \medskip It is very important to see that above \isakeyword{defs} are
- not directly connected with \isakeyword{instance} at all! We were
- just following our convention to specify @{text \<odot>} on @{typ bool}
- after having instantiated @{text "bool \<Colon> product"}. Isabelle does
- not require these definitions, which is in contrast to programming
- languages like Haskell \cite{haskell-report}.
-
- \medskip While Isabelle type classes and those of Haskell are almost
- the same as far as type-checking and type inference are concerned,
- there are important semantic differences. Haskell classes require
- their instances to \emph{provide operations} of certain \emph{names}.
- Therefore, its \texttt{instance} has a \texttt{where} part that tells
- the system what these ``member functions'' should be.
-
- This style of \texttt{instance} would not make much sense in
- Isabelle's meta-logic, because there is no internal notion of
- ``providing operations'' or even ``names of functions''.
-*}
-
-end
--- a/doc-src/AxClass/Group/ROOT.ML Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-
-use_thy "Semigroups";
-use_thy "Group";
-use_thy "Product";
--- a/doc-src/AxClass/Group/Semigroups.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-
-header {* Semigroups *}
-
-theory Semigroups imports Main begin
-
-text {*
- \medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain properties, which are also called \emph{class
- axioms}. Thus, type classes may be also understood as type
- predicates --- i.e.\ abstractions over a single type argument @{typ
- 'a}. Class axioms typically contain polymorphic constants that
- depend on this type @{typ 'a}. These \emph{characteristic
- constants} behave like operations associated with the ``carrier''
- type @{typ 'a}.
-
- We illustrate these basic concepts by the following formulation of
- semigroups.
-*}
-
-consts
- times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
-axclass semigroup \<subseteq> type
- assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
-
-text {*
- \noindent Above we have first declared a polymorphic constant @{text
- "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
- all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
- associative operator. The @{text assoc} axiom contains exactly one
- type variable, which is invisible in the above presentation, though.
- Also note that free term variables (like @{term x}, @{term y},
- @{term z}) are allowed for user convenience --- conceptually all of
- these are bound by outermost universal quantifiers.
-
- \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier @{typ 'a} and a fixed
- \emph{signature}. Different signatures require different classes.
- Below, class @{text plus_semigroup} represents semigroups @{text
- "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
- correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
-*}
-
-consts
- plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
-axclass plus_semigroup \<subseteq> type
- assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-
-text {*
- \noindent Even if classes @{text plus_semigroup} and @{text
- semigroup} both represent semigroups in a sense, they are certainly
- not quite the same.
-*}
-
-end
--- a/doc-src/AxClass/Group/document/Group.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,512 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Group}%
-%
-\isamarkupheader{Basic group theory%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Group\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent The meta-level type system of Isabelle supports
- \emph{intersections} and \emph{inclusions} of type classes. These
- directly correspond to intersections and inclusions of type
- predicates in a purely set theoretic sense. This is sufficient as a
- means to describe simple hierarchies of structures. As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Monoids and Groups%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-First we declare some polymorphic constants required later for the
- signature parts of our structures.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ invers\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
-\ \ one\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\noindent Next we define class \isa{monoid} of monoids with
- operations \isa{{\isasymodot}} and \isa{{\isasymone}}. Note that multiple class
- axioms are allowed for user convenience --- they simply represent
- the conjunction of their respective universal closures.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ monoid\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent So class \isa{monoid} contains exactly those types
- \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymone}\ {\isasymColon}\ {\isasymtau}}
- are specified appropriately, such that \isa{{\isasymodot}} is associative and
- \isa{{\isasymone}} is a left and right unit element for the \isa{{\isasymodot}}
- operation.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\medskip Independently of \isa{monoid}, we now define a linear
- hierarchy of semigroups, general groups and Abelian groups. Note
- that the names of class axioms are automatically qualified with each
- class name, so we may re-use common names such as \isa{assoc}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ group\ {\isasymsubseteq}\ semigroup\isanewline
-\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ left{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymodot}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ agroup\ {\isasymsubseteq}\ group\isanewline
-\ \ commute{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isacharequal}\ y\ {\isasymodot}\ x{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
- from \isa{semigroup} and adds two further group axioms. Similarly,
- \isa{agroup} is defined as the subset of \isa{group} such that
- for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Abstract reasoning%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}. Above class definitions gives rise to abstract axioms
- \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}. \emph{Sort constraints} like this express a logical
- precondition for the whole formula. For example, \isa{assoc}
- states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
-
- \medskip From a technical point of view, abstract axioms are just
- ordinary Isabelle theorems, which may be used in proofs without
- special treatment. Such ``abstract proofs'' usually yield new
- ``abstract theorems''. For example, we may now derive the following
- well-known laws of general groups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ {\isacharparenleft}x\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ {\isacharparenleft}{\isasymone}\ {\isasymodot}\ x{\isasyminv}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isacharparenleft}x{\isasyminv}{\isacharparenright}{\isasyminv}\ {\isasymodot}\ x{\isasyminv}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
- much easier.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{theorem}\isamarkupfalse%
-\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}x{\isasyminv}\ {\isasymodot}\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x\ {\isasymodot}\ x{\isasyminv}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ {\isasymone}\ {\isasymodot}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\ \ \isacommand{also}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isachardot}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ only{\isacharcolon}\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{finally}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\medskip Abstract theorems may be instantiated to only those types
- \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
- known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Abstract instantiation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-From the definition, the \isa{monoid} and \isa{group} classes
- have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit}
- had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other
- axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group
- theory (see page~\pageref{thm:group-right-unit}), we may now
- instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}).
-
- \begin{figure}[htbp]
- \begin{center}
- \small
- \unitlength 0.6mm
- \begin{picture}(65,90)(0,-10)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(1,1){10}} \put(35,60){\line(1,-1){10}}
- \put(15,5){\makebox(0,0){\isa{agroup}}}
- \put(15,25){\makebox(0,0){\isa{group}}}
- \put(15,45){\makebox(0,0){\isa{semigroup}}}
- \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
- \end{picture}
- \hspace{4em}
- \begin{picture}(30,90)(0,0)
- \put(15,10){\line(0,1){10}} \put(15,30){\line(0,1){10}}
- \put(15,50){\line(0,1){10}} \put(15,70){\line(0,1){10}}
- \put(15,5){\makebox(0,0){\isa{agroup}}}
- \put(15,25){\makebox(0,0){\isa{group}}}
- \put(15,45){\makebox(0,0){\isa{monoid}}}
- \put(15,65){\makebox(0,0){\isa{semigroup}}}
- \put(15,85){\makebox(0,0){\isa{type}}}
- \end{picture}
- \caption{Monoids and groups: according to definition, and by proof}
- \label{fig:monoid-group}
- \end{center}
- \end{figure}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ monoid\ {\isasymsubseteq}\ semigroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ monoid{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ group\ {\isasymsubseteq}\ monoid\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymone}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ group{\isacharunderscore}class{\isachardot}left{\isacharunderscore}unit{\isacharparenright}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}x\ {\isasymodot}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}rule\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\medskip The \isakeyword{instance} command sets up an appropriate
- goal that represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}). The initial proof step causes
- back-chaining of class membership statements wrt.\ the hierarchy of
- any classes defined in the current theory; the effect is to reduce
- to the initial statement to a number of goals that directly
- correspond to any class axioms encountered on the path upwards
- through the class hierarchy.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-So far we have covered the case of the form
- \isakeyword{instance}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely
- \emph{abstract instantiation} --- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance of \isa{c\isactrlsub {\isadigit{2}}}. Even more
- interesting for practical applications are \emph{concrete
- instantiations} of axiomatic type classes. That is, certain simple
- schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class
- membership may be established at the logical level and then
- transferred to Isabelle's type signature level.
-
- \medskip As a typical example, we show that type \isa{bool} with
- exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
- \isa{False} as \isa{{\isasymone}} forms an Abelian group.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ inverse{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{\isachardoublequoteclose}\isanewline
-\ \ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ False{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\medskip It is important to note that above \isakeyword{defs} are
- just overloaded meta-level constant definitions, where type classes
- are not yet involved at all. This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
- required for overloading. Nevertheless, overloaded definitions are
- best applied in the context of type classes.
-
- \medskip Since we have chosen above \isakeyword{defs} of the generic
- group operations on type \isa{bool} appropriately, the class
- membership \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\isanewline
-\ \ \ \ unfold\ times{\isacharunderscore}bool{\isacharunderscore}def\ inverse{\isacharunderscore}bool{\isacharunderscore}def\ unit{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\ y\ z\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isasymnoteq}\ z{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymnoteq}\ {\isacharparenleft}y\ {\isasymnoteq}\ z{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}False\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ x{\isacharparenright}\ {\isacharequal}\ False{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymnoteq}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y\ {\isasymnoteq}\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ blast\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-The result of an \isakeyword{instance} statement is both expressed
- as a theorem of Isabelle's meta-logic, and as a type arity of the
- type signature. The latter enables type-inference system to take
- care of this new instance automatically.
-
- \medskip We could now also instantiate our group theory classes to
- many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup}
- (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
- and \isa{{\isasymone}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
- (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the
- characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymone}}
- really become overloaded, i.e.\ have different meanings on different
- types.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lifting and Functors%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
- contain constants of name \isa{c} on the right-hand side --- if
- these have types that are structurally simpler than \isa{{\isasymtau}}.
-
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces. Subsequently we lift
- \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\ {\isasymodot}\ q\ {\isasymequiv}\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
- and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups
- to semigroups. This may be established formally as follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}intro{\isacharunderscore}classes{\isacharcomma}\ unfold\ times{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ q\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\isanewline
-\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}fst\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ fst\ r{\isacharcomma}\isanewline
-\ \ \ \ \ \ snd\ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ q{\isacharcomma}\ snd\ p\ {\isasymodot}\ snd\ q{\isacharparenright}\ {\isasymodot}\ snd\ r{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}fst\ p\ {\isasymodot}\ fst\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharcomma}\isanewline
-\ \ \ \ \ \ \ \ snd\ p\ {\isasymodot}\ snd\ {\isacharparenleft}fst\ q\ {\isasymodot}\ fst\ r{\isacharcomma}\ snd\ q\ {\isasymodot}\ snd\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ semigroup{\isacharunderscore}class{\isachardot}assoc{\isacharparenright}\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/AxClass/Group/document/Product.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Product}%
-%
-\isamarkupheader{Syntactic classes%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Product\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet discussed. When declaring polymorphic
- constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
- may be constrained by type classes (or even general sorts) in an
- arbitrary way. Note that by default, in Isabelle/HOL the
- declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
- for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
- universal class of HOL, this is not really a constraint at all.
-
- The \isa{product} class below provides a less degenerate example of
- syntactic type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{axclass}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isasymsubseteq}\ type\isanewline
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}%
-\begin{isamarkuptext}%
-Here class \isa{product} is defined as subclass of \isa{type}
- without any additional axioms. This effects in logical equivalence
- of \isa{product} and \isa{type}, as is reflected by the trivial
- introduction rule generated for this definition.
-
- \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway? In this particular case where \isa{product\ {\isasymequiv}\ type}, it should be obvious that both declarations are the same
- from the logic's point of view. It even makes the most sense to
- remove sort constraints from constant declarations, as far as the
- purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
-
- On the other hand there are syntactic differences, of course.
- Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
- type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
- type signature. In our example, this arity may be always added when
- required by means of an \isakeyword{instance} with the default proof
- (double-dot).
-
- \medskip Thus, we may observe the following discipline of using
- syntactic classes. Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class
- \isa{c}. Only immediately before \emph{specifying} these
- constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
-
- This is done for class \isa{product} and type \isa{bool} as
- follows.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ bool\ {\isacharcolon}{\isacharcolon}\ product%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isacommand{defs}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
-\ \ product{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymodot}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-The definition \isa{prod{\isacharunderscore}bool{\isacharunderscore}def} becomes syntactically
- well-formed only after the arity \isa{bool\ {\isasymColon}\ product} is made
- known to the type checker.
-
- \medskip It is very important to see that above \isakeyword{defs} are
- not directly connected with \isakeyword{instance} at all! We were
- just following our convention to specify \isa{{\isasymodot}} on \isa{bool}
- after having instantiated \isa{bool\ {\isasymColon}\ product}. Isabelle does
- not require these definitions, which is in contrast to programming
- languages like Haskell \cite{haskell-report}.
-
- \medskip While Isabelle type classes and those of Haskell are almost
- the same as far as type-checking and type inference are concerned,
- there are important semantic differences. Haskell classes require
- their instances to \emph{provide operations} of certain \emph{names}.
- Therefore, its \texttt{instance} has a \texttt{where} part that tells
- the system what these ``member functions'' should be.
-
- This style of \texttt{instance} would not make much sense in
- Isabelle's meta-logic, because there is no internal notion of
- ``providing operations'' or even ``names of functions''.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/AxClass/Group/document/Semigroups.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Semigroups}%
-%
-\isamarkupheader{Semigroups%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Semigroups\ \isakeyword{imports}\ Main\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain properties, which are also called \emph{class
- axioms}. Thus, type classes may be also understood as type
- predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}. Class axioms typically contain polymorphic constants that
- depend on this type \isa{{\isacharprime}a}. These \emph{characteristic
- constants} behave like operations associated with the ``carrier''
- type \isa{{\isacharprime}a}.
-
- We illustrate these basic concepts by the following formulation of
- semigroups.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymodot}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
- all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
- associative operator. The \isa{assoc} axiom contains exactly one
- type variable, which is invisible in the above presentation, though.
- Also note that free term variables (like \isa{x}, \isa{y},
- \isa{z}) are allowed for user convenience --- conceptually all of
- these are bound by outermost universal quantifiers.
-
- \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
- \emph{signature}. Different signatures require different classes.
- Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
- correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
-\ \ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
- not quite the same.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/AxClass/IsaMakefile Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-
-## targets
-
-default: Group Nat
-images:
-test: Group Nat
-
-all: images test
-
-
-## global settings
-
-SRC = $(ISABELLE_HOME)/src
-OUT = $(ISABELLE_OUTPUT)
-LOG = $(OUT)/log
-USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
-
-
-## Group
-
-Group: HOL $(LOG)/HOL-Group.gz
-
-HOL:
- @cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-
-$(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/Group.thy \
- Group/Product.thy Group/Semigroups.thy
- @$(USEDIR) $(OUT)/HOL Group
- @rm -f Group/document/pdfsetup.sty Group/document/session.tex
-
-
-## Nat
-
-Nat: FOL $(LOG)/FOL-Nat.gz
-
-FOL:
- @cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
-
-$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
- @$(USEDIR) $(OUT)/FOL Nat
- @rm -f Nat/document/*.sty Nat/document/session.tex
-
-
-## clean
-
-clean:
- @rm -f $(LOG)/HOL-Group.gz $(LOG)/FOL-Nat.gz
--- a/doc-src/AxClass/Makefile Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-#
-# $Id$
-#
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = axclass
-
-FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
- ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
- Group/document/Group.tex Nat/document/NatClass.tex \
- Group/document/Product.tex Group/document/Semigroups.tex
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle_isar.eps
- $(LATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(LATEX) $(NAME)
- $(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle_isar.pdf
- $(PDFLATEX) $(NAME)
- $(FIXBOOKMARKS) $(NAME).out
- $(BIBTEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
--- a/doc-src/AxClass/Nat/NatClass.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-
-header {* Defining natural numbers in FOL \label{sec:ex-natclass} *}
-
-theory NatClass imports FOL begin
-
-text {*
- \medskip\noindent Axiomatic type classes abstract over exactly one
- type argument. Thus, any \emph{axiomatic} theory extension where each
- axiom refers to at most one type variable, may be trivially turned
- into a \emph{definitional} one.
-
- We illustrate this with the natural numbers in
- Isabelle/FOL.\footnote{See also
- \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}
-*}
-
-consts
- zero :: 'a ("\<zero>")
- Suc :: "'a \<Rightarrow> 'a"
- rec :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
-
-axclass nat \<subseteq> "term"
- induct: "P(\<zero>) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> P(Suc(x))) \<Longrightarrow> P(n)"
- Suc_inject: "Suc(m) = Suc(n) \<Longrightarrow> m = n"
- Suc_neq_0: "Suc(m) = \<zero> \<Longrightarrow> R"
- rec_0: "rec(\<zero>, a, f) = a"
- rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
-
-constdefs
- add :: "'a::nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60)
- "m + n \<equiv> rec(m, n, \<lambda>x y. Suc(y))"
-
-text {*
- This is an abstract version of the plain @{text Nat} theory in
- FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type @{text nat} by @{typ
- 'a} and used the natural number axioms to define class @{text nat}.
- There is only a minor snag, that the original recursion operator
- @{term rec} had to be made monomorphic.
-
- Thus class @{text nat} contains exactly those types @{text \<tau>} that
- are isomorphic to ``the'' natural numbers (with signature @{term
- \<zero>}, @{term Suc}, @{term rec}).
-
- \medskip What we have done here can be also viewed as \emph{type
- specification}. Of course, it still remains open if there is some
- type at all that meets the class axioms. Now a very nice property of
- axiomatic type classes is that abstract reasoning is always possible
- --- independent of satisfiability. The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty later ---
- ``inconsistent'' class definitions may be useless, but do not cause
- any harm.
-
- Theorems of the abstract natural numbers may be derived in the same
- way as for the concrete version. The original proof scripts may be
- re-used with some trivial changes only (mostly adding some type
- constraints).
-*}
-
-(*<*)
-lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
-apply (rule_tac n = k in induct)
-apply (rule notI)
-apply (erule Suc_neq_0)
-apply (rule notI)
-apply (erule notE)
-apply (erule Suc_inject)
-done
-
-lemma "(k+m)+n = k+(m+n)"
-apply (rule induct)
-back
-back
-back
-back
-back
-back
-oops
-
-lemma add_0 [simp]: "\<zero>+n = n"
-apply (unfold add_def)
-apply (rule rec_0)
-done
-
-lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
-apply (unfold add_def)
-apply (rule rec_Suc)
-done
-
-lemma add_assoc: "(k+m)+n = k+(m+n)"
-apply (rule_tac n = k in induct)
-apply simp
-apply simp
-done
-
-lemma add_0_right: "m+\<zero> = m"
-apply (rule_tac n = m in induct)
-apply simp
-apply simp
-done
-
-lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
-apply (rule_tac n = m in induct)
-apply simp_all
-done
-
-lemma
- assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
- shows "f(i+j) = i+f(j)"
-apply (rule_tac n = i in induct)
-apply simp
-apply (simp add: prem)
-done
-(*>*)
-
-end
\ No newline at end of file
--- a/doc-src/AxClass/Nat/ROOT.ML Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-use_thy "NatClass";
--- a/doc-src/AxClass/Nat/document/NatClass.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{NatClass}%
-%
-\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
-}
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ NatClass\ \isakeyword{imports}\ FOL\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\medskip\noindent Axiomatic type classes abstract over exactly one
- type argument. Thus, any \emph{axiomatic} theory extension where each
- axiom refers to at most one type variable, may be trivially turned
- into a \emph{definitional} one.
-
- We illustrate this with the natural numbers in
- Isabelle/FOL.\footnote{See also
- \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\isamarkupfalse%
-\isanewline
-\ \ zero\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymzero}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ Suc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\ \ rec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{axclass}\isamarkupfalse%
-\ nat\ {\isasymsubseteq}\ {\isachardoublequoteopen}term{\isachardoublequoteclose}\isanewline
-\ \ induct{\isacharcolon}\ {\isachardoublequoteopen}P{\isacharparenleft}{\isasymzero}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}Suc{\isacharparenleft}x{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P{\isacharparenleft}n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ Suc{\isacharunderscore}inject{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ Suc{\isacharparenleft}n{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ Suc{\isacharunderscore}neq{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}Suc{\isacharparenleft}m{\isacharparenright}\ {\isacharequal}\ {\isasymzero}\ {\isasymLongrightarrow}\ R{\isachardoublequoteclose}\isanewline
-\ \ rec{\isacharunderscore}{\isadigit{0}}{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}{\isasymzero}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ a{\isachardoublequoteclose}\isanewline
-\ \ rec{\isacharunderscore}Suc{\isacharcolon}\ {\isachardoublequoteopen}rec{\isacharparenleft}Suc{\isacharparenleft}m{\isacharparenright}{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}m{\isacharcomma}\ rec{\isacharparenleft}m{\isacharcomma}\ a{\isacharcomma}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{constdefs}\isamarkupfalse%
-\isanewline
-\ \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ n\ {\isasymequiv}\ rec{\isacharparenleft}m{\isacharcomma}\ n{\isacharcomma}\ {\isasymlambda}x\ y{\isachardot}\ Suc{\isacharparenleft}y{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-This is an abstract version of the plain \isa{Nat} theory in
- FOL.\footnote{See
- \url{http://isabelle.in.tum.de/library/FOL/ex/Nat.html}} Basically,
- we have just replaced all occurrences of type \isa{nat} by \isa{{\isacharprime}a} and used the natural number axioms to define class \isa{nat}.
- There is only a minor snag, that the original recursion operator
- \isa{rec} had to be made monomorphic.
-
- Thus class \isa{nat} contains exactly those types \isa{{\isasymtau}} that
- are isomorphic to ``the'' natural numbers (with signature \isa{{\isasymzero}}, \isa{Suc}, \isa{rec}).
-
- \medskip What we have done here can be also viewed as \emph{type
- specification}. Of course, it still remains open if there is some
- type at all that meets the class axioms. Now a very nice property of
- axiomatic type classes is that abstract reasoning is always possible
- --- independent of satisfiability. The meta-logic won't break, even
- if some classes (or general sorts) turns out to be empty later ---
- ``inconsistent'' class definitions may be useless, but do not cause
- any harm.
-
- Theorems of the abstract natural numbers may be derived in the same
- way as for the concrete version. The original proof scripts may be
- re-used with some trivial changes only (mostly adding some type
- constraints).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-\isanewline
-%
-\endisadelimproof
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/AxClass/axclass.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{report}
-\usepackage{graphicx,../iman,../extra,../isar}
-\usepackage{../isabelle,../isabellesym}
-\usepackage{../pdfsetup} % last one!
-
-\isabellestyle{it}
-\newcommand{\isasyminv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymzero}{\isamath{0}}
-\renewcommand{\isasymone}{\isamath{1}}
-
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\hyphenation{Haskell}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Using Axiomatic Type Classes in Isabelle}
-\author{\emph{Markus Wenzel} \\ TU M\"unchen}
-
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-\pagestyle{headings}
-\sloppy
-\binperiod %%%treat . like a binary operator
-
-
-\begin{document}
-
-\underscoreoff
-
-\maketitle
-
-\begin{abstract}
- Isabelle offers order-sorted type classes on top of the simple types of
- plain Higher-Order Logic. The resulting type system is similar to that of
- the programming language Haskell. Its interpretation within the logic
- enables further application, though, apart from restricting polymorphism
- syntactically. In particular, the concept of \emph{Axiomatic Type Classes}
- provides a useful light-weight mechanism for hierarchically-structured
- abstract theories. Subsequently, we demonstrate typical uses of Isabelle's
- axiomatic type classes to model basic algebraic structures.
-
- This document describes axiomatic type classes using Isabelle/Isar theories,
- with proofs expressed via Isar proof language elements. The new theory
- format greatly simplifies the arrangement of the overall development, since
- definitions and proofs may be freely intermixed. Users who prefer tactic
- scripts over structured proofs do not need to fall back on separate ML
- scripts, though, but may refer to Isar's tactic emulation commands.
-\end{abstract}
-
-
-\pagenumbering{roman} \tableofcontents \clearfirst
-
-\include{body}
-
-%FIXME
-\nocite{nipkow-types93}
-\nocite{nipkow-sorts93}
-\nocite{Wenzel:1997:TPHOL}
-\nocite{paulson-isa-book}
-\nocite{isabelle-isar-ref}
-\nocite{Wenzel:1999:TPHOL}
-
-\begingroup
- \bibliographystyle{plain} \small\raggedright\frenchspacing
- \bibliography{../manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-% LocalWords: Isabelle FIXME
--- a/doc-src/AxClass/body.tex Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,166 +0,0 @@
-
-\chapter{Introduction}
-
-A Haskell-style type-system \cite{haskell-report} with ordered type-classes
-has been present in Isabelle since 1991 already \cite{nipkow-sorts93}.
-Initially, classes have mainly served as a \emph{purely syntactic} tool to
-formulate polymorphic object-logics in a clean way, such as the standard
-Isabelle formulation of many-sorted FOL \cite{paulson-isa-book}.
-
-Applying classes at the \emph{logical level} to provide a simple notion of
-abstract theories and instantiations to concrete ones, has been long proposed
-as well \cite{nipkow-types93,nipkow-sorts93}. At that time, Isabelle still
-lacked built-in support for these \emph{axiomatic type classes}. More
-importantly, their semantics was not yet fully fleshed out (and unnecessarily
-complicated, too).
-
-Since Isabelle94, actual axiomatic type classes have been an integral part of
-Isabelle's meta-logic. This very simple implementation is based on a
-straight-forward extension of traditional simply-typed Higher-Order Logic, by
-including types qualified by logical predicates and overloaded constant
-definitions (see \cite{Wenzel:1997:TPHOL} for further details).
-
-Yet even until Isabelle99, there used to be still a fundamental methodological
-problem in using axiomatic type classes conveniently, due to the traditional
-distinction of Isabelle theory files vs.\ ML proof scripts. This has been
-finally overcome with the advent of Isabelle/Isar theories
-\cite{isabelle-isar-ref}: now definitions and proofs may be freely intermixed.
-This nicely accommodates the usual procedure of defining axiomatic type
-classes, proving abstract properties, defining operations on concrete types,
-proving concrete properties for instantiation of classes etc.
-
-\medskip
-
-So to cut a long story short, the present version of axiomatic type classes
-now provides an even more useful and convenient mechanism for light-weight
-abstract theories, without any special technical provisions to be observed by
-the user.
-
-
-\chapter{Examples}\label{sec:ex}
-
-Axiomatic type classes are a concept of Isabelle's meta-logic
-\cite{paulson-isa-book,Wenzel:1997:TPHOL}. They may be applied to any
-object-logic that directly uses the meta type system, such as Isabelle/HOL
-\cite{isabelle-HOL}. Subsequently, we present various examples that are all
-formulated within HOL, except the one of \secref{sec:ex-natclass} which is in
-FOL. See also \url{http://isabelle.in.tum.de/library/HOL/AxClasses/} and
-\url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}.
-
-\input{Group/document/Semigroups}
-
-\input{Group/document/Group}
-
-\input{Group/document/Product}
-
-\input{Nat/document/NatClass}
-
-
-%% FIXME move some parts to ref or isar-ref manual (!?);
-
-% \chapter{The user interface of Isabelle's axclass package}
-
-% The actual axiomatic type class package of Isabelle/Pure mainly consists
-% of two new theory sections: \texttt{axclass} and \texttt{instance}. Some
-% typical applications of these have already been demonstrated in
-% \secref{sec:ex}, below their syntax and semantics are presented more
-% completely.
-
-
-% \section{The axclass section}
-
-% Within theory files, \texttt{axclass} introduces an axiomatic type class
-% definition. Its concrete syntax is:
-
-% \begin{matharray}{l}
-% \texttt{axclass} \\
-% \ \ c \texttt{ < } c@1\texttt, \ldots\texttt, c@n \\
-% \ \ id@1\ axm@1 \\
-% \ \ \vdots \\
-% \ \ id@m\ axm@m
-% \emphnd{matharray}
-
-% Where $c, c@1, \ldots, c@n$ are classes (category $id$ or
-% $string$) and $axm@1, \ldots, axm@m$ (with $m \geq
-% 0$) are formulas (category $string$).
-
-% Class $c$ has to be new, and sort $\{c@1, \ldots, c@n\}$ a subsort of
-% \texttt{logic}. Each class axiom $axm@j$ may contain any term
-% variables, but at most one type variable (which need not be the same
-% for all axioms). The sort of this type variable has to be a supersort
-% of $\{c@1, \ldots, c@n\}$.
-
-% \medskip
-
-% The \texttt{axclass} section declares $c$ as subclass of $c@1, \ldots,
-% c@n$ to the type signature.
-
-% Furthermore, $axm@1, \ldots, axm@m$ are turned into the
-% ``abstract axioms'' of $c$ with names $id@1, \ldots,
-% id@m$. This is done by replacing all occurring type variables
-% by $\alpha :: c$. Original axioms that do not contain any type
-% variable will be prefixed by the logical precondition
-% $\texttt{OFCLASS}(\alpha :: \texttt{logic}, c\texttt{_class})$.
-
-% Another axiom of name $c\texttt{I}$ --- the ``class $c$ introduction
-% rule'' --- is built from the respective universal closures of
-% $axm@1, \ldots, axm@m$ appropriately.
-
-
-% \section{The instance section}
-
-% Section \texttt{instance} proves class inclusions or type arities at the
-% logical level and then transfers these into the type signature.
-
-% Its concrete syntax is:
-
-% \begin{matharray}{l}
-% \texttt{instance} \\
-% \ \ [\ c@1 \texttt{ < } c@2 \ |\
-% t \texttt{ ::\ (}sort@1\texttt, \ldots \texttt, sort@n\texttt) sort\ ] \\
-% \ \ [\ \texttt(name@1 \texttt, \ldots\texttt, name@m\texttt)\ ] \\
-% \ \ [\ \texttt{\{|} text \texttt{|\}}\ ]
-% \emphnd{matharray}
-
-% Where $c@1, c@2$ are classes and $t$ is an $n$-place type constructor
-% (all of category $id$ or $string)$. Furthermore,
-% $sort@i$ are sorts in the usual Isabelle-syntax.
-
-% \medskip
-
-% Internally, \texttt{instance} first sets up an appropriate goal that
-% expresses the class inclusion or type arity as a meta-proposition.
-% Then tactic \texttt{AxClass.axclass_tac} is applied with all preceding
-% meta-definitions of the current theory file and the user-supplied
-% witnesses. The latter are $name@1, \ldots, name@m$, where
-% $id$ refers to an \ML-name of a theorem, and $string$ to an
-% axiom of the current theory node\footnote{Thus, the user may reference
-% axioms from above this \texttt{instance} in the theory file. Note
-% that new axioms appear at the \ML-toplevel only after the file is
-% processed completely.}.
-
-% Tactic \texttt{AxClass.axclass_tac} first unfolds the class definition by
-% resolving with rule $c\texttt\texttt{I}$, and then applies the witnesses
-% according to their form: Meta-definitions are unfolded, all other
-% formulas are repeatedly resolved\footnote{This is done in a way that
-% enables proper object-\emph{rules} to be used as witnesses for
-% corresponding class axioms.} with.
-
-% The final optional argument $text$ is \ML-code of an arbitrary
-% user tactic which is applied last to any remaining goals.
-
-% \medskip
-
-% Because of the complexity of \texttt{instance}'s witnessing mechanisms,
-% new users of the axclass package are advised to only use the simple
-% form $\texttt{instance}\ \ldots\ (id@1, \ldots, id@!m)$, where
-% the identifiers refer to theorems that are appropriate type instances
-% of the class axioms. This typically requires an auxiliary theory,
-% though, which defines some constants and then proves these witnesses.
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "axclass"
-%%% End:
-% LocalWords: Isabelle FOL
--- a/src/HOL/AxClasses/Group.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-(* Title: HOL/AxClasses/Group.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-theory Group imports Main begin
-
-subsection {* Monoids and Groups *}
-
-consts
- times :: "'a => 'a => 'a" (infixl "[*]" 70)
- invers :: "'a => 'a"
- one :: 'a
-
-
-axclass monoid < type
- assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
- left_unit: "one [*] x = x"
- right_unit: "x [*] one = x"
-
-axclass semigroup < type
- assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
-
-axclass group < semigroup
- left_unit: "one [*] x = x"
- left_inverse: "invers x [*] x = one"
-
-axclass agroup < group
- commute: "x [*] y = y [*] x"
-
-
-subsection {* Abstract reasoning *}
-
-theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
-proof -
- have "x [*] invers x = one [*] (x [*] invers x)"
- by (simp only: group_class.left_unit)
- also have "... = one [*] x [*] invers x"
- by (simp only: semigroup_class.assoc)
- also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
- by (simp only: group_class.left_inverse)
- also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
- by (simp only: semigroup_class.assoc)
- also have "... = invers (invers x) [*] one [*] invers x"
- by (simp only: group_class.left_inverse)
- also have "... = invers (invers x) [*] (one [*] invers x)"
- by (simp only: semigroup_class.assoc)
- also have "... = invers (invers x) [*] invers x"
- by (simp only: group_class.left_unit)
- also have "... = one"
- by (simp only: group_class.left_inverse)
- finally show ?thesis .
-qed
-
-theorem group_right_unit: "x [*] one = (x::'a::group)"
-proof -
- have "x [*] one = x [*] (invers x [*] x)"
- by (simp only: group_class.left_inverse)
- also have "... = x [*] invers x [*] x"
- by (simp only: semigroup_class.assoc)
- also have "... = one [*] x"
- by (simp only: group_right_inverse)
- also have "... = x"
- by (simp only: group_class.left_unit)
- finally show ?thesis .
-qed
-
-
-subsection {* Abstract instantiation *}
-
-instance monoid < semigroup
-proof intro_classes
- fix x y z :: "'a::monoid"
- show "x [*] y [*] z = x [*] (y [*] z)"
- by (rule monoid_class.assoc)
-qed
-
-instance group < monoid
-proof intro_classes
- fix x y z :: "'a::group"
- show "x [*] y [*] z = x [*] (y [*] z)"
- by (rule semigroup_class.assoc)
- show "one [*] x = x"
- by (rule group_class.left_unit)
- show "x [*] one = x"
- by (rule group_right_unit)
-qed
-
-
-subsection {* Concrete instantiation *}
-
-defs (overloaded)
- times_bool_def: "x [*] y == x ~= (y::bool)"
- inverse_bool_def: "invers x == x::bool"
- unit_bool_def: "one == False"
-
-instance bool :: agroup
-proof (intro_classes,
- unfold times_bool_def inverse_bool_def unit_bool_def)
- fix x y z
- show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast
- show "(False ~= x) = x" by blast
- show "(x ~= x) = False" by blast
- show "(x ~= y) = (y ~= x)" by blast
-qed
-
-
-subsection {* Lifting and Functors *}
-
-defs (overloaded)
- times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"
-
-instance * :: (semigroup, semigroup) semigroup
-proof (intro_classes, unfold times_prod_def)
- fix p q r :: "'a::semigroup * 'b::semigroup"
- show
- "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r,
- snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
- (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
- snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"
- by (simp add: semigroup_class.assoc)
-qed
-
-end
--- a/src/HOL/AxClasses/Lattice/OrdInsts.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: OrdInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some order instantiations.
-*)
-
-OrdInsts = OrdDefs +
-
-
-(* binary / general products of quasi_orders / orders *)
-
-instance
- "*" :: (quasi_order, quasi_order) quasi_order (le_prod_refl, le_prod_trans)
-
-instance
- "*" :: (partial_order, partial_order) partial_order (le_prod_antisym)
-
-
-instance
- fun :: (term, quasi_order) quasi_order (le_fun_refl, le_fun_trans)
-
-instance
- fun :: (term, partial_order) partial_order (le_fun_antisym)
-
-
-(* duals of quasi orders / partial orders / linear orders *)
-
-instance
- dual :: (quasi_order) quasi_order (le_dual_refl, le_dual_trans)
-
-instance
- dual :: (partial_order) partial_order (le_dual_antisym)
-
-
-(*FIXME: had to be moved to LatInsts.thy due to some unpleasant
- 'feature' in Pure/type.ML
-
-instance
- dual :: (linear_order) linear_order (le_dual_lin)
-*)
-
-end
--- a/src/HOL/AxClasses/Product.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOL/AxClasses/Product.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-theory Product imports Main begin
-
-axclass product < type
-
-consts
- product :: "'a::product => 'a => 'a" (infixl "[*]" 70)
-
-
-instance bool :: product
- by intro_classes
-
-defs (overloaded)
- product_bool_def: "x [*] y == x & y"
-
-end
--- a/src/HOL/AxClasses/README.html Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<html>
-
-<head>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <title>HOL/AxClasses</title>
-</head>
-
-<body>
-<h1>HOL/AxClasses</h1>
-
-These are the HOL examples of the tutorial <a
-href="http://isabelle.in.tum.de/dist/Isabelle/doc/axclass.pdf">Using Axiomatic Type
-Classes in Isabelle</a>. See also FOL/ex/NatClass for the natural
-number example.
-</body>
-</html>
--- a/src/HOL/AxClasses/ROOT.ML Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(* $Id$ *)
-
-use_thys ["Semigroups", "Group", "Product"];
--- a/src/HOL/AxClasses/Semigroups.thy Sun Feb 15 21:26:25 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* Title: HOL/AxClasses/Semigroups.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-*)
-
-theory Semigroups imports Main begin
-
-consts
- times :: "'a => 'a => 'a" (infixl "[*]" 70)
-
-axclass semigroup < type
- assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
-
-
-consts
- plus :: "'a => 'a => 'a" (infixl "[+]" 70)
-
-axclass plus_semigroup < type
- assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
-
-end
--- a/src/HOL/IsaMakefile Sun Feb 15 21:26:25 2009 +0100
+++ b/src/HOL/IsaMakefile Mon Feb 16 12:27:30 2009 +0100
@@ -13,7 +13,6 @@
HOL-Library \
HOL-ex \
HOL-Auth \
- HOL-AxClasses \
HOL-Bali \
HOL-Extraction \
HOL-HahnBanach \
@@ -770,15 +769,6 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
-## HOL-AxClasses
-
-HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
-
-$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
- AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
-
-
## HOL-Lattice
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
@@ -1045,22 +1035,22 @@
## clean
clean:
- @rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL $(OUT)/HOL-Nominal $(OUT)/TLA \
- $(LOG)/HOL.gz $(LOG)/TLA.gz \
- $(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
- $(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
- $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
- $(LOG)/HOL-HoareParallel.gz \
- $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
- $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
- $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
- $(LOG)/HOL-Bali.gz \
- $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
- $(LOG)/HOL-Nominal-Examples.gz \
- $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
- $(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
- $(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
- $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
- $(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz \
- $(OUT)/HOL-Word $(LOG)/HOL-Word.gz $(LOG)/HOL-Word-Examples.gz \
- $(OUT)/HOL-NSA $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz
+ @rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL \
+ $(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz \
+ $(LOG)/TLA.gz $(LOG)/HOL-Isar_examples.gz \
+ $(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz \
+ $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
+ $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
+ $(LOG)/HOL-HoareParallel.gz $(LOG)/HOL-Lex.gz \
+ $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \
+ $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz \
+ $(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz \
+ $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
+ $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz \
+ $(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
+ $(LOG)/HOL-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
+ $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
+ $(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz \
+ $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \
+ $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \
+ $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz