--- a/doc-src/TutorialI/Inductive/advanced-examples.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex Thu Jul 12 16:33:36 2001 +0200
@@ -10,6 +10,8 @@
\subsection{Universal Quantifiers in Introduction Rules}
\label{sec:gterm-datatype}
+\index{ground terms example|(}%
+\index{quantifiers!and inductive definitions|(}%
As a running example, this section develops the theory of \textbf{ground
terms}: terms constructed from constant and function
symbols but not variables. To simplify matters further, we regard a
@@ -111,14 +113,16 @@
%
The inductive definition neatly captures the reasoning above.
The universal quantification over the
-\isa{set} of arguments expresses that all of them are well-formed.
+\isa{set} of arguments expresses that all of them are well-formed.%
+\index{quantifiers!and inductive definitions|)}
\subsection{Alternative Definition Using a Monotone Function}
-An inductive definition may refer to the inductively defined
-set through an arbitrary monotone function. To demonstrate this
-powerful feature, let us
+\index{monotone functions!and inductive definitions|(}%
+An inductive definition may refer to the
+inductively defined set through an arbitrary monotone function. To
+demonstrate this powerful feature, let us
change the inductive definition above, replacing the
quantifier by a use of the function \isa{lists}. This
function, from the Isabelle theory of lists, is analogous to the
@@ -182,7 +186,8 @@
new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotone,
applications of the rule remain valid as new terms are constructed.
Further lists of well-formed
-terms become available and none are taken away.
+terms become available and none are taken away.%
+\index{monotone functions!and inductive definitions|)}
\subsection{A Proof of Equivalence}
@@ -248,9 +253,10 @@
call to
\isa{auto} does all this work.
-This example is typical of how monotone functions can be used. In
-particular, many of them distribute over intersection. Monotonicity
-implies one direction of this set equality; we have this theorem:
+This example is typical of how monotone functions
+\index{monotone functions} can be used. In particular, many of them
+distribute over intersection. Monotonicity implies one direction of
+this set equality; we have this theorem:
\begin{isabelle}
mono\ f\ \isasymLongrightarrow \ f\ (A\ \isasyminter \ B)\ \isasymsubseteq \
f\ A\ \isasyminter \ f\ B%
@@ -260,6 +266,7 @@
\subsection{Another Example of Rule Inversion}
+\index{rule inversion|(}%
Does \isa{gterms} distribute over intersection? We have proved that this
function is monotone, so \isa{mono_Int} gives one of the inclusions. The
opposite inclusion asserts that if \isa{t} is a ground term over both of the
@@ -275,7 +282,7 @@
\isa{Apply\ f\ args\ \isasymin\ gterms\ G}, which cannot be broken down.
It looks like a job for rule inversion:
\begin{isabelle}
-\isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
+\commdx{inductive\protect\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
\isasymin\ gterms\ F"
\end{isabelle}
%
@@ -330,6 +337,8 @@
\ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
\isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)
\end{isabelle}
+\index{rule inversion|)}%
+\index{ground terms example|)}
\begin{exercise}
--- a/doc-src/TutorialI/Inductive/even-example.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/even-example.tex Thu Jul 12 16:33:36 2001 +0200
@@ -1,6 +1,7 @@
% $Id$
\section{The Set of Even Numbers}
+\index{even numbers!defining inductively|(}%
The set of even numbers can be inductively defined as the least set
containing 0 and closed under the operation $+2$. Obviously,
\emph{even} can also be expressed using the divides relation (\isa{dvd}).
@@ -11,7 +12,7 @@
\subsection{Making an Inductive Definition}
Using \isacommand{consts}, we declare the constant \isa{even} to be a set
-of natural numbers. The \isacommand{inductive} declaration gives it the
+of natural numbers. The \commdx{inductive} declaration gives it the
desired properties.
\begin{isabelle}
\isacommand{consts}\ even\ ::\ "nat\ set"\isanewline
@@ -41,8 +42,10 @@
\rulename{even.step}
\end{isabelle}
-The introduction rules can be given attributes. Here both rules are
-specified as \isa{intro!}, directing the classical reasoner to
+The introduction rules can be given attributes. Here
+both rules are specified as \isa{intro!},%
+\index{intro"!@\isa {intro"!} (attribute)}
+directing the classical reasoner to
apply them aggressively. Obviously, regarding 0 as even is safe. The
\isa{step} rule is also safe because $n+2$ is even if and only if $n$ is
even. We prove this equivalence later.
@@ -83,6 +86,7 @@
\subsection{Rule Induction}
\label{sec:rule-induction}
+\index{rule induction|(}%
From the definition of the set
\isa{even}, Isabelle has
generated an induction rule:
@@ -161,6 +165,7 @@
\subsection{Generalization and Rule Induction}
\label{sec:gen-rule-induction}
+\index{generalizing for induction}%
Before applying induction, we typically must generalize
the induction formula. With rule induction, the required generalization
can be hard to find and sometimes requires a complete reformulation of the
@@ -200,7 +205,8 @@
\end{isabelle}
The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is
even. The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to
-\isa{n}, matching the assumption.
+\isa{n}, matching the assumption.%
+\index{rule induction|)} %the sequel isn't really about induction
\medskip
Using our lemma, we can easily prove the result we originally wanted:
@@ -210,8 +216,8 @@
\end{isabelle}
We have just proved the converse of the introduction rule \isa{even.step}.
-This suggests proving the following equivalence. We give it the \isa{iff}
-attribute because of its obvious value for simplification.
+This suggests proving the following equivalence. We give it the
+\attrdx{iff} attribute because of its obvious value for simplification.
\begin{isabelle}
\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
\isasymin \ even)"\isanewline
@@ -221,10 +227,12 @@
\subsection{Rule Inversion}\label{sec:rule-inversion}
-Case analysis on an inductive definition is called \textbf{rule inversion}.
-It is frequently used in proofs about operational semantics. It can be
-highly effective when it is applied automatically. Let us look at how rule
-inversion is done in Isabelle/HOL\@.
+\index{rule inversion|(}%
+Case analysis on an inductive definition is called \textbf{rule
+inversion}. It is frequently used in proofs about operational
+semantics. It can be highly effective when it is applied
+automatically. Let us look at how rule inversion is done in
+Isabelle/HOL\@.
Recall that \isa{even} is the minimal set closed under these two rules:
\begin{isabelle}
@@ -258,7 +266,8 @@
\isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
\ "Suc(Suc\ n)\ \isasymin \ even"
\end{isabelle}
-The \isacommand{inductive\_cases} command generates an instance of the
+The \commdx{inductive\protect\_cases} command generates an instance of
+the
\isa{cases} rule for the supplied pattern and gives it the supplied name:
%
\begin{isabelle}
@@ -273,8 +282,10 @@
(list ``cons''); freeness reasoning discards all but one or two cases.
In the \isacommand{inductive\_cases} command we supplied an
-attribute, \isa{elim!}, indicating that this elimination rule can be applied
-aggressively. The original
+attribute, \isa{elim!},
+\index{elim"!@\isa {elim"!} (attribute)}%
+indicating that this elimination rule can be
+applied aggressively. The original
\isa{cases} rule would loop if used in that manner because the
pattern~\isa{a} matches everything.
@@ -300,10 +311,12 @@
as an elimination rule.
To summarize, every inductive definition produces a \isa{cases} rule. The
-\isacommand{inductive\_cases} command stores an instance of the \isa{cases}
-rule for a given pattern. Within a proof, the \isa{ind_cases} method
-applies an instance of the \isa{cases}
+\commdx{inductive\protect\_cases} command stores an instance of the
+\isa{cases} rule for a given pattern. Within a proof, the
+\isa{ind_cases} method applies an instance of the \isa{cases}
rule.
The even numbers example has shown how inductive definitions can be
-used. Later examples will show that they are actually worth using.
+used. Later examples will show that they are actually worth using.%
+\index{rule inversion|)}%
+\index{even numbers!defining inductively|)}
--- a/doc-src/TutorialI/Inductive/inductive.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/inductive.tex Thu Jul 12 16:33:36 2001 +0200
@@ -1,6 +1,5 @@
\chapter{Inductively Defined Sets} \label{chap:inductive}
\index{inductive definition|(}
-\index{*inductive|(}
This chapter is dedicated to the most important definition principle after
recursive functions and datatypes: inductively defined sets.
@@ -25,4 +24,3 @@
\input{Inductive/document/AB}
\index{inductive definition|)}
-\index{*inductive|)}
--- a/doc-src/TutorialI/Rules/rules.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jul 12 16:33:36 2001 +0200
@@ -855,7 +855,7 @@
\section{Quantifiers}
-\index{quantifiers|(}\index{quantifiers!universal|(}%
+\index{quantifiers!universal|(}%
Quantifiers require formalizing syntactic substitution and the notion of
arbitrary value. Consider the universal quantifier. In a logic
book, its introduction rule looks like this:
@@ -1035,7 +1035,7 @@
\emph{Hint}: the proof is similar
to the one just above for the universal quantifier.
\end{exercise}
-\index{quantifiers|)}\index{quantifiers!existential|)}
+\index{quantifiers!existential|)}
\subsection{Renaming an Assumption: {\tt\slshape rename_tac}}
--- a/doc-src/TutorialI/Sets/sets.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Jul 12 16:33:36 2001 +0200
@@ -1017,8 +1017,8 @@
operators only in \S\ref{sec:VMC}.
\end{warn}
-The theory applies only to monotonic functions. Isabelle's
-definition of monotone is overloaded over all orderings:
+The theory applies only to monotonic functions.\index{monotone functions|bold}
+Isabelle's definition of monotone is overloaded over all orderings:
\begin{isabelle}
mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
\rulename{mono_def}