--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Thu Jul 26 16:43:02 2001 +0200
@@ -4,7 +4,7 @@
subsection{*Case Study: Boolean Expressions*}
-text{*\label{sec:boolex}
+text{*\label{sec:boolex}\index{boolean expressions example|(}
The aim of this case study is twofold: it shows how to model boolean
expressions and some algorithms for manipulating them, and it demonstrates
the constructs introduced above.
@@ -120,7 +120,7 @@
"norm (IF b t e) = normif b (norm t) (norm e)";
text{*\noindent
-Their interplay is a bit tricky, and we leave it to the reader to develop an
+Their interplay is tricky; we leave it to you to develop an
intuitive understanding. Fortunately, Isabelle can help us to verify that the
transformation preserves the value of the expression:
*}
@@ -129,7 +129,7 @@
text{*\noindent
The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what @{term"normif"} does):
+lemma, which also helps to understand what @{term"normif"} does:
*}
lemma [simp]:
@@ -147,7 +147,7 @@
of the theorem shown above because of the @{text"[simp]"} attribute.
But how can we be sure that @{term"norm"} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality
+the above sense? We define a function that tests If-expressions for normality:
*}
consts normal :: "ifex \<Rightarrow> bool";
@@ -158,7 +158,7 @@
(case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
text{*\noindent
-and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
+Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
normality of @{term"normif"}:
*}
@@ -186,6 +186,7 @@
some of the goals as implications (@{text"\<longrightarrow>"}) rather than
equalities (@{text"="}).)
\end{exercise}
+\index{boolean expressions example|)}
*}
(*<*)
end
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jul 26 16:43:02 2001 +0200
@@ -6,7 +6,7 @@
}
%
\begin{isamarkuptext}%
-\label{sec:boolex}
+\label{sec:boolex}\index{boolean expressions example|(}
The aim of this case study is twofold: it shows how to model boolean
expressions and some algorithms for manipulating them, and it demonstrates
the constructs introduced above.%
@@ -114,7 +114,7 @@
{\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Their interplay is a bit tricky, and we leave it to the reader to develop an
+Their interplay is tricky; we leave it to you to develop an
intuitive understanding. Fortunately, Isabelle can help us to verify that the
transformation preserves the value of the expression:%
\end{isamarkuptext}%
@@ -122,7 +122,7 @@
\begin{isamarkuptext}%
\noindent
The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what \isa{normif} does):%
+lemma, which also helps to understand what \isa{normif} does:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}%
@@ -132,7 +132,7 @@
of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute.
But how can we be sure that \isa{norm} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality%
+the above sense? We define a function that tests If-expressions for normality:%
\end{isamarkuptext}%
\isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
@@ -142,7 +142,7 @@
\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-and prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
+Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
normality of \isa{normif}:%
\end{isamarkuptext}%
\isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
@@ -160,7 +160,8 @@
development to this changed requirement. (Hint: you may need to formulate
some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
equalities (\isa{{\isacharequal}}).)
-\end{exercise}%
+\end{exercise}
+\index{boolean expressions example|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/Translations.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Translations.thy Thu Jul 26 16:43:02 2001 +0200
@@ -4,34 +4,34 @@
subsection{*Syntax Translations*}
text{*\label{sec:def-translations}
-\indexbold{syntax translations|(}%
-\indexbold{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definition-like facility,
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
\textbf{syntax translations}.
They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition, and this is reversed upon printing. For example,
+replaced by its definition. This effect is reversed upon printing. For example,
the symbol @{text"\<noteq>"} is defined via a syntax translation:
*}
translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
-text{*\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, @{text"\<noteq>"} never appears.
In addition to @{text"\<rightleftharpoons>"} there are
-@{text"\<rightharpoonup>"}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
-and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
-parsing or printing. We do not want to cover the details of
-translations at this point. We have mentioned the concept merely because it
-crops up occasionally: a number of HOL's built-in constructs are defined
+parsing or printing. This tutorial will not cover the details of
+translations. We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
about @{text"="} still apply.%
-\indexbold{syntax translations|)}%
-\indexbold{translations@\isacommand {translations} (command)|)}
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}
*}
(*<*)
--- a/doc-src/TutorialI/Misc/Tree.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Thu Jul 26 16:43:02 2001 +0200
@@ -3,7 +3,7 @@
(*>*)
text{*\noindent
-Define the datatype of binary trees
+Define the datatype of \rmindex{binary trees}:
*}
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
@@ -14,7 +14,7 @@
"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
-and a function @{term"mirror"} that mirrors a binary tree
+Define a function @{term"mirror"} that mirrors a binary tree
by swapping subtrees recursively. Prove
*}
--- a/doc-src/TutorialI/Misc/case_exprs.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy Thu Jul 26 16:43:02 2001 +0200
@@ -4,8 +4,8 @@
subsection{*Case Expressions*}
-text{*\label{sec:case-expressions}
-HOL also features \sdx{case}-expressions for analyzing
+text{*\label{sec:case-expressions}\index{*case expressions}%
+HOL also features \isa{case}-expressions for analyzing
elements of a datatype. For example,
@{term[display]"case xs of [] => 1 | y#ys => y"}
evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if
@@ -43,14 +43,11 @@
subsection{*Structural Induction and Case Distinction*}
text{*\label{sec:struct-ind-case}
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \methdx{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \methdx{case_tac}. A trivial example:
+\index{case distinctions}\index{induction!structural}%
+Induction is invoked by \methdx{induct_tac}, as we have seen above;
+it works for any datatype. In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices. This is performed
+by \methdx{case_tac}. Here is a trivial example:
*}
lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
@@ -67,8 +64,11 @@
text{*
Note that we do not need to give a lemma a name if we do not intend to refer
to it explicitly in the future.
+Other basic laws about a datatype are applied automatically during
+simplification, so no special methods are provided for them.
\begin{warn}
+
Induction is only allowed on free (or \isasymAnd-bound) variables that
should not occur among the assumptions of the subgoal; see
\S\ref{sec:ind-var-in-prems} for details. Case distinction
--- a/doc-src/TutorialI/Misc/document/Translations.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Translations.tex Thu Jul 26 16:43:02 2001 +0200
@@ -7,33 +7,33 @@
%
\begin{isamarkuptext}%
\label{sec:def-translations}
-\indexbold{syntax translations|(}%
-\indexbold{translations@\isacommand {translations} (command)|(}
-Isabelle offers an additional definition-like facility,
+\index{syntax translations|(}%
+\index{translations@\isacommand {translations} (command)|(}
+Isabelle offers an additional definitional facility,
\textbf{syntax translations}.
They resemble macros: upon parsing, the defined concept is immediately
-replaced by its definition, and this is reversed upon printing. For example,
+replaced by its definition. This effect is reversed upon printing. For example,
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
\end{isamarkuptext}%
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
+\index{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, \isa{{\isasymnoteq}} never appears.
In addition to \isa{{\isasymrightleftharpoons}} there are
-\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
-and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
+\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
+and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
-parsing or printing. We do not want to cover the details of
-translations at this point. We have mentioned the concept merely because it
-crops up occasionally: a number of HOL's built-in constructs are defined
+parsing or printing. This tutorial will not cover the details of
+translations. We have mentioned the concept merely because it
+crops up occasionally; a number of HOL's built-in constructs are defined
via translations. Translations are preferable to definitions when the new
concept is a trivial variation on an existing one. For example, we
don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
about \isa{{\isacharequal}} still apply.%
-\indexbold{syntax translations|)}%
-\indexbold{translations@\isacommand {translations} (command)|)}%
+\index{syntax translations|)}%
+\index{translations@\isacommand {translations} (command)|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Tree.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Thu Jul 26 16:43:02 2001 +0200
@@ -4,12 +4,12 @@
%
\begin{isamarkuptext}%
\noindent
-Define the datatype of binary trees%
+Define the datatype of \rmindex{binary trees}:%
\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ tree{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-and a function \isa{mirror} that mirrors a binary tree
+Define a function \isa{mirror} that mirrors a binary tree
by swapping subtrees recursively. Prove%
\end{isamarkuptext}%
\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}%
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Thu Jul 26 16:43:02 2001 +0200
@@ -6,8 +6,8 @@
}
%
\begin{isamarkuptext}%
-\label{sec:case-expressions}
-HOL also features \sdx{case}-expressions for analyzing
+\label{sec:case-expressions}\index{*case expressions}%
+HOL also features \isa{case}-expressions for analyzing
elements of a datatype. For example,
\begin{isabelle}%
\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{1}}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
@@ -54,14 +54,11 @@
%
\begin{isamarkuptext}%
\label{sec:struct-ind-case}
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \methdx{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \methdx{case_tac}. A trivial example:%
+\index{case distinctions}\index{induction!structural}%
+Induction is invoked by \methdx{induct_tac}, as we have seen above;
+it works for any datatype. In some cases, induction is overkill and a case
+distinction over all constructors of the datatype suffices. This is performed
+by \methdx{case_tac}. Here is a trivial example:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}%
@@ -79,8 +76,11 @@
\begin{isamarkuptext}%
Note that we do not need to give a lemma a name if we do not intend to refer
to it explicitly in the future.
+Other basic laws about a datatype are applied automatically during
+simplification, so no special methods are provided for them.
\begin{warn}
+
Induction is only allowed on free (or \isasymAnd-bound) variables that
should not occur among the assumptions of the subgoal; see
\S\ref{sec:ind-var-in-prems} for details. Case distinction
--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Jul 26 16:43:02 2001 +0200
@@ -24,6 +24,7 @@
\begin{isamarkuptext}%
\newcommand{\mystar}{*%
}
+\index{arithmetic operations!for \protect\isa{nat}}%
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
\sdx{div}, \sdx{mod}, \cdx{min} and
@@ -31,13 +32,15 @@
\indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
-\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}, although
-Isabelle does not prove this automatically. Note that \isa{{\isadigit{1}}}
+\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{1}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}}.
+\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
+ The following needs changing with our new system of numbers.}
+Note that \isa{{\isadigit{1}}}
and \isa{{\isadigit{2}}} are available as abbreviations for the corresponding
\isa{Suc}-expressions. If you need the full set of numerals,
see~\S\ref{sec:numerals}.
-\begin{warn}
+\begin{warn}\index{overloading}
The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
@@ -60,23 +63,23 @@
operations.
\end{warn}
-Simple arithmetic goals are proved automatically by both \isa{auto} and the
-simplification method introduced in \S\ref{sec:Simplification}. For
-example,%
+Both \isa{auto} and \isa{simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove
+simple arithmetic goals automatically:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
+For efficiency's sake, this built-in prover ignores quantified formulae and all
+arithmetic operations apart from addition.
-For more complex goals, there is the special method \methdx{arith}
-(which attacks the first subgoal). It proves arithmetic goals involving the
+The method \methdx{arith} is more general. It attempts to prove
+the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
+Such formulas may involve the
usual logical connectives (\isa{{\isasymnot}}, \isa{{\isasymand}}, \isa{{\isasymor}},
\isa{{\isasymlongrightarrow}}), the relations \isa{{\isacharequal}}, \isa{{\isasymle}} and \isa{{\isacharless}},
and the operations
-\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}. Technically, this is
-known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
+\isa{{\isacharplus}}, \isa{{\isacharminus}}, \isa{min} and \isa{max}.
For example,%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
@@ -88,7 +91,7 @@
\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-is not even proved by \isa{arith} because the proof relies essentially
+is not proved even by \isa{arith} because the proof relies
on properties of multiplication.
\begin{warn}
@@ -96,10 +99,9 @@
of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
\cdx{max} because they are first eliminated by case distinctions.
- \isa{arith} is incomplete even for the restricted class of
- linear arithmetic formulae. If divisibility plays a
+ Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
role, it may fail to prove a valid formula, for example
- \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare in practice.
+ \isa{m\ {\isacharplus}\ m\ {\isasymnoteq}\ n\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}}. Fortunately, such examples are rare.
\end{warn}%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Thu Jul 26 16:43:02 2001 +0200
@@ -18,7 +18,7 @@
\begin{itemize}
\item
There is also the type \tydx{unit}, which contains exactly one
-element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+element denoted by~\cdx{()}. This type can be viewed
as a degenerate product with 0 components.
\item
Products, like type \isa{nat}, are datatypes, which means
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Thu Jul 26 16:43:02 2001 +0200
@@ -5,14 +5,14 @@
\begin{isamarkuptext}%
\begin{warn}
A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
+variables on the right-hand side. Consider the following, flawed definition
+(where \isa{dvd} means ``divides''):
\begin{isabelle}%
\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
\end{isabelle}
-where \isa{dvd} means ``divides''.
Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency (why?). What you
-should have written is
+right-hand side, which would introduce an inconsistency (why?).
+The correct version is
\begin{isabelle}%
\ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ {\isadigit{1}}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}%
\end{isabelle}
--- a/doc-src/TutorialI/Misc/document/types.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Thu Jul 26 16:43:02 2001 +0200
@@ -9,7 +9,7 @@
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
-type:%
+type. Here, we declare two constants of type \isa{gate}:%
\end{isamarkuptext}%
\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ xor\ \ {\isacharcolon}{\isacharcolon}\ gate%
@@ -18,19 +18,20 @@
%
\begin{isamarkuptext}%
\label{sec:ConstDefinitions}\indexbold{definitions}%
-The above constants \isa{nand} and \isa{xor} are non-recursive and can
-therefore be defined directly by%
+The constants \isa{nand} and \isa{xor} above are non-recursive and can
+be defined directly:%
\end{isamarkuptext}%
\isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
\ \ \ \ \ xor{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}xor\ A\ B\ \ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent%
-where \commdx{defs} is a keyword and
+Here \commdx{defs} is a keyword and
\isa{nand{\isacharunderscore}def} and \isa{xor{\isacharunderscore}def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
-Declarations and definitions can also be merged in a \commdx{constdefs}
-command:%
+A \commdx{constdefs} command combines the effects of \isacommand{consts} and
+\isacommand{defs}. For instance, we can introduce \isa{nand} and \isa{xor} by a
+single command:%
\end{isamarkuptext}%
\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Misc/natsum.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu Jul 26 16:43:02 2001 +0200
@@ -22,6 +22,7 @@
text{*\newcommand{\mystar}{*%
}
+\index{arithmetic operations!for \protect\isa{nat}}%
The usual arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
\sdx{div}, \sdx{mod}, \cdx{min} and
@@ -29,13 +30,15 @@
\indexboldpos{\isasymle}{$HOL2arithrel} and
\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = 0"} if
@{prop"m<n"}. There is even a least number operation
-\sdx{LEAST}\@. For example, @{prop"(LEAST n. 1 < n) = 2"}, although
-Isabelle does not prove this automatically. Note that @{term 1}
+\sdx{LEAST}\@. For example, @{prop"(LEAST n. 1 < n) = 2"}.
+\REMARK{Isabelle CAN prove it automatically, using \isa{auto intro: Least_equality}.
+ The following needs changing with our new system of numbers.}
+Note that @{term 1}
and @{term 2} are available as abbreviations for the corresponding
@{term Suc}-expressions. If you need the full set of numerals,
see~\S\ref{sec:numerals}.
-\begin{warn}
+\begin{warn}\index{overloading}
The constant \cdx{0} and the operations
\ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
\ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
@@ -58,25 +61,25 @@
operations.
\end{warn}
-Simple arithmetic goals are proved automatically by both @{term auto} and the
-simplification method introduced in \S\ref{sec:Simplification}. For
-example,
+Both @{text auto} and @{text simp}
+(a method introduced below, \S\ref{sec:Simplification}) prove
+simple arithmetic goals automatically:
*}
lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
(*<*)by(auto)(*>*)
text{*\noindent
-is proved automatically. The main restriction is that only addition is taken
-into account; other arithmetic operations and quantified formulae are ignored.
+For efficiency's sake, this built-in prover ignores quantified formulae and all
+arithmetic operations apart from addition.
-For more complex goals, there is the special method \methdx{arith}
-(which attacks the first subgoal). It proves arithmetic goals involving the
+The method \methdx{arith} is more general. It attempts to prove
+the first subgoal provided it is a quantifier free \textbf{linear arithmetic} formula.
+Such formulas may involve the
usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
and the operations
-@{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
-known as the class of (quantifier free) \textbf{linear arithmetic} formulae.
+@{text"+"}, @{text"-"}, @{term min} and @{term max}.
For example,
*}
@@ -92,7 +95,7 @@
(*<*)oops(*>*)
text{*\noindent
-is not even proved by @{text arith} because the proof relies essentially
+is not proved even by @{text arith} because the proof relies
on properties of multiplication.
\begin{warn}
@@ -100,10 +103,9 @@
of \ttindexboldpos{-}{$HOL2arithfun}, \cdx{min} and
\cdx{max} because they are first eliminated by case distinctions.
- \isa{arith} is incomplete even for the restricted class of
- linear arithmetic formulae. If divisibility plays a
+ Even for linear arithmetic formulae, \isa{arith} is incomplete. If divisibility plays a
role, it may fail to prove a valid formula, for example
- @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare in practice.
+ @{prop"m+m \<noteq> n+n+1"}. Fortunately, such examples are rare.
\end{warn}
*}
--- a/doc-src/TutorialI/Misc/pairs.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Thu Jul 26 16:43:02 2001 +0200
@@ -16,7 +16,7 @@
\begin{itemize}
\item
There is also the type \tydx{unit}, which contains exactly one
-element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed
+element denoted by~\cdx{()}. This type can be viewed
as a degenerate product with 0 components.
\item
Products, like type @{typ nat}, are datatypes, which means
--- a/doc-src/TutorialI/Misc/prime_def.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy Thu Jul 26 16:43:02 2001 +0200
@@ -5,12 +5,12 @@
text{*
\begin{warn}
A common mistake when writing definitions is to introduce extra free
-variables on the right-hand side as in the following fictitious definition:
+variables on the right-hand side. Consider the following, flawed definition
+(where @{text"dvd"} means ``divides''):
@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
-where @{text"dvd"} means ``divides''.
Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
-right-hand side, which would introduce an inconsistency (why?). What you
-should have written is
+right-hand side, which would introduce an inconsistency (why?).
+The correct version is
@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
\end{warn}
*}
--- a/doc-src/TutorialI/Misc/types.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Misc/types.thy Thu Jul 26 16:43:02 2001 +0200
@@ -7,7 +7,7 @@
Internally all synonyms are fully expanded. As a consequence Isabelle's
output never contains synonyms. Their main purpose is to improve the
readability of theories. Synonyms can be used just like any other
-type:
+type. Here, we declare two constants of type \isa{gate}:
*}
consts nand :: gate
@@ -16,20 +16,21 @@
subsection{*Constant Definitions*}
text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
-The above constants @{term"nand"} and @{term"xor"} are non-recursive and can
-therefore be defined directly by
+The constants @{term"nand"} and @{term"xor"} above are non-recursive and can
+be defined directly:
*}
defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
text{*\noindent%
-where \commdx{defs} is a keyword and
+Here \commdx{defs} is a keyword and
@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
that must be used in constant definitions.
-Declarations and definitions can also be merged in a \commdx{constdefs}
-command:
+A \commdx{constdefs} command combines the effects of \isacommand{consts} and
+\isacommand{defs}. For instance, we can introduce @{term"nand"} and @{term"xor"} by a
+single command:
*}
constdefs nor :: gate
--- a/doc-src/TutorialI/Rules/Basic.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Thu Jul 26 16:43:02 2001 +0200
@@ -309,13 +309,13 @@
theorem Least_equality:
"\<lbrakk> P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
-apply (simp add: Least_def LeastM_def)
+apply (simp add: Least_def)
txt{*omit maybe?
@{subgoals[display,indent=0,margin=65]}
*};
-apply (rule some_equality)
+apply (rule the_equality)
txt{*
@{subgoals[display,indent=0,margin=65]}
--- a/doc-src/TutorialI/Rules/Force.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Force.thy Thu Jul 26 16:43:02 2001 +0200
@@ -1,6 +1,7 @@
(* ID: $Id$ *)
-theory Force = Divides: (*Divides rather than Main so that the first proof
- isn't done by the nat_divide_cancel_factor simprocs.*)
+theory Force = Main:
+ (*Use Divides rather than Main to experiment with the first proof.
+ Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
declare div_mult_self_is_m [simp del];
--- a/doc-src/TutorialI/ToyList/ToyList.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Jul 26 16:43:02 2001 +0200
@@ -33,10 +33,11 @@
The @{text 65} is the priority of the infix @{text"#"}.
\begin{warn}
- Syntax annotations are a powerful but optional feature. You
+ Syntax annotations are can be powerful, but they are difficult to master and
+ are never necessary. You
could drop them from theory @{text"ToyList"} and go back to the identifiers
@{term[source]Nil} and @{term[source]Cons}.
- We recommend that novices avoid using
+ Novices should avoid using
syntax annotations in their own theories.
\end{warn}
Next, two functions @{text"app"} and \cdx{rev} are declared:
@@ -49,7 +50,7 @@
\noindent
In contrast to many functional programming languages,
Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}). Apart from the declaration-before-use
+(keyword \commdx{consts}). Apart from the declaration-before-use
restriction, the order of items in a theory file is unconstrained. Function
@{text"app"} is annotated with concrete syntax too. Instead of the
prefix syntax @{text"app xs ys"} the infix
@@ -66,7 +67,7 @@
"rev (x # xs) = (rev xs) @ (x # [])";
text{*
-\noindent
+\noindent\index{*rev (constant)|(}\index{append function|(}
The equations for @{text"app"} and @{term"rev"} hardly need comments:
@{text"app"} appends two lists and @{term"rev"} reverses a list. The
keyword \commdx{primrec} indicates that the recursion is
@@ -82,16 +83,16 @@
% However, this is a subtle issue that we cannot discuss here further.
\begin{warn}
- As we have indicated, the requirement for total functions is not a gratuitous
- restriction but an essential characteristic of HOL\@. It is only
+ As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
because of totality that reasoning in HOL is comparatively easy. More
- generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+ generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
function definitions whose totality has not been proved) because they
quickly lead to inconsistencies. Instead, fixed constructs for introducing
types and functions are offered (such as \isacommand{datatype} and
\isacommand{primrec}) which are guaranteed to preserve consistency.
\end{warn}
+\index{syntax}%
A remark about syntax. The textual definition of a theory follows a fixed
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
@@ -108,7 +109,7 @@
text{*\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
+the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
\section{An Introductory Proof}
@@ -119,27 +120,24 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main Goal: @{text"rev(rev xs) = xs"}.}
+\subsubsection*{Main Goal}
Our goal is to show that reversing a list twice produces the original
-list. The input line
+list.
*}
theorem rev_rev [simp]: "rev(rev xs) = xs";
txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
-\index{*simp (attribute)|bold}
\noindent
-does several things. It
+This \isacommand{theorem} command does several things:
\begin{itemize}
\item
-establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
+It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}.
\item
-gives that theorem the name @{text"rev_rev"} by which it can be
-referred to,
+It gives that theorem the name @{text"rev_rev"}, for later reference.
\item
-and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
-proved) as a simplification rule, i.e.\ all future proofs involving
+It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
simplification will replace occurrences of @{term"rev(rev xs)"} by
@{term"xs"}.
@@ -156,7 +154,7 @@
The first three lines tell us that we are 0 steps into the proof of
theorem @{text"rev_rev"}; for compactness reasons we rarely show these
initial lines in this tutorial. The remaining lines display the current
-proof state.
+\rmindex{proof state}.
Until we have finished a proof, the proof state always looks like this:
\begin{isabelle}
$G$\isanewline
@@ -167,7 +165,8 @@
where $G$
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At @{text"step 0"} there is only one subgoal, which is
+establish $G$.\index{subgoals}
+At @{text"step 0"} there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.
@@ -187,16 +186,18 @@
(@{term[source]Cons}):
@{subgoals[display,indent=0,margin=65]}
-The induction step is an example of the general format of a subgoal:
+The induction step is an example of the general format of a subgoal:\index{subgoals}
\begin{isabelle}
~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
ignored most of the time, or simply treated as a list of variables local to
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
-The {\it assumptions} are the local assumptions for this subgoal and {\it
- conclusion} is the actual proposition to be proved. Typical proof steps
-that add new assumptions are induction or case distinction. In our example
+The {\it assumptions}\index{assumptions!of subgoal}
+are the local assumptions for this subgoal and {\it
+ conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
+Typical proof steps
+that add new assumptions are induction and case distinction. In our example
the only assumption is the induction hypothesis @{term"rev (rev list) =
list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
are multiple assumptions, they are enclosed in the bracket pair
@@ -262,7 +263,7 @@
subsubsection{*Second Lemma*}
text{*
-This time the canonical proof procedure
+We again try the canonical proof procedure:
*}
lemma app_Nil2 [simp]: "xs @ [] = xs";
@@ -271,7 +272,7 @@
txt{*
\noindent
-leads to the desired message @{text"No subgoals!"}:
+It works, yielding the desired message @{text"No subgoals!"}:
@{goals[display,indent=0]}
We still need to confirm that the proof is now finished:
*}
@@ -312,10 +313,11 @@
*}
(*<*)oops(*>*)
-subsubsection{*Third Lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
+subsubsection{*Third Lemma*}
text{*
-Abandoning the previous proof, the canonical proof procedure
+Abandoning the previous attempt, the canonical proof procedure
+succeeds without further ado.
*}
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
@@ -325,8 +327,7 @@
text{*
\noindent
-succeeds without further ado.
-Now we can prove the first lemma
+Now we can prove the first lemma:
*}
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
@@ -335,7 +336,7 @@
done
text{*\noindent
-and then prove our main theorem:
+Finally, we prove our main theorem:
*}
theorem rev_rev [simp]: "rev(rev xs) = xs";
@@ -344,8 +345,9 @@
done
text{*\noindent
-The final \isacommand{end} tells Isabelle to close the current theory because
-we are finished with its development:
+The final \commdx{end} tells Isabelle to close the current theory because
+we are finished with its development:%
+\index{*rev (constant)|)}\index{append function|)}
*}
end
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Jul 26 16:43:02 2001 +0200
@@ -35,10 +35,11 @@
The \isa{{\isadigit{6}}{\isadigit{5}}} is the priority of the infix \isa{{\isacharhash}}.
\begin{warn}
- Syntax annotations are a powerful but optional feature. You
+ Syntax annotations are can be powerful, but they are difficult to master and
+ are never necessary. You
could drop them from theory \isa{ToyList} and go back to the identifiers
\isa{Nil} and \isa{Cons}.
- We recommend that novices avoid using
+ Novices should avoid using
syntax annotations in their own theories.
\end{warn}
Next, two functions \isa{app} and \cdx{rev} are declared:%
@@ -49,7 +50,7 @@
\noindent
In contrast to many functional programming languages,
Isabelle insists on explicit declarations of all functions
-(keyword \isacommand{consts}). Apart from the declaration-before-use
+(keyword \commdx{consts}). Apart from the declaration-before-use
restriction, the order of items in a theory file is unconstrained. Function
\isa{app} is annotated with concrete syntax too. Instead of the
prefix syntax \isa{app\ xs\ ys} the infix
@@ -64,7 +65,7 @@
{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
-\noindent
+\noindent\index{*rev (constant)|(}\index{append function|(}
The equations for \isa{app} and \isa{rev} hardly need comments:
\isa{app} appends two lists and \isa{rev} reverses a list. The
keyword \commdx{primrec} indicates that the recursion is
@@ -80,16 +81,16 @@
% However, this is a subtle issue that we cannot discuss here further.
\begin{warn}
- As we have indicated, the requirement for total functions is not a gratuitous
- restriction but an essential characteristic of HOL\@. It is only
+ As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only
because of totality that reasoning in HOL is comparatively easy. More
- generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+ generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as
function definitions whose totality has not been proved) because they
quickly lead to inconsistencies. Instead, fixed constructs for introducing
types and functions are offered (such as \isacommand{datatype} and
\isacommand{primrec}) which are guaranteed to preserve consistency.
\end{warn}
+\index{syntax}%
A remark about syntax. The textual definition of a theory follows a fixed
syntax with keywords like \isacommand{datatype} and \isacommand{end}.
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
@@ -105,7 +106,7 @@
\begin{isamarkuptext}%
\noindent
When Isabelle prints a syntax error message, it refers to the HOL syntax as
-the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
+the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
\section{An Introductory Proof}
@@ -116,26 +117,23 @@
illustrate not just the basic proof commands but also the typical proof
process.
-\subsubsection*{Main Goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
+\subsubsection*{Main Goal}
Our goal is to show that reversing a list twice produces the original
-list. The input line%
+list.%
\end{isamarkuptext}%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
\begin{isamarkuptxt}%
\index{theorem@\isacommand {theorem} (command)|bold}%
-\index{*simp (attribute)|bold}
\noindent
-does several things. It
+This \isacommand{theorem} command does several things:
\begin{itemize}
\item
-establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
+It establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.
\item
-gives that theorem the name \isa{rev{\isacharunderscore}rev} by which it can be
-referred to,
+It gives that theorem the name \isa{rev{\isacharunderscore}rev}, for later reference.
\item
-and tells Isabelle (via \isa{{\isacharbrackleft}simp{\isacharbrackright}}) to use the theorem (once it has been
-proved) as a simplification rule, i.e.\ all future proofs involving
+It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving
simplification will replace occurrences of \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}} by
\isa{xs}.
@@ -152,7 +150,7 @@
The first three lines tell us that we are 0 steps into the proof of
theorem \isa{rev{\isacharunderscore}rev}; for compactness reasons we rarely show these
initial lines in this tutorial. The remaining lines display the current
-proof state.
+\rmindex{proof state}.
Until we have finished a proof, the proof state always looks like this:
\begin{isabelle}
$G$\isanewline
@@ -163,7 +161,8 @@
where $G$
is the overall goal that we are trying to prove, and the numbered lines
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$. At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
+establish $G$.\index{subgoals}
+At \isa{step\ {\isadigit{0}}} there is only one subgoal, which is
identical with the overall goal. Normally $G$ is constant and only serves as
a reminder. Hence we rarely show it in this tutorial.
@@ -186,16 +185,18 @@
\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list\ {\isasymLongrightarrow}\ rev\ {\isacharparenleft}rev\ {\isacharparenleft}a\ {\isacharhash}\ list{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ a\ {\isacharhash}\ list%
\end{isabelle}
-The induction step is an example of the general format of a subgoal:
+The induction step is an example of the general format of a subgoal:\index{subgoals}
\begin{isabelle}
~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
ignored most of the time, or simply treated as a list of variables local to
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
-The {\it assumptions} are the local assumptions for this subgoal and {\it
- conclusion} is the actual proposition to be proved. Typical proof steps
-that add new assumptions are induction or case distinction. In our example
+The {\it assumptions}\index{assumptions!of subgoal}
+are the local assumptions for this subgoal and {\it
+ conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
+Typical proof steps
+that add new assumptions are induction and case distinction. In our example
the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ list{\isacharparenright}\ {\isacharequal}\ list}, where \isa{list} is a variable name chosen by Isabelle. If there
are multiple assumptions, they are enclosed in the bracket pair
\indexboldpos{\isasymlbrakk}{$Isabrl} and
@@ -256,14 +257,14 @@
}
%
\begin{isamarkuptext}%
-This time the canonical proof procedure%
+We again try the canonical proof procedure:%
\end{isamarkuptext}%
\isacommand{lemma}\ app{\isacharunderscore}Nil{\isadigit{2}}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-leads to the desired message \isa{No\ subgoals{\isacharbang}}:
+It works, yielding the desired message \isa{No\ subgoals{\isacharbang}}:
\begin{isabelle}%
xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs\isanewline
No\ subgoals{\isacharbang}%
@@ -307,11 +308,12 @@
and the missing lemma is associativity of \isa{{\isacharat}}.%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Third Lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+\isamarkupsubsubsection{Third Lemma%
}
%
\begin{isamarkuptext}%
-Abandoning the previous proof, the canonical proof procedure%
+Abandoning the previous attempt, the canonical proof procedure
+succeeds without further ado.%
\end{isamarkuptext}%
\isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -319,8 +321,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-succeeds without further ado.
-Now we can prove the first lemma%
+Now we can prove the first lemma:%
\end{isamarkuptext}%
\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -328,7 +329,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-and then prove our main theorem:%
+Finally, we prove our main theorem:%
\end{isamarkuptext}%
\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
@@ -336,8 +337,9 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-The final \isacommand{end} tells Isabelle to close the current theory because
+The final \commdx{end} tells Isabelle to close the current theory because
we are finished with its development:%
+\index{*rev (constant)|)}\index{append function|)}%
\end{isamarkuptext}%
\isacommand{end}\isanewline
\end{isabellebody}%
--- a/doc-src/TutorialI/basics.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/basics.tex Thu Jul 26 16:43:02 2001 +0200
@@ -8,10 +8,10 @@
of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
HOL step by step following the equation
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We do not assume that you are familiar with mathematical logic but that
-you are used to logical and set theoretic notation, such as covered
-in a good discrete mathematics course~\cite{Rosen-DMA}.
-In contrast, we do assume
+We do not assume that you are familiar with mathematical logic.
+However, we do assume that
+you are used to logical and set theoretic notation, as covered
+in a good discrete mathematics course~\cite{Rosen-DMA}, and
that you are familiar with the basic concepts of functional
programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
Although this tutorial initially concentrates on functional programming, do
--- a/doc-src/TutorialI/fp.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/fp.tex Thu Jul 26 16:43:02 2001 +0200
@@ -70,7 +70,7 @@
There are two kinds of commands used during a proof: the actual proof
commands and auxiliary commands for examining the proof state and controlling
the display. Simple proof commands are of the form
-\commdx{apply}\isa{(method)}, where \isa{method} is typically
+\commdx{apply}\isa{(\textit{method})}, where \textit{method} is typically
\isa{induct_tac} or \isa{auto}. All such theorem proving operations
are referred to as \bfindex{methods}, and further ones are
introduced throughout the tutorial. Unless stated otherwise, you may
@@ -98,8 +98,9 @@
\commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
prints the named theorems.
\item[Displaying types:] We have already mentioned the flag
- \ttindex{show_types} above. It can also be useful for detecting typos in
- formulae early on. For example, if \texttt{show_types} is set and the goal
+ \texttt{show_types} above.\index{*show_types (flag)}
+ It can also be useful for detecting misspellings in
+ formulae. For example, if \texttt{show_types} is set and the goal
\isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
\par\noindent
\begin{isabelle}%
@@ -124,7 +125,7 @@
\commdx{typ} \textit{string} reads and prints the given
string as a type in the current context.
\item[(Re)loading theories:] When you start your interaction you must open a
- named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
+ named theory with the line \commdx{theory}~\isa{T~=~\dots~:}. Isabelle
automatically loads all the required parent theories from their respective
files (which may take a moment, unless the theories are already loaded and
the files have not been modified).
@@ -152,6 +153,7 @@
\section{Datatypes}
\label{sec:datatype}
+\index{datatypes|(}%
Inductive datatypes are part of almost every non-trivial application of HOL.
First we take another look at a very important example, the datatype of
lists, before we turn to datatypes in general. The section closes with a
@@ -161,8 +163,7 @@
\subsection{Lists}
\index{*list (type)}%
-Lists are one of the essential datatypes in computing. Readers of this
-tutorial and users of HOL need to be familiar with their basic operations.
+Lists are one of the essential datatypes in computing. You need to be familiar with their basic operations.
Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
The latter contains many further operations. For example, the functions
@@ -199,9 +200,14 @@
Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
- 1}. In general, \cdx{size} returns \isa{0} for all constructors
-that do not have an argument of type $t$, and for all other constructors
-\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
+ 1}. In general, \cdx{size} returns
+\begin{itemize}
+\item \isa{0} for all constructors
+that do not have an argument of type $t$\\
+\item for all other constructors,
+one plus the sum of the sizes of all arguments of type~$t$.
+\end{itemize}
+Note that because
\isa{size} is defined on every datatype, it is overloaded; on lists
\isa{size} is also called \sdx{length}, which is not overloaded.
Isabelle will always show \isa{size} on lists as \isa{length}.
@@ -209,6 +215,7 @@
\subsection{Primitive Recursion}
+\index{recursion!primitive}%
Functions on datatypes are usually defined by recursion. In fact, most of the
time they are defined by what is called \textbf{primitive recursion}.
The keyword \commdx{primrec} is followed by a list of
@@ -229,12 +236,14 @@
\input{Misc/document/case_exprs.tex}
\input{Ifexpr/document/Ifexpr.tex}
+\index{datatypes|)}
+
\section{Some Basic Types}
\subsection{Natural Numbers}
-\label{sec:nat}
+\label{sec:nat}\index{natural numbers}%
\index{linear arithmetic|(}
\input{Misc/document/fakenat.tex}
@@ -256,23 +265,23 @@
A definition is simply an abbreviation, i.e.\ a new name for an existing
construction. In particular, definitions cannot be recursive. Isabelle offers
definitions on the level of types and terms. Those on the type level are
-called type synonyms, those on the term level are called (constant)
+called \textbf{type synonyms}; those on the term level are simply called
definitions.
\subsection{Type Synonyms}
-\indexbold{type synonyms|(}%
-Type synonyms are similar to those found in ML\@. They are issued by a
+\index{type synonyms|(}%
+Type synonyms are similar to those found in ML\@. They are created by a
\commdx{types} command:
\input{Misc/document/types.tex}%
-Note that pattern-matching is not allowed, i.e.\ each definition must be of
+Pattern-matching is not allowed, i.e.\ each definition must be of
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
Section~{\S}\ref{sec:Simp-with-Defs} explains how definitions are used
in proofs.%
-\indexbold{type synonyms|)}
+\index{type synonyms|)}
\input{Misc/document/prime_def.tex}
@@ -283,23 +292,16 @@
\label{sec:definitional}
As we pointed out at the beginning of the chapter, asserting arbitrary
-axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
+axioms such as $f(n) = f(n) + 1$ can easily lead to contradictions. In order
to avoid this danger, this tutorial advocates the definitional rather than
-the axiomatic approach: introduce new concepts by definitions, thus
-preserving consistency. However, on the face of it, Isabelle/HOL seems to
-support many more constructs than just definitions, for example
-\isacommand{primrec}. The crucial point is that internally, everything
-(except real axioms) is reduced to a definition. For example, given some
-\isacommand{primrec} function definition, this is turned into a proper
-(nonrecursive!) definition, and the user-supplied recursion equations are
-derived as theorems from that definition. This tricky process is completely
-hidden from the user and it is not necessary to understand the details. The
-result of the definitional approach is that \isacommand{primrec} is as safe
-as pure \isacommand{defs} are, but more convenient. And this is not just the
-case for \isacommand{primrec} but also for the other commands described
-later, like \isacommand{recdef} and \isacommand{inductive}.
-This strict adherence to the definitional approach reduces the risk of
-soundness errors inside Isabelle/HOL.
+the axiomatic approach: introduce new concepts by definitions. However, Isabelle/HOL seems to
+support many richer definitional constructs, such as
+\isacommand{primrec}. The point is that Isabelle reduces such constructs to first principles. For example, each
+\isacommand{primrec} function definition is turned into a proper
+(nonrecursive!) definition from which the user-supplied recursion equations are
+derived as theorems. This process is
+hidden from the user, who does not have to understand the details. Other commands described
+later, like \isacommand{recdef} and \isacommand{inductive}, are treated similarly. This strict adherence to the definitional approach reduces the risk of soundness errors.
\chapter{More Functional Programming}
--- a/doc-src/TutorialI/tutorial.sty Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/tutorial.sty Thu Jul 26 16:43:02 2001 +0200
@@ -50,8 +50,12 @@
\newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
\newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
-\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
-\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
+%Commented-out the original versions to see what the index looks like without them.
+% In any event, they need to use \isa or \protect\isa rather than \texttt.
+%%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}
+%%\newcommand{\ttindexboldpos}[2]{\texttt{#1}\index{#2@\texttt{#1}|bold}\@}
+\newcommand{\indexboldpos}[2]{#1\@}
+\newcommand{\ttindexboldpos}[2]{\isa{#1}\@}
%\newtheorem{theorem}{Theorem}[section]
\newtheorem{Exercise}{Exercise}[section]
--- a/doc-src/TutorialI/tutorial.tex Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex Thu Jul 26 16:43:02 2001 +0200
@@ -11,8 +11,9 @@
\makeindex
\index{conditional expressions|see{\isa{if} expressions}}
-\index{primitive recursion|see{\isacommand{primrec}}}
+\index{primitive recursion|see{recursion, primitive}}
\index{product type|see{pairs and tuples}}
+\index{structural induction|see{induction, structural}}
\index{termination|see{functions, total}}
\index{tuples|see{pairs and tuples}}
\index{settings|see{flags}}