# HG changeset patch # User wenzelm # Date 1346099476 -7200 # Node ID 9965099f51ad125b741ca7f5b19e1f7a3c2c45c9 # Parent a773af3e37d65da6bbf071bc4df9d3c8bf4954aa more standard document preparation within session context; diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Classes.thy --- /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 \ \ \ \ \ bool"} which is overloaded on + different types for @{text "\"}, 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 \ \ \ \ \ bool"} + + \medskip\noindent@{text "instance nat \ 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 (\\eq, \\eq) pair \ eq where"} \\ + \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \ eq y1 y2"} + + \medskip\noindent@{text "class ord extends eq where"} \\ + \hspace*{2ex}@{text "less_eq \ \ \ \ \ bool"} \\ + \hspace*{2ex}@{text "less \ \ \ \ \ 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 \ \ \ \ \ bool"} \\ + @{text "satisfying"} \\ + \hspace*{2ex}@{text "refl: eq x x"} \\ + \hspace*{2ex}@{text "sym: eq x y \ eq x y"} \\ + \hspace*{2ex}@{text "trans: eq x y \ eq y z \ 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 "\"}, class @{text + "semigroup"} introduces a binary operator @{text "(\)"} that is + assumed to be associative: +*} + +class %quote semigroup = + fixes mult :: "\ \ \ \ \" (infixl "\" 70) + assumes assoc: "(x \ y) \ z = x \ (y \ 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 \ \\semigroup \ \ \ \"} and the + global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\x y z \ + \\semigroup. (x \ y) \ z = x \ (y \ 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 + "(\)"} 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 \ j = i + (j\int)" + +instance %quote proof + fix i j k :: int have "(i + j) + k = i + (j + k)" by simp + then show "(i \ j) \ k = i \ (j \ 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\nat) \ n = n" + | "Suc m \ n = Suc (m \ n)" + +instance %quote proof + fix m n q :: nat + show "m \ n \ q = m \ (n \ 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 \} is + mangled as @{text f_\}. 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" + +instance %quote proof + fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" + show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ 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 "(\)"} 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 :: "\" ("\") + assumes neutl: "\ \ 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: "\ = (0\nat)" + +definition %quote + neutral_int_def: "\ = (0\int)" + +instance %quote proof + fix n :: nat + show "\ \ n = n" + unfolding neutral_nat_def by simp +next + fix k :: int + show "\ \ 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: "\ = (\, \)" + +instance %quote proof + fix p :: "\\monoidl \ \\monoidl" + show "\ \ 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 \ \ = x" + +instantiation %quote nat and int :: monoid +begin + +instance %quote proof + fix n :: nat + show "n \ \ = n" + unfolding neutral_nat_def by (induct n) simp_all +next + fix k :: int + show "k \ \ = 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 :: "\\monoid \ \\monoid" + show "p \ \ = 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 :: "\ \ \" ("(_\
)" [1000] 999) + assumes invl: "x\
\ x = \" + +instantiation %quote int :: group +begin + +definition %quote + inverse_int_def: "i\
= - (i\int)" + +instance %quote proof + fix i :: int + have "-i + i = 0" by simp + then show "i\
\ i = \" + 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 :: "\ \ \" + assumes idem: "f (f x) = f x" + +text {* + \noindent essentially introduces the locale +*} (*<*)setup %invisible {* Sign.add_path "foo" *} +(*>*) +locale %quote idem = + fixes f :: "\ \ \" + assumes idem: "f (f x) = f x" + +text {* \noindent together with corresponding constant(s): *} + +consts %quote f :: "\ \ \" + +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::\\idem)) = f x" +setup %invisible {* Sign.parent_path *}(*>*) + +text {* \noindent together with a corresponding interpretation: *} + +interpretation %quote idem_class: + idem "f \ (\\idem) \ \" +(*<*)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 \)"} is injective: +*} + +lemma %quote (in group) left_cancel: "x \ y = x \ z \ y = z" +proof + assume "x \ y = x \ z" + then have "x\
\ (x \ y) = x\
\ (x \ z)" by simp + then have "(x\
\ x) \ y = (x\
\ x) \ z" using assoc by simp + then show "y = z" using neutl and invl by simp +next + assume "y = z" + then show "x \ y = x \ 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] "\x y z \ + \\group. x \ y = x \ z \ 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] "\x y z \ int. x \ y = x \ z \ y = + z"}. +*} + + +subsection {* Derived definitions *} + +text {* + Isabelle locales are targets which support local definitions: +*} + +primrec %quote (in monoid) pow_nat :: "nat \ \ \ \" where + "pow_nat 0 x = \" + | "pow_nat (Suc n) x = x \ 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 \ nat \ \\monoid \ \\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 \ \ list \ \ 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\
\ x = \" by simp + with assoc [symmetric] neutl invl have "x\
\ (x \ \) = x\
\ x" by simp + with left_cancel show "x \ \ = 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 \ 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 \ \ \ \" where + "pow_int k x = (if k >= 0 + then pow_nat (nat k) x + else (pow_nat (nat (- k)) x)\
)" + +text {* + \noindent yields the global definition of @{term [source] "pow_int \ + int \ \\group \ \\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 \ y" -- {* example 1 *} +term %quote "(x\nat) \ y" -- {* example 2 *} + +end %quote + +term %quote "x \ y" -- {* example 3 *} + +text {* + \noindent Here in example 1, the term refers to the local class + operation @{text "mult [\]"}, 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 [?\ \ 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 diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Makefile --- 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) diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Setup.thy --- /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_ofsort" :: "sort \ type" ("\()\_" [0] 1000) + "_beta" :: "type" ("\") + "_beta_ofsort" :: "sort \ type" ("\()\_" [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 diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Thy/Classes.thy --- 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 \ \ \ \ \ bool"} which is overloaded on - different types for @{text "\"}, 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 \ \ \ \ \ bool"} - - \medskip\noindent@{text "instance nat \ 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 (\\eq, \\eq) pair \ eq where"} \\ - \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \ eq y1 y2"} - - \medskip\noindent@{text "class ord extends eq where"} \\ - \hspace*{2ex}@{text "less_eq \ \ \ \ \ bool"} \\ - \hspace*{2ex}@{text "less \ \ \ \ \ 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 \ \ \ \ \ bool"} \\ - @{text "satisfying"} \\ - \hspace*{2ex}@{text "refl: eq x x"} \\ - \hspace*{2ex}@{text "sym: eq x y \ eq x y"} \\ - \hspace*{2ex}@{text "trans: eq x y \ eq y z \ 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 "\"}, class @{text - "semigroup"} introduces a binary operator @{text "(\)"} that is - assumed to be associative: -*} - -class %quote semigroup = - fixes mult :: "\ \ \ \ \" (infixl "\" 70) - assumes assoc: "(x \ y) \ z = x \ (y \ 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 \ \\semigroup \ \ \ \"} and the - global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\x y z \ - \\semigroup. (x \ y) \ z = x \ (y \ 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 - "(\)"} 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 \ j = i + (j\int)" - -instance %quote proof - fix i j k :: int have "(i + j) + k = i + (j + k)" by simp - then show "(i \ j) \ k = i \ (j \ 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\nat) \ n = n" - | "Suc m \ n = Suc (m \ n)" - -instance %quote proof - fix m n q :: nat - show "m \ n \ q = m \ (n \ 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 \} is - mangled as @{text f_\}. 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 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" - -instance %quote proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" - show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ 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 "(\)"} 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 :: "\" ("\") - assumes neutl: "\ \ 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: "\ = (0\nat)" - -definition %quote - neutral_int_def: "\ = (0\int)" - -instance %quote proof - fix n :: nat - show "\ \ n = n" - unfolding neutral_nat_def by simp -next - fix k :: int - show "\ \ 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: "\ = (\, \)" - -instance %quote proof - fix p :: "\\monoidl \ \\monoidl" - show "\ \ 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 \ \ = x" - -instantiation %quote nat and int :: monoid -begin - -instance %quote proof - fix n :: nat - show "n \ \ = n" - unfolding neutral_nat_def by (induct n) simp_all -next - fix k :: int - show "k \ \ = 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 :: "\\monoid \ \\monoid" - show "p \ \ = 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 :: "\ \ \" ("(_\
)" [1000] 999) - assumes invl: "x\
\ x = \" - -instantiation %quote int :: group -begin - -definition %quote - inverse_int_def: "i\
= - (i\int)" - -instance %quote proof - fix i :: int - have "-i + i = 0" by simp - then show "i\
\ i = \" - 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 :: "\ \ \" - assumes idem: "f (f x) = f x" - -text {* - \noindent essentially introduces the locale -*} (*<*)setup %invisible {* Sign.add_path "foo" *} -(*>*) -locale %quote idem = - fixes f :: "\ \ \" - assumes idem: "f (f x) = f x" - -text {* \noindent together with corresponding constant(s): *} - -consts %quote f :: "\ \ \" - -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::\\idem)) = f x" -setup %invisible {* Sign.parent_path *}(*>*) - -text {* \noindent together with a corresponding interpretation: *} - -interpretation %quote idem_class: - idem "f \ (\\idem) \ \" -(*<*)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 \)"} is injective: -*} - -lemma %quote (in group) left_cancel: "x \ y = x \ z \ y = z" -proof - assume "x \ y = x \ z" - then have "x\
\ (x \ y) = x\
\ (x \ z)" by simp - then have "(x\
\ x) \ y = (x\
\ x) \ z" using assoc by simp - then show "y = z" using neutl and invl by simp -next - assume "y = z" - then show "x \ y = x \ 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] "\x y z \ - \\group. x \ y = x \ z \ 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] "\x y z \ int. x \ y = x \ z \ y = - z"}. -*} - - -subsection {* Derived definitions *} - -text {* - Isabelle locales are targets which support local definitions: -*} - -primrec %quote (in monoid) pow_nat :: "nat \ \ \ \" where - "pow_nat 0 x = \" - | "pow_nat (Suc n) x = x \ 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 \ nat \ \\monoid \ \\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 \ \ list \ \ 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\
\ x = \" by simp - with assoc [symmetric] neutl invl have "x\
\ (x \ \) = x\
\ x" by simp - with left_cancel show "x \ \ = 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 \ 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 \ \ \ \" where - "pow_int k x = (if k >= 0 - then pow_nat (nat k) x - else (pow_nat (nat (- k)) x)\
)" - -text {* - \noindent yields the global definition of @{term [source] "pow_int \ - int \ \\group \ \\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 \ y" -- {* example 1 *} -term %quote "(x\nat) \ y" -- {* example 2 *} - -end %quote - -term %quote "x \ y" -- {* example 3 *} - -text {* - \noindent Here in example 1, the term refers to the local class - operation @{text "mult [\]"}, 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 [?\ \ 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 diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Thy/Setup.thy --- 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_ofsort" :: "sort \ type" ("\()\_" [0] 1000) - "_beta" :: "type" ("\") - "_beta_ofsort" :: "sort \ type" ("\()\_" [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 diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/Thy/document/Classes.tex --- 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: diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/classes.tex --- 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: diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/document/root.tex --- /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: diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/document/style.sty --- /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: diff -r a773af3e37d6 -r 9965099f51ad doc-src/Classes/style.sty --- 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: diff -r a773af3e37d6 -r 9965099f51ad doc-src/ROOT --- 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,