*** empty log message ***
authornipkow
Mon Oct 23 20:58:12 2000 +0200 (2000-10-23)
changeset 10305adff80268127
parent 10304 a372910d82d6
child 10306 b0ab988a27a9
*** empty log message ***
doc-src/TutorialI/Types/Overloading.thy
doc-src/TutorialI/Types/Overloading0.thy
doc-src/TutorialI/Types/Overloading1.thy
doc-src/TutorialI/Types/Overloading2.thy
doc-src/TutorialI/Types/document/Overloading.tex
doc-src/TutorialI/Types/document/Overloading0.tex
doc-src/TutorialI/Types/document/Overloading1.tex
doc-src/TutorialI/Types/document/Overloading2.tex
doc-src/TutorialI/Types/document/root.tex
doc-src/TutorialI/Types/types.tex
doc-src/TutorialI/tutorial.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Types/Overloading.thy	Mon Oct 23 20:58:12 2000 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*<*)theory Overloading = Overloading1:(*>*)
     1.5 +instance list :: ("term")ordrel
     1.6 +by intro_classes
     1.7 +
     1.8 +text{*\noindent
     1.9 +This means. Of course we should also define the meaning of @{text <<=} and
    1.10 +@{text <<} on lists.
    1.11 +*}
    1.12 +
    1.13 +defs (overloaded)
    1.14 +prefix_def:
    1.15 +  "xs <<= (ys::'a::ordrel list)  \<equiv>  \<exists>zs. ys = xs@zs"
    1.16 +strict_prefix_def:
    1.17 +  "xs << (ys::'a::ordrel list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
    1.18 +  
    1.19 +text{*
    1.20 +We could also have made the second definition non-overloaded once and for
    1.21 +all: @{prop"x << y \<equiv> x <<= y \<and> x \<noteq> y"}.  This would have saved us writing
    1.22 +many similar definitions at different types, but it would also have fixed
    1.23 +that @{text <<} is defined in terms of @{text <<=} and never the other way
    1.24 +around. Below you will see why we want to avoid this asymmetry.
    1.25 +*}
    1.26 +(*<*)end(*>*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Types/Overloading0.thy	Mon Oct 23 20:58:12 2000 +0200
     2.3 @@ -0,0 +1,40 @@
     2.4 +(*<*)theory Overloading0 = Main:(*>*)
     2.5 +
     2.6 +subsubsection{*An initial example*}
     2.7 +
     2.8 +text{* We start with a concept that is required for type classes but already
     2.9 +useful on its own: \emph{overloading}. Isabelle allows overloading: a
    2.10 +constant may have multiple definitions at non-overlapping types. For example,
    2.11 +if we want to introduce the notion of an \emph{inverse} at arbitrary types we
    2.12 +give it a polymorphic type *}
    2.13 +
    2.14 +consts inverse :: "'a \<Rightarrow> 'a"
    2.15 +
    2.16 +text{*\noindent
    2.17 +and provide different definitions at different instances:
    2.18 +*}
    2.19 +
    2.20 +defs (overloaded)
    2.21 +inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
    2.22 +inverse_set:  "inverse(A::'a set) \<equiv> -A"
    2.23 +inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
    2.24 +
    2.25 +text{*\noindent
    2.26 +Isabelle will not complain because the three definitions do not overlap: no
    2.27 +two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
    2.28 +common instance. What is more, the recursion in @{thm[source]inverse_pair} is
    2.29 +benign because the type of @{term inverse} becomes smaller: on the left it is
    2.30 +@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
    2.31 +'b"}. The @{text"(overloaded)"} tells Isabelle that the definitions do
    2.32 +intentionally define @{term inverse} only at instances of its declared type
    2.33 +@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
    2.34 +
    2.35 +However, there is nothing to prevent the user from forming terms such as
    2.36 +@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
    2.37 +although we never defined inverse on lists. We hasten to say that there is
    2.38 +nothing wrong with such terms and theorems. But it would be nice if we could
    2.39 +prevent their formation, simply because it is very likely that the user did
    2.40 +not mean to write what he did. Thus he had better not waste his time pursuing
    2.41 +it further. This requires the use of type classes.
    2.42 +*}
    2.43 +(*<*)end(*>*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/Types/Overloading1.thy	Mon Oct 23 20:58:12 2000 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*<*)theory Overloading1 = Main:(*>*)
     3.5 +
     3.6 +subsubsection{*Controlled overloading with type classes*}
     3.7 +
     3.8 +text{*
     3.9 +We now start with the theory of ordering relations, which we want to phrase
    3.10 +in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have
    3.11 +been chosen to avoid clashes with @{text"\<le>"} and @{text"<"} in theory @{text
    3.12 +Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
    3.13 +introduce the class @{text ordrel}:
    3.14 +*}
    3.15 +
    3.16 +axclass ordrel < "term"
    3.17 +
    3.18 +text{*\noindent
    3.19 +This is a degenerate form of axiomatic type class without any axioms.
    3.20 +Its sole purpose is to restrict the use of overloaded constants to meaningful
    3.21 +instances:
    3.22 +*}
    3.23 +
    3.24 +consts
    3.25 +  "<<"        :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
    3.26 +  "<<="       :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
    3.27 +
    3.28 +instance bool :: ordrel
    3.29 +by intro_classes
    3.30 +
    3.31 +defs (overloaded)
    3.32 +le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
    3.33 +less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
    3.34 +
    3.35 +text{*
    3.36 +Now @{prop"False <<= False"} is provable
    3.37 +*}
    3.38 +
    3.39 +lemma "False <<= False"
    3.40 +by(simp add: le_bool_def)
    3.41 +
    3.42 +text{*\noindent
    3.43 +whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
    3.44 +we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Mon Oct 23 20:58:12 2000 +0200
     4.3 @@ -0,0 +1,21 @@
     4.4 +(*<*)theory Overloading2 = Overloading1:(*>*)
     4.5 +
     4.6 +text{*
     4.7 +Of course this is not the only possible definition of the two relations.
     4.8 +Componentwise
     4.9 +*}
    4.10 +
    4.11 +instance list :: (ordrel)ordrel
    4.12 +by intro_classes
    4.13 +
    4.14 +defs (overloaded)
    4.15 +le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
    4.16 +              size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
    4.17 +
    4.18 +text{*
    4.19 +%However, we retract the componetwise comparison of lists and return
    4.20 +
    4.21 +Note: only one definition because based on name.
    4.22 +*}
    4.23 +(*<*)end(*>*)
    4.24 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/TutorialI/Types/document/Overloading.tex	Mon Oct 23 20:58:12 2000 +0200
     5.3 @@ -0,0 +1,27 @@
     5.4 +%
     5.5 +\begin{isabellebody}%
     5.6 +\def\isabellecontext{Overloading}%
     5.7 +\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
     5.8 +\isacommand{by}\ intro{\isacharunderscore}classes%
     5.9 +\begin{isamarkuptext}%
    5.10 +\noindent
    5.11 +This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
    5.12 +\isa{{\isacharless}{\isacharless}} on lists.%
    5.13 +\end{isamarkuptext}%
    5.14 +\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
    5.15 +prefix{\isacharunderscore}def{\isacharcolon}\isanewline
    5.16 +\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
    5.17 +strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
    5.18 +\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}%
    5.19 +\begin{isamarkuptext}%
    5.20 +We could also have made the second definition non-overloaded once and for
    5.21 +all: \isa{x\ {\isacharless}{\isacharless}\ y\ {\isasymequiv}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.  This would have saved us writing
    5.22 +many similar definitions at different types, but it would also have fixed
    5.23 +that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and never the other way
    5.24 +around. Below you will see why we want to avoid this asymmetry.%
    5.25 +\end{isamarkuptext}%
    5.26 +\end{isabellebody}%
    5.27 +%%% Local Variables:
    5.28 +%%% mode: latex
    5.29 +%%% TeX-master: "root"
    5.30 +%%% End:
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Oct 23 20:58:12 2000 +0200
     6.3 @@ -0,0 +1,45 @@
     6.4 +%
     6.5 +\begin{isabellebody}%
     6.6 +\def\isabellecontext{Overloading{\isadigit{0}}}%
     6.7 +%
     6.8 +\isamarkupsubsubsection{An initial example}
     6.9 +%
    6.10 +\begin{isamarkuptext}%
    6.11 +We start with a concept that is required for type classes but already
    6.12 +useful on its own: \emph{overloading}. Isabelle allows overloading: a
    6.13 +constant may have multiple definitions at non-overlapping types. For example,
    6.14 +if we want to introduce the notion of an \emph{inverse} at arbitrary types we
    6.15 +give it a polymorphic type%
    6.16 +\end{isamarkuptext}%
    6.17 +\isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
    6.18 +\begin{isamarkuptext}%
    6.19 +\noindent
    6.20 +and provide different definitions at different instances:%
    6.21 +\end{isamarkuptext}%
    6.22 +\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
    6.23 +inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline
    6.24 +inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline
    6.25 +inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    6.26 +\begin{isamarkuptext}%
    6.27 +\noindent
    6.28 +Isabelle will not complain because the three definitions do not overlap: no
    6.29 +two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
    6.30 +common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
    6.31 +benign because the type of \isa{inverse} becomes smaller: on the left it is
    6.32 +\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
    6.33 +intentionally define \isa{inverse} only at instances of its declared type
    6.34 +\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
    6.35 +
    6.36 +However, there is nothing to prevent the user from forming terms such as
    6.37 +\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}},
    6.38 +although we never defined inverse on lists. We hasten to say that there is
    6.39 +nothing wrong with such terms and theorems. But it would be nice if we could
    6.40 +prevent their formation, simply because it is very likely that the user did
    6.41 +not mean to write what he did. Thus he had better not waste his time pursuing
    6.42 +it further. This requires the use of type classes.%
    6.43 +\end{isamarkuptext}%
    6.44 +\end{isabellebody}%
    6.45 +%%% Local Variables:
    6.46 +%%% mode: latex
    6.47 +%%% TeX-master: "root"
    6.48 +%%% End:
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Mon Oct 23 20:58:12 2000 +0200
     7.3 @@ -0,0 +1,44 @@
     7.4 +%
     7.5 +\begin{isabellebody}%
     7.6 +\def\isabellecontext{Overloading{\isadigit{1}}}%
     7.7 +%
     7.8 +\isamarkupsubsubsection{Controlled overloading with type classes}
     7.9 +%
    7.10 +\begin{isamarkuptext}%
    7.11 +We now start with the theory of ordering relations, which we want to phrase
    7.12 +in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have
    7.13 +been chosen to avoid clashes with \isa{{\isasymle}} and \isa{{\isacharless}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
    7.14 +introduce the class \isa{ordrel}:%
    7.15 +\end{isamarkuptext}%
    7.16 +\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%
    7.17 +\begin{isamarkuptext}%
    7.18 +\noindent
    7.19 +This is a degenerate form of axiomatic type class without any axioms.
    7.20 +Its sole purpose is to restrict the use of overloaded constants to meaningful
    7.21 +instances:%
    7.22 +\end{isamarkuptext}%
    7.23 +\isacommand{consts}\isanewline
    7.24 +\ \ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ \ \ \ \ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
    7.25 +\ \ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ \ \ \ \ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
    7.26 +\isanewline
    7.27 +\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isanewline
    7.28 +\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
    7.29 +\isanewline
    7.30 +\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
    7.31 +le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline
    7.32 +less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%
    7.33 +\begin{isamarkuptext}%
    7.34 +Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ False} is provable%
    7.35 +\end{isamarkuptext}%
    7.36 +\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ False{\isachardoublequote}\isanewline
    7.37 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
    7.38 +\begin{isamarkuptext}%
    7.39 +\noindent
    7.40 +whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped
    7.41 +we need to make lists a type of class \isa{ordrel}:%
    7.42 +\end{isamarkuptext}%
    7.43 +\end{isabellebody}%
    7.44 +%%% Local Variables:
    7.45 +%%% mode: latex
    7.46 +%%% TeX-master: "root"
    7.47 +%%% End:
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Oct 23 20:58:12 2000 +0200
     8.3 @@ -0,0 +1,25 @@
     8.4 +%
     8.5 +\begin{isabellebody}%
     8.6 +\def\isabellecontext{Overloading{\isadigit{2}}}%
     8.7 +%
     8.8 +\begin{isamarkuptext}%
     8.9 +Of course this is not the only possible definition of the two relations.
    8.10 +Componentwise%
    8.11 +\end{isamarkuptext}%
    8.12 +\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
    8.13 +\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
    8.14 +\isanewline
    8.15 +\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
    8.16 +le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
    8.17 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
    8.18 +\begin{isamarkuptext}%
    8.19 +%However, we retract the componetwise comparison of lists and return
    8.20 +
    8.21 +Note: only one definition because based on name.%
    8.22 +\end{isamarkuptext}%
    8.23 +\isanewline
    8.24 +\end{isabellebody}%
    8.25 +%%% Local Variables:
    8.26 +%%% mode: latex
    8.27 +%%% TeX-master: "root"
    8.28 +%%% End:
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/TutorialI/Types/document/root.tex	Mon Oct 23 20:58:12 2000 +0200
     9.3 @@ -0,0 +1,4 @@
     9.4 +\documentclass{article}
     9.5 +\begin{document}
     9.6 +xxx
     9.7 +\end{document}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/TutorialI/Types/types.tex	Mon Oct 23 20:58:12 2000 +0200
    10.3 @@ -0,0 +1,51 @@
    10.4 +\chapter{More about Types}
    10.5 +
    10.6 +So far we have learned about a few basic types (for example \isa{bool} and
    10.7 +\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes
    10.8 +(\isacommand{datatype}). This chapter will introduce the following more
    10.9 +advanced material:
   10.10 +\begin{itemize}
   10.11 +\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
   10.12 +  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
   10.13 +  about them.
   10.14 +\item Introducing your own types: how to introduce your own new types that
   10.15 +  cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
   10.16 +\item Type classes: how to specify and reason about axiomatic collections of
   10.17 +  types ({\S}\ref{sec:axclass}).
   10.18 +\end{itemize}
   10.19 +
   10.20 +\section{Axiomatic type classes}
   10.21 +\label{sec:axclass}
   10.22 +\index{axiomatic type class|(}
   10.23 +\index{*axclass|(}
   10.24 +
   10.25 +
   10.26 +The programming language Haskell has popularized the notion of type classes.
   10.27 +Isabelle offers the related concept of an \textbf{axiomatic type class}.
   10.28 +Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
   10.29 +an axiomatic specification of a class of types. Thus we can talk about a type
   10.30 +$t$ being in a class $c$, which is written $\tau :: c$.  This is the case of
   10.31 +$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
   10.32 +organized in a hierarchy. Thus there is the notion of a class $d$ being a
   10.33 +\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
   10.34 +axioms of $c$ are also provable in $d$. Let us now introduce these concepts
   10.35 +by means of a running example, ordering relations.
   10.36 +
   10.37 +\subsection{Overloading}
   10.38 +\label{sec:overloading}
   10.39 +\index{overloading|(}
   10.40 +
   10.41 +\input{Types/document/Overloading0}
   10.42 +\input{Types/document/Overloading1}
   10.43 +\input{Types/document/Overloading}
   10.44 +\input{Types/document/Overloading2}
   10.45 +
   10.46 +\index{overloading|)}
   10.47 +
   10.48 +Finally we should remind our readers that \isa{Main} contains a much more
   10.49 +developed theory of orderings phrased in terms of the usual $\leq$ and
   10.50 +\isa{<}. It is recommended that, if possible, you base your own
   10.51 +ordering relations on this theory.
   10.52 +
   10.53 +\index{axiomatic type class|)}
   10.54 +\index{*axclass|)}
    11.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Oct 23 18:55:00 2000 +0200
    11.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 23 20:58:12 2000 +0200
    11.3 @@ -81,7 +81,7 @@
    11.4  \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
    11.5  \input{Inductive/inductive}
    11.6  \input{Advanced/advanced}
    11.7 -\chapter{More about Types}
    11.8 +\input{Types/types}
    11.9  \chapter{Theory Presentation}
   11.10  \chapter{Case Study: The Needhamd-Schroeder Protocol}
   11.11  \chapter{Structured Proofs}