--- a/src/Doc/ROOT Mon Apr 18 20:56:13 2016 +0200
+++ b/src/Doc/ROOT Mon Apr 18 20:56:18 2016 +0200
@@ -483,3 +483,23 @@
"tutorial.sty"
"typedef.pdf"
"types0.tex"
+
+session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" +
+ options [document_variants = "typeclass_hierarchy"]
+ theories Typeclass_Hierarchy
+ document_files (in "..")
+ "prepare_document"
+ "pdfsetup.sty"
+ "iman.sty"
+ "extra.sty"
+ "isar.sty"
+ "manual.bib"
+ document_files
+ "build"
+ "root.tex"
+ "style.sty"
+
+session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" +
+ options [document = false]
+ theories
+ Setup
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Mon Apr 18 20:56:18 2016 +0200
@@ -0,0 +1,16 @@
+theory Setup
+imports Complex_Main "~~/src/HOL/Library/Lattice_Syntax"
+begin
+
+ML_file "../antiquote_setup.ML"
+ML_file "../more_antiquote.ML"
+
+attribute_setup all =
+ \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
+ "quantified schematic vars"
+
+setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
+
+declare [[show_sorts]]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Mon Apr 18 20:56:18 2016 +0200
@@ -0,0 +1,176 @@
+theory Typeclass_Hierarchy
+imports Setup
+begin
+
+section \<open>Introduction\<close>
+
+text \<open>
+ The {Isabelle/HOL} type-class hierarchy entered the stage
+ in a quite ancient era -- first related \emph{NEWS} entries date
+ back to release {Isabelle99-1}. Since then, there have been
+ ongoing modifications and additions, leading to ({Isabelle2016})
+ more than 180 type-classes. This sheer complexity makes access
+ and understanding of that type-class hierarchy difficult and
+ involved, let alone maintenance.
+
+ The purpose of this primer is to shed some light on this,
+ not only on the mere ingredients, but also on the design
+ principles which have evolved and proven useful over time.
+\<close>
+
+section \<open>Foundations\<close>
+
+subsection \<open>Locales and type classes\<close>
+
+text \<open>
+ Some familiarity with the Isabelle module system is assumed:
+ defining locales and type-classes, interpreting locales and
+ instantiating type-classes, adding relationships between
+ locales (@{command sublocale}) and type-classes
+ (@{command subclass}). Handy introductions are the
+ respective tutorials \cite{isabelle-locale}
+ \cite{isabelle-classes}.
+\<close>
+
+subsection \<open>Strengths and restrictions of type classes\<close>
+
+text \<open>
+ The primary motivation for using type classes in {Isabelle/HOL}
+ always have been numerical types, which form an inclusion chain:
+
+ \begin{center}
+ @{typ nat} @{text \<sqsubset>} @{typ int} @{text \<sqsubset>} @{typ rat}
+ @{text \<sqsubset>} @{typ real} @{text \<sqsubset>} @{typ complex}
+ \end{center}
+
+ \noindent The inclusion @{text \<sqsubset>} means that any value of the numerical
+ type to the left hand side mathematically can be transferred
+ to the numerical type on the right hand side.
+
+ How to accomplish this given the quite restrictive type system
+ of {Isabelle/HOL}? Paulson \cite{paulson-numerical} explains
+ that each numerical type has some characteristic properties
+ which define an characteristic algebraic structure; @{text \<sqsubset>}
+ then corresponds to specialization of the corresponding
+ characteristic algebraic structures. These algebraic structures
+ are expressed using algebraic type classes and embeddings
+ of numerical types into them:
+
+ \begin{center}\begin{tabular}{lccc}
+ @{term of_nat} @{text "::"} & @{typ nat} & @{text \<Rightarrow>} & @{typ [source] "'a::semiring_1"} \\
+ & @{text \<sqinter>} & & @{text \<up>} \\
+ @{term of_int} @{text "::"} & @{typ int} & @{text \<Rightarrow>} & @{typ [source] "'a::ring_1"} \\
+ & @{text \<sqinter>} & & @{text \<up>} \\
+ @{term of_rat} @{text "::"} & @{typ rat} & @{text \<Rightarrow>} & @{typ [source] "'a::field_char_0"} \\
+ & @{text \<sqinter>} & & @{text \<up>} \\
+ @{term of_real} @{text "::"} & @{typ real} & @{text \<Rightarrow>} & @{typ [source] "'a::real_algebra_1"} \\
+ & @{text \<sqinter>} \\
+ & @{typ complex}
+ \end{tabular}\end{center}
+
+ \noindent @{text "d \<leftarrow> c"} means that @{text c} is subclass of @{text d}.
+ Hence each characteristic embedding @{text of_num} can transform
+ any value of type @{text num} to any numerical type further
+ up in the inclusion chain.
+
+ This canonical example exhibits key strengths of type classes:
+
+ \<^item> Sharing of operations and facts among different
+ types, hence also sharing of notation and names: there
+ is only one plus operation using infix syntax @{text "+"},
+ only one zero written @{text 0}, and neutrality
+ (@{thm add_0_left [all, no_vars]} and
+ @{thm add_0_right [all, no_vars]})
+ is referred to
+ uniformly by names @{fact add_0_left} and @{fact add_0_right}.
+
+ \<^item> Proof tool setups are shared implicitly:
+ @{fact add_0} and @{fact add_0_right} are simplification
+ rules by default.
+
+ \<^item> Hence existing proofs about particular numerical
+ types are often easy to generalize to algebraic structures,
+ given that they do not depend on specific properties of
+ those numerical types.
+
+ Considerable restrictions include:
+
+ \<^item> Type class operations are restricted to one
+ type parameter; this is insufficient e.g. for expressing
+ a unified power operation adequately (see \secref{sec:power}).
+
+ \<^item> Parameters are fixed over the whole type class
+ hierarchy and cannot be refined in specific situations:
+ think of integral domains with a predicate @{term is_unit};
+ for natural numbers, this degenerates to the much simpler
+ @{term [source] "HOL.equal (1::nat)"} but facts
+ refer to @{term is_unit} nonetheless.
+
+ \<^item> Type classes are not apt for meta-theory. There
+ is no practically usable way to express that the units
+ of an integral domain form a multiplicative group using
+ type classes. But see session @{text "HOL-Algebra"}
+ which provides locales with an explicit carrier.
+\<close>
+
+
+subsection \<open>Navigating the hierarchy\<close>
+
+text \<open>
+ An indispensable tool to inspect the class hierarchy is
+ @{command class_deps} which displays the graph of classes,
+ optionally showing the logical content for each class also.
+ Optional parameters restrict the graph to a particular segment
+ which is useful to get a graspable view. See
+ the Isar reference manual \cite{isabelle-isar-ref} for details.
+\<close>
+
+
+section \<open>The hierarchy\<close>
+
+subsection \<open>Syntactic type classes\<close>
+
+text \<open>
+ At the top of the hierarchy there are a couple of syntactic type
+ classes, ie. classes with operations but with no axioms,
+ most notably:
+
+ \<^item> @{class plus} with @{term [source] "(a::'a::plus) + b"}
+
+ \<^item> @{class zero} with @{term [source] "0::'a::zero"}
+
+ \<^item> @{class times} with @{term [source] "(a::'a::times) * b"}
+
+ \<^item> @{class one} with @{term [source] "1::'a::one"}
+
+ \noindent Before the introduction of the @{command class} statement in
+ Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible
+ to define operations with associated axioms in the same class,
+ hence there were always pairs of syntactic and logical type
+ classes. This restriction is lifted nowadays, but there are
+ still reasons to maintain syntactic type classes:
+
+ \<^item> Syntactic type classes allow generic notation to be used
+ regardless of a particular logical interpretation; e.g.
+ although multiplication @{text "*"} is usually associative,
+ there are examples where it is not (e.g. octonions), and
+ leaving @{text "*"} without axioms allows to re-use this
+ syntax by means of type class instantiation also for such
+ exotic examples.
+
+ \<^item> Type classes might share operations but not necessarily
+ axioms on them, e.g. @{term gcd} (see \secref{sec:gcd}).
+ Hence their common base is a syntactic type class.
+
+ \noindent However syntactic type classes should only be used with striking
+ cause. Otherwise there is risk for confusion if the notation
+ suggests properties which do not hold without particular
+ constraints. This can be illustrated using numerals
+ (see \secref{sec:numerals}): @{lemma "2 + 2 = 4" by simp} is
+ provable without further ado, and this also meets the typical
+ expectation towards a numeral notation; in more ancient releases
+ numerals were purely syntactic and @{prop "2 + 2 = 4"} was
+ not provable without particular type constraints.
+\<close>
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Typeclass_Hierarchy/document/build Mon Apr 18 20:56:18 2016 +0200
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" logo Isar
+"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Typeclass_Hierarchy/document/root.tex Mon Apr 18 20:56:18 2016 +0200
@@ -0,0 +1,38 @@
+\documentclass[12pt,a4paper,fleqn]{article}
+\usepackage{latexsym,graphicx}
+\usepackage{iman,extra,isar}
+\usepackage{isabelle,isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+\hyphenation{Isabelle}
+\hyphenation{Isar}
+\isadroptag{theory}
+
+\title{\includegraphics[scale=0.5]{isabelle_isar}
+ \\[4ex] The {Isabelle/HOL} type-class hierarchy}
+\author{\emph{Florian Haftmann}}
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+ \noindent This primer introduces corner stones of the {Isabelle/HOL}
+ type-class hierarchy and gives some insights into its internal
+ organization.
+\end{abstract}
+
+\thispagestyle{empty}\clearpage
+
+\pagenumbering{roman}
+\clearfirst
+
+\input{Typeclass_Hierarchy.tex}
+
+\begingroup
+\bibliographystyle{plain} \small\raggedright\frenchspacing
+\bibliography{manual}
+\endgroup
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Typeclass_Hierarchy/document/style.sty Mon Apr 18 20:56:18 2016 +0200
@@ -0,0 +1,38 @@
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% paragraphs
+\setlength{\parindent}{1em}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+%% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+%% presentation
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+\binperiod
+
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
--- a/src/Doc/manual.bib Mon Apr 18 20:56:13 2016 +0200
+++ b/src/Doc/manual.bib Mon Apr 18 20:56:18 2016 +0200
@@ -909,6 +909,18 @@
number = 5,
month = May}
+@inproceedings{Hoelzl-Huffman-Immler:2013:typeclasses,
+ author = {Johannes H{\"o}lzl and Fabian Immler and Brian Huffman},
+ title = {Type Classes and Filters for Mathematical Analysis in {Isabelle/HOL}},
+ booktitle = {Interactive Theorem Proving (ITP 2013)},
+ editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
+ year = 2013,
+ volume = 7998,
+ series = LNCS,
+ publisher = Springer,
+ isbn = {978-3-642-39633-5},
+ pages = {279--294}}
+
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
@@ -1476,6 +1488,16 @@
month = mar,
pages = {175-204}}
+@article{paulson-numerical,
+ author = {Lawrence C. Paulson},
+ title = {Organizing numerical theories using axiomatic type
+ classes},
+ journal = JAR,
+ year = 2004,
+ volume = 33,
+ number = 1,
+ pages = {29-49}}
+
@manual{isabelle-intro,
author = {Lawrence C. Paulson},
title = {Old Introduction to {Isabelle}},
--- a/src/Doc/more_antiquote.ML Mon Apr 18 20:56:13 2016 +0200
+++ b/src/Doc/more_antiquote.ML Mon Apr 18 20:56:18 2016 +0200
@@ -1,12 +1,30 @@
(* Title: Doc/more_antiquote.ML
Author: Florian Haftmann, TU Muenchen
-More antiquotations (depending on Isabelle/HOL).
+More antiquotations (partly depending on Isabelle/HOL).
*)
structure More_Antiquote : sig end =
struct
+(* class specifications *)
+
+local
+
+fun class_spec ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val class = Sign.intern_class thy s;
+ in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
+
+in
+
+val _ =
+ Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
+ (fn {context, ...} => class_spec context));
+
+end;
+
(* code theorem antiquotation *)
local
@@ -21,7 +39,7 @@
val ((_, [thm]), _) = Variable.import true [thm] ctxt';
in thm end;
-fun pretty_code_thm src ctxt raw_const =
+fun pretty_code_thm ctxt source raw_const =
let
val thy = Proof_Context.theory_of ctxt;
val const = Code.check_const thy raw_const;
@@ -33,13 +51,13 @@
|> these
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
|> map (holize o no_vars ctxt o Axclass.overload thy);
- in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
+ in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end;
in
val _ =
Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
- (fn {source, context, ...} => pretty_code_thm source context));
+ (fn {source, context, ...} => pretty_code_thm context source));
end;