# HG changeset patch
# User nipkow
# Date 972327492 -7200
# Node ID adff80268127cf13ea05393ef818b8d37d5bd35f
# Parent  a372910d82d6507a0218a93b0cf8ae17d1f4569c
*** empty log message ***

diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/Overloading.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,23 @@
+(*<*)theory Overloading = Overloading1:(*>*)
+instance list :: ("term")ordrel
+by intro_classes
+
+text{*\noindent
+This means. Of course we should also define the meaning of @{text <<=} and
+@{text <<} on lists.
+*}
+
+defs (overloaded)
+prefix_def:
+  "xs <<= (ys::'a::ordrel list)  \<equiv>  \<exists>zs. ys = xs@zs"
+strict_prefix_def:
+  "xs << (ys::'a::ordrel list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
+  
+text{*
+We could also have made the second definition non-overloaded once and for
+all: @{prop"x << y \<equiv> x <<= y \<and> x \<noteq> y"}.  This would have saved us writing
+many similar definitions at different types, but it would also have fixed
+that @{text <<} is defined in terms of @{text <<=} and never the other way
+around. Below you will see why we want to avoid this asymmetry.
+*}
+(*<*)end(*>*)
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/Overloading0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading0.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,40 @@
+(*<*)theory Overloading0 = Main:(*>*)
+
+subsubsection{*An initial example*}
+
+text{* We start with a concept that is required for type classes but already
+useful on its own: \emph{overloading}. Isabelle allows overloading: a
+constant may have multiple definitions at non-overlapping types. For example,
+if we want to introduce the notion of an \emph{inverse} at arbitrary types we
+give it a polymorphic type *}
+
+consts inverse :: "'a \<Rightarrow> 'a"
+
+text{*\noindent
+and provide different definitions at different instances:
+*}
+
+defs (overloaded)
+inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
+inverse_set:  "inverse(A::'a set) \<equiv> -A"
+inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
+
+text{*\noindent
+Isabelle will not complain because the three definitions do not overlap: no
+two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
+common instance. What is more, the recursion in @{thm[source]inverse_pair} is
+benign because the type of @{term inverse} becomes smaller: on the left it is
+@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
+'b"}. The @{text"(overloaded)"} tells Isabelle that the definitions do
+intentionally define @{term inverse} only at instances of its declared type
+@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
+
+However, there is nothing to prevent the user from forming terms such as
+@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
+although we never defined inverse on lists. We hasten to say that there is
+nothing wrong with such terms and theorems. But it would be nice if we could
+prevent their formation, simply because it is very likely that the user did
+not mean to write what he did. Thus he had better not waste his time pursuing
+it further. This requires the use of type classes.
+*}
+(*<*)end(*>*)
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/Overloading1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,41 @@
+(*<*)theory Overloading1 = Main:(*>*)
+
+subsubsection{*Controlled overloading with type classes*}
+
+text{*
+We now start with the theory of ordering relations, which we want to phrase
+in terms of the two binary symbols @{text"<<"} and @{text"<<="}: they have
+been chosen to avoid clashes with @{text"\<le>"} and @{text"<"} in theory @{text
+Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
+introduce the class @{text ordrel}:
+*}
+
+axclass ordrel < "term"
+
+text{*\noindent
+This is a degenerate form of axiomatic type class without any axioms.
+Its sole purpose is to restrict the use of overloaded constants to meaningful
+instances:
+*}
+
+consts
+  "<<"        :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
+  "<<="       :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"             (infixl 50)
+
+instance bool :: ordrel
+by intro_classes
+
+defs (overloaded)
+le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
+less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
+
+text{*
+Now @{prop"False <<= False"} is provable
+*}
+
+lemma "False <<= False"
+by(simp add: le_bool_def)
+
+text{*\noindent
+whereas @{text"[] <<= []"} is not even welltyped. In order to make it welltyped
+we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/Overloading2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,21 @@
+(*<*)theory Overloading2 = Overloading1:(*>*)
+
+text{*
+Of course this is not the only possible definition of the two relations.
+Componentwise
+*}
+
+instance list :: (ordrel)ordrel
+by intro_classes
+
+defs (overloaded)
+le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
+              size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
+
+text{*
+%However, we retract the componetwise comparison of lists and return
+
+Note: only one definition because based on name.
+*}
+(*<*)end(*>*)
+
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/document/Overloading.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,27 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Overloading}%
+\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
+\isacommand{by}\ intro{\isacharunderscore}classes%
+\begin{isamarkuptext}%
+\noindent
+This means. Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
+\isa{{\isacharless}{\isacharless}} on lists.%
+\end{isamarkuptext}%
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+prefix{\isacharunderscore}def{\isacharcolon}\isanewline
+\ \ {\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
+strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
+\ \ {\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}%
+\begin{isamarkuptext}%
+We could also have made the second definition non-overloaded once and for
+all: \isa{x\ {\isacharless}{\isacharless}\ y\ {\isasymequiv}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.  This would have saved us writing
+many similar definitions at different types, but it would also have fixed
+that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and never the other way
+around. Below you will see why we want to avoid this asymmetry.%
+\end{isamarkuptext}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/document/Overloading0.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,45 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Overloading{\isadigit{0}}}%
+%
+\isamarkupsubsubsection{An initial example}
+%
+\begin{isamarkuptext}%
+We start with a concept that is required for type classes but already
+useful on its own: \emph{overloading}. Isabelle allows overloading: a
+constant may have multiple definitions at non-overlapping types. For example,
+if we want to introduce the notion of an \emph{inverse} at arbitrary types we
+give it a polymorphic type%
+\end{isamarkuptext}%
+\isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+and provide different definitions at different instances:%
+\end{isamarkuptext}%
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline
+inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline
+inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+Isabelle will not complain because the three definitions do not overlap: no
+two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
+common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
+benign because the type of \isa{inverse} becomes smaller: on the left it is
+\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
+intentionally define \isa{inverse} only at instances of its declared type
+\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
+
+However, there is nothing to prevent the user from forming terms such as
+\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}},
+although we never defined inverse on lists. We hasten to say that there is
+nothing wrong with such terms and theorems. But it would be nice if we could
+prevent their formation, simply because it is very likely that the user did
+not mean to write what he did. Thus he had better not waste his time pursuing
+it further. This requires the use of type classes.%
+\end{isamarkuptext}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/document/Overloading1.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,44 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Overloading{\isadigit{1}}}%
+%
+\isamarkupsubsubsection{Controlled overloading with type classes}
+%
+\begin{isamarkuptext}%
+We now start with the theory of ordering relations, which we want to phrase
+in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have
+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
+introduce the class \isa{ordrel}:%
+\end{isamarkuptext}%
+\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
+This is a degenerate form of axiomatic type class without any axioms.
+Its sole purpose is to restrict the use of overloaded constants to meaningful
+instances:%
+\end{isamarkuptext}%
+\isacommand{consts}\isanewline
+\ \ {\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
+\ \ {\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
+\isanewline
+\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isanewline
+\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
+\isanewline
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline
+less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%
+\begin{isamarkuptext}%
+Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ False} is provable%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ False{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even welltyped. In order to make it welltyped
+we need to make lists a type of class \isa{ordrel}:%
+\end{isamarkuptext}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/document/Overloading2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,25 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Overloading{\isadigit{2}}}%
+%
+\begin{isamarkuptext}%
+Of course this is not the only possible definition of the two relations.
+Componentwise%
+\end{isamarkuptext}%
+\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
+\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
+\isanewline
+\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
+le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
+\begin{isamarkuptext}%
+%However, we retract the componetwise comparison of lists and return
+
+Note: only one definition because based on name.%
+\end{isamarkuptext}%
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/document/root.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/Types/types.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/types.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -0,0 +1,51 @@
+\chapter{More about Types}
+
+So far we have learned about a few basic types (for example \isa{bool} and
+\isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes
+(\isacommand{datatype}). This chapter will introduce the following more
+advanced material:
+\begin{itemize}
+\item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
+  ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to reason
+  about them.
+\item Introducing your own types: how to introduce your own new types that
+  cannot be constructed with any of the basic methods ({\S}\ref{sec:typedef}).
+\item Type classes: how to specify and reason about axiomatic collections of
+  types ({\S}\ref{sec:axclass}).
+\end{itemize}
+
+\section{Axiomatic type classes}
+\label{sec:axclass}
+\index{axiomatic type class|(}
+\index{*axclass|(}
+
+
+The programming language Haskell has popularized the notion of type classes.
+Isabelle offers the related concept of an \textbf{axiomatic type class}.
+Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
+an axiomatic specification of a class of types. Thus we can talk about a type
+$t$ being in a class $c$, which is written $\tau :: c$.  This is the case of
+$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
+organized in a hierarchy. Thus there is the notion of a class $d$ being a
+\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
+axioms of $c$ are also provable in $d$. Let us now introduce these concepts
+by means of a running example, ordering relations.
+
+\subsection{Overloading}
+\label{sec:overloading}
+\index{overloading|(}
+
+\input{Types/document/Overloading0}
+\input{Types/document/Overloading1}
+\input{Types/document/Overloading}
+\input{Types/document/Overloading2}
+
+\index{overloading|)}
+
+Finally we should remind our readers that \isa{Main} contains a much more
+developed theory of orderings phrased in terms of the usual $\leq$ and
+\isa{<}. It is recommended that, if possible, you base your own
+ordering relations on this theory.
+
+\index{axiomatic type class|)}
+\index{*axclass|)}
diff -r a372910d82d6 -r adff80268127 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Mon Oct 23 18:55:00 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 23 20:58:12 2000 +0200
@@ -81,7 +81,7 @@
 \input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
 \input{Inductive/inductive}
 \input{Advanced/advanced}
-\chapter{More about Types}
+\input{Types/types}
 \chapter{Theory Presentation}
 \chapter{Case Study: The Needhamd-Schroeder Protocol}
 \chapter{Structured Proofs}