author nipkow Mon, 06 Nov 2000 11:32:23 +0100 changeset 10396 5ab08609e6c8 parent 10395 7ef380745743 child 10397 e2d0dda41f2c
*** empty log message ***
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -21,32 +21,24 @@
component decreases (as in the inner call in the third equation).

In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
+This is called \textbf{well-founded
recursion}\indexbold{recursion!well-founded}\index{well-founded
-recursion|see{recursion, well-founded}}.  A relation $<$ is
-\bfindex{well-founded} if it has no infinite descending chain $\cdots < -a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
-of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
-of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a well-founded relation.  For a
-systematic account of termination proofs via well-founded relations
-see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of well-founded relations. For example
-@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
-well-founded.
+recursion|see{recursion, well-founded}}. Clearly, a function definition is
+total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+left-hand side of an equation and $r$ the argument of some recursive call on
+the corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations see, for

-Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a well-founded relation on the argument type
-of the function. For example, \isaindexbold{measure} is defined by
-@{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
-and it has been proved that @{term"measure f"} is always well-founded.
-
-In addition to @{term measure}, the library provides
-a number of further constructions for obtaining well-founded relations.
-Above we have already met @{text"<*lex*>"} of type
-@{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"}
-Of course the lexicographic product can also be interated, as in the following
-function definition:
+Each \isacommand{recdef} definition should be accompanied (after the name of
+the function) by a well-founded relation on the argument type of the
+function.  The HOL library formalizes some of the most important
+constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
+example, @{term"measure f"} is always well-founded, and the lexicographic
+product of two well-founded relations is again well-founded, which we relied
+on when defining Ackermann's function above.
+Of course the lexicographic product can also be interated:
*}

consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"
@@ -58,20 +50,10 @@
"contrived(0,0,0)     = 0"

text{*
-Lexicographic products of measure functions already go a long way. A
-further useful construction is the embedding of some type in an
-existing well-founded relation via the inverse image of a function:
-@{thm[display,show_types]inv_image_def[no_vars]}
-\begin{sloppypar}
-\noindent
-For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where
-@{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat}
-(as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}).
-\end{sloppypar}
-
-%Finally there is also {finite_psubset} the proper subset relation on finite sets
-
-All the above constructions are known to \isacommand{recdef}. Thus you
+Lexicographic products of measure functions already go a long
+way. Furthermore you may embedding some type in an
+existing well-founded relation via the inverse image construction @{term
+inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
will never have to prove well-foundedness of any relation composed
solely of these building blocks. But of course the proof of
termination of your function definition, i.e.\ that the arguments
@@ -87,18 +69,18 @@
"f 0 = 0"
"f (Suc n) = f n"

-text{*
+text{*\noindent
Since \isacommand{recdef} is not prepared for @{term id}, the identity
function, this leads to the complaint that it could not prove
-@{prop"wf (id less_than)"}, the well-foundedness of @{term"id
-less_than"}. We should first have proved that @{term id} preserves well-foundedness
+@{prop"wf (id less_than)"}.
+We should first have proved that @{term id} preserves well-foundedness
*}

lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
by simp;

text{*\noindent
-and should have added the following hint to our above definition:
+and should have appended the following hint to our above definition:
*}
(*<*)
consts g :: "nat \<Rightarrow> nat"
@@ -107,4 +89,4 @@
"g (Suc n) = g n"
(*>*)
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -23,36 +23,24 @@
component decreases (as in the inner call in the third equation).

In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
+This is called \textbf{well-founded
recursion}\indexbold{recursion!well-founded}\index{well-founded
-recursion|see{recursion, well-founded}}.  A relation $<$ is
-\bfindex{well-founded} if it has no infinite descending chain $\cdots < -a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
-of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
-of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a well-founded relation.  For a
-systematic account of termination proofs via well-founded relations
-see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of well-founded relations. For example
-\isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
-well-founded.
+recursion|see{recursion, well-founded}}. Clearly, a function definition is
+total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+left-hand side of an equation and $r$ the argument of some recursive call on
+the corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations see, for

-Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a well-founded relation on the argument type
-of the function. For example, \isaindexbold{measure} is defined by
-\begin{isabelle}%
-\ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
-\end{isabelle}
-and it has been proved that \isa{measure\ f} is always well-founded.
-
-In addition to \isa{measure}, the library provides
-a number of further constructions for obtaining well-founded relations.
-Above we have already met \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} of type
-\begin{isabelle}%
-\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}{\isacharparenright}set{\isachardoublequote}%
-\end{isabelle}
-Of course the lexicographic product can also be interated, as in the following
-function definition:%
+Each \isacommand{recdef} definition should be accompanied (after the name of
+the function) by a well-founded relation on the argument type of the
+function.  The HOL library formalizes some of the most important
+constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
+example, \isa{measure\ f} is always well-founded, and the lexicographic
+product of two well-founded relations is again well-founded, which we relied
+on when defining Ackermann's function above.
+Of course the lexicographic product can also be interated:%
\end{isamarkuptext}%
\isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ contrived\isanewline
@@ -62,23 +50,9 @@
\begin{isamarkuptext}%
-Lexicographic products of measure functions already go a long way. A
-further useful construction is the embedding of some type in an
-existing well-founded relation via the inverse image of a function:
-\begin{isabelle}%
-\ \ \ \ \ inv{\isacharunderscore}image\ {\isacharparenleft}r{\isasymColon}{\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set{\isacharparenright}\ {\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymequiv}\isanewline
-\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharcomma}\ y{\isasymColon}{\isacharprime}a{\isacharparenright}{\isachardot}\ {\isacharparenleft}f\ x{\isacharcomma}\ f\ y{\isacharparenright}\ {\isasymin}\ r{\isacharbraceright}%
-\end{isabelle}
-\begin{sloppypar}
-\noindent
-For example, \isa{measure} is actually defined as \isa{inv{\isacharunderscore}mage\ less{\isacharunderscore}than}, where
-\isa{less{\isacharunderscore}than} of type \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set} is the less-than relation on type \isa{nat}
-(as opposed to \isa{op\ {\isacharless}}, which is of type \isa{{\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool}).
-\end{sloppypar}
-
-%Finally there is also {finite_psubset} the proper subset relation on finite sets
-
-All the above constructions are known to \isacommand{recdef}. Thus you
+Lexicographic products of measure functions already go a long
+way. Furthermore you may embedding some type in an
+existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
will never have to prove well-foundedness of any relation composed
solely of these building blocks. But of course the proof of
termination of your function definition, i.e.\ that the arguments
@@ -93,15 +67,17 @@
{\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}%
\begin{isamarkuptext}%
+\noindent
Since \isacommand{recdef} is not prepared for \isa{id}, the identity
function, this leads to the complaint that it could not prove
-\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the well-foundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves well-foundedness%
+\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}.
+We should first have proved that \isa{id} preserves well-foundedness%
\end{isamarkuptext}%
\isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}\ simp%
\begin{isamarkuptext}%
\noindent
-and should have added the following hint to our above definition:%
+and should have appended the following hint to our above definition:%
\end{isamarkuptext}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/AB.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -303,6 +303,6 @@
similar to the other cases (which are automatic in Isabelle). We conclude
overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.  *}
+atypical for pencil-and-paper proofs, once analysed in detail.  *}

(*<*)end(*>*)
--- a/doc-src/TutorialI/Inductive/Star.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -8,10 +8,9 @@

A perfect example of an inductive definition is the reflexive transitive
closure of a relation. This concept was already introduced in
-\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
-the operator @{text"^*"} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
-inductive definitions are not yet available. But now they are:
+\S\ref{sec:Relations}, where the operator @{text"^*"} was
+defined as a least fixed point because
+inductive definitions were not yet available. But now they are:
*}

consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -276,7 +276,7 @@
similar to the other cases (which are automatic in Isabelle). We conclude
overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pen-and-paper proofs, once analysed in detail.%
+atypical for pencil-and-paper proofs, once analysed in detail.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Star.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -12,10 +12,9 @@

A perfect example of an inductive definition is the reflexive transitive
closure of a relation. This concept was already introduced in
-\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
-the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
-fixed point because at that point in the theory hierarchy
-inductive definitions are not yet available. But now they are:%
+\S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
+defined as a least fixed point because
+inductive definitions were not yet available. But now they are:%
\end{isamarkuptext}%
\isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -5,9 +5,10 @@
text{*\noindent
Now that we have learned about rules and logic, we take another look at the
finer points of induction. The two questions we answer are: what to do if the
-proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas. We conclude with some slightly subtle
-examples of induction.
+proposition to be proved is not directly amenable to induction
+(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
+and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
+with an extended example of induction (\S\ref{sec:CTL-revisited}).
*};

subsection{*Massaging the proposition*};
@@ -160,7 +161,7 @@
not introduce an inconsistency because, for example, the identity function
satisfies it.}
for @{term"f"} it follows that @{prop"n <= f n"}, which can
-be proved by induction on @{term"f n"}. Following the recipy outlined
+be proved by induction on @{term"f n"}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:
*};

@@ -278,7 +279,7 @@
Now it is straightforward to derive the original version of
@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
-remove the trivial condition @{prop"n < Sc n"}. Fortunately, this
+remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:
*};
@@ -287,17 +288,11 @@
by(insert induct_lem, blast);

text{*
-Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{well-founded
-induction}\indexbold{induction!well-founded}\index{well-founded
-induction|see{induction, well-founded}} (@{thm[source]wf_induct}):
-@{thm[display]wf_induct[no_vars]}
-where @{term"wf r"} means that the relation @{term r} is well-founded
-(see \S\ref{sec:well-founded}).
-For example, theorem @{thm[source]nat_less_induct} can be viewed (and
-derived) as a special case of @{thm[source]wf_induct} where
-@{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.
-For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.
+Finally we should remind the reader that HOL already provides the mother of
+all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
+example theorem @{thm[source]nat_less_induct} can be viewed (and derived) as
+a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
+@{typ nat}. The details can be found in the HOL library.
*};

(*<*)
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -6,13 +6,13 @@
\noindent
Now that we have learned about rules and logic, we take another look at the
finer points of induction. The two questions we answer are: what to do if the
-proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas. We conclude with some slightly subtle
-examples of induction.%
+proposition to be proved is not directly amenable to induction
+(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
+and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
+with an extended example of induction (\S\ref{sec:CTL-revisited}).%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Massaging the proposition%
-}
+\isamarkupsubsection{Massaging the proposition}
%
\begin{isamarkuptext}%
\label{sec:ind-var-in-prems}
@@ -123,8 +123,7 @@
the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Beyond structural and recursion induction%
-}
+\isamarkupsubsection{Beyond structural and recursion induction}
%
\begin{isamarkuptext}%
\label{sec:complete-ind}
@@ -153,7 +152,7 @@
not introduce an inconsistency because, for example, the identity function
satisfies it.}
for \isa{f} it follows that \isa{n\ {\isasymle}\ f\ n}, which can
-be proved by induction on \isa{f\ n}. Following the recipy outlined
+be proved by induction on \isa{f\ n}. Following the recipe outlined
above, we have to phrase the proposition as follows to allow induction:%
\end{isamarkuptext}%
\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
@@ -242,8 +241,7 @@
\end{quote}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Derivation of new induction schemas%
-}
+\isamarkupsubsection{Derivation of new induction schemas}
%
\begin{isamarkuptext}%
\label{sec:derive-ind}
@@ -273,26 +271,18 @@
Now it is straightforward to derive the original version of
\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
-remove the trivial condition \isa{n\ {\isacharless}\ Sc\ n}. Fortunately, this
+remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
happens automatically when we add the lemma as a new premise to the
desired goal:%
\end{isamarkuptext}%
\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
-Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{well-founded
-induction}\indexbold{induction!well-founded}\index{well-founded
-induction|see{induction, well-founded}} (\isa{wf{\isacharunderscore}induct}):
-\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
-\end{isabelle}
-where \isa{wf\ r} means that the relation \isa{r} is well-founded
-(see \S\ref{sec:well-founded}).
-For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
-derived) as a special case of \isa{wf{\isacharunderscore}induct} where
-\isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.
-For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.%
+Finally we should remind the reader that HOL already provides the mother of
+all inductions, well-founded induction (see \S\ref{sec:Well-founded}).  For
+example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and derived) as
+a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
+\isa{nat}. The details can be found in the HOL library.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Itrev}%
%
-\isamarkupsection{Induction heuristics%
-}
+\isamarkupsection{Induction heuristics}
%
\begin{isamarkuptext}%
\label{sec:InductionHeuristics}
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{case{\isacharunderscore}exprs}%
%
-\isamarkupsubsection{Case expressions%
-}
+\isamarkupsubsection{Case expressions}
%
\begin{isamarkuptext}%
\label{sec:case-expressions}
@@ -49,8 +48,7 @@
indicate their scope%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Structural induction and case distinction%
-}
+\isamarkupsubsection{Structural induction and case distinction}
%
\begin{isamarkuptext}%
\indexbold{structural induction}
--- a/doc-src/TutorialI/Misc/document/simp.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsubsubsection{Simplification rules%
-}
+\isamarkupsubsubsection{Simplification rules}
%
\begin{isamarkuptext}%
\indexbold{simplification rule}
@@ -40,8 +39,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The simplification method%
-}
+\isamarkupsubsubsection{The simplification method}
%
\begin{isamarkuptext}%
\index{*simp (method)|bold}
@@ -57,8 +55,7 @@
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
%
-}
%
\begin{isamarkuptext}%
If a certain theorem is merely needed in a few proofs by simplification,
@@ -76,8 +73,7 @@
\end{quote}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Assumptions%
-}
+\isamarkupsubsubsection{Assumptions}
%
\begin{isamarkuptext}%
\index{simplification!with/of assumptions}
@@ -127,8 +123,7 @@
other arguments.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Rewriting with definitions%
-}
+\isamarkupsubsubsection{Rewriting with definitions}
%
\begin{isamarkuptext}%
\index{simplification!with definitions}
@@ -176,8 +171,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying let-expressions%
-}
+\isamarkupsubsubsection{Simplifying let-expressions}
%
\begin{isamarkuptext}%
\index{simplification!of let-expressions}
@@ -196,8 +190,7 @@
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations%
-}
+\isamarkupsubsubsection{Conditional equations}
%
\begin{isamarkuptext}%
So far all examples of rewrite rules were equations. The simplifier also
@@ -224,8 +217,7 @@
assumption of the subgoal.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Automatic case splits%
-}
+\isamarkupsubsubsection{Automatic case splits}
%
\begin{isamarkuptext}%
\indexbold{case splits}\index{*split|(}
@@ -318,8 +310,7 @@
\index{*split|)}%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Arithmetic%
-}
+\isamarkupsubsubsection{Arithmetic}
%
\begin{isamarkuptext}%
\index{arithmetic}
@@ -339,8 +330,7 @@
is not proved by simplification and requires \isa{arith}.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Tracing%
-}
+\isamarkupsubsubsection{Tracing}
%
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
--- a/doc-src/TutorialI/Types/Axioms.thy	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Mon Nov 06 11:32:23 2000 +0100
@@ -135,30 +135,11 @@
apply(blast intro: refl);
done

-text{*\noindent
-The result is the following subclass diagram:
-$-\begin{array}{c} -\isa{term}\\ -|\\ -\isa{ordrel}\\ -|\\ -\isa{strord}\\ -|\\ -\isa{parord} -\end{array} -$
+text{*
+The subclass relation must always be acyclic. Therefore Isabelle will
+complain if you also prove the relationship @{text"strord < parord"}.
+*}

-In general, the subclass diagram must be acyclic. Therefore Isabelle will
-complain if you also prove the relationship @{text"strord < parord"}.
-Multiple inheritance is however permitted.
-
-This finishes our demonstration of type classes based on orderings.  We
-remind our readers that \isa{Main} contains a much more developed theory of
-orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
-It is recommended that, if possible,
-you base your own ordering relations on this theory.
-*}

(*
instance strord < parord
@@ -174,6 +155,61 @@
done
*)

+subsubsection{*Multiple inheritance and sorts*}
+
+text{*
+A class may inherit from more than one direct superclass. This is called
+multiple inheritance and is certainly permitted. For example we could define
+the classes of well-founded orderings and well-orderings:
+*}
+
+axclass wford < parord
+wford: "wf {(y,x). y << x}"
+
+axclass wellord < linord, wford
+
+text{*\noindent
+The last line expresses the usual definition: a well-ordering is a linear
+well-founded ordering. The result is the subclass diagram in
+Figure~\ref{fig:subclass}.
+
+\begin{figure}[htbp]
+$+\begin{array}{r@ {}r@ {}c@ {}l@ {}l} +& & \isa{term}\\ +& & |\\ +& & \isa{ordrel}\\ +& & |\\ +& & \isa{strord}\\ +& & |\\ +& & \isa{parord} \\ +& / & & \backslash \\ +\isa{linord} & & & & \isa{wford} \\ +& \backslash & & / \\ +& & \isa{wellord} +\end{array} +$
+\caption{Subclass diagramm}
+\label{fig:subclass}
+\end{figure}
+
+Since class @{text wellord} does not introduce any new axioms, it can simply
+be viewed as the intersection of the two classes @{text linord} and @{text
+wford}. Such intersections need not be given a new name but can be created on
+the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
+represents the intersection of the $C@i$. Such an expression is called a
+\bfindex{sort}, and sorts can appear in most places where we have only shown
+classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
+In fact, @{text"'a::ord"} is short for @{text"'a::{ord}"}.
+However, we do not pursue this rarefied concept further.
+
+This concludes our demonstration of type classes based on orderings.  We
+remind our readers that \isa{Main} contains a theory of
+orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
+It is recommended that, if possible,
+you base your own ordering relations on this theory.
+*}
+
subsubsection{*Inconsistencies*}

text{* The reader may be wondering what happens if we, maybe accidentally,
--- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Nov 04 18:54:22 2000 +0100
@@ -26,6 +26,10 @@
le   :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)

text{*\noindent
+Note that only one occurrence of a type variable in a type needs to be
+constrained with a class; the constraint is propagated to the other
+occurrences automatically.
+
So far there is not a single type of class @{text ordrel}. To breathe life
into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
@{text ordrel}:
--- a/doc-src/TutorialI/Types/Overloading2.thy	Sat Nov 04 18:54:22 2000 +0100
@@ -16,6 +16,35 @@

text{*\noindent
The infix function @{text"!"} yields the nth element of a list.
-%However, we retract the componetwise comparison of lists and return
-%Note: only one definition because based on name.
+*}
+
+
+text{*
+HOL comes with a number of overloaded constants and corresponding classes.
+defined on all numeric types and somtimes on other types as well, for example
+@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{lll}
+Constant & Type & Syntax \\
+\hline
+@{term 0} & @{text "'a::zero"} \\
+@{text"+"} & @{text "('a::plus) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 65) \\
+@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a \<Rightarrow> 'a"} &  (infixl 65) \\
+@{text"*"} & @{text "('a::times) \<Rightarrow> 'a \<Rightarrow> 'a"} & (infixl 70) \\
+@{text"^"} & @{text "('a::power) \<Rightarrow> nat \<Rightarrow> 'a"} & (infixr 80) \\
+@{text"-"} & @{text "('a::minus) \<Rightarrow> 'a"} \\
+@{term abs} &  @{text "('a::minus) \<Rightarrow> 'a"} \\
+@{text"\<le>"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
+@{text"<"} & @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> bool"} & (infixl 50) \\
+@{term min} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
+@{term max} &  @{text "('a::ord) \<Rightarrow> 'a \<Rightarrow> 'a"} \\
+\end{tabular}
+\end{center}
+\end{table}
*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Axioms}%
%
-\isamarkupsubsection{Axioms%
-}
+\isamarkupsubsection{Axioms}
%
\begin{isamarkuptext}%
Now we want to attach axioms to our classes. Then we can reason on the
@@ -12,8 +11,7 @@
our above ordering relations.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Partial orders%
-}
+\isamarkupsubsubsection{Partial orders}
%
\begin{isamarkuptext}%
A \emph{partial order} is a subclass of \isa{ordrel}
@@ -88,8 +86,7 @@
proof for each instance.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Linear orders%
-}
+\isamarkupsubsubsection{Linear orders}
%
\begin{isamarkuptext}%
If any two elements of a partial order are comparable it is a
@@ -115,8 +112,7 @@
section.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Strict orders%
-}
+\isamarkupsubsubsection{Strict orders}
%
\begin{isamarkuptext}%
An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
@@ -139,33 +135,64 @@
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
+The subclass relation must always be acyclic. Therefore Isabelle will
+complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
+\end{isamarkuptext}%
+%
+\isamarkupsubsubsection{Multiple inheritance and sorts}
+%
+\begin{isamarkuptext}%
+A class may inherit from more than one direct superclass. This is called
+multiple inheritance and is certainly permitted. For example we could define
+the classes of well-founded orderings and well-orderings:%
+\end{isamarkuptext}%
+\isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline
+wford{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ y\ {\isacharless}{\isacharless}\ x{\isacharbraceright}{\isachardoublequote}\isanewline
+\isanewline
+\isacommand{axclass}\ wellord\ {\isacharless}\ linord{\isacharcomma}\ wford%
+\begin{isamarkuptext}%
\noindent
-The result is the following subclass diagram:
+The last line expresses the usual definition: a well-ordering is a linear
+well-founded ordering. The result is the subclass diagram in
+Figure~\ref{fig:subclass}.
+
+\begin{figure}[htbp]
$-\begin{array}{c} -\isa{term}\\ -|\\ -\isa{ordrel}\\ -|\\ -\isa{strord}\\ -|\\ -\isa{parord} +\begin{array}{r@ {}r@ {}c@ {}l@ {}l} +& & \isa{term}\\ +& & |\\ +& & \isa{ordrel}\\ +& & |\\ +& & \isa{strord}\\ +& & |\\ +& & \isa{parord} \\ +& / & & \backslash \\ +\isa{linord} & & & & \isa{wford} \\ +& \backslash & & / \\ +& & \isa{wellord} \end{array}$
+\caption{Subclass diagramm}
+\label{fig:subclass}
+\end{figure}

-In general, the subclass diagram must be acyclic. Therefore Isabelle will
-complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.
-Multiple inheritance is however permitted.
+Since class \isa{wellord} does not introduce any new axioms, it can simply
+be viewed as the intersection of the two classes \isa{linord} and \isa{wford}. Such intersections need not be given a new name but can be created on
+the fly: the expression $\{C@1,\dots,C@n\}$, where the $C@i$ are classes,
+represents the intersection of the $C@i$. Such an expression is called a
+\bfindex{sort}, and sorts can appear in most places where we have only shown
+classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
+In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ord} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}ord{\isacharbraceright}}.
+However, we do not pursue this rarefied concept further.

-This finishes our demonstration of type classes based on orderings.  We
-remind our readers that \isa{Main} contains a much more developed theory of
+This concludes our demonstration of type classes based on orderings.  We
+remind our readers that \isa{Main} contains a theory of
orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
It is recommended that, if possible,
you base your own ordering relations on this theory.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Inconsistencies%
-}
+\isamarkupsubsubsection{Inconsistencies}
%
\begin{isamarkuptext}%
The reader may be wondering what happens if we, maybe accidentally,
--- a/doc-src/TutorialI/Types/document/Overloading0.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -8,8 +8,7 @@
constant may have multiple definitions at non-overlapping types.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{An initial example%
-}
+\isamarkupsubsubsection{An initial example}
%
\begin{isamarkuptext}%
If we want to introduce the notion of an \emph{inverse} for arbitrary types we
--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
%
-}
%
\begin{isamarkuptext}%
We now start with the theory of ordering relations, which we want to phrase
@@ -26,6 +25,10 @@
\ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
+Note that only one occurrence of a type variable in a type needs to be
+constrained with a class; the constraint is propagated to the other
+occurrences automatically.
+
So far there is not a single type of class \isa{ordrel}. To breathe life
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
\isa{ordrel}:%
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -16,9 +16,38 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ 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}%
\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.
-%However, we retract the componetwise comparison of lists and return
-%Note: only one definition because based on name.%
+The infix function \isa{{\isacharbang}} yields the nth element of a list.%
+\end{isamarkuptext}%
+%
+%
+\begin{isamarkuptext}%
+HOL comes with a number of overloaded constants and corresponding classes.
+defined on all numeric types and somtimes on other types as well, for example
+\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{lll}
+Constant & Type & Syntax \\
+\hline
+\isa{{\isacharplus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}plus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 65) \\
+\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} &  (infixl 65) \\
+\isa{{\isacharasterisk}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}times{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} & (infixl 70) \\
+\isa{{\isacharcircum}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}power{\isacharparenright}\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ {\isacharprime}a} & (infixr 80) \\
+\isa{{\isacharminus}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{abs} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}minus{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{{\isasymle}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
+\isa{{\isacharless}} & \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} & (infixl 50) \\
+\isa{min} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\isa{max} &  \isa{{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ord{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} \\
+\end{tabular}
+\end{center}
+\end{table}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Typedef}%
%
-\isamarkupsection{Introducing new types%
-}
+\isamarkupsection{Introducing new types}
%
\begin{isamarkuptext}%
@@ -19,8 +18,7 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Declaring new types%
-}
+\isamarkupsubsection{Declaring new types}
%
\begin{isamarkuptext}%
\label{sec:typedecl}
@@ -57,8 +55,7 @@
unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Defining new types%
-}
+\isamarkupsubsection{Defining new types}
%
\begin{isamarkuptext}%
\label{sec:typedef}
--- a/doc-src/TutorialI/Types/types.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -14,6 +14,18 @@
types ({\S}\ref{sec:axclass}).
\end{itemize}

+\section{Basic types}
+
+\subsection{Numbers}
+\label{sec:numbers}
+
+\subsection{Pairs}
+\label{sec:products}
+% Check refs to this section to see what is expected of it.
+
+\subsection{Records}
+\label{sec:records}
+
\input{Types/document/Typedef}

\section{Axiomatic type classes}
--- a/doc-src/TutorialI/basics.tex	Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/basics.tex	Mon Nov 06 11:32:23 2000 +0100
@@ -186,8 +186,8 @@
\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as \isa{(x < y)::nat}. The main reason for type constraints are overloaded -functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for -a full discussion of overloading.) +functions like \isa{+}, \isa{*} and \isa{<}. See \S\ref{sec:overloading} for +a full discussion of overloading. \begin{warn} In general, HOL's concrete syntax tries to follow the conventions of --- a/doc-src/TutorialI/fp.tex Sat Nov 04 18:54:22 2000 +0100 +++ b/doc-src/TutorialI/fp.tex Mon Nov 06 11:32:23 2000 +0100 @@ -257,7 +257,7 @@ \indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{\$HOL2arithrel} are overloaded, i.e.\ they are available
not just for natural numbers but at other types as well (see
-  \S\ref{sec:TypeClasses}). For example, given the goal \isa{x+0 = x}, there
is nothing to indicate that you are talking about natural numbers.  Hence
Isabelle can only infer that \isa{x} is of some arbitrary type where
\isa{0} and \isa{+} are declared. As a consequence, you will be unable to
@@ -305,7 +305,7 @@
\index{arithmetic|)}

-\subsection{Products}
+\subsection{Pairs}
\input{Misc/document/pairs.tex}

%FIXME move stuff below into section on proofs about products?
@@ -315,16 +315,16 @@
of a term may differ, which can affect proofs. If you want to avoid this
complication, use \isa{fst} and \isa{snd}, i.e.\ write
\isa{\isasymlambda{}p.~fst p + snd p} instead of
-  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{proofs-about-products} for
+  \isa{\isasymlambda(x,y).~x + y}.  See~\S\ref{sec:products} for
theorem proving with tuple patterns.
\end{warn}

-Note that products, like natural numbers, are datatypes, which means
+Note that products, like type \isa{nat}, are datatypes, which means
in particular that \isa{induct_tac} and \isa{case_tac} are applicable to
Instead of tuples with many components (where many'' is not much above 2),
\label{sec:Definitions}