--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/IsaMakefile Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,33 @@
+
+## targets
+
+default: Thy
+images:
+test: Thy
+
+all: images test
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+
+USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+
+
+## Thy
+
+THY = $(LOG)/HOL-Thy.gz
+
+Thy: $(THY)
+
+$(THY): Thy/ROOT.ML Thy/Classes.thy
+ @$(USEDIR) HOL Thy
+
+
+## clean
+
+clean:
+ @rm -f $(THY)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/Makefile Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,37 @@
+#
+# $Id$
+#
+
+## 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 \
+ ../../manual.bib ../../proof.sty
+
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES) isabelle_isar.eps
+ $(LATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(LATEX) $(NAME)
+ $(LATEX) $(NAME)
+
+pdf: $(NAME).pdf
+
+$(NAME).pdf: $(FILES) isabelle_isar.pdf
+ $(PDFLATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
+ $(FIXBOOKMARKS) $(NAME).out
+ $(PDFLATEX) $(NAME)
+ $(PDFLATEX) $(NAME)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,373 @@
+
+(* $Id$ *)
+
+theory Classes
+imports Main
+begin
+
+(*<*)
+syntax
+ "_alpha" :: "type" ("\<alpha>")
+ "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
+ "_beta" :: "type" ("\<beta>")
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()::_" [0] 1000)
+ "_gamma" :: "type" ("\<gamma>")
+ "_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()::_" [0] 1000)
+ "_alpha_f" :: "type" ("\<alpha>\<^sub>f")
+ "_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()::_" [0] 1000)
+ "_beta_f" :: "type" ("\<beta>\<^sub>f")
+ "_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()::_" [0] 1000)
+ "_gamma_f" :: "type" ("\<gamma>\<^sub>f")
+ "_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()::_" [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);
+ fun gamma_ast_tr [] = Syntax.Variable "'c"
+ | gamma_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
+ fun gamma_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c", ast]
+ | gamma_ofsort_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
+ fun alpha_f_ast_tr [] = Syntax.Variable "'a_f"
+ | alpha_f_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
+ fun alpha_f_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a_f", ast]
+ | alpha_f_ofsort_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
+ fun beta_f_ast_tr [] = Syntax.Variable "'b_f"
+ | beta_f_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
+ fun beta_f_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b_f", ast]
+ | beta_f_ofsort_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
+ fun gamma_f_ast_tr [] = Syntax.Variable "'c_f"
+ | gamma_f_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
+ fun gamma_f_ofsort_ast_tr [ast] =
+ Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c_f", ast]
+ | gamma_f_ofsort_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
+ in [
+ ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
+ ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr),
+ ("_gamma", gamma_ast_tr), ("_gamma_ofsort", gamma_ofsort_ast_tr),
+ ("_alpha_f", alpha_f_ast_tr), ("_alpha_f_ofsort", alpha_f_ofsort_ast_tr),
+ ("_beta_f", beta_f_ast_tr), ("_beta_f_ofsort", beta_f_ofsort_ast_tr),
+ ("_gamma_f", gamma_f_ast_tr), ("_gamma_f_ofsort", gamma_f_ofsort_ast_tr)
+ ] end
+*}
+(*>*)
+
+
+chapter {* Haskell-style classes with Isabelle/Isar *}
+
+section {* Introduction *}
+
+text {*
+ The well-known concept of type classes
+ \cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
+ offers a useful structuring mechanism for programs and proofs, which
+ is more light-weight than a fully featured module mechanism. Type
+ classes are able to qualify types by associating operations and
+ logical properties. For example, class @{text "eq"} could provide
+ an equivalence relation @{text "="} on type @{text "\<alpha>"}, and class
+ @{text "ord"} could extend @{text "eq"} by providing a strict order
+ @{text "<"} etc.
+
+ Isabelle/Isar offers Haskell-style type classes, combining operational
+ and logical specifications.
+*}
+
+section {* A simple algebra example \label{sec:example} *}
+
+text {*
+ We demonstrate 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{Nipkow-et-al:2002:tutorial}, which uses fairly
+ standard notation from mathematics and functional programming. We
+ also refer to basic vernacular commands for definitions and
+ statements, e.g.\ @{text "\<DEFINITION>"} and @{text "\<LEMMA>"};
+ proofs will be recorded using structured elements of Isabelle/Isar
+ \cite{Wenzel-PhD,Nipkow:2002}, notably @{text "\<PROOF>"}/@{text
+ "\<QED>"} and @{text "\<FIX>"}/@{text "\<ASSUME>"}/@{text
+ "\<SHOW>"}.
+
+ Our main concern are the new @{text "\<CLASS>"}
+ and @{text "\<INSTANCE>"} elements used below.
+ Here we merely present the
+ look-and-feel for end users, which is quite similar to Haskell's
+ \texttt{class} and \texttt{instance} \cite{hall96type}, but
+ augmented by logical specifications and proofs;
+ Internally, those are mapped to more primitive Isabelle concepts.
+ See \cite{haftmann_wenzel2006classes} for more detail.
+*}
+
+
+subsection {* Class definition *}
+
+text {*
+ Depending on an arbitrary type @{text "\<alpha>"}, class @{text
+ "semigroup"} introduces a binary operation @{text "\<circ>"} that is
+ assumed to be associative:
+*}
+
+ class semigroup =
+ fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<^loc>\<otimes>" 70)
+ assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
+
+text {*
+ \noindent This @{text "\<CLASS>"} specification consists of two
+ parts: the \qn{operational} part names the class operation (@{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
+ operation @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
+ global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
+ z::\<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
+*}
+
+
+subsection {* Class instantiation \label{sec:class_inst} *}
+
+text {*
+ The concrete type @{text "int"} is made a @{text "semigroup"}
+ instance by providing a suitable definition for the class operation
+ @{text "mult"} and a proof for the specification of @{text "assoc"}.
+*}
+
+ instance int :: semigroup
+ mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
+ 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
+
+text {*
+ \noindent From now on, the type-checker will consider @{text "int"}
+ as a @{text "semigroup"} automatically, i.e.\ any general results
+ are immediately available on concrete instances.
+
+ Another instance of @{text "semigroup"} are the natural numbers:
+*}
+
+ instance nat :: semigroup
+ "m \<otimes> n \<equiv> m + n"
+ proof
+ fix m n q :: nat
+ show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding semigroup_nat_def by simp
+ qed
+
+text {*
+ Also @{text "list"}s form a semigroup with @{const "op @"} as
+ operation:
+*}
+
+ instance list :: (type) semigroup
+ "xs \<otimes> ys \<equiv> xs @ ys"
+ proof
+ fix xs ys zs :: "\<alpha> list"
+ show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
+ proof -
+ from semigroup_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
+ thus ?thesis by simp
+ qed
+ qed
+
+
+subsection {* Subclasses *}
+
+text {*
+ We define a subclass @{text "monoidl"} (a semigroup with an left-hand neutral)
+ by extending @{text "semigroup"}
+ with one additional operation @{text "neutral"} together
+ with its property:
+*}
+
+ class monoidl = semigroup +
+ fixes neutral :: "\<alpha>" ("\<^loc>\<one>")
+ assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
+
+text {*
+ \noindent Again, we make some instances, by
+ providing suitable operation definitions and proofs for the
+ additional specifications.
+*}
+
+ instance nat :: monoidl
+ "\<one> \<equiv> 0"
+ proof
+ fix n :: nat
+ show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
+ qed
+
+ instance int :: monoidl
+ "\<one> \<equiv> 0"
+ proof
+ fix k :: int
+ show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
+ qed
+
+ instance list :: (type) monoidl
+ "\<one> \<equiv> []"
+ proof
+ fix xs :: "\<alpha> list"
+ show "\<one> \<otimes> xs = xs"
+ proof -
+ from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
+ moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
+ ultimately show ?thesis by simp
+ qed
+ qed
+
+text {*
+ To finish our small algebra example, we add @{text "monoid"}
+ and @{text "group"} classes with corresponding instances
+*}
+
+ class monoid = monoidl +
+ assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
+
+ instance nat :: monoid
+ proof
+ fix n :: nat
+ show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
+ qed
+
+ instance int :: monoid
+ proof
+ fix k :: int
+ show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
+ qed
+
+ instance list :: (type) monoid
+ proof
+ fix xs :: "\<alpha> list"
+ show "xs \<otimes> \<one> = xs"
+ proof -
+ from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
+ moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
+ ultimately show ?thesis by simp
+ qed
+ qed
+
+ class group = monoidl +
+ fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
+ assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
+
+ instance int :: group
+ "i\<div> \<equiv> - i"
+ proof
+ fix i :: int
+ have "-i + i = 0" by simp
+ then show "i\<div> \<otimes> i = \<one>" unfolding mult_int_def and neutral_int_def and inverse_int_def .
+ qed
+
+
+subsection {* Abstract reasoning *}
+
+text {*
+ Abstract theories 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 \<circ>)"} is injective:
+*}
+
+ lemma (in group) left_cancel: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z \<longleftrightarrow> y = z"
+ proof
+ assume "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
+ then have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> y) = x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
+ then have "(x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> y = (x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> z" using assoc by simp
+ then show "y = z" using neutl and invl by simp
+ next
+ assume "y = z"
+ then show "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
+ qed
+
+text {*
+ \noindent Here the \qt{@{text "\<IN> 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
+ "group.left_cancel:"} @{prop [source] "\<And>x y z::\<alpha>::group. x \<otimes> y = x \<otimes>
+ z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
+ @{text "group"} before, we may refer to that fact as well: @{prop
+ [source] "\<And>x y z::int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
+*}
+
+
+(*subsection {* Derived definitions *}
+
+text {*
+*}*)
+
+
+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:
+*}
+
+ instance group < monoid
+ proof -
+ fix x
+ from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
+ with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
+ with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
+ qed
+
+
+(* subsection {* Same logical content -- different syntax *}
+
+text {*
+
+*} *)
+
+
+section {* Code generation *}
+
+text {*
+ Code generation takes account of type classes,
+ resulting either in Haskell type classes or SML dictionaries.
+ As example, we define the natural power function on groups:
+*}
+
+ function
+ pow_nat :: "nat \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
+ "pow_nat 0 x = \<one>"
+ "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
+ by pat_completeness auto
+ termination pow_nat by (auto_term "measure fst")
+ declare pow_nat.simps [code func]
+
+ definition
+ pow_int :: "int \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group"
+ "pow_int k x = (if k >= 0
+ then pow_nat (nat k) x
+ else (pow_nat (nat (- k)) x)\<div>)"
+
+ definition
+ example :: int
+ "example = pow_int 10 (-2)"
+
+text {*
+ \noindent Now we generate and compile code for SML:
+*}
+
+ code_gen example (SML -)
+
+text {*
+ \noindent The result is as expected:
+*}
+
+ ML {*
+ if ROOT.Classes.example = ~20 then () else error "Wrong result"
+ *}
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,4 @@
+
+(* $Id$ *)
+
+use_thy "Classes";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/classes.bib Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,211 @@
+
+@InProceedings{Ballarin:2004,
+ author = {Clemens Ballarin},
+ title = {Locales and Locale Expressions in {Isabelle/Isar}},
+ booktitle = {Types for Proofs and Programs (TYPES 2003)},
+ year = 2004,
+ editor = {Stefano Berardi and others},
+ series = {LNCS 3085}
+}
+
+@InProceedings{Ballarin:2006,
+ author = {Clemens Ballarin},
+ title = {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
+ booktitle = {Mathematical Knowledge Management (MKM 2006)},
+ year = 2006,
+ editor = {J.M. Borwein and W.M. Farmer},
+ series = {LNAI 4108}
+}
+
+@InProceedings{Berghofer-Nipkow:2000,
+ author = {Stefan Berghofer and Tobias Nipkow},
+ title = {Proof terms for simply typed higher order logic},
+ booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)},
+ editor = {J. Harrison and M. Aagaard},
+ series = {LNCS 1869},
+ year = 2000
+}
+
+@Manual{Coq-Manual:2006,
+ title = {The {Coq} Proof Assistant Reference Manual, version 8},
+ author = {B. Barras and others},
+ organization = {INRIA},
+ year = 2006
+}
+
+@Article{Courant:2006,
+ author = {Judica{\"e}l Courant},
+ title = {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}},
+ journal = {The Journal of Functional Programming},
+ year = 2006,
+ note = {To appear},
+ abstract = {Several proof-assistants rely on the very formal basis
+ of Pure Type Systems (PTS) as their foundations. We are concerned
+ with the issues involved in the development of large proofs in
+ these provers such as namespace management, development of
+ reusable proof libraries and separate verification. Although
+ implementations offer many features to address them, few
+ theoretical foundations have been laid for them up to now. This is
+ a problem as features dealing with modularity may have harmful,
+ unsuspected effects on the reliability or usability of an
+ implementation.
+
+ In this paper, we propose an extension of Pure Type Systems with a
+ module system, MC2, adapted from SML-like module systems for
+ programming languages. This system gives a theoretical framework
+ addressing the issues mentioned above in a quite uniform way. It
+ is intended to be a theoretical foundation for the module systems
+ of proof-assistants such as Coq or Agda. We show how reliability
+ and usability can be formalized as metatheoretical properties and
+ prove they hold for MC2.}
+}
+
+@PhdThesis{Jacek:2004,
+ author = {Jacek Chrz\c{a}szcz},
+ title = {Modules in type theory with generative definitions},
+ school = {Universit{\'e} Paris-Sud},
+ year = {2004},
+}
+
+@InProceedings{Kamm-et-al:1999,
+ author = {Florian Kamm{\"u}ller and Markus Wenzel and
+ Lawrence C. Paulson},
+ title = {Locales: A Sectioning Concept for {Isabelle}},
+ booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '99)},
+ editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
+ Paulin, C. and Thery, L.},
+ series = {LNCS 1690},
+ year = 1999
+}
+
+@InProceedings{Nipkow-Prehofer:1993,
+ author = {T. Nipkow and C. Prehofer},
+ title = {Type checking type classes},
+ booktitle = {ACM Symp.\ Principles of Programming Languages},
+ year = 1993
+}
+
+@Book{Nipkow-et-al:2002:tutorial,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+ series = {LNCS 2283},
+ year = 2002
+}
+
+@InCollection{Nipkow:1993,
+ author = {T. Nipkow},
+ title = {Order-Sorted Polymorphism in {Isabelle}},
+ booktitle = {Logical Environments},
+ publisher = {Cambridge University Press},
+ year = 1993,
+ editor = {G. Huet and G. Plotkin}
+}
+
+@InProceedings{Nipkow:2002,
+ author = {Tobias Nipkow},
+ title = {Structured Proofs in {Isar/HOL}},
+ booktitle = {Types for Proofs and Programs (TYPES 2002)},
+ year = 2003,
+ editor = {H. Geuvers and F. Wiedijk},
+ series = {LNCS 2646}
+}
+
+@InCollection{Paulson:1990,
+ author = {L. C. Paulson},
+ title = {Isabelle: the next 700 theorem provers},
+ booktitle = {Logic and Computer Science},
+ publisher = {Academic Press},
+ year = 1990,
+ editor = {P. Odifreddi}
+}
+
+@BOOK{Pierce:TypeSystems,
+ AUTHOR = {B.C. Pierce},
+ TITLE = {Types and Programming Languages},
+ PUBLISHER = {MIT Press},
+ YEAR = 2002,
+ PLCLUB = {Yes},
+ BCP = {Yes},
+ KEYS = {books},
+ HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
+ ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
+}
+
+@Book{Schmidt-Schauss:1989,
+ author = {Manfred Schmidt-Schau{\ss}},
+ title = {Computational Aspects of an Order-Sorted Logic with Term Declarations},
+ series = {LNAI 395},
+ year = 1989
+}
+
+@InProceedings{Wenzel:1997,
+ author = {M. Wenzel},
+ title = {Type Classes and Overloading in Higher-Order Logic},
+ booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '97)},
+ editor = {Elsa L. Gunter and Amy Felty},
+ series = {LNCS 1275},
+ year = 1997}
+
+@article{hall96type,
+ author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler",
+ title = "Type Classes in {Haskell}",
+ journal = "ACM Transactions on Programming Languages and Systems",
+ volume = "18",
+ number = "2",
+ publisher = "ACM Press",
+ year = "1996"
+}
+
+@inproceedings{hindleymilner,
+ author = {L. Damas and H. Milner},
+ title = {Principal type schemes for functional programs},
+ booktitle = {ACM Symp. Principles of Programming Languages},
+ year = 1982
+}
+
+@manual{isabelle-axclass,
+ author = {Markus Wenzel},
+ title = {Using Axiomatic Type Classes in {I}sabelle},
+ institution = {TU Munich},
+ year = 2005,
+ note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
+
+@InProceedings{krauss:2006:functions,
+ author = {A. Krauss},
+ title = {Partial Recursive Functions in Higher-Order Logic},
+ booktitle = {Int. Joint Conference on Automated Reasoning (IJCAR 2006)},
+ year = 2006,
+ editor = {Ulrich Furbach and Natarajan Shankar},
+ series = {LNCS}
+}
+
+@inproceedings{peterson93implementing,
+ author = "J. Peterson and Peyton Jones, S.",
+ title = "Implementing Type Classes",
+ booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
+ year = 1993
+}
+
+@inproceedings{wadler89how,
+ author = {P. Wadler and S. Blott},
+ title = {How to make ad-hoc polymorphism less ad-hoc},
+ booktitle = {ACM Symp.\ Principles of Programming Languages},
+ year = 1989
+}
+
+@misc{jones97type,
+ author = "S. Jones and M. Jones and E. Meijer",
+ title = "Type classes: an exploration of the design space",
+ text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration
+ of the design space. In Haskell Workshop, June 1997.",
+ year = "1997",
+ url = "citeseer.ist.psu.edu/peytonjones97type.html"
+}
+
+@article{haftmann_wenzel2006classes,
+ author = "Florian Haftmann and Makarius Wenzel",
+ title = "Constructive Type Classes in Isabelle",
+ year = 2006,
+ note = {To appear}
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/classes.tex Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,82 @@
+
+%% $Id$
+
+\documentclass[12pt,a4paper,fleqn]{report}
+\usepackage{latexsym,graphicx}
+\usepackage[refpage]{nomencl}
+\usepackage{../../iman,../../extra,../../isar,../../proof}
+\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
+\usepackage{style}
+\usepackage{Thy/document/pdfsetup}
+
+\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{\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}}
+\newcommand{\isasymIN}{\cmd{in}}
+
+\newcommand{\qt}[1]{``#1''}
+\newcommand{\qtt}[1]{"{}{#1}"{}}
+\newcommand{\qn}[1]{\emph{#1}}
+\newcommand{\strong}[1]{{\bfseries #1}}
+\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
+
+\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}
+ This tutorial introduces the look-and-feel of Isar type classes
+ to the end-user; Isar type classes are a convenient mechanism
+ for organizing specifications, overcoming some drawbacks
+ of raw axiomatic type classes. 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
+%\tocentry{\bibname}
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{../../manual,classes}
+\endgroup
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Classes/style.sty Tue Oct 10 11:38:43 2006 +0200
@@ -0,0 +1,64 @@
+
+%% $Id$
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\chref}[1]{chapter~\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% glossary
+\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
+\newcommand{\seeglossary}[1]{\emph{#1}}
+\newcommand{\glossaryname}{Glossary}
+\renewcommand{\nomname}{\glossaryname}
+\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
+
+%% index
+\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
+\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
+\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
+\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
+
+%% math
+\newcommand{\text}[1]{\mbox{#1}}
+\newcommand{\isasymvartheta}{\isamath{\theta}}
+\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+\pagestyle{headings}
+\sloppy
+\binperiod
+\underscoreon
+
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+
+\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
+
+\isafoldtag{FIXME}
+\isakeeptag{mlref}
+\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
+\renewcommand{\endisatagmlref}{\endgroup}
+
+\newcommand{\isasymGUESS}{\isakeyword{guess}}
+\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
+\newcommand{\isasymTHEORY}{\isakeyword{theory}}
+\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
+\newcommand{\isasymUSES}{\isakeyword{uses}}
+\newcommand{\isasymBEGIN}{\isakeyword{begin}}
+\newcommand{\isasymEND}{\isakeyword{end}}
+\newcommand{\isasymCONSTS}{\isakeyword{consts}}
+\newcommand{\isasymDEFS}{\isakeyword{defs}}
+\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
+\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
+
+\isabellestyle{it}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End: