--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Oct 10 15:52:45 2008 +0200
@@ -1,41 +1,7 @@
-(* $Id$ *)
-
-(*<*)
theory Classes
-imports Main Code_Integer
-uses "../../../more_antiquote"
+imports Main Setup
begin
-ML {*
-Code_Target.code_width := 74;
-*}
-
-syntax
- "_alpha" :: "type" ("\<alpha>")
- "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
- "_beta" :: "type" ("\<beta>")
- "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
-
-parse_ast_translation {*
- let
- fun alpha_ast_tr [] = Syntax.Variable "'a"
- | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
- fun alpha_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
- | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
- fun beta_ast_tr [] = Syntax.Variable "'b"
- | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
- fun beta_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
- | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
- in [
- ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
- ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
- ] end
-*}
-(*>*)
-
-
chapter {* Haskell-style classes with Isabelle/Isar *}
section {* Introduction *}
@@ -52,23 +18,27 @@
of the @{text eq} function from its overloaded definitions by means
of @{text class} and @{text instance} declarations:
- \medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
- \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+ \begin{quote}
+
+ \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
- \medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
- \hspace*{4ex}@{text "eq 0 0 = True"} \\
- \hspace*{4ex}@{text "eq 0 _ = False"} \\
- \hspace*{4ex}@{text "eq _ 0 = False"} \\
- \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
+ \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
+ \hspace*{2ex}@{text "eq 0 0 = True"} \\
+ \hspace*{2ex}@{text "eq 0 _ = False"} \\
+ \hspace*{2ex}@{text "eq _ 0 = False"} \\
+ \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
- \medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
- \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
+ \medskip\noindent\@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
+ \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
- \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
- \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
+ \medskip\noindent@{text "class ord extends eq where"} \\
+ \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
- \medskip\noindent Type variables are annotated with (finitely many) classes;
+ \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.
@@ -85,14 +55,18 @@
@{text "class eq"} is an equivalence relation obeying reflexivity,
symmetry and transitivity:
- \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
- \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
- \hspace*{2ex}@{text "satisfying"} \\
- \hspace*{4ex}@{text "refl: eq x x"} \\
- \hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
- \hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+ \begin{quote}
- \medskip\noindent From a theoretic point of view, type classes are lightweight
+ \noindent@{text "class eq where"} \\
+ \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
+ @{text "satisfying"} \\
+ \hspace*{2ex}@{text "refl: eq x x"} \\
+ \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
+ \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
+
+ \end{quote}
+
+ \noindent From a theoretic 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
@@ -128,22 +102,23 @@
text {*
Depending on an arbitrary type @{text "\<alpha>"}, class @{text
- "semigroup"} introduces a binary operator @{text "\<otimes>"} that is
+ "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
assumed to be associative:
*}
- class semigroup = type +
- fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
- assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
+class %quote semigroup = type +
+ fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<otimes>" 70)
+ assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
text {*
- \noindent This @{text "\<CLASS>"} specification consists of two
- parts: the \qn{operational} part names the class parameter (@{text
- "\<FIXES>"}), the \qn{logical} part specifies properties on them
- (@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text
- "\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
+ \noindent This @{command class} specification consists of two
+ parts: the \qn{operational} part names the class parameter
+ (@{element "fixes"}), the \qn{logical} part specifies properties on them
+ (@{element "assumes"}). The local @{element "fixes"} and
+ @{element "assumes"} are lifted to the theory toplevel,
+ yielding the global
parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
- global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
+ global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
*}
@@ -151,65 +126,66 @@
subsection {* Class instantiation \label{sec:class_inst} *}
text {*
- The concrete type @{text "int"} is made a @{text "semigroup"}
+ The concrete type @{typ int} is made a @{class semigroup}
instance by providing a suitable definition for the class parameter
- @{text "mult"} and a proof for the specification of @{text "assoc"}.
- This is accomplished by the @{text "\<INSTANTIATION>"} target:
+ @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
+ This is accomplished by the @{command instantiation} target:
*}
- instantiation int :: semigroup
- begin
+instantiation %quote int :: semigroup
+begin
- definition
- mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
+definition %quote
+ mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
- instance proof
- fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
- then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
- unfolding mult_int_def .
- qed
+instance %quote proof
+ fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
+ then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
+ unfolding mult_int_def .
+qed
- end
+end %quote
text {*
- \noindent @{text "\<INSTANTIATION>"} allows to define class parameters
+ \noindent @{command instantiation} allows to define class parameters
at a particular instance using common specification tools (here,
- @{text "\<DEFINITION>"}). The concluding @{text "\<INSTANCE>"}
+ @{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 @{text default} method,
- which for such instance proofs maps to the @{text intro_classes} method.
+ is the @{method default} method,
+ which for such instance proofs maps to the @{method intro_classes} method.
This boils down an instance judgement to the relevant primitive
proof goals and should conveniently always be the first method applied
in an instantiation proof.
- From now on, the type-checker will consider @{text "int"}
- as a @{text "semigroup"} automatically, i.e.\ any general results
+ 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 @{text "semigroup"} are the natural numbers:
+
+ \medskip Another instance of @{class semigroup} are the natural numbers:
*}
- instantiation nat :: semigroup
- begin
+instantiation %quote nat :: semigroup
+begin
- primrec mult_nat where
- "(0\<Colon>nat) \<otimes> n = n"
- | "Suc m \<otimes> n = Suc (m \<otimes> n)"
+primrec %quote mult_nat where
+ "(0\<Colon>nat) \<otimes> n = n"
+ | "Suc m \<otimes> n = Suc (m \<otimes> n)"
- instance proof
- fix m n q :: nat
- show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
- by (induct m) auto
- qed
+instance %quote proof
+ fix m n q :: nat
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
+ by (induct m) auto
+qed
- end
+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 instantiate on type constructor
@{text \<kappa>} are mangled as @{text f_\<kappa>}. In case of uncertainty,
- these names may be inspected using the @{text "\<PRINTCONTEXT>"} command
+ these names may be inspected using the @{command "print_context"} command
or the corresponding ProofGeneral button.
*}
@@ -222,27 +198,27 @@
using our simple algebra:
*}
- instantiation * :: (semigroup, semigroup) semigroup
- begin
+instantiation %quote * :: (semigroup, semigroup) semigroup
+begin
- definition
- mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
+definition %quote
+ mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
- instance proof
- fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
- show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
- unfolding mult_prod_def by (simp add: assoc)
- qed
+instance %quote proof
+ fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
+ show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
+ unfolding mult_prod_def by (simp add: assoc)
+qed
- end
+end %quote
text {*
\noindent Associativity from product semigroups is
established using
- the definition of @{text \<otimes>} on products and the hypothetical
+ the definition of @{text "(\<otimes>)"} on products and the hypothetical
associativity of the type components; these hypotheses
- are facts due to the @{text semigroup} constraints imposed
- on the type components by the @{text instance} proposition.
+ are facts 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.
*}
@@ -251,15 +227,15 @@
subsection {* Subclassing *}
text {*
- We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
- by extending @{text "semigroup"}
- with one additional parameter @{text "neutral"} together
+ 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 property:
*}
- class monoidl = semigroup +
- fixes neutral :: "\<alpha>" ("\<one>")
- assumes neutl: "\<one> \<otimes> x = x"
+class %quote monoidl = semigroup +
+ fixes neutral :: "\<alpha>" ("\<one>")
+ assumes neutl: "\<one> \<otimes> x = x"
text {*
\noindent Again, we prove some instances, by
@@ -338,7 +314,7 @@
end
text {*
- \noindent To finish our small algebra example, we add a @{text "group"} class
+ \noindent To finish our small algebra example, we add a @{text group} class
with a corresponding instance:
*}
@@ -379,7 +355,9 @@
text {*
\noindent essentially introduces the locale
*}
-(*<*) setup {* Sign.add_path "foo" *} (*>*)
+
+setup %invisible {* Sign.add_path "foo" *}
+
locale idem =
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
assumes idem: "f (f x) = f x"
@@ -401,7 +379,9 @@
interpretation idem_class:
idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
by unfold_locales (rule idem)
-(*<*) setup {* Sign.parent_path *} (*>*)
+
+setup %invisible {* Sign.parent_path *}
+
text {*
This give you at hand the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
@@ -429,9 +409,9 @@
qed
text {*
- \noindent Here the \qt{@{text "\<IN> group"}} target specification
+ \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 @{text
+ use. This local theorem is also lifted to the global one @{fact
"group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
@{text "group"} before, we may refer to that fact as well: @{prop
@@ -474,15 +454,15 @@
classes essentially correspond to functors which have
a canonical interpretation as type classes.
Anyway, there is also the possibility of other interpretations.
- For example, also @{text "list"}s form a monoid with
- @{term "op @"} and @{term "[]"} as operations, but it
+ For example, also @{text list}s 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 simply can do a particular interpretation
of monoids for lists:
*}
- interpretation list_monoid: monoid ["op @" "[]"]
+ interpretation list_monoid: monoid [append "[]"]
by unfold_locales auto
text {*
@@ -497,14 +477,14 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
- interpretation list_monoid: monoid ["op @" "[]"] where
- "monoid.pow_nat (op @) [] = replicate"
+ interpretation list_monoid: monoid [append "[]"] where
+ "monoid.pow_nat append [] = replicate"
proof -
- interpret monoid ["op @" "[]"] ..
- show "monoid.pow_nat (op @) [] = replicate"
+ interpret monoid [append "[]"] ..
+ show "monoid.pow_nat append [] = replicate"
proof
fix n
- show "monoid.pow_nat (op @) [] n = replicate n"
+ show "monoid.pow_nat append [] n = replicate n"
by (induct n) auto
qed
qed intro_locales
@@ -571,11 +551,10 @@
in @{text group} which uses @{text pow_nat}:
*}
- definition (in group)
- pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
- "pow_int k x = (if k >= 0
- then pow_nat (nat k) x
- else (pow_nat (nat (- k)) x)\<div>)"
+definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+ "pow_int k x = (if k >= 0
+ then pow_nat (nat k) x
+ else (pow_nat (nat (- k)) x)\<div>)"
text {*
\noindent yields the global definition of
@@ -591,15 +570,15 @@
uniformly; type inference resolves ambiguities. For example:
*}
-context semigroup
+context %quote semigroup
begin
-term "x \<otimes> y" -- {* example 1 *}
-term "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
+term %quote "x \<otimes> y" -- {* example 1 *}
+term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
end
-term "x \<otimes> y" -- {* example 3 *}
+term %quote "x \<otimes> y" -- {* example 3 *}
text {*
\noindent Here in example 1, the term refers to the local class operation
@@ -614,8 +593,8 @@
text {*
Turning back to the first motivation for type classes,
namely overloading, it is obvious that overloading
- stemming from @{text "\<CLASS>"} statements and
- @{text "\<INSTANTIATION>"}
+ 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. Concerning target languages
@@ -624,20 +603,19 @@
As example, let's go back to the power function:
*}
- definition
- example :: int where
- "example = pow_int 10 (-2)"
+definition %quote example :: int where
+ "example = pow_int 10 (-2)"
text {*
\noindent This maps to Haskell as:
*}
-text %quoteme {*@{code_stmts example (Haskell)}*}
+text %quote {*@{code_stmts example (Haskell)}*}
text {*
\noindent The whole code in SML with explicit dictionary passing:
*}
-text %quoteme {*@{code_stmts example (SML)}*}
+text %quote {*@{code_stmts example (SML)}*}
end
--- a/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML Fri Oct 10 15:52:45 2008 +0200
@@ -1,4 +1,6 @@
(* $Id$ *)
+no_document use_thy "Setup";
+
use_thy "Classes";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/Thy/Setup.thy Fri Oct 10 15:52:45 2008 +0200
@@ -0,0 +1,34 @@
+theory Setup
+imports Main Code_Integer
+uses
+ "../../../antiquote_setup"
+ "../../../more_antiquote"
+begin
+
+ML {* Code_Target.code_width := 74 *}
+
+syntax
+ "_alpha" :: "type" ("\<alpha>")
+ "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
+ "_beta" :: "type" ("\<beta>")
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
+
+parse_ast_translation {*
+ let
+ fun alpha_ast_tr [] = Syntax.Variable "'a"
+ | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+ fun alpha_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
+ | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+ fun beta_ast_tr [] = Syntax.Variable "'b"
+ | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+ fun beta_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+ | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+ in [
+ ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
+ ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
+ ] end
+*}
+
+end
\ No newline at end of file
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Oct 10 15:52:45 2008 +0200
@@ -3,12 +3,14 @@
\def\isabellecontext{Classes}%
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
%
\isatagtheory
-%
+\isacommand{theory}\isamarkupfalse%
+\ Classes\isanewline
+\isakeyword{imports}\ Main\ Setup\isanewline
+\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
@@ -16,32 +18,6 @@
%
\endisadelimtheory
%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
}
\isamarkuptrue%
@@ -62,23 +38,27 @@
of the \isa{eq} function from its overloaded definitions by means
of \isa{class} and \isa{instance} declarations:
- \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
- \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+ \begin{quote}
+
+ \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
- \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
- \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
- \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
- \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
- \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
+ \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
+ \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
+ \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
+ \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
+ \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
- \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
- \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
+ \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
+ \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
- \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
- \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
- \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
+ \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
+ \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
+ \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
- \medskip\noindent Type variables are annotated with (finitely many) classes;
+ \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.
@@ -95,14 +75,18 @@
\isa{class\ eq} is an equivalence relation obeying reflexivity,
symmetry and transitivity:
- \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
- \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
- \hspace*{2ex}\isa{satisfying} \\
- \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
- \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
- \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
+ \begin{quote}
- \medskip\noindent From a theoretic point of view, type classes are lightweight
+ \noindent\isa{class\ eq\ where} \\
+ \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
+ \isa{satisfying} \\
+ \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
+ \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
+ \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
+
+ \end{quote}
+
+ \noindent From a theoretic 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
@@ -142,20 +126,36 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
+Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
assumed to be associative:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
-\noindent This \isa{{\isasymCLASS}} specification consists of two
- parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
- (\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
+\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{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
- global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
+ global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -166,57 +166,57 @@
\begin{isamarkuptext}%
The concrete type \isa{int} is made a \isa{semigroup}
instance by providing a suitable definition for the class parameter
- \isa{mult} and a proof for the specification of \isa{assoc}.
- This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
+ \isa{{\isacharparenleft}{\isasymotimes}{\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%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
\ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isakeyword{begin}\isanewline
\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
\ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
-\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
+\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
at a particular instance using common specification tools (here,
- \isa{{\isasymDEFINITION}}). The concluding \isa{{\isasymINSTANCE}}
+ \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 \isa{default} method,
- which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
+ is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
+ which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
This boils down an instance judgement to the relevant primitive
proof goals and should conveniently always be the first method applied
in an instantiation proof.
@@ -224,51 +224,52 @@
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} are the natural numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{primrec}\isamarkupfalse%
-\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
%
-\isadelimproof
-\ %
-\endisadelimproof
+\isadelimquote
+%
+\endisadelimquote
%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
\isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{primrec}\isamarkupfalse%
+\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
\isanewline
\isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
in the primrec declaration; by default, the local name of
a class operation \isa{f} to instantiate on type constructor
\isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty,
- these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
+ these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
or the corresponding ProofGeneral button.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -284,49 +285,49 @@
using our simple algebra:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
-\ \ \ \ \isakeyword{begin}\isanewline
-\isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isanewline
-\ \ \ \ \isacommand{instance}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
+\isatagquote
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
\isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
+\ \ \isacommand{unfolding}\isamarkupfalse%
\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
+\isacommand{qed}\isamarkupfalse%
\ \ \ \ \ \ \isanewline
\isanewline
-\ \ \ \ \isacommand{end}\isamarkupfalse%
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent Associativity from product semigroups is
established using
- the definition of \isa{{\isasymotimes}} on products and the hypothetical
+ the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
associativity of the type components; these hypotheses
are facts due to the \isa{semigroup} constraints imposed
- on the type components by the \isa{instance} proposition.
+ 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}%
@@ -343,10 +344,23 @@
with its property:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{class}\isamarkupfalse%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{class}\isamarkupfalse%
\ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
-\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
\noindent Again, we prove some instances, by
providing suitable parameter definitions and proofs for the
@@ -597,18 +611,21 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimML
+\isadeliminvisible
%
-\endisadelimML
-%
-\isatagML
+\endisadeliminvisible
%
-\endisatagML
-{\isafoldML}%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
%
-\isadelimML
+\isadeliminvisible
%
-\endisadelimML
+\endisadeliminvisible
+\isanewline
+\isanewline
\isacommand{locale}\isamarkupfalse%
\ idem\ {\isacharequal}\isanewline
\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
@@ -646,21 +663,24 @@
{\isafoldproof}%
%
\isadelimproof
+\isanewline
%
\endisadelimproof
%
-\isadelimML
+\isadeliminvisible
+\isanewline
%
-\endisadelimML
-%
-\isatagML
+\endisadeliminvisible
%
-\endisatagML
-{\isafoldML}%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
%
-\isadelimML
+\isadeliminvisible
%
-\endisadelimML
+\endisadeliminvisible
%
\begin{isamarkuptext}%
This give you at hand the full power of the Isabelle module system;
@@ -724,9 +744,9 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
+\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 \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
+ use. This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of
\isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -772,7 +792,7 @@
a canonical interpretation as type classes.
Anyway, there is also the possibility of other interpretations.
For example, also \isa{list}s form a monoid with
- \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
+ \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
seems inappropriate to apply to lists
the same operations as for genuinely algebraic types.
In such a case, we simply can do a particular interpretation
@@ -780,7 +800,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
%
\isadelimproof
\ \ \ \ \ \ %
@@ -810,8 +830,8 @@
\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
\isanewline
\ \ \ \ \isacommand{interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
%
\isadelimproof
\ \ \ \ %
@@ -821,16 +841,16 @@
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
-\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
\ n\isanewline
\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -932,12 +952,24 @@
in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
-\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
-\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
+\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
+\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
\noindent yields the global definition of
\isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
@@ -955,6 +987,12 @@
uniformly; type inference resolves ambiguities. For example:%
\end{isamarkuptext}%
\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
\isacommand{context}\isamarkupfalse%
\ semigroup\isanewline
\isakeyword{begin}\isanewline
@@ -968,16 +1006,36 @@
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
\isamarkupcmt{example 2%
}
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
\isanewline
\isanewline
\isacommand{end}\isamarkupfalse%
\isanewline
+%
+\isadelimquote
\isanewline
+%
+\endisadelimquote
+%
+\isatagquote
\isacommand{term}\isamarkupfalse%
\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\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\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
@@ -994,30 +1052,42 @@
\begin{isamarkuptext}%
Turning back to the first motivation for type classes,
namely overloading, it is obvious that overloading
- stemming from \isa{{\isasymCLASS}} statements and
- \isa{{\isasymINSTANTIATION}}
+ 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. Concerning target languages
lacking type classes (e.g.~SML), type classes
are implemented by explicit dictionary construction.
- For example, lets go back to the power function:%
+ As example, let's go back to the power function:%
\end{isamarkuptext}%
\isamarkuptrue%
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
-\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
\begin{isamarkuptext}%
\noindent This maps to Haskell as:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
%
\begin{isamarkuptext}%
\isaverbatim%
@@ -1088,23 +1158,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent The whole code in SML with explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
-\isatagquoteme
+\isatagquote
%
\begin{isamarkuptext}%
\isaverbatim%
@@ -1170,12 +1240,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagquoteme
-{\isafoldquoteme}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquoteme
+\isadelimquote
%
-\endisadelimquoteme
+\endisadelimquote
%
\isadelimtheory
%
--- a/doc-src/IsarAdvanced/Classes/classes.tex Fri Oct 10 15:23:33 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex Fri Oct 10 15:52:45 2008 +0200
@@ -3,71 +3,51 @@
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
-\usepackage{listings}
\usepackage[refpage]{nomencl}
\usepackage{../../iman,../../extra,../../isar,../../proof}
\usepackage{../../isabelle,../../isabellesym}
\usepackage{style}
\usepackage{../../pdfsetup}
-\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
-
-\makeatletter
-
-\isakeeptag{quoteme}
-\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquoteme}{\begin{quoteme}}
-\renewcommand{\endisatagquoteme}{\end{quoteme}}
-
-\makeatother
-
-\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
-\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
-\renewcommand{\isasymotimes}{\isamath{\circ}}
-
-\newcommand{\cmd}[1]{\isacommand{#1}}
-\newcommand{\isasymINFIX}{\cmd{infix}}
-\newcommand{\isasymLOCALE}{\cmd{locale}}
-\newcommand{\isasymINCLUDES}{\cmd{includes}}
-\newcommand{\isasymDATATYPE}{\cmd{datatype}}
-\newcommand{\isasymAXCLASS}{\cmd{axclass}}
-\newcommand{\isasymFIXES}{\cmd{fixes}}
-\newcommand{\isasymASSUMES}{\cmd{assumes}}
-\newcommand{\isasymDEFINES}{\cmd{defines}}
-\newcommand{\isasymNOTES}{\cmd{notes}}
-\newcommand{\isasymSHOWS}{\cmd{shows}}
-\newcommand{\isasymCLASS}{\cmd{class}}
-\newcommand{\isasymINSTANCE}{\cmd{instance}}
-\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
-\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
-\newcommand{\isasymLEMMA}{\cmd{lemma}}
-\newcommand{\isasymPROOF}{\cmd{proof}}
-\newcommand{\isasymQED}{\cmd{qed}}
-\newcommand{\isasymFIX}{\cmd{fix}}
-\newcommand{\isasymASSUME}{\cmd{assume}}
-\newcommand{\isasymSHOW}{\cmd{show}}
-\newcommand{\isasymNOTE}{\cmd{note}}
+%% setup
-\newcommand{\qt}[1]{``#1''}
-\newcommand{\qtt}[1]{"{}{#1}"{}}
-\newcommand{\qn}[1]{\emph{#1}}
-\newcommand{\strong}[1]{{\bfseries #1}}
-\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
-
-\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
-\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
-\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
-
+% hyphenation
\hyphenation{Isabelle}
\hyphenation{Isar}
+% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+% verbatim text
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+% invisibility
\isadroptag{theory}
+
+% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
+
+%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
+%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
+%\renewcommand{\isasymotimes}{\isamath{\circ}}
+
+
+%% content
+
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Haskell-style type classes with Isabelle/Isar}
\author{\emph{Florian Haftmann}}
-
\begin{document}
\maketitle