# HG changeset patch # User haftmann # Date 1160473123 -7200 # Node ID 75b56e51fadef68b2c48c2b82a36718b5f1a760a # Parent 1de0d565b4838be1311f2e2c00970c4b534492eb initial draft diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/IsaMakefile --- /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) diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/Makefile --- /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) diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- /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_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_beta" :: "type" ("\") + "_beta_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_gamma" :: "type" ("\") + "_gamma_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_alpha_f" :: "type" ("\\<^sub>f") + "_alpha_f_ofsort" :: "sort \ type" ("\\<^sub>f()::_" [0] 1000) + "_beta_f" :: "type" ("\\<^sub>f") + "_beta_f_ofsort" :: "sort \ type" ("\\<^sub>f()::_" [0] 1000) + "_gamma_f" :: "type" ("\\<^sub>f") + "_gamma_ofsort_f" :: "sort \ type" ("\\<^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 "\"}, 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 "\"} and @{text "\"}; + proofs will be recorded using structured elements of Isabelle/Isar + \cite{Wenzel-PhD,Nipkow:2002}, notably @{text "\"}/@{text + "\"} and @{text "\"}/@{text "\"}/@{text + "\"}. + + Our main concern are the new @{text "\"} + and @{text "\"} 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 "\"}, class @{text + "semigroup"} introduces a binary operation @{text "\"} that is + assumed to be associative: +*} + + class semigroup = + fixes mult :: "\ \ \ \ \" (infixl "\<^loc>\" 70) + assumes assoc: "(x \<^loc>\ y) \<^loc>\ z = x \<^loc>\ (y \<^loc>\ z)" + +text {* + \noindent This @{text "\"} specification consists of two + parts: the \qn{operational} part names the class operation (@{text + "\"}), the \qn{logical} part specifies properties on them + (@{text "\"}). The local @{text "\"} and @{text + "\"} are lifted to the theory toplevel, yielding the global + operation @{term [source] "mult :: \::semigroup \ \ \ \"} and the + global theorem @{text "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 @{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: "\i j :: int. i \ j \ i + j" + 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 + +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 \ n \ m + n" + proof + fix m n q :: nat + show "m \ n \ q = m \ (n \ 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 \ ys \ xs @ ys" + proof + fix xs ys zs :: "\ list" + show "xs \ ys \ zs = xs \ (ys \ zs)" + proof - + from semigroup_list_def have "\xs ys\\ list. xs \ ys \ 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 :: "\" ("\<^loc>\") + assumes neutl: "\<^loc>\ \<^loc>\ x = x" + +text {* + \noindent Again, we make some instances, by + providing suitable operation definitions and proofs for the + additional specifications. +*} + + instance nat :: monoidl + "\ \ 0" + proof + fix n :: nat + show "\ \ n = n" unfolding neutral_nat_def mult_nat_def by simp + qed + + instance int :: monoidl + "\ \ 0" + proof + fix k :: int + show "\ \ k = k" unfolding neutral_int_def mult_int_def by simp + qed + + instance list :: (type) monoidl + "\ \ []" + proof + fix xs :: "\ list" + show "\ \ xs = xs" + proof - + from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . + moreover from mult_list_def neutral_list_def have "\ \ []\\ 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>\ \<^loc>\ = x" + + instance nat :: monoid + proof + fix n :: nat + show "n \ \ = n" unfolding neutral_nat_def mult_nat_def by simp + qed + + instance int :: monoid + proof + fix k :: int + show "k \ \ = k" unfolding neutral_int_def mult_int_def by simp + qed + + instance list :: (type) monoid + proof + fix xs :: "\ list" + show "xs \ \ = xs" + proof - + from mult_list_def have "\xs ys\\ list. xs \ ys \ xs @ ys" . + moreover from mult_list_def neutral_list_def have "\ \ []\'a list" by simp + ultimately show ?thesis by simp + qed + qed + + class group = monoidl + + fixes inverse :: "\ \ \" ("(_\<^loc>\
)" [1000] 999) + assumes invl: "x\<^loc>\
\<^loc>\ x = \<^loc>\" + + instance int :: group + "i\
\ - i" + proof + fix i :: int + have "-i + i = 0" by simp + then show "i\
\ i = \" 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 \)"} is injective: +*} + + lemma (in group) left_cancel: "x \<^loc>\ y = x \<^loc>\ z \ y = z" + proof + assume "x \<^loc>\ y = x \<^loc>\ z" + then have "x\<^loc>\
\<^loc>\ (x \<^loc>\ y) = x\<^loc>\
\<^loc>\ (x \<^loc>\ z)" by simp + then have "(x\<^loc>\
\<^loc>\ x) \<^loc>\ y = (x\<^loc>\
\<^loc>\ x) \<^loc>\ z" using assoc by simp + then show "y = z" using neutl and invl by simp + next + assume "y = z" + then show "x \<^loc>\ y = x \<^loc>\ z" by simp + qed + +text {* + \noindent Here the \qt{@{text "\ 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] "\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 {* +*}*) + + +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>\
\<^loc>\ x = \<^loc>\" by simp + with assoc [symmetric] neutl invl have "x\<^loc>\
\<^loc>\ (x \<^loc>\ \<^loc>\) = x\<^loc>\
\<^loc>\ x" by simp + with left_cancel show "x \<^loc>\ \<^loc>\ = 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 \ 'a\monoidl \ 'a\monoidl" where + "pow_nat 0 x = \" + "pow_nat (Suc n) x = x \ 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 \ 'a\group \ 'a\group" + "pow_int k x = (if k >= 0 + then pow_nat (nat k) x + else (pow_nat (nat (- k)) x)\
)" + + 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 diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/Thy/ROOT.ML --- /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"; diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/classes.bib --- /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} +} + diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/classes.tex --- /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: diff -r 1de0d565b483 -r 75b56e51fade doc-src/IsarAdvanced/Classes/style.sty --- /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: