# HG changeset patch
# User paulson
# Date 994948416 -7200
# Node ID c315dda167488d7188e087efb79c55fa89361508
# Parent  b3b61ea9632caecbea957068e61ae80713617bc6
indexing

diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Inductive/advanced-examples.tex
--- 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}
diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Inductive/even-example.tex
--- 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|)}
diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Inductive/inductive.tex
--- 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|)}
diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Rules/rules.tex
--- 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}}
diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Sets/sets.tex
--- 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}