summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 12 Jul 2001 16:33:36 +0200 | |

changeset 11411 | c315dda16748 |

parent 11410 | b3b61ea9632c |

child 11412 | 54dd65d0ae87 |

indexing

--- 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}