--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/Classes.thy Mon Aug 27 22:31:16 2012 +0200
@@ -0,0 +1,642 @@
+theory Classes
+imports Main Setup
+begin
+
+section {* Introduction *}
+
+text {*
+ Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ into the Haskell language to allow for a reasonable implementation
+ of overloading\footnote{throughout this tutorial, we are referring
+ to classical Haskell 1.0 type classes, not considering later
+ additions in expressiveness}. As a canonical example, a polymorphic
+ equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
+ different types for @{text "\<alpha>"}, which is achieved by splitting
+ introduction of the @{text eq} function from its overloaded
+ definitions by means of @{text class} and @{text instance}
+ declarations: \footnote{syntax here is a kind of isabellized
+ Haskell}
+
+ \begin{quote}
+
+ \noindent@{text "class eq where"} \\
+ \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+
+ \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
+ \hspace*{2ex}@{text "eq 0 0 = True"} \\
+ \hspace*{2ex}@{text "eq 0 _ = False"} \\
+ \hspace*{2ex}@{text "eq _ 0 = False"} \\
+ \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
+
+ \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+ \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
+
+ \medskip\noindent@{text "class ord extends eq where"} \\
+ \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+
+ \end{quote}
+
+ \noindent Type variables are annotated with (finitely many) classes;
+ these annotations are assertions that a particular polymorphic type
+ provides definitions for overloaded functions.
+
+ Indeed, type classes not only allow for simple overloading but form
+ a generic calculus, an instance of order-sorted algebra
+ \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+
+ From a software engineering point of view, type classes roughly
+ correspond to interfaces in object-oriented languages like Java; so,
+ it is naturally desirable that type classes do not only provide
+ functions (class parameters) but also state specifications
+ implementations must obey. For example, the @{text "class eq"}
+ above could be given the following specification, demanding that
+ @{text "class eq"} is an equivalence relation obeying reflexivity,
+ symmetry and transitivity:
+
+ \begin{quote}
+
+ \noindent@{text "class eq where"} \\
+ \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ @{text "satisfying"} \\
+ \hspace*{2ex}@{text "refl: eq x x"} \\
+ \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
+ \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+
+ \end{quote}
+
+ \noindent From a theoretical point of view, type classes are
+ lightweight modules; Haskell type classes may be emulated by SML
+ functors \cite{classes_modules}. Isabelle/Isar offers a discipline
+ of type classes which brings all those aspects together:
+
+ \begin{enumerate}
+ \item specifying abstract parameters together with
+ corresponding specifications,
+ \item instantiating those abstract parameters by a particular
+ type
+ \item in connection with a ``less ad-hoc'' approach to overloading,
+ \item with a direct link to the Isabelle module system:
+ locales \cite{kammueller-locales}.
+ \end{enumerate}
+
+ \noindent Isar type classes also directly support code generation in
+ a Haskell like fashion. Internally, they are mapped to more
+ primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+
+ This tutorial demonstrates common elements of structured
+ specifications and abstract reasoning with type classes by the
+ algebraic hierarchy of semigroups, monoids and groups. Our
+ background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
+ which some familiarity is assumed.
+*}
+
+section {* A simple algebra example \label{sec:example} *}
+
+subsection {* Class definition *}
+
+text {*
+ Depending on an arbitrary type @{text "\<alpha>"}, class @{text
+ "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
+ assumed to be associative:
+*}
+
+class %quote semigroup =
+ fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
+ assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+
+text {*
+ \noindent This @{command class} specification consists of two parts:
+ the \qn{operational} part names the class parameter (@{element
+ "fixes"}), the \qn{logical} part specifies properties on them
+ (@{element "assumes"}). The local @{element "fixes"} and @{element
+ "assumes"} are lifted to the theory toplevel, yielding the global
+ parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+ global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+*}
+
+
+subsection {* Class instantiation \label{sec:class_inst} *}
+
+text {*
+ The concrete type @{typ int} is made a @{class semigroup} instance
+ by providing a suitable definition for the class parameter @{text
+ "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is
+ accomplished by the @{command instantiation} target:
+*}
+
+instantiation %quote int :: semigroup
+begin
+
+definition %quote
+ mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+
+instance %quote proof
+ fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
+ then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+ unfolding mult_int_def .
+qed
+
+end %quote
+
+text {*
+ \noindent @{command instantiation} defines class parameters at a
+ particular instance using common specification tools (here,
+ @{command definition}). The concluding @{command instance} opens a
+ proof that the given parameters actually conform to the class
+ specification. Note that the first proof step is the @{method
+ default} method, which for such instance proofs maps to the @{method
+ intro_classes} method. This reduces an instance judgement to the
+ relevant primitive proof goals; typically it is the first method
+ applied in an instantiation proof.
+
+ From now on, the type-checker will consider @{typ int} as a @{class
+ semigroup} automatically, i.e.\ any general results are immediately
+ available on concrete instances.
+
+ \medskip Another instance of @{class semigroup} yields the natural
+ numbers:
+*}
+
+instantiation %quote nat :: semigroup
+begin
+
+primrec %quote mult_nat where
+ "(0\<Colon>nat) \<otimes> n = n"
+ | "Suc m \<otimes> n = Suc (m \<otimes> n)"
+
+instance %quote proof
+ fix m n q :: nat
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+ by (induct m) auto
+qed
+
+end %quote
+
+text {*
+ \noindent Note the occurence of the name @{text mult_nat} in the
+ primrec declaration; by default, the local name of a class operation
+ @{text f} to be instantiated on type constructor @{text \<kappa>} is
+ mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
+ inspected using the @{command "print_context"} command or the
+ corresponding ProofGeneral button.
+*}
+
+subsection {* Lifting and parametric types *}
+
+text {*
+ Overloaded definitions given at a class instantiation may include
+ recursion over the syntactic structure of types. As a canonical
+ example, we model product semigroups using our simple algebra:
+*}
+
+instantiation %quote prod :: (semigroup, semigroup) semigroup
+begin
+
+definition %quote
+ mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+
+instance %quote proof
+ fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+ show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+ unfolding mult_prod_def by (simp add: assoc)
+qed
+
+end %quote
+
+text {*
+ \noindent Associativity of product semigroups is established using
+ the definition of @{text "(\<otimes>)"} on products and the hypothetical
+ associativity of the type components; these hypotheses are
+ legitimate due to the @{class semigroup} constraints imposed on the
+ type components by the @{command instance} proposition. Indeed,
+ this pattern often occurs with parametric types and type classes.
+*}
+
+
+subsection {* Subclassing *}
+
+text {*
+ We define a subclass @{text monoidl} (a semigroup with a left-hand
+ neutral) by extending @{class semigroup} with one additional
+ parameter @{text neutral} together with its characteristic property:
+*}
+
+class %quote monoidl = semigroup +
+ fixes neutral :: "\<alpha>" ("\<one>")
+ assumes neutl: "\<one> \<otimes> x = x"
+
+text {*
+ \noindent Again, we prove some instances, by providing suitable
+ parameter definitions and proofs for the additional specifications.
+ Observe that instantiations for types with the same arity may be
+ simultaneous:
+*}
+
+instantiation %quote nat and int :: monoidl
+begin
+
+definition %quote
+ neutral_nat_def: "\<one> = (0\<Colon>nat)"
+
+definition %quote
+ neutral_int_def: "\<one> = (0\<Colon>int)"
+
+instance %quote proof
+ fix n :: nat
+ show "\<one> \<otimes> n = n"
+ unfolding neutral_nat_def by simp
+next
+ fix k :: int
+ show "\<one> \<otimes> k = k"
+ unfolding neutral_int_def mult_int_def by simp
+qed
+
+end %quote
+
+instantiation %quote prod :: (monoidl, monoidl) monoidl
+begin
+
+definition %quote
+ neutral_prod_def: "\<one> = (\<one>, \<one>)"
+
+instance %quote proof
+ fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
+ show "\<one> \<otimes> p = p"
+ unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
+qed
+
+end %quote
+
+text {*
+ \noindent Fully-fledged monoids are modelled by another subclass,
+ which does not add new parameters but tightens the specification:
+*}
+
+class %quote monoid = monoidl +
+ assumes neutr: "x \<otimes> \<one> = x"
+
+instantiation %quote nat and int :: monoid
+begin
+
+instance %quote proof
+ fix n :: nat
+ show "n \<otimes> \<one> = n"
+ unfolding neutral_nat_def by (induct n) simp_all
+next
+ fix k :: int
+ show "k \<otimes> \<one> = k"
+ unfolding neutral_int_def mult_int_def by simp
+qed
+
+end %quote
+
+instantiation %quote prod :: (monoid, monoid) monoid
+begin
+
+instance %quote proof
+ fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
+ show "p \<otimes> \<one> = p"
+ unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
+qed
+
+end %quote
+
+text {*
+ \noindent To finish our small algebra example, we add a @{text
+ group} class with a corresponding instance:
+*}
+
+class %quote group = monoidl +
+ fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
+ assumes invl: "x\<div> \<otimes> x = \<one>"
+
+instantiation %quote int :: group
+begin
+
+definition %quote
+ inverse_int_def: "i\<div> = - (i\<Colon>int)"
+
+instance %quote proof
+ fix i :: int
+ have "-i + i = 0" by simp
+ then show "i\<div> \<otimes> i = \<one>"
+ unfolding mult_int_def neutral_int_def inverse_int_def .
+qed
+
+end %quote
+
+
+section {* Type classes as locales *}
+
+subsection {* A look behind the scenes *}
+
+text {*
+ The example above gives an impression how Isar type classes work in
+ practice. As stated in the introduction, classes also provide a
+ link to Isar's locale system. Indeed, the logical core of a class
+ is nothing other than a locale:
+*}
+
+class %quote idem =
+ fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
+ assumes idem: "f (f x) = f x"
+
+text {*
+ \noindent essentially introduces the locale
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
+locale %quote idem =
+ fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
+ assumes idem: "f (f x) = f x"
+
+text {* \noindent together with corresponding constant(s): *}
+
+consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
+
+text {*
+ \noindent The connection to the type system is done by means
+ of a primitive type class
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
+classes %quote idem < type
+(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
+setup %invisible {* Sign.parent_path *}(*>*)
+
+text {* \noindent together with a corresponding interpretation: *}
+
+interpretation %quote idem_class:
+ idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
+(*<*)proof qed (rule idem)(*>*)
+
+text {*
+ \noindent This gives you the full power of the Isabelle module system;
+ conclusions in locale @{text idem} are implicitly propagated
+ to class @{text idem}.
+*} (*<*)setup %invisible {* Sign.parent_path *}
+(*>*)
+subsection {* Abstract reasoning *}
+
+text {*
+ Isabelle locales enable reasoning at a general level, while results
+ are implicitly transferred to all instances. For example, we can
+ now establish the @{text "left_cancel"} lemma for groups, which
+ states that the function @{text "(x \<otimes>)"} is injective:
+*}
+
+lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
+proof
+ assume "x \<otimes> y = x \<otimes> z"
+ then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
+ then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
+ then show "y = z" using neutl and invl by simp
+next
+ assume "y = z"
+ then show "x \<otimes> y = x \<otimes> z" by simp
+qed
+
+text {*
+ \noindent Here the \qt{@{keyword "in"} @{class group}} target
+ specification indicates that the result is recorded within that
+ context for later use. This local theorem is also lifted to the
+ global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
+ \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been
+ made an instance of @{text "group"} before, we may refer to that
+ fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
+ z"}.
+*}
+
+
+subsection {* Derived definitions *}
+
+text {*
+ Isabelle locales are targets which support local definitions:
+*}
+
+primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+ "pow_nat 0 x = \<one>"
+ | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+
+text {*
+ \noindent If the locale @{text group} is also a class, this local
+ definition is propagated onto a global definition of @{term [source]
+ "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
+
+ @{thm pow_nat.simps [no_vars]}.
+
+ \noindent As you can see from this example, for local definitions
+ you may use any specification tool which works together with
+ locales, such as Krauss's recursive function package
+ \cite{krauss2006}.
+*}
+
+
+subsection {* A functor analogy *}
+
+text {*
+ We introduced Isar classes by analogy to type classes in functional
+ programming; if we reconsider this in the context of what has been
+ said about type classes and locales, we can drive this analogy
+ further by stating that type classes essentially correspond to
+ functors that have a canonical interpretation as type classes.
+ There is also the possibility of other interpretations. For
+ example, @{text list}s also form a monoid with @{text append} and
+ @{term "[]"} as operations, but it seems inappropriate to apply to
+ lists the same operations as for genuinely algebraic types. In such
+ a case, we can simply make a particular interpretation of monoids
+ for lists:
+*}
+
+interpretation %quote list_monoid: monoid append "[]"
+ proof qed auto
+
+text {*
+ \noindent This enables us to apply facts on monoids
+ to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
+
+ When using this interpretation pattern, it may also
+ be appropriate to map derived definitions accordingly:
+*}
+
+primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
+ "replicate 0 _ = []"
+ | "replicate (Suc n) xs = xs @ replicate n xs"
+
+interpretation %quote list_monoid: monoid append "[]" where
+ "monoid.pow_nat append [] = replicate"
+proof -
+ interpret monoid append "[]" ..
+ show "monoid.pow_nat append [] = replicate"
+ proof
+ fix n
+ show "monoid.pow_nat append [] n = replicate n"
+ by (induct n) auto
+ qed
+qed intro_locales
+
+text {*
+ \noindent This pattern is also helpful to reuse abstract
+ specifications on the \emph{same} type. For example, think of a
+ class @{text preorder}; for type @{typ nat}, there are at least two
+ possible instances: the natural order or the order induced by the
+ divides relation. But only one of these instances can be used for
+ @{command instantiation}; using the locale behind the class @{text
+ preorder}, it is still possible to utilise the same abstract
+ specification again using @{command interpretation}.
+*}
+
+subsection {* Additional subclass relations *}
+
+text {*
+ Any @{text "group"} is also a @{text "monoid"}; this can be made
+ explicit by claiming an additional subclass relation, together with
+ a proof of the logical difference:
+*}
+
+subclass %quote (in group) monoid
+proof
+ fix x
+ from invl have "x\<div> \<otimes> x = \<one>" by simp
+ with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
+ with left_cancel show "x \<otimes> \<one> = x" by simp
+qed
+
+text {*
+ The logical proof is carried out on the locale level. Afterwards it
+ is propagated to the type system, making @{text group} an instance
+ of @{text monoid} by adding an additional edge to the graph of
+ subclass relations (\figref{fig:subclass}).
+
+ \begin{figure}[htbp]
+ \begin{center}
+ \small
+ \unitlength 0.6mm
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(25,35){\vector(1,-3){10}}
+ \end{picture}
+ \hspace{8em}
+ \begin{picture}(40,60)(0,0)
+ \put(20,60){\makebox(0,0){@{text semigroup}}}
+ \put(20,40){\makebox(0,0){@{text monoidl}}}
+ \put(00,20){\makebox(0,0){@{text monoid}}}
+ \put(40,00){\makebox(0,0){@{text group}}}
+ \put(20,55){\vector(0,-1){10}}
+ \put(15,35){\vector(-1,-1){10}}
+ \put(05,15){\vector(3,-1){30}}
+ \end{picture}
+ \caption{Subclass relationship of monoids and groups:
+ before and after establishing the relationship
+ @{text "group \<subseteq> monoid"}; transitive edges are left out.}
+ \label{fig:subclass}
+ \end{center}
+ \end{figure}
+
+ For illustration, a derived definition in @{text group} using @{text
+ pow_nat}
+*}
+
+definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+ "pow_int k x = (if k >= 0
+ then pow_nat (nat k) x
+ else (pow_nat (nat (- k)) x)\<div>)"
+
+text {*
+ \noindent yields the global definition of @{term [source] "pow_int \<Colon>
+ int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
+ pow_int_def [no_vars]}.
+*}
+
+subsection {* A note on syntax *}
+
+text {*
+ As a convenience, class context syntax allows references to local
+ class operations and their global counterparts uniformly; type
+ inference resolves ambiguities. For example:
+*}
+
+context %quote semigroup
+begin
+
+term %quote "x \<otimes> y" -- {* example 1 *}
+term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+
+end %quote
+
+term %quote "x \<otimes> y" -- {* example 3 *}
+
+text {*
+ \noindent Here in example 1, the term refers to the local class
+ operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
+ constraint enforces the global class operation @{text "mult [nat]"}.
+ In the global context in example 3, the reference is to the
+ polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
+*}
+
+section {* Further issues *}
+
+subsection {* Type classes and code generation *}
+
+text {*
+ Turning back to the first motivation for type classes, namely
+ overloading, it is obvious that overloading stemming from @{command
+ class} statements and @{command instantiation} targets naturally
+ maps to Haskell type classes. The code generator framework
+ \cite{isabelle-codegen} takes this into account. If the target
+ language (e.g.~SML) lacks type classes, then they are implemented by
+ an explicit dictionary construction. As example, let's go back to
+ the power function:
+*}
+
+definition %quote example :: int where
+ "example = pow_int 10 (-2)"
+
+text {*
+ \noindent This maps to Haskell as follows:
+*}
+(*<*)code_include %invisible Haskell "Natural" -(*>*)
+text %quotetypewriter {*
+ @{code_stmts example (Haskell)}
+*}
+
+text {*
+ \noindent The code in SML has explicit dictionary passing:
+*}
+text %quotetypewriter {*
+ @{code_stmts example (SML)}
+*}
+
+
+text {*
+ \noindent In Scala, implicts are used as dictionaries:
+*}
+(*<*)code_include %invisible Scala "Natural" -(*>*)
+text %quotetypewriter {*
+ @{code_stmts example (Scala)}
+*}
+
+
+subsection {* Inspecting the type class universe *}
+
+text {*
+ To facilitate orientation in complex subclass structures, two
+ diagnostics commands are provided:
+
+ \begin{description}
+
+ \item[@{command "print_classes"}] print a list of all classes
+ together with associated operations etc.
+
+ \item[@{command "class_deps"}] visualizes the subclass relation
+ between all classes as a Hasse diagram.
+
+ \end{description}
+*}
+
+end
--- a/doc-src/Classes/Makefile Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = classes
-
-FILES = $(NAME).tex classes.tex Thy/document/Classes.tex \
- style.sty ../iman.sty ../extra.sty ../isar.sty \
- ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty \
- ../manual.bib ../proof.sty
-
-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)
- $(BIBTEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(FIXBOOKMARKS) $(NAME).out
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/Setup.thy Mon Aug 27 22:31:16 2012 +0200
@@ -0,0 +1,40 @@
+theory Setup
+imports Main "~~/src/HOL/Library/Code_Integer"
+begin
+
+ML_file "../antiquote_setup.ML"
+ML_file "../more_antiquote.ML"
+
+setup {*
+ Antiquote_Setup.setup #>
+ More_Antiquote.setup #>
+ Code_Target.set_default_code_width 74
+*}
+
+syntax
+ "_alpha" :: "type" ("\<alpha>")
+ "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
+ "_beta" :: "type" ("\<beta>")
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
+
+parse_ast_translation {*
+ let
+ fun alpha_ast_tr [] = Ast.Variable "'a"
+ | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
+ fun alpha_ofsort_ast_tr [ast] =
+ Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
+ | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
+ fun beta_ast_tr [] = Ast.Variable "'b"
+ | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
+ fun beta_ofsort_ast_tr [ast] =
+ Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
+ | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
+ in
+ [(@{syntax_const "_alpha"}, alpha_ast_tr),
+ (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
+ (@{syntax_const "_beta"}, beta_ast_tr),
+ (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
+ end
+*}
+
+end
\ No newline at end of file
--- a/doc-src/Classes/Thy/Classes.thy Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,642 +0,0 @@
-theory Classes
-imports Main Setup
-begin
-
-section {* Introduction *}
-
-text {*
- Type classes were introduced by Wadler and Blott \cite{wadler89how}
- into the Haskell language to allow for a reasonable implementation
- of overloading\footnote{throughout this tutorial, we are referring
- to classical Haskell 1.0 type classes, not considering later
- additions in expressiveness}. As a canonical example, a polymorphic
- equality function @{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on
- different types for @{text "\<alpha>"}, which is achieved by splitting
- introduction of the @{text eq} function from its overloaded
- definitions by means of @{text class} and @{text instance}
- declarations: \footnote{syntax here is a kind of isabellized
- Haskell}
-
- \begin{quote}
-
- \noindent@{text "class eq where"} \\
- \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
-
- \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
- \hspace*{2ex}@{text "eq 0 0 = True"} \\
- \hspace*{2ex}@{text "eq 0 _ = False"} \\
- \hspace*{2ex}@{text "eq _ 0 = False"} \\
- \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
-
- \medskip\noindent@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
- \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
-
- \medskip\noindent@{text "class ord extends eq where"} \\
- \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
-
- \end{quote}
-
- \noindent Type variables are annotated with (finitely many) classes;
- these annotations are assertions that a particular polymorphic type
- provides definitions for overloaded functions.
-
- Indeed, type classes not only allow for simple overloading but form
- a generic calculus, an instance of order-sorted algebra
- \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
-
- From a software engineering point of view, type classes roughly
- correspond to interfaces in object-oriented languages like Java; so,
- it is naturally desirable that type classes do not only provide
- functions (class parameters) but also state specifications
- implementations must obey. For example, the @{text "class eq"}
- above could be given the following specification, demanding that
- @{text "class eq"} is an equivalence relation obeying reflexivity,
- symmetry and transitivity:
-
- \begin{quote}
-
- \noindent@{text "class eq where"} \\
- \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- @{text "satisfying"} \\
- \hspace*{2ex}@{text "refl: eq x x"} \\
- \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
- \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
-
- \end{quote}
-
- \noindent From a theoretical point of view, type classes are
- lightweight modules; Haskell type classes may be emulated by SML
- functors \cite{classes_modules}. Isabelle/Isar offers a discipline
- of type classes which brings all those aspects together:
-
- \begin{enumerate}
- \item specifying abstract parameters together with
- corresponding specifications,
- \item instantiating those abstract parameters by a particular
- type
- \item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system:
- locales \cite{kammueller-locales}.
- \end{enumerate}
-
- \noindent Isar type classes also directly support code generation in
- a Haskell like fashion. Internally, they are mapped to more
- primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
-
- This tutorial demonstrates common elements of structured
- specifications and abstract reasoning with type classes by the
- algebraic hierarchy of semigroups, monoids and groups. Our
- background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
- which some familiarity is assumed.
-*}
-
-section {* A simple algebra example \label{sec:example} *}
-
-subsection {* Class definition *}
-
-text {*
- Depending on an arbitrary type @{text "\<alpha>"}, class @{text
- "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
- assumed to be associative:
-*}
-
-class %quote semigroup =
- fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
-
-text {*
- \noindent This @{command class} specification consists of two parts:
- the \qn{operational} part names the class parameter (@{element
- "fixes"}), the \qn{logical} part specifies properties on them
- (@{element "assumes"}). The local @{element "fixes"} and @{element
- "assumes"} are lifted to the theory toplevel, yielding the global
- parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
- global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y z \<Colon>
- \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
-*}
-
-
-subsection {* Class instantiation \label{sec:class_inst} *}
-
-text {*
- The concrete type @{typ int} is made a @{class semigroup} instance
- by providing a suitable definition for the class parameter @{text
- "(\<otimes>)"} and a proof for the specification of @{fact assoc}. This is
- accomplished by the @{command instantiation} target:
-*}
-
-instantiation %quote int :: semigroup
-begin
-
-definition %quote
- mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
-
-instance %quote proof
- fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
- then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
- unfolding mult_int_def .
-qed
-
-end %quote
-
-text {*
- \noindent @{command instantiation} defines class parameters at a
- particular instance using common specification tools (here,
- @{command definition}). The concluding @{command instance} opens a
- proof that the given parameters actually conform to the class
- specification. Note that the first proof step is the @{method
- default} method, which for such instance proofs maps to the @{method
- intro_classes} method. This reduces an instance judgement to the
- relevant primitive proof goals; typically it is the first method
- applied in an instantiation proof.
-
- From now on, the type-checker will consider @{typ int} as a @{class
- semigroup} automatically, i.e.\ any general results are immediately
- available on concrete instances.
-
- \medskip Another instance of @{class semigroup} yields the natural
- numbers:
-*}
-
-instantiation %quote nat :: semigroup
-begin
-
-primrec %quote mult_nat where
- "(0\<Colon>nat) \<otimes> n = n"
- | "Suc m \<otimes> n = Suc (m \<otimes> n)"
-
-instance %quote proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) auto
-qed
-
-end %quote
-
-text {*
- \noindent Note the occurence of the name @{text mult_nat} in the
- primrec declaration; by default, the local name of a class operation
- @{text f} to be instantiated on type constructor @{text \<kappa>} is
- mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
- inspected using the @{command "print_context"} command or the
- corresponding ProofGeneral button.
-*}
-
-subsection {* Lifting and parametric types *}
-
-text {*
- Overloaded definitions given at a class instantiation may include
- recursion over the syntactic structure of types. As a canonical
- example, we model product semigroups using our simple algebra:
-*}
-
-instantiation %quote prod :: (semigroup, semigroup) semigroup
-begin
-
-definition %quote
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
-
-instance %quote proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
- unfolding mult_prod_def by (simp add: assoc)
-qed
-
-end %quote
-
-text {*
- \noindent Associativity of product semigroups is established using
- the definition of @{text "(\<otimes>)"} on products and the hypothetical
- associativity of the type components; these hypotheses are
- legitimate due to the @{class semigroup} constraints imposed on the
- type components by the @{command instance} proposition. Indeed,
- this pattern often occurs with parametric types and type classes.
-*}
-
-
-subsection {* Subclassing *}
-
-text {*
- We define a subclass @{text monoidl} (a semigroup with a left-hand
- neutral) by extending @{class semigroup} with one additional
- parameter @{text neutral} together with its characteristic property:
-*}
-
-class %quote monoidl = semigroup +
- fixes neutral :: "\<alpha>" ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
-
-text {*
- \noindent Again, we prove some instances, by providing suitable
- parameter definitions and proofs for the additional specifications.
- Observe that instantiations for types with the same arity may be
- simultaneous:
-*}
-
-instantiation %quote nat and int :: monoidl
-begin
-
-definition %quote
- neutral_nat_def: "\<one> = (0\<Colon>nat)"
-
-definition %quote
- neutral_int_def: "\<one> = (0\<Colon>int)"
-
-instance %quote proof
- fix n :: nat
- show "\<one> \<otimes> n = n"
- unfolding neutral_nat_def by simp
-next
- fix k :: int
- show "\<one> \<otimes> k = k"
- unfolding neutral_int_def mult_int_def by simp
-qed
-
-end %quote
-
-instantiation %quote prod :: (monoidl, monoidl) monoidl
-begin
-
-definition %quote
- neutral_prod_def: "\<one> = (\<one>, \<one>)"
-
-instance %quote proof
- fix p :: "\<alpha>\<Colon>monoidl \<times> \<beta>\<Colon>monoidl"
- show "\<one> \<otimes> p = p"
- unfolding neutral_prod_def mult_prod_def by (simp add: neutl)
-qed
-
-end %quote
-
-text {*
- \noindent Fully-fledged monoids are modelled by another subclass,
- which does not add new parameters but tightens the specification:
-*}
-
-class %quote monoid = monoidl +
- assumes neutr: "x \<otimes> \<one> = x"
-
-instantiation %quote nat and int :: monoid
-begin
-
-instance %quote proof
- fix n :: nat
- show "n \<otimes> \<one> = n"
- unfolding neutral_nat_def by (induct n) simp_all
-next
- fix k :: int
- show "k \<otimes> \<one> = k"
- unfolding neutral_int_def mult_int_def by simp
-qed
-
-end %quote
-
-instantiation %quote prod :: (monoid, monoid) monoid
-begin
-
-instance %quote proof
- fix p :: "\<alpha>\<Colon>monoid \<times> \<beta>\<Colon>monoid"
- show "p \<otimes> \<one> = p"
- unfolding neutral_prod_def mult_prod_def by (simp add: neutr)
-qed
-
-end %quote
-
-text {*
- \noindent To finish our small algebra example, we add a @{text
- group} class with a corresponding instance:
-*}
-
-class %quote group = monoidl +
- fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<div>)" [1000] 999)
- assumes invl: "x\<div> \<otimes> x = \<one>"
-
-instantiation %quote int :: group
-begin
-
-definition %quote
- inverse_int_def: "i\<div> = - (i\<Colon>int)"
-
-instance %quote proof
- fix i :: int
- have "-i + i = 0" by simp
- then show "i\<div> \<otimes> i = \<one>"
- unfolding mult_int_def neutral_int_def inverse_int_def .
-qed
-
-end %quote
-
-
-section {* Type classes as locales *}
-
-subsection {* A look behind the scenes *}
-
-text {*
- The example above gives an impression how Isar type classes work in
- practice. As stated in the introduction, classes also provide a
- link to Isar's locale system. Indeed, the logical core of a class
- is nothing other than a locale:
-*}
-
-class %quote idem =
- fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
- assumes idem: "f (f x) = f x"
-
-text {*
- \noindent essentially introduces the locale
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-locale %quote idem =
- fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
- assumes idem: "f (f x) = f x"
-
-text {* \noindent together with corresponding constant(s): *}
-
-consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
-
-text {*
- \noindent The connection to the type system is done by means
- of a primitive type class
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-classes %quote idem < type
-(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
-setup %invisible {* Sign.parent_path *}(*>*)
-
-text {* \noindent together with a corresponding interpretation: *}
-
-interpretation %quote idem_class:
- idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-(*<*)proof qed (rule idem)(*>*)
-
-text {*
- \noindent This gives you the full power of the Isabelle module system;
- conclusions in locale @{text idem} are implicitly propagated
- to class @{text idem}.
-*} (*<*)setup %invisible {* Sign.parent_path *}
-(*>*)
-subsection {* Abstract reasoning *}
-
-text {*
- Isabelle locales enable reasoning at a general level, while results
- are implicitly transferred to all instances. For example, we can
- now establish the @{text "left_cancel"} lemma for groups, which
- states that the function @{text "(x \<otimes>)"} is injective:
-*}
-
-lemma %quote (in group) left_cancel: "x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"
-proof
- assume "x \<otimes> y = x \<otimes> z"
- then have "x\<div> \<otimes> (x \<otimes> y) = x\<div> \<otimes> (x \<otimes> z)" by simp
- then have "(x\<div> \<otimes> x) \<otimes> y = (x\<div> \<otimes> x) \<otimes> z" using assoc by simp
- then show "y = z" using neutl and invl by simp
-next
- assume "y = z"
- then show "x \<otimes> y = x \<otimes> z" by simp
-qed
-
-text {*
- \noindent Here the \qt{@{keyword "in"} @{class group}} target
- specification indicates that the result is recorded within that
- context for later use. This local theorem is also lifted to the
- global one @{fact "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon>
- \<alpha>\<Colon>group. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been
- made an instance of @{text "group"} before, we may refer to that
- fact as well: @{prop [source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y =
- z"}.
-*}
-
-
-subsection {* Derived definitions *}
-
-text {*
- Isabelle locales are targets which support local definitions:
-*}
-
-primrec %quote (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
- "pow_nat 0 x = \<one>"
- | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
-
-text {*
- \noindent If the locale @{text group} is also a class, this local
- definition is propagated onto a global definition of @{term [source]
- "pow_nat \<Colon> nat \<Rightarrow> \<alpha>\<Colon>monoid \<Rightarrow> \<alpha>\<Colon>monoid"} with corresponding theorems
-
- @{thm pow_nat.simps [no_vars]}.
-
- \noindent As you can see from this example, for local definitions
- you may use any specification tool which works together with
- locales, such as Krauss's recursive function package
- \cite{krauss2006}.
-*}
-
-
-subsection {* A functor analogy *}
-
-text {*
- We introduced Isar classes by analogy to type classes in functional
- programming; if we reconsider this in the context of what has been
- said about type classes and locales, we can drive this analogy
- further by stating that type classes essentially correspond to
- functors that have a canonical interpretation as type classes.
- There is also the possibility of other interpretations. For
- example, @{text list}s also form a monoid with @{text append} and
- @{term "[]"} as operations, but it seems inappropriate to apply to
- lists the same operations as for genuinely algebraic types. In such
- a case, we can simply make a particular interpretation of monoids
- for lists:
-*}
-
-interpretation %quote list_monoid: monoid append "[]"
- proof qed auto
-
-text {*
- \noindent This enables us to apply facts on monoids
- to lists, e.g. @{thm list_monoid.neutl [no_vars]}.
-
- When using this interpretation pattern, it may also
- be appropriate to map derived definitions accordingly:
-*}
-
-primrec %quote replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
- "replicate 0 _ = []"
- | "replicate (Suc n) xs = xs @ replicate n xs"
-
-interpretation %quote list_monoid: monoid append "[]" where
- "monoid.pow_nat append [] = replicate"
-proof -
- interpret monoid append "[]" ..
- show "monoid.pow_nat append [] = replicate"
- proof
- fix n
- show "monoid.pow_nat append [] n = replicate n"
- by (induct n) auto
- qed
-qed intro_locales
-
-text {*
- \noindent This pattern is also helpful to reuse abstract
- specifications on the \emph{same} type. For example, think of a
- class @{text preorder}; for type @{typ nat}, there are at least two
- possible instances: the natural order or the order induced by the
- divides relation. But only one of these instances can be used for
- @{command instantiation}; using the locale behind the class @{text
- preorder}, it is still possible to utilise the same abstract
- specification again using @{command interpretation}.
-*}
-
-subsection {* Additional subclass relations *}
-
-text {*
- Any @{text "group"} is also a @{text "monoid"}; this can be made
- explicit by claiming an additional subclass relation, together with
- a proof of the logical difference:
-*}
-
-subclass %quote (in group) monoid
-proof
- fix x
- from invl have "x\<div> \<otimes> x = \<one>" by simp
- with assoc [symmetric] neutl invl have "x\<div> \<otimes> (x \<otimes> \<one>) = x\<div> \<otimes> x" by simp
- with left_cancel show "x \<otimes> \<one> = x" by simp
-qed
-
-text {*
- The logical proof is carried out on the locale level. Afterwards it
- is propagated to the type system, making @{text group} an instance
- of @{text monoid} by adding an additional edge to the graph of
- subclass relations (\figref{fig:subclass}).
-
- \begin{figure}[htbp]
- \begin{center}
- \small
- \unitlength 0.6mm
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){@{text semigroup}}}
- \put(20,40){\makebox(0,0){@{text monoidl}}}
- \put(00,20){\makebox(0,0){@{text monoid}}}
- \put(40,00){\makebox(0,0){@{text group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(25,35){\vector(1,-3){10}}
- \end{picture}
- \hspace{8em}
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){@{text semigroup}}}
- \put(20,40){\makebox(0,0){@{text monoidl}}}
- \put(00,20){\makebox(0,0){@{text monoid}}}
- \put(40,00){\makebox(0,0){@{text group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(05,15){\vector(3,-1){30}}
- \end{picture}
- \caption{Subclass relationship of monoids and groups:
- before and after establishing the relationship
- @{text "group \<subseteq> monoid"}; transitive edges are left out.}
- \label{fig:subclass}
- \end{center}
- \end{figure}
-
- For illustration, a derived definition in @{text group} using @{text
- pow_nat}
-*}
-
-definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
- "pow_int k x = (if k >= 0
- then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"
-
-text {*
- \noindent yields the global definition of @{term [source] "pow_int \<Colon>
- int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group"} with the corresponding theorem @{thm
- pow_int_def [no_vars]}.
-*}
-
-subsection {* A note on syntax *}
-
-text {*
- As a convenience, class context syntax allows references to local
- class operations and their global counterparts uniformly; type
- inference resolves ambiguities. For example:
-*}
-
-context %quote semigroup
-begin
-
-term %quote "x \<otimes> y" -- {* example 1 *}
-term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
-
-end %quote
-
-term %quote "x \<otimes> y" -- {* example 3 *}
-
-text {*
- \noindent Here in example 1, the term refers to the local class
- operation @{text "mult [\<alpha>]"}, whereas in example 2 the type
- constraint enforces the global class operation @{text "mult [nat]"}.
- In the global context in example 3, the reference is to the
- polymorphic global class operation @{text "mult [?\<alpha> \<Colon> semigroup]"}.
-*}
-
-section {* Further issues *}
-
-subsection {* Type classes and code generation *}
-
-text {*
- Turning back to the first motivation for type classes, namely
- overloading, it is obvious that overloading stemming from @{command
- class} statements and @{command instantiation} targets naturally
- maps to Haskell type classes. The code generator framework
- \cite{isabelle-codegen} takes this into account. If the target
- language (e.g.~SML) lacks type classes, then they are implemented by
- an explicit dictionary construction. As example, let's go back to
- the power function:
-*}
-
-definition %quote example :: int where
- "example = pow_int 10 (-2)"
-
-text {*
- \noindent This maps to Haskell as follows:
-*}
-(*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quotetypewriter {*
- @{code_stmts example (Haskell)}
-*}
-
-text {*
- \noindent The code in SML has explicit dictionary passing:
-*}
-text %quotetypewriter {*
- @{code_stmts example (SML)}
-*}
-
-
-text {*
- \noindent In Scala, implicts are used as dictionaries:
-*}
-(*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quotetypewriter {*
- @{code_stmts example (Scala)}
-*}
-
-
-subsection {* Inspecting the type class universe *}
-
-text {*
- To facilitate orientation in complex subclass structures, two
- diagnostics commands are provided:
-
- \begin{description}
-
- \item[@{command "print_classes"}] print a list of all classes
- together with associated operations etc.
-
- \item[@{command "class_deps"}] visualizes the subclass relation
- between all classes as a Hasse diagram.
-
- \end{description}
-*}
-
-end
--- a/doc-src/Classes/Thy/Setup.thy Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-theory Setup
-imports Main "~~/src/HOL/Library/Code_Integer"
-begin
-
-ML_file "../../antiquote_setup.ML"
-ML_file "../../more_antiquote.ML"
-
-setup {*
- Antiquote_Setup.setup #>
- More_Antiquote.setup #>
- Code_Target.set_default_code_width 74
-*}
-
-syntax
- "_alpha" :: "type" ("\<alpha>")
- "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
- "_beta" :: "type" ("\<beta>")
- "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
-
-parse_ast_translation {*
- let
- fun alpha_ast_tr [] = Ast.Variable "'a"
- | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
- fun alpha_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
- | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
- fun beta_ast_tr [] = Ast.Variable "'b"
- | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
- fun beta_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
- | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
- in
- [(@{syntax_const "_alpha"}, alpha_ast_tr),
- (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
- (@{syntax_const "_beta"}, beta_ast_tr),
- (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
- end
-*}
-
-end
\ No newline at end of file
--- a/doc-src/Classes/Thy/document/Classes.tex Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1561 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Classes}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Classes\isanewline
-\isakeyword{imports}\ Main\ Setup\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Introduction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Type classes were introduced by Wadler and Blott \cite{wadler89how}
- into the Haskell language to allow for a reasonable implementation
- of overloading\footnote{throughout this tutorial, we are referring
- to classical Haskell 1.0 type classes, not considering later
- additions in expressiveness}. As a canonical example, a polymorphic
- equality function \isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} which is overloaded on
- different types for \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, which is achieved by splitting
- introduction of the \isa{eq} function from its overloaded
- definitions by means of \isa{class} and \isa{instance}
- declarations: \footnote{syntax here is a kind of isabellized
- Haskell}
-
- \begin{quote}
-
- \noindent\isa{class\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
-
- \medskip\noindent\isa{instance\ nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ True} \\
- \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\
- \hspace*{2ex}\isa{eq\ {\isaliteral{5F}{\isacharunderscore}}\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ False} \\
- \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ n\ m}
-
- \medskip\noindent\isa{instance\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}eq{\isaliteral{29}{\isacharparenright}}\ pair\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ y{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
-
- \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
- \hspace*{2ex}\isa{less{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\
- \hspace*{2ex}\isa{less\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}
-
- \end{quote}
-
- \noindent Type variables are annotated with (finitely many) classes;
- these annotations are assertions that a particular polymorphic type
- provides definitions for overloaded functions.
-
- Indeed, type classes not only allow for simple overloading but form
- a generic calculus, an instance of order-sorted algebra
- \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
-
- From a software engineering point of view, type classes roughly
- correspond to interfaces in object-oriented languages like Java; so,
- it is naturally desirable that type classes do not only provide
- functions (class parameters) but also state specifications
- implementations must obey. For example, the \isa{class\ eq}
- above could be given the following specification, demanding that
- \isa{class\ eq} is an equivalence relation obeying reflexivity,
- symmetry and transitivity:
-
- \begin{quote}
-
- \noindent\isa{class\ eq\ where} \\
- \hspace*{2ex}\isa{eq\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool} \\
- \isa{satisfying} \\
- \hspace*{2ex}\isa{refl{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ x} \\
- \hspace*{2ex}\isa{sym{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ eq\ x\ y} \\
- \hspace*{2ex}\isa{trans{\isaliteral{3A}{\isacharcolon}}\ eq\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ eq\ y\ z\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ eq\ x\ z}
-
- \end{quote}
-
- \noindent From a theoretical point of view, type classes are
- lightweight modules; Haskell type classes may be emulated by SML
- functors \cite{classes_modules}. Isabelle/Isar offers a discipline
- of type classes which brings all those aspects together:
-
- \begin{enumerate}
- \item specifying abstract parameters together with
- corresponding specifications,
- \item instantiating those abstract parameters by a particular
- type
- \item in connection with a ``less ad-hoc'' approach to overloading,
- \item with a direct link to the Isabelle module system:
- locales \cite{kammueller-locales}.
- \end{enumerate}
-
- \noindent Isar type classes also directly support code generation in
- a Haskell like fashion. Internally, they are mapped to more
- primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
-
- This tutorial demonstrates common elements of structured
- specifications and abstract reasoning with type classes by the
- algebraic hierarchy of semigroups, monoids and groups. Our
- background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
- which some familiarity is assumed.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{A simple algebra example \label{sec:example}%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Class definition%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Depending on an arbitrary type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, class \isa{semigroup} introduces a binary operator \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} that is
- assumed to be associative:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isakeyword{assumes}\ assoc{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two parts:
- the \qn{operational} part names the class parameter (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
- (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, yielding the global
- parameter \isa{{\isaliteral{22}{\isachardoublequote}}mult\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequote}}} and the
- global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isaliteral{2E}{\isachardot}}assoc{\isaliteral{3A}{\isacharcolon}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Class instantiation \label{sec:class_inst}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The concrete type \isa{int} is made a \isa{semigroup} instance
- by providing a suitable definition for the class parameter \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. This is
- accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{instantiation}\isamarkupfalse%
-\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ i\ j\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} defines class parameters at a
- particular instance using common specification tools (here,
- \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} opens a
- proof that the given parameters actually conform to the class
- specification. Note that the first proof step is the \hyperlink{method.default}{\mbox{\isa{default}}} method, which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isaliteral{5F}{\isacharunderscore}}classes}}} method. This reduces an instance judgement to the
- relevant primitive proof goals; typically it is the first method
- applied in an instantiation proof.
-
- From now on, the type-checker will consider \isa{int} as a \isa{semigroup} automatically, i.e.\ any general results are immediately
- available on concrete instances.
-
- \medskip Another instance of \isa{semigroup} yields the natural
- numbers:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ semigroup\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ m\ n\ q\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\ \isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ q{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ m{\isaliteral{29}{\isacharparenright}}\ auto\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Note the occurence of the name \isa{mult{\isaliteral{5F}{\isacharunderscore}}nat} in the
- primrec declaration; by default, the local name of a class operation
- \isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is
- mangled as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be
- inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the
- corresponding ProofGeneral button.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lifting and parametric types%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Overloaded definitions given at a class instantiation may include
- recursion over the syntactic structure of types. As a canonical
- example, we model product semigroups using our simple algebra:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{2C}{\isacharcomma}}\ semigroup{\isaliteral{29}{\isacharparenright}}\ semigroup\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ fst\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ snd\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}semigroup{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ assoc{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-\ \ \ \ \ \ \isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Associativity of product semigroups is established using
- the definition of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} on products and the hypothetical
- associativity of the type components; these hypotheses are
- legitimate due to the \isa{semigroup} constraints imposed on the
- type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. Indeed,
- this pattern often occurs with parametric types and type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Subclassing%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We define a subclass \isa{monoidl} (a semigroup with a left-hand
- neutral) by extending \isa{semigroup} with one additional
- parameter \isa{neutral} together with its characteristic property:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup\ {\isaliteral{2B}{\isacharplus}}\isanewline
-\ \ \isakeyword{fixes}\ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isakeyword{assumes}\ neutl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Again, we prove some instances, by providing suitable
- parameter definitions and proofs for the additional specifications.
- Observe that instantiations for types with the same arity may be
- simultaneous:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{instantiation}\isamarkupfalse%
-\ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoidl\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ k\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{2C}{\isacharcomma}}\ monoidl{\isaliteral{29}{\isacharparenright}}\ monoidl\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoidl{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ p\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutl{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Fully-fledged monoids are modelled by another subclass,
- which does not add new parameters but tightens the specification:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline
-\ \ \isakeyword{assumes}\ neutr{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ nat\ \isakeyword{and}\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ monoid\ \isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}k\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{2C}{\isacharcomma}}\ monoid{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\ \isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ p\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}p\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ mult{\isaliteral{5F}{\isacharunderscore}}prod{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ neutr{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent To finish our small algebra example, we add a \isa{group} class with a corresponding instance:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ group\ {\isaliteral{3D}{\isacharequal}}\ monoidl\ {\isaliteral{2B}{\isacharplus}}\isanewline
-\ \ \isakeyword{fixes}\ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \isakeyword{assumes}\ invl{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instantiation}\isamarkupfalse%
-\ int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ group\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{instance}\isamarkupfalse%
-\ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\isanewline
-\ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2D}{\isacharminus}}i\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}i{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isamarkupsection{Type classes as locales%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{A look behind the scenes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The example above gives an impression how Isar type classes work in
- practice. As stated in the introduction, classes also provide a
- link to Isar's locale system. Indeed, the logical core of a class
- is nothing other than a locale:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{class}\isamarkupfalse%
-\ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent essentially introduces the locale%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\ %
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{locale}\isamarkupfalse%
-\ idem\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isakeyword{assumes}\ idem{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent together with corresponding constant(s):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{consts}\isamarkupfalse%
-\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The connection to the type system is done by means
- of a primitive type class%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\ %
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{classes}\isamarkupfalse%
-\ idem\ {\isaliteral{3C}{\isacharless}}\ type%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\begin{isamarkuptext}%
-\noindent together with a corresponding interpretation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{interpretation}\isamarkupfalse%
-\ idem{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ idem\ {\isaliteral{22}{\isachardoublequoteopen}}f\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}idem{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This gives you the full power of the Isabelle module system;
- conclusions in locale \isa{idem} are implicitly propagated
- to class \isa{idem}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\ %
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isamarkupsubsection{Abstract reasoning%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle locales enable reasoning at a general level, while results
- are implicitly transferred to all instances. For example, we can
- now establish the \isa{left{\isaliteral{5F}{\isacharunderscore}}cancel} lemma for groups, which
- states that the function \isa{{\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}{\isaliteral{29}{\isacharparenright}}} is injective:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
-\ assoc\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{using}\isamarkupfalse%
-\ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{next}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{then}\isamarkupfalse%
-\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target
- specification indicates that the result is recorded within that
- context for later use. This local theorem is also lifted to the
- global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isaliteral{2E}{\isachardot}}left{\isaliteral{5F}{\isacharunderscore}}cancel{\isaliteral{3A}{\isacharcolon}}}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}. Since type \isa{int} has been
- made an instance of \isa{group} before, we may refer to that
- fact as well: \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ z\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ z{\isaliteral{22}{\isachardoublequote}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Derived definitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Isabelle locales are targets which support local definitions:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{primrec}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ monoid{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent If the locale \isa{group} is also a class, this local
- definition is propagated onto a global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}monoid{\isaliteral{22}{\isachardoublequote}}} with corresponding theorems
-
- \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isadigit{0}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\isasep\isanewline%
-pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x}.
-
- \noindent As you can see from this example, for local definitions
- you may use any specification tool which works together with
- locales, such as Krauss's recursive function package
- \cite{krauss2006}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{A functor analogy%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We introduced Isar classes by analogy to type classes in functional
- programming; if we reconsider this in the context of what has been
- said about type classes and locales, we can drive this analogy
- further by stating that type classes essentially correspond to
- functors that have a canonical interpretation as type classes.
- There is also the possibility of other interpretations. For
- example, \isa{list}s also form a monoid with \isa{append} and
- \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} as operations, but it seems inappropriate to apply to
- lists the same operations as for genuinely algebraic types. In such
- a case, we can simply make a particular interpretation of monoids
- for lists:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{interpretation}\isamarkupfalse%
-\ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{proof}\isamarkupfalse%
-\ \isacommand{qed}\isamarkupfalse%
-\ auto%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This enables us to apply facts on monoids
- to lists, e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x}.
-
- When using this interpretation pattern, it may also
- be appropriate to map derived definitions accordingly:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{primrec}\isamarkupfalse%
-\ replicate\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isadigit{0}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}replicate\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ replicate\ n\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{interpretation}\isamarkupfalse%
-\ list{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{3A}{\isacharcolon}}\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ \isacommand{interpret}\isamarkupfalse%
-\ monoid\ append\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ replicate{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ n\isanewline
-\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}monoid{\isaliteral{2E}{\isachardot}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ append\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ replicate\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}induct\ n{\isaliteral{29}{\isacharparenright}}\ auto\isanewline
-\ \ \isacommand{qed}\isamarkupfalse%
-\isanewline
-\isacommand{qed}\isamarkupfalse%
-\ intro{\isaliteral{5F}{\isacharunderscore}}locales%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This pattern is also helpful to reuse abstract
- specifications on the \emph{same} type. For example, think of a
- class \isa{preorder}; for type \isa{nat}, there are at least two
- possible instances: the natural order or the order induced by the
- divides relation. But only one of these instances can be used for
- \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}; using the locale behind the class \isa{preorder}, it is still possible to utilise the same abstract
- specification again using \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Additional subclass relations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Any \isa{group} is also a \isa{monoid}; this can be made
- explicit by claiming an additional subclass relation, together with
- a proof of the logical difference:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{subclass}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ monoid\isanewline
-\isacommand{proof}\isamarkupfalse%
-\isanewline
-\ \ \isacommand{fix}\isamarkupfalse%
-\ x\isanewline
-\ \ \isacommand{from}\isamarkupfalse%
-\ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{with}\isamarkupfalse%
-\ assoc\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\ neutl\ invl\ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C6469763E}{\isasymdiv}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\ \ \isacommand{with}\isamarkupfalse%
-\ left{\isaliteral{5F}{\isacharunderscore}}cancel\ \isacommand{show}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ {\isaliteral{5C3C6F6E653E}{\isasymone}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-The logical proof is carried out on the locale level. Afterwards it
- is propagated to the type system, making \isa{group} an instance
- of \isa{monoid} by adding an additional edge to the graph of
- subclass relations (\figref{fig:subclass}).
-
- \begin{figure}[htbp]
- \begin{center}
- \small
- \unitlength 0.6mm
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){\isa{semigroup}}}
- \put(20,40){\makebox(0,0){\isa{monoidl}}}
- \put(00,20){\makebox(0,0){\isa{monoid}}}
- \put(40,00){\makebox(0,0){\isa{group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(25,35){\vector(1,-3){10}}
- \end{picture}
- \hspace{8em}
- \begin{picture}(40,60)(0,0)
- \put(20,60){\makebox(0,0){\isa{semigroup}}}
- \put(20,40){\makebox(0,0){\isa{monoidl}}}
- \put(00,20){\makebox(0,0){\isa{monoid}}}
- \put(40,00){\makebox(0,0){\isa{group}}}
- \put(20,55){\vector(0,-1){10}}
- \put(15,35){\vector(-1,-1){10}}
- \put(05,15){\vector(3,-1){30}}
- \end{picture}
- \caption{Subclass relationship of monoids and groups:
- before and after establishing the relationship
- \isa{group\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ monoid}; transitive edges are left out.}
- \label{fig:subclass}
- \end{center}
- \end{figure}
-
- For illustration, a derived definition in \isa{group} using \isa{pow{\isaliteral{5F}{\isacharunderscore}}nat}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{in}\ group{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\isanewline
-\ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent yields the global definition of \isa{{\isaliteral{22}{\isachardoublequote}}pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}group{\isaliteral{22}{\isachardoublequote}}} with the corresponding theorem \isa{pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\ else\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6469763E}{\isasymdiv}}{\isaliteral{29}{\isacharparenright}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{A note on syntax%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-As a convenience, class context syntax allows references to local
- class operations and their global counterparts uniformly; type
- inference resolves ambiguities. For example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{context}\isamarkupfalse%
-\ semigroup\isanewline
-\isakeyword{begin}\isanewline
-\isanewline
-\isacommand{term}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\isamarkupcmt{example 1%
-}
-\isanewline
-\isacommand{term}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\isamarkupcmt{example 2%
-}
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{term}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ %
-\isamarkupcmt{example 3%
-}
-%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Here in example 1, the term refers to the local class
- operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}, whereas in example 2 the type
- constraint enforces the global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}nat{\isaliteral{5D}{\isacharbrackright}}}.
- In the global context in example 3, the reference is to the
- polymorphic global class operation \isa{mult\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ semigroup{\isaliteral{5D}{\isacharbrackright}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Further issues%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Type classes and code generation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Turning back to the first motivation for type classes, namely
- overloading, it is obvious that overloading stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} targets naturally
- maps to Haskell type classes. The code generator framework
- \cite{isabelle-codegen} takes this into account. If the target
- language (e.g.~SML) lacks type classes, then they are implemented by
- an explicit dictionary construction. As example, let's go back to
- the power function:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\ example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This maps to Haskell as follows:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\isanewline
-import\ Prelude\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3C}{\isacharless}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3C}{\isacharless}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2E}{\isachardot}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{24}{\isachardollar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{24}{\isachardollar}}{\isaliteral{21}{\isacharbang}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{21}{\isacharbang}}{\isaliteral{21}{\isacharbang}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Eq{\isaliteral{2C}{\isacharcomma}}\ error{\isaliteral{2C}{\isacharcomma}}\ id{\isaliteral{2C}{\isacharcomma}}\ return{\isaliteral{2C}{\isacharcomma}}\ not{\isaliteral{2C}{\isacharcomma}}\ fst{\isaliteral{2C}{\isacharcomma}}\ snd{\isaliteral{2C}{\isacharcomma}}\ map{\isaliteral{2C}{\isacharcomma}}\ filter{\isaliteral{2C}{\isacharcomma}}\ concat{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ concatMap{\isaliteral{2C}{\isacharcomma}}\ reverse{\isaliteral{2C}{\isacharcomma}}\ zip{\isaliteral{2C}{\isacharcomma}}\ null{\isaliteral{2C}{\isacharcomma}}\ takeWhile{\isaliteral{2C}{\isacharcomma}}\ dropWhile{\isaliteral{2C}{\isacharcomma}}\ all{\isaliteral{2C}{\isacharcomma}}\ any{\isaliteral{2C}{\isacharcomma}}\ Integer{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ negate{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{2C}{\isacharcomma}}\ divMod{\isaliteral{2C}{\isacharcomma}}\ String{\isaliteral{2C}{\isacharcomma}}\ Bool{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Maybe{\isaliteral{28}{\isacharparenleft}}Nothing{\isaliteral{2C}{\isacharcomma}}\ Just{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-import\ qualified\ Prelude{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-data\ Num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ Num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ Num{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-apsnd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a\ b\ c{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ i\ then\ {\isadigit{1}}\ else\ negate\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ then\ negate\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Integer{\isaliteral{2C}{\isacharcomma}}\ Integer{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C}{\isacharbackslash}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ then\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}negate\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}negate\ r\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
-\ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-class\ {\isaliteral{28}{\isacharparenleft}}Semigroup\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoidl\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ neutral\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-class\ {\isaliteral{28}{\isacharparenleft}}Monoidl\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Monoid\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-class\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Group\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ inverse\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ negate\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-instance\ Semigroup\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-instance\ Monoidl\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-instance\ Monoid\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-instance\ Group\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Monoid\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-pow{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ mult\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Group\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-pow{\isaliteral{5F}{\isacharunderscore}}int\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
-\ \ \ \ else\ inverse\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}negate\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-example\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-example\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isadigit{1}}{\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\begin{isamarkuptext}%
-\noindent The code in SML has explicit dictionary passing:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
-\ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
-\ \ datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num\isanewline
-\ \ val\ apsnd\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b\isanewline
-\ \ val\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2A}{\isacharasterisk}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
-\ \ val\ nat\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
-\ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline
-\ \ val\ mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
-\ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline
-\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline
-\ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
-\ \ type\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline
-\ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\isanewline
-\ \ type\ {\isaliteral{27}{\isacharprime}}a\ group\isanewline
-\ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\isanewline
-\ \ val\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
-\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-\ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup\isanewline
-\ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl\isanewline
-\ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid\isanewline
-\ \ val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ group\isanewline
-\ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
-\ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
-\ \ val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
-end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
-\isanewline
-datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isadigit{0}}\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ else\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\isanewline
-\ \ \ \ \ \ \ \ \ \ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}abs{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
-\ \ \ \ else\ let\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ in\isanewline
-\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ mult\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-type\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ neutral\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-type\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-type\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-val\ inverse\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}inverse\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ {\isaliteral{3D}{\isacharequal}}\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ inverse\ {\isaliteral{3D}{\isacharequal}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline
-\ \ IntInf{\isaliteral{2E}{\isachardot}}int\ group{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ x\ {\isaliteral{3D}{\isacharequal}}\ neutral\ {\isaliteral{28}{\isacharparenleft}}monoidl{\isaliteral{5F}{\isacharunderscore}}monoid\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ mult\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ o\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-fun\ pow{\isaliteral{5F}{\isacharunderscore}}int\ A{\isaliteral{5F}{\isacharunderscore}}\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
-\ \ \ \ else\ inverse\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-val\ example\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ pow{\isaliteral{5F}{\isacharunderscore}}int\ group{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7E}{\isachartilde}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
-end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\begin{isamarkuptext}%
-\noindent In Scala, implicts are used as dictionaries:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isatagquotetypewriter
-%
-\begin{isamarkuptext}%
-object\ Example\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\isanewline
-abstract\ sealed\ class\ nat\isanewline
-final\ case\ object\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ extends\ nat\isanewline
-final\ case\ class\ Suc{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ extends\ nat\isanewline
-\isanewline
-abstract\ sealed\ class\ num\isanewline
-final\ case\ object\ One\ extends\ num\isanewline
-final\ case\ class\ Bit{\isadigit{0}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline
-final\ case\ class\ Bit{\isadigit{1}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline
-\isanewline
-def\ apsnd{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{2C}{\isacharcomma}}\ C{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ B{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ case\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3C}{\isacharless}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\ else\ i{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ else\ apsnd{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{2C}{\isacharcomma}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline
-\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{2C}{\isacharcomma}}\ Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ n\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
-\ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ n{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ val\ la{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ la\ else\ Suc{\isaliteral{28}{\isacharparenleft}}la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-trait\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-def\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-trait\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-def\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\isanewline
-\isanewline
-trait\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoidl{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-trait\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ extends\ monoid{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-def\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{28}{\isacharparenleft}}implicit\ A{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{2E}{\isachardot}}{\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j\isanewline
-\isanewline
-implicit\ def\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-implicit\ def\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-implicit\ def\ monoid{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoid{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-implicit\ def\ group{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ group{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ inverse{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
-\ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ monoid{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xa{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
-\ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ neutral{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\isanewline
-\ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\isanewline
-\isanewline
-def\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}A\ {\isaliteral{3A}{\isacharcolon}}\ group{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ else\ inverse{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-def\ example{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ pow{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
-{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{2A}{\isacharasterisk}}\ object\ Example\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\isanewline%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagquotetypewriter
-{\isafoldquotetypewriter}%
-%
-\isadelimquotetypewriter
-%
-\endisadelimquotetypewriter
-%
-\isamarkupsubsection{Inspecting the type class universe%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-To facilitate orientation in complex subclass structures, two
- diagnostics commands are provided:
-
- \begin{description}
-
- \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}] print a list of all classes
- together with associated operations etc.
-
- \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}] visualizes the subclass relation
- between all classes as a Hasse diagram.
-
- \end{description}%
-\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/Classes/classes.tex Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{article}
-\usepackage{latexsym,graphicx}
-\usepackage[refpage]{nomencl}
-\usepackage{../iman,../extra,../isar,../proof}
-\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{style}
-\usepackage{../pdfsetup}
-
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\isadroptag{theory}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Haskell-style type classes with Isabelle/Isar}
-\author{\emph{Florian Haftmann}}
-
-\begin{document}
-
-\maketitle
-
-\begin{abstract}
- \noindent This tutorial introduces Isar type classes, which
- are a convenient mechanism for organizing specifications.
- Essentially, they combine an operational aspect (in the
- manner of Haskell) with a logical aspect, both managed uniformly.
-\end{abstract}
-
-\thispagestyle{empty}\clearpage
-
-\pagenumbering{roman}
-\clearfirst
-
-\input{Thy/document/Classes.tex}
-
-\begingroup
-\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{../manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/document/root.tex Mon Aug 27 22:31:16 2012 +0200
@@ -0,0 +1,46 @@
+\documentclass[12pt,a4paper,fleqn]{article}
+\usepackage{latexsym,graphicx}
+\usepackage{iman,extra,isar,proof}
+\usepackage{isabelle,isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+\isadroptag{theory}
+
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+ \\[4ex] Haskell-style type classes with Isabelle/Isar}
+\author{\emph{Florian Haftmann}}
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+ \noindent This tutorial introduces Isar type classes, which
+ are a convenient mechanism for organizing specifications.
+ Essentially, they combine an operational aspect (in the
+ manner of Haskell) with a logical aspect, both managed uniformly.
+\end{abstract}
+
+\thispagestyle{empty}\clearpage
+
+\pagenumbering{roman}
+\clearfirst
+
+\input{Classes.tex}
+
+\begingroup
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{manual}
+\endgroup
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/document/style.sty Mon Aug 27 22:31:16 2012 +0200
@@ -0,0 +1,58 @@
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% paragraphs
+\setlength{\parindent}{1em}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+%% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+%% typewriter text
+\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
+\renewcommand{\isadigit}[1]{{##1}}%
+\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
+\isabellestyle{tt}\isastyle%
+\fontsize{9pt}{9pt}\selectfont}{}
+
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
+
+%% presentation
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+\binperiod
+\underscoreoff
+
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End:
--- a/doc-src/Classes/style.sty Mon Aug 27 22:22:42 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-
-%% toc
-\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
-\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
-
-%% paragraphs
-\setlength{\parindent}{1em}
-
-%% references
-\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% logical markup
-\newcommand{\strong}[1]{{\bfseries {#1}}}
-\newcommand{\qn}[1]{\emph{#1}}
-
-%% typographic conventions
-\newcommand{\qt}[1]{``{#1}''}
-\newcommand{\ditem}[1]{\item[\isastyletext #1]}
-
-%% quote environment
-\isakeeptag{quote}
-\renewenvironment{quote}
- {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
- {\endlist}
-\renewcommand{\isatagquote}{\begin{quote}}
-\renewcommand{\endisatagquote}{\end{quote}}
-\newcommand{\quotebreak}{\\[1.2ex]}
-
-%% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
-\renewcommand{\isadigit}[1]{{##1}}%
-\parindent0pt%
-\makeatletter\isa@parindent0pt\makeatother%
-\isabellestyle{tt}\isastyle%
-\fontsize{9pt}{9pt}\selectfont}{}
-
-\isakeeptag{quotetypewriter}
-\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
-\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
-
-%% presentation
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-%% character detail
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-\binperiod
-\underscoreoff
-
-%% format
-\pagestyle{headings}
-\isabellestyle{it}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "implementation"
-%%% End:
--- a/doc-src/ROOT Mon Aug 27 22:22:42 2012 +0200
+++ b/doc-src/ROOT Mon Aug 27 22:31:16 2012 +0200
@@ -1,8 +1,11 @@
-session Classes (doc) in "Classes/Thy" = HOL +
- options [browser_info = false, document = false,
- document_dump = document, document_dump_mode = "tex"]
+session Classes (doc) in "Classes" = HOL +
+ options [document_variants = "classes"]
theories [document = false] Setup
theories Classes
+ files
+ "document/build"
+ "document/root.tex"
+ "document/style.sty"
session Codegen (doc) in "Codegen/Thy" = "HOL-Library" +
options [browser_info = false, document = false,