--- a/doc-src/TutorialI/Advanced/Partial.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Aug 09 18:12:15 2001 +0200
@@ -1,7 +1,7 @@
(*<*)theory Partial = While_Combinator:(*>*)
-text{*\noindent Throughout the tutorial we have emphasized the fact
-that all functions in HOL are total. Hence we cannot hope to define
+text{*\noindent Throughout this tutorial, we have emphasized
+that all functions in HOL are total. We cannot hope to define
truly partial functions, but must make them total. A straightforward
method is to lift the result type of the function from $\tau$ to
$\tau$~@{text option} (see \ref{sec:option}), where @{term None} is
@@ -45,7 +45,9 @@
subsubsection{*Guarded Recursion*}
-text{* Neither \isacommand{primrec} nor \isacommand{recdef} allow to
+text{*
+\index{recursion!guarded}%
+Neither \isacommand{primrec} nor \isacommand{recdef} allow to
prefix an equation with a condition in the way ordinary definitions do
(see @{term minus} above). Instead we have to move the condition over
to the right-hand side of the equation. Given a partial function $f$
@@ -73,7 +75,7 @@
As a more substantial example we consider the problem of searching a graph.
For simplicity our graph is given by a function @{term f} of
type @{typ"'a \<Rightarrow> 'a"} which
-maps each node to its successor, i.e.\ the graph is really a tree.
+maps each node to its successor; the graph is really a tree.
The task is to find the end of a chain, modelled by a node pointing to
itself. Here is a first attempt:
@{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
@@ -118,21 +120,21 @@
f"}. The proof requires unfolding the definition of @{term step1},
as specified in the \isacommand{hints} above.
-Normally you will then derive the following conditional variant of and from
-the recursion equation
+Normally you will then derive the following conditional variant from
+the recursion equation:
*}
lemma [simp]:
"wf(step1 f) \<Longrightarrow> find(f,x) = (if f x = x then x else find(f, f x))"
by simp
-text{*\noindent and then disable the original recursion equation:*}
+text{*\noindent Then you should disable the original recursion equation:*}
declare find.simps[simp del]
text{*
-We can reason about such underdefined functions just like about any other
-recursive function. Here is a simple example of recursion induction:
+Reasoning about such underdefined functions is like that for other
+recursive functions. Here is a simple example of recursion induction:
*}
lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
@@ -154,8 +156,8 @@
\begin{verbatim}
x := s; while b(x) do x := c(x); return x
\end{verbatim}
-In general, @{term s} will be a tuple (better still: a record). As an example
-consider the following definition of function @{term find} above:
+In general, @{term s} will be a tuple or record. As an example
+consider the following definition of function @{term find}:
*}
constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -171,7 +173,7 @@
Although the definition of tail recursive functions via @{term while} avoids
termination proofs, there is no free lunch. When proving properties of
functions defined by @{term while}, termination rears its ugly head
-again. Here is @{thm[source]while_rule}, the well known proof rule for total
+again. Here is \tdx{while_rule}, the well known proof rule for total
correctness of loops expressed with @{term while}:
@{thm[display,margin=50]while_rule[no_vars]} @{term P} needs to be true of
the initial state @{term s} and invariant under @{term c} (premises 1
@@ -205,7 +207,7 @@
text{* Let us conclude this section on partial functions by a
discussion of the merits of the @{term while} combinator. We have
-already seen that the advantage (if it is one) of not having to
+already seen that the advantage of not having to
provide a termination argument when defining a function via @{term
while} merely puts off the evil hour. On top of that, tail recursive
functions tend to be more complicated to reason about. So why use
--- a/doc-src/TutorialI/Advanced/WFrec.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Thu Aug 09 18:12:15 2001 +0200
@@ -2,7 +2,7 @@
text{*\noindent
So far, all recursive definitions were shown to terminate via measure
-functions. Sometimes this can be quite inconvenient or even
+functions. Sometimes this can be inconvenient or
impossible. Fortunately, \isacommand{recdef} supports much more
general definitions. For example, termination of Ackermann's function
can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
@@ -23,18 +23,19 @@
In general, \isacommand{recdef} supports termination proofs based on
arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
This is called \textbf{well-founded
-recursion}\indexbold{recursion!well-founded}. Clearly, a function definition
-is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+recursion}\indexbold{recursion!well-founded}. A function definition
+is total if and only if the set of
+all pairs $(r,l)$, where $l$ is the argument on the
left-hand side of an equation and $r$ the argument of some recursive call on
the corresponding right-hand side, induces a well-founded relation. For a
systematic account of termination proofs via well-founded relations see, for
example, Baader and Nipkow~\cite{Baader-Nipkow}.
-Each \isacommand{recdef} definition should be accompanied (after the name of
-the function) by a well-founded relation on the argument type of the
-function. Isabelle/HOL formalizes some of the most important
+Each \isacommand{recdef} definition should be accompanied (after the function's
+name) by a well-founded relation on the function's argument type.
+Isabelle/HOL formalizes some of the most important
constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
-example, @{term"measure f"} is always well-founded, and the lexicographic
+example, @{term"measure f"} is always well-founded. The lexicographic
product of two well-founded relations is again well-founded, which we relied
on when defining Ackermann's function above.
Of course the lexicographic product can also be iterated:
@@ -55,8 +56,8 @@
inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
will never have to prove well-foundedness of any relation composed
solely of these building blocks. But of course the proof of
-termination of your function definition, i.e.\ that the arguments
-decrease with every recursive call, may still require you to provide
+termination of your function definition --- that the arguments
+decrease with every recursive call --- may still require you to provide
additional lemmas.
It is also possible to use your own well-founded relations with
@@ -79,7 +80,7 @@
txt{*\noindent
The proof is by showing that our relation is a subset of another well-founded
-relation: one given by a measure function.
+relation: one given by a measure function.\index{*wf_subset (theorem)}
*};
apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast);
--- a/doc-src/TutorialI/Advanced/advanced.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/advanced.tex Thu Aug 09 18:12:15 2001 +0200
@@ -12,15 +12,15 @@
\section{Advanced Forms of Recursion}
\index{recdef@\isacommand {recdef} (command)|(}
-The purpose of this section is to introduce advanced forms of
+This section introduces advanced forms of
\isacommand{recdef}: how to establish termination by means other than measure
-functions, how to define recursive function over nested recursive datatypes,
+functions, how to define recursive functions over nested recursive datatypes
and how to deal with partial functions.
If, after reading this section, you feel that the definition of recursive
functions is overly complicated by the requirement of
-totality, you should ponder the alternative, a logic of partial functions,
-where recursive definitions are always wellformed. For a start, there are many
+totality, you should ponder the alternatives. In a logic of partial functions,
+recursive definitions are always accepted. But there are many
such logics, and no clear winner has emerged. And in all of these logics you
are (more or less frequently) required to reason about the definedness of
terms explicitly. Thus one shifts definedness arguments from definition time to
@@ -38,7 +38,7 @@
\input{Recdef/document/Nested2.tex}
\subsection{Partial Functions}
-\index{partial function}
+\index{functions!partial}
\input{Advanced/document/Partial.tex}
\index{recdef@\isacommand {recdef} (command)|)}
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Thu Aug 09 18:12:15 2001 +0200
@@ -3,8 +3,8 @@
\def\isabellecontext{Partial}%
%
\begin{isamarkuptext}%
-\noindent Throughout the tutorial we have emphasized the fact
-that all functions in HOL are total. Hence we cannot hope to define
+\noindent Throughout this tutorial, we have emphasized
+that all functions in HOL are total. We cannot hope to define
truly partial functions, but must make them total. A straightforward
method is to lift the result type of the function from $\tau$ to
$\tau$~\isa{option} (see \ref{sec:option}), where \isa{None} is
@@ -47,6 +47,7 @@
}
%
\begin{isamarkuptext}%
+\index{recursion!guarded}%
Neither \isacommand{primrec} nor \isacommand{recdef} allow to
prefix an equation with a condition in the way ordinary definitions do
(see \isa{minus} above). Instead we have to move the condition over
@@ -76,7 +77,7 @@
As a more substantial example we consider the problem of searching a graph.
For simplicity our graph is given by a function \isa{f} of
type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
-maps each node to its successor, i.e.\ the graph is really a tree.
+maps each node to its successor; the graph is really a tree.
The task is to find the end of a chain, modelled by a node pointing to
itself. Here is a first attempt:
\begin{isabelle}%
@@ -126,19 +127,19 @@
argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}},
as specified in the \isacommand{hints} above.
-Normally you will then derive the following conditional variant of and from
-the recursion equation%
+Normally you will then derive the following conditional variant from
+the recursion equation:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymLongrightarrow}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}\ simp%
\begin{isamarkuptext}%
-\noindent and then disable the original recursion equation:%
+\noindent Then you should disable the original recursion equation:%
\end{isamarkuptext}%
\isacommand{declare}\ find{\isachardot}simps{\isacharbrackleft}simp\ del{\isacharbrackright}%
\begin{isamarkuptext}%
-We can reason about such underdefined functions just like about any other
-recursive function. Here is a simple example of recursion induction:%
+Reasoning about such underdefined functions is like that for other
+recursive functions. Here is a simple example of recursion induction:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
@@ -162,8 +163,8 @@
\begin{verbatim}
x := s; while b(x) do x := c(x); return x
\end{verbatim}
-In general, \isa{s} will be a tuple (better still: a record). As an example
-consider the following definition of function \isa{find} above:%
+In general, \isa{s} will be a tuple or record. As an example
+consider the following definition of function \isa{find}:%
\end{isamarkuptext}%
\isacommand{constdefs}\ find{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}find{\isadigit{2}}\ f\ x\ {\isasymequiv}\isanewline
@@ -178,7 +179,7 @@
Although the definition of tail recursive functions via \isa{while} avoids
termination proofs, there is no free lunch. When proving properties of
functions defined by \isa{while}, termination rears its ugly head
-again. Here is \isa{while{\isacharunderscore}rule}, the well known proof rule for total
+again. Here is \tdx{while_rule}, the well known proof rule for total
correctness of loops expressed with \isa{while}:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymAnd}s{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ b\ s{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}c\ s{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -214,7 +215,7 @@
\begin{isamarkuptext}%
Let us conclude this section on partial functions by a
discussion of the merits of the \isa{while} combinator. We have
-already seen that the advantage (if it is one) of not having to
+already seen that the advantage of not having to
provide a termination argument when defining a function via \isa{while} merely puts off the evil hour. On top of that, tail recursive
functions tend to be more complicated to reason about. So why use
\isa{while} at all? The only reason is executability: the recursion
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Thu Aug 09 18:12:15 2001 +0200
@@ -5,7 +5,7 @@
\begin{isamarkuptext}%
\noindent
So far, all recursive definitions were shown to terminate via measure
-functions. Sometimes this can be quite inconvenient or even
+functions. Sometimes this can be inconvenient or
impossible. Fortunately, \isacommand{recdef} supports much more
general definitions. For example, termination of Ackermann's function
can be shown by means of the \rmindex{lexicographic product} \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
@@ -25,18 +25,19 @@
In general, \isacommand{recdef} supports termination proofs based on
arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
This is called \textbf{well-founded
-recursion}\indexbold{recursion!well-founded}. Clearly, a function definition
-is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
+recursion}\indexbold{recursion!well-founded}. A function definition
+is total if and only if the set of
+all pairs $(r,l)$, where $l$ is the argument on the
left-hand side of an equation and $r$ the argument of some recursive call on
the corresponding right-hand side, induces a well-founded relation. For a
systematic account of termination proofs via well-founded relations see, for
example, Baader and Nipkow~\cite{Baader-Nipkow}.
-Each \isacommand{recdef} definition should be accompanied (after the name of
-the function) by a well-founded relation on the argument type of the
-function. Isabelle/HOL formalizes some of the most important
+Each \isacommand{recdef} definition should be accompanied (after the function's
+name) by a well-founded relation on the function's argument type.
+Isabelle/HOL formalizes some of the most important
constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
-example, \isa{measure\ f} is always well-founded, and the lexicographic
+example, \isa{measure\ f} is always well-founded. The lexicographic
product of two well-founded relations is again well-founded, which we relied
on when defining Ackermann's function above.
Of course the lexicographic product can also be iterated:%
@@ -54,8 +55,8 @@
existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you
will never have to prove well-foundedness of any relation composed
solely of these building blocks. But of course the proof of
-termination of your function definition, i.e.\ that the arguments
-decrease with every recursive call, may still require you to provide
+termination of your function definition --- that the arguments
+decrease with every recursive call --- may still require you to provide
additional lemmas.
It is also possible to use your own well-founded relations with
@@ -76,7 +77,7 @@
\begin{isamarkuptxt}%
\noindent
The proof is by showing that our relation is a subset of another well-founded
-relation: one given by a measure function.%
+relation: one given by a measure function.\index{*wf_subset (theorem)}%
\end{isamarkuptxt}%
\isacommand{apply}\ {\isacharparenleft}rule\ wf{\isacharunderscore}subset\ {\isacharbrackleft}of\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}k{\isacharcolon}{\isacharcolon}nat{\isachardot}\ N{\isacharminus}k{\isacharparenright}{\isachardoublequote}{\isacharbrackright}{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptxt}%
--- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Thu Aug 09 18:12:15 2001 +0200
@@ -7,10 +7,9 @@
%
\begin{isamarkuptext}%
\label{sec:simplification-II}\index{simplification|(}
-This section discusses some additional nifty features not covered so far and
-gives a short introduction to the simplification process itself. The latter
-is helpful to understand why a particular rule does or does not apply in some
-situation.%
+This section describes features not covered until now. It also
+outlines the simplification process itself, which can be helpful
+when the simplifier does not do what you expect of it.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Advanced Features%
@@ -21,9 +20,10 @@
%
\begin{isamarkuptext}%
\label{sec:simp-cong}
-It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
-kind of contextual information can also be made available for other
+While simplifying the conclusion $Q$
+of $P \Imp Q$, it is legal use the assumption $P$.
+For $\Imp$ this policy is hardwired, but
+contextual information can also be made available for other
operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is
controlled by so-called \bfindex{congruence rules}. This is the one for
\isa{{\isasymlongrightarrow}}:
@@ -41,14 +41,14 @@
\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
\end{isabelle}
-The congruence rule for conditional expressions supplies contextual
+One congruence rule for conditional expressions supplies contextual
information for simplifying the \isa{then} and \isa{else} cases:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
\end{isabelle}
-A congruence rule can also \emph{prevent} simplification of some arguments.
-Here is an alternative congruence rule for conditional expressions:
+An alternative congruence rule for conditional expressions
+actually \emph{prevents} simplification of some arguments:
\begin{isabelle}%
\ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ x\ else\ y{\isacharparenright}%
\end{isabelle}
@@ -83,11 +83,8 @@
}
%
\begin{isamarkuptext}%
-\index{rewrite rule!permutative|bold}
-\index{rewriting!ordered|bold}
-\index{ordered rewriting|bold}
-\index{simplification!ordered|bold}
-An equation is a \bfindex{permutative rewrite rule} if the left-hand
+\index{rewrite rules!permutative|bold}%
+An equation is a \textbf{permutative rewrite rule} if the left-hand
side and right-hand side are the same up to renaming of variables. The most
common permutative rule is commutativity: \isa{x\ {\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}\ x}. Other examples
include \isa{x\ {\isacharminus}\ y\ {\isacharminus}\ z\ {\isacharequal}\ x\ {\isacharminus}\ z\ {\isacharminus}\ y} in arithmetic and \isa{insert\ x\ {\isacharparenleft}insert\ y\ A{\isacharparenright}\ {\isacharequal}\ insert\ y\ {\isacharparenleft}insert\ x\ A{\isacharparenright}} for sets. Such rules are problematic because
@@ -125,14 +122,15 @@
such tricks.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{How it Works%
+\isamarkupsubsection{How the Simplifier Works%
}
%
\begin{isamarkuptext}%
\label{sec:SimpHow}
-Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
-first) and a conditional equation is only applied if its condition could be
-proved (again by simplification). Below we explain some special features of the rewriting process.%
+Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
+first. A conditional equation is only applied if its condition can be
+proved, again by simplification. Below we explain some special features of
+the rewriting process.%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Higher-Order Patterns%
@@ -141,32 +139,34 @@
\begin{isamarkuptext}%
\index{simplification rule|(}
So far we have pretended the simplifier can deal with arbitrary
-rewrite rules. This is not quite true. Due to efficiency (and
-potentially also computability) reasons, the simplifier expects the
+rewrite rules. This is not quite true. For reasons of feasibility,
+the simplifier expects the
left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{higher-order
-pattern}\indexbold{pattern, higher-order}. This restricts where
+pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
+This restricts where
unknowns may occur. Higher-order patterns are terms in $\beta$-normal
-form (this will always be the case unless you have done something
-strange) where each occurrence of an unknown is of the form
+form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
+Each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are OK: if an unknown is
+of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are acceptable: if an unknown is
of base type, it cannot have any arguments. Additionally, the rule
-\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also OK, in
+\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also acceptable, in
both directions: all arguments of the unknowns \isa{{\isacharquery}P} and
\isa{{\isacharquery}Q} are distinct bound variables.
-If the left-hand side is not a higher-order pattern, not all is lost
-and the simplifier will still try to apply the rule, but only if it
-matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus
-pocus. For example, \isa{{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} rewrites
+If the left-hand side is not a higher-order pattern, all is not lost.
+The simplifier will still try to apply the rule provided it
+matches directly: without much $\lambda$-calculus hocus
+pocus. For example, \isa{{\isacharparenleft}{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f{\isacharparenright}\ {\isacharequal}\ True} rewrites
\isa{g\ a\ {\isasymin}\ range\ g} to \isa{True}, but will fail to match
\isa{g{\isacharparenleft}h\ b{\isacharparenright}\ {\isasymin}\ range{\isacharparenleft}{\isasymlambda}x{\isachardot}\ g{\isacharparenleft}h\ x{\isacharparenright}{\isacharparenright}}. However, you can
-replace the offending subterms (in our case \isa{{\isacharquery}f\ {\isacharquery}x}, which
-is not a pattern) by adding new variables and conditions: \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} is fine
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate \isa{{\isacharquery}f\ {\isacharquery}x} and obtain
+ \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f{\isacharparenright}\ {\isacharequal}\ True}, which is fine
as a conditional rewrite rule since conditions can be arbitrary
-terms. However, this trick is not a panacea because the newly
+terms. However, this trick is not a panacea because the newly
introduced conditions may be hard to solve.
There is no restriction on the form of the right-hand
--- a/doc-src/TutorialI/Advanced/simp.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Thu Aug 09 18:12:15 2001 +0200
@@ -5,10 +5,9 @@
section{*Simplification*}
text{*\label{sec:simplification-II}\index{simplification|(}
-This section discusses some additional nifty features not covered so far and
-gives a short introduction to the simplification process itself. The latter
-is helpful to understand why a particular rule does or does not apply in some
-situation.
+This section describes features not covered until now. It also
+outlines the simplification process itself, which can be helpful
+when the simplifier does not do what you expect of it.
*}
subsection{*Advanced Features*}
@@ -16,9 +15,10 @@
subsubsection{*Congruence Rules*}
text{*\label{sec:simp-cong}
-It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
-kind of contextual information can also be made available for other
+While simplifying the conclusion $Q$
+of $P \Imp Q$, it is legal use the assumption $P$.
+For $\Imp$ this policy is hardwired, but
+contextual information can also be made available for other
operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
xs"}. The generation of contextual information during simplification is
@@ -33,11 +33,11 @@
Here are some more examples. The congruence rules for bounded
quantifiers supply contextual information about the bound variable:
@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
-The congruence rule for conditional expressions supplies contextual
+One congruence rule for conditional expressions supplies contextual
information for simplifying the @{text then} and @{text else} cases:
@{thm[display]if_cong[no_vars]}
-A congruence rule can also \emph{prevent} simplification of some arguments.
-Here is an alternative congruence rule for conditional expressions:
+An alternative congruence rule for conditional expressions
+actually \emph{prevents} simplification of some arguments:
@{thm[display]if_weak_cong[no_vars]}
Only the first argument is simplified; the others remain unchanged.
This makes simplification much faster and is faithful to the evaluation
@@ -67,11 +67,8 @@
subsubsection{*Permutative Rewrite Rules*}
text{*
-\index{rewrite rule!permutative|bold}
-\index{rewriting!ordered|bold}
-\index{ordered rewriting|bold}
-\index{simplification!ordered|bold}
-An equation is a \bfindex{permutative rewrite rule} if the left-hand
+\index{rewrite rules!permutative|bold}%
+An equation is a \textbf{permutative rewrite rule} if the left-hand
side and right-hand side are the same up to renaming of variables. The most
common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
@@ -110,45 +107,48 @@
such tricks.
*}
-subsection{*How it Works*}
+subsection{*How the Simplifier Works*}
text{*\label{sec:SimpHow}
-Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
-first) and a conditional equation is only applied if its condition could be
-proved (again by simplification). Below we explain some special features of the rewriting process.
+Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified
+first. A conditional equation is only applied if its condition can be
+proved, again by simplification. Below we explain some special features of
+the rewriting process.
*}
subsubsection{*Higher-Order Patterns*}
text{*\index{simplification rule|(}
So far we have pretended the simplifier can deal with arbitrary
-rewrite rules. This is not quite true. Due to efficiency (and
-potentially also computability) reasons, the simplifier expects the
+rewrite rules. This is not quite true. For reasons of feasibility,
+the simplifier expects the
left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{higher-order
-pattern}\indexbold{pattern, higher-order}. This restricts where
+pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
+This restricts where
unknowns may occur. Higher-order patterns are terms in $\beta$-normal
-form (this will always be the case unless you have done something
-strange) where each occurrence of an unknown is of the form
+form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
+Each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example @{thm add_assoc}, are OK: if an unknown is
+of base type, for example @{thm add_assoc}, are acceptable: if an unknown is
of base type, it cannot have any arguments. Additionally, the rule
-@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
+@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in
both directions: all arguments of the unknowns @{text"?P"} and
@{text"?Q"} are distinct bound variables.
-If the left-hand side is not a higher-order pattern, not all is lost
-and the simplifier will still try to apply the rule, but only if it
-matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus
-pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites
+If the left-hand side is not a higher-order pattern, all is not lost.
+The simplifier will still try to apply the rule provided it
+matches directly: without much $\lambda$-calculus hocus
+pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites
@{term"g a \<in> range g"} to @{term True}, but will fail to match
@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
-replace the offending subterms (in our case @{text"?f ?x"}, which
-is not a pattern) by adding new variables and conditions: @{text"?y =
-?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine
+eliminate the offending subterms --- those that are not patterns ---
+by adding new variables and conditions.
+In our example, we eliminate @{text"?f ?x"} and obtain
+ @{text"?y =
+?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine
as a conditional rewrite rule since conditions can be arbitrary
-terms. However, this trick is not a panacea because the newly
+terms. However, this trick is not a panacea because the newly
introduced conditions may be hard to solve.
There is no restriction on the form of the right-hand
--- a/doc-src/TutorialI/CTL/CTL.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
subsection{*Computation Tree Logic --- CTL*};
text{*\label{sec:CTL}
+\index{CTL|(}%
The semantics of PDL only needs reflexive transitive closure.
Let us be adventurous and introduce a more expressive temporal operator.
We extend the datatype
@@ -27,7 +28,7 @@
"Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
text{*\noindent
-This definition allows a very succinct statement of the semantics of @{term AF}:
+This definition allows a succinct statement of the semantics of @{term AF}:
\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation. In reality one has to define a new datatype and a new function.}
@@ -108,9 +109,9 @@
"lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
txt{*\noindent
-In contrast to the analogous property for @{term EF}, and just
-for a change, we do not use fixed point induction but a weaker theorem,
-also known in the literature (after David Park) as \emph{Park-induction}:
+In contrast to the analogous proof for @{term EF}, and just
+for a change, we do not use fixed point induction. Park-induction,
+named after David Park, is weaker but sufficient for this proof:
\begin{center}
@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
\end{center}
@@ -137,20 +138,19 @@
txt{*
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
-It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, i.e.\ @{term p} without its
-first element. The rest is practically automatic:
+It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, that is,
+@{term p} without its first element. The rest is automatic:
*};
apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
-apply simp;
-apply blast;
+apply force;
done;
text{*
The opposite inclusion is proved by contradiction: if some state
@{term s} is not in @{term"lfp(af A)"}, then we can construct an
-infinite @{term A}-avoiding path starting from @{term s}. The reason is
+infinite @{term A}-avoiding path starting from~@{term s}. The reason is
that by unfolding @{term lfp} we find that if @{term s} is not in
@{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
direct successor of @{term s} that is again not in \mbox{@{term"lfp(af
@@ -219,9 +219,9 @@
apply(clarsimp);
txt{*\noindent
-After simplification and clarification, the subgoal has the following form
+After simplification and clarification, the subgoal has the following form:
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
-and invites a proof by induction on @{term i}:
+It invites a proof by induction on @{term i}:
*};
apply(induct_tac i);
@@ -244,7 +244,7 @@
apply(fast intro:someI2_ex);
txt{*\noindent
-What is worth noting here is that we have used @{text fast} rather than
+What is worth noting here is that we have used \methdx{fast} rather than
@{text blast}. The reason is that @{text blast} would fail because it cannot
cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
subgoal is non-trivial because of the nested schematic variables. For
@@ -349,8 +349,8 @@
The language defined above is not quite CTL\@. The latter also includes an
until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path
-where @{term f} is true \emph{U}ntil @{term g} becomes true''. With the help
-of an auxiliary function
+where @{term f} is true \emph{U}ntil @{term g} becomes true''. We need
+an auxiliary function:
*}
consts until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool"
@@ -362,7 +362,7 @@
"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)
text{*\noindent
-the semantics of @{term EU} is straightforward:
+Expressing the semantics of @{term EU} is now straightforward:
@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}
Note that @{term EU} is not definable in terms of the other operators!
@@ -465,6 +465,7 @@
in the case of finite sets and a monotone function~@{term F},
the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
a fixed point is reached. It is actually possible to generate executable functional programs
-from HOL definitions, but that is beyond the scope of the tutorial.
+from HOL definitions, but that is beyond the scope of the tutorial.%
+\index{CTL|)}
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/CTL/CTLind.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,13 +3,14 @@
subsection{*CTL Revisited*}
text{*\label{sec:CTL-revisited}
-The purpose of this section is twofold: we want to demonstrate
-some of the induction principles and heuristics discussed above and we want to
+\index{CTL|(}%
+The purpose of this section is twofold: to demonstrate
+some of the induction principles and heuristics discussed above and to
show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL\@. In particular the proof of the
@{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
-simple as one might intuitively expect, due to the @{text SOME} operator
+simple as one might expect, due to the @{text SOME} operator
involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
based on an auxiliary inductive definition.
@@ -50,7 +51,7 @@
done
text{*\noindent
-The base case (@{prop"t = s"}) is trivial (@{text blast}).
+The base case (@{prop"t = s"}) is trivial and proved by @{text blast}.
In the induction step, we have an infinite @{term A}-avoiding path @{term f}
starting from @{term u}, a successor of @{term t}. Now we simply instantiate
the @{text"\<forall>f\<in>Paths t"} in the induction hypothesis by the path starting with
@@ -61,7 +62,7 @@
Now we come to the key lemma. Assuming that no infinite @{term A}-avoiding
path starts from @{term s}, we want to show @{prop"s \<in> lfp(af A)"}. For the
inductive proof this must be generalized to the statement that every point @{term t}
-``between'' @{term s} and @{term A}, i.e.\ all of @{term"Avoid s A"},
+``between'' @{term s} and @{term A}, in other words all of @{term"Avoid s A"},
is contained in @{term"lfp(af A)"}:
*}
@@ -77,7 +78,7 @@
again trivial.
The formal counterpart of this proof sketch is a well-founded induction
-w.r.t.\ @{term M} restricted to (roughly speaking) @{term"Avoid s A - A"}:
+on~@{term M} restricted to @{term"Avoid s A - A"}, roughly speaking:
@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}"}
As we shall see presently, the absence of infinite @{term A}-avoiding paths
starting from @{term s} implies well-foundedness of this relation. For the
@@ -95,11 +96,11 @@
then all successors of @{term t} that are in @{term"Avoid s A"} are in
@{term"lfp (af A)"}. Unfolding @{term lfp} in the conclusion of the first
subgoal once, we have to prove that @{term t} is in @{term A} or all successors
-of @{term t} are in @{term"lfp (af A)"}: if @{term t} is not in @{term A},
+of @{term t} are in @{term"lfp (af A)"}. But if @{term t} is not in @{term A},
the second
@{term Avoid}-rule implies that all successors of @{term t} are in
-@{term"Avoid s A"} (because we also assume @{prop"t \<in> Avoid s A"}), and
-hence, by the induction hypothesis, all successors of @{term t} are indeed in
+@{term"Avoid s A"}, because we also assume @{prop"t \<in> Avoid s A"}.
+Hence, by the induction hypothesis, all successors of @{term t} are indeed in
@{term"lfp(af A)"}. Mechanically:
*}
@@ -108,8 +109,8 @@
apply(blast intro:Avoid.intros);
txt{*
-Having proved the main goal we return to the proof obligation that the above
-relation is indeed well-founded. This is proved by contradiction: if
+Having proved the main goal, we return to the proof obligation that the
+relation used above is indeed well-founded. This is proved by contradiction: if
the relation is not well-founded then there exists an infinite @{term
A}-avoiding path all in @{term"Avoid s A"}, by theorem
@{thm[source]wf_iff_no_infinite_down_chain}:
@@ -128,14 +129,15 @@
text{*
The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the
statement of the lemma means
-that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
+that the assumption is left unchanged; otherwise the @{text"\<forall>p"}
+would be turned
into a @{text"\<And>p"}, which would complicate matters below. As it is,
@{thm[source]Avoid_in_lfp} is now
@{thm[display]Avoid_in_lfp[no_vars]}
The main theorem is simply the corollary where @{prop"t = s"},
-in which case the assumption @{prop"t \<in> Avoid s A"} is trivially true
-by the first @{term Avoid}-rule. Isabelle confirms this:
-*}
+when the assumption @{prop"t \<in> Avoid s A"} is trivially true
+by the first @{term Avoid}-rule. Isabelle confirms this:%
+\index{CTL|)}*}
theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
by(auto elim:Avoid_in_lfp intro:Avoid.intros);
--- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Aug 09 18:12:15 2001 +0200
@@ -7,6 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:CTL}
+\index{CTL|(}%
The semantics of PDL only needs reflexive transitive closure.
Let us be adventurous and introduce a more expressive temporal operator.
We extend the datatype
@@ -24,7 +25,7 @@
\ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-This definition allows a very succinct statement of the semantics of \isa{AF}:
+This definition allows a succinct statement of the semantics of \isa{AF}:
\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation. In reality one has to define a new datatype and a new function.}%
@@ -62,9 +63,9 @@
\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-In contrast to the analogous property for \isa{EF}, and just
-for a change, we do not use fixed point induction but a weaker theorem,
-also known in the literature (after David Park) as \emph{Park-induction}:
+In contrast to the analogous proof for \isa{EF}, and just
+for a change, we do not use fixed point induction. Park-induction,
+named after David Park, is weaker but sufficient for this proof:
\begin{center}
\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
\end{center}
@@ -95,21 +96,20 @@
\begin{isamarkuptxt}%
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}pa{\isachardot}\ p\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
\end{isabelle}
-It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its
-first element. The rest is practically automatic:%
+It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is,
+\isa{p} without its first element. The rest is automatic:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{apply}\ blast\isanewline
+\isacommand{apply}\ force\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
The opposite inclusion is proved by contradiction: if some state
\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
-infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
+infinite \isa{A}-avoiding path starting from~\isa{s}. The reason is
that by unfolding \isa{lfp} we find that if \isa{s} is not in
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
@@ -171,13 +171,13 @@
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-After simplification and clarification, the subgoal has the following form
+After simplification and clarification, the subgoal has the following form:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}%
\end{isabelle}
-and invites a proof by induction on \isa{i}:%
+It invites a proof by induction on \isa{i}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
@@ -203,7 +203,7 @@
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-What is worth noting here is that we have used \isa{fast} rather than
+What is worth noting here is that we have used \methdx{fast} rather than
\isa{blast}. The reason is that \isa{blast} would fail because it cannot
cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
subgoal is non-trivial because of the nested schematic variables. For
@@ -283,8 +283,8 @@
\begin{isamarkuptext}%
The language defined above is not quite CTL\@. The latter also includes an
until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
-where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help
-of an auxiliary function%
+where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. We need
+an auxiliary function:%
\end{isamarkuptext}%
\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
@@ -292,7 +292,7 @@
{\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-the semantics of \isa{EU} is straightforward:
+Expressing the semantics of \isa{EU} is now straightforward:
\begin{isabelle}%
\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
\end{isabelle}
@@ -327,6 +327,7 @@
the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
+\index{CTL|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Thu Aug 09 18:12:15 2001 +0200
@@ -7,13 +7,14 @@
%
\begin{isamarkuptext}%
\label{sec:CTL-revisited}
-The purpose of this section is twofold: we want to demonstrate
-some of the induction principles and heuristics discussed above and we want to
+\index{CTL|(}%
+The purpose of this section is twofold: to demonstrate
+some of the induction principles and heuristics discussed above and to
show how inductive definitions can simplify proofs.
In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
model checker for CTL\@. In particular the proof of the
\isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
-simple as one might intuitively expect, due to the \isa{SOME} operator
+simple as one might expect, due to the \isa{SOME} operator
involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}
based on an auxiliary inductive definition.
@@ -50,7 +51,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-The base case (\isa{t\ {\isacharequal}\ s}) is trivial (\isa{blast}).
+The base case (\isa{t\ {\isacharequal}\ s}) is trivial and proved by \isa{blast}.
In the induction step, we have an infinite \isa{A}-avoiding path \isa{f}
starting from \isa{u}, a successor of \isa{t}. Now we simply instantiate
the \isa{{\isasymforall}f{\isasymin}Paths\ t} in the induction hypothesis by the path starting with
@@ -61,7 +62,7 @@
Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. For the
inductive proof this must be generalized to the statement that every point \isa{t}
-``between'' \isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A},
+``between'' \isa{s} and \isa{A}, in other words all of \isa{Avoid\ s\ A},
is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
\end{isamarkuptext}%
\isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
@@ -75,7 +76,7 @@
again trivial.
The formal counterpart of this proof sketch is a well-founded induction
-w.r.t.\ \isa{M} restricted to (roughly speaking) \isa{Avoid\ s\ A\ {\isacharminus}\ A}:
+on~\isa{M} restricted to \isa{Avoid\ s\ A\ {\isacharminus}\ A}, roughly speaking:
\begin{isabelle}%
\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
\end{isabelle}
@@ -100,19 +101,19 @@
then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
-of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}: if \isa{t} is not in \isa{A},
+of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. But if \isa{t} is not in \isa{A},
the second
\isa{Avoid}-rule implies that all successors of \isa{t} are in
-\isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and
-hence, by the induction hypothesis, all successors of \isa{t} are indeed in
+\isa{Avoid\ s\ A}, because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}.
+Hence, by the induction hypothesis, all successors of \isa{t} are indeed in
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
\end{isamarkuptxt}%
\ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
\begin{isamarkuptxt}%
-Having proved the main goal we return to the proof obligation that the above
-relation is indeed well-founded. This is proved by contradiction: if
+Having proved the main goal, we return to the proof obligation that the
+relation used above is indeed well-founded. This is proved by contradiction: if
the relation is not well-founded then there exists an infinite \isa{A}-avoiding path all in \isa{Avoid\ s\ A}, by theorem
\isa{wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain}:
\begin{isabelle}%
@@ -130,15 +131,17 @@
\begin{isamarkuptext}%
The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
statement of the lemma means
-that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
+that the assumption is left unchanged; otherwise the \isa{{\isasymforall}p}
+would be turned
into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
\isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}%
\end{isabelle}
The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
-in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
+when the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
by the first \isa{Avoid}-rule. Isabelle confirms this:%
+\index{CTL|)}%
\end{isamarkuptext}%
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Inductive/AB.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
section{*Case Study: A Context Free Grammar*}
text{*\label{sec:CFG}
+\index{grammars!defining inductively|(}%
Grammars are nothing but shorthands for inductive definitions of nonterminals
which represent sets of strings. For example, the production
$A \to B c$ is short for
@@ -136,8 +137,7 @@
by(force simp add:zabs_def take_Cons split:nat.split if_splits);
text{*
-Finally we come to the above mentioned lemma about cutting in half a word with two
-more elements of one sort than of the other sort:
+Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:
*}
lemma part1:
@@ -212,7 +212,7 @@
holds for all words shorter than @{term w}.
The proof continues with a case distinction on @{term w},
-i.e.\ if @{term w} is empty or not.
+on whether @{term w} is empty or not.
*}
apply(case_tac w);
@@ -285,7 +285,9 @@
text{*
We conclude this section with a comparison of our proof with
-Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
+Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
+\cite[p.\ts81]{HopcroftUllman}.
+For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
@@ -302,7 +304,9 @@
thus is not at all similar to the other cases (which are automatic in
Isabelle). The authors are at least cavalier about this point and may
even have overlooked the slight difficulty lurking in the omitted
-cases. This is not atypical for pen-and-paper proofs, once analysed in
-detail. *}
+cases. Such errors are found in many pen-and-paper proofs when they
+are scrutinized formally.%
+\index{grammars!defining inductively|)}
+*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Inductive/Mutual.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Mutual.thy Thu Aug 09 18:12:15 2001 +0200
@@ -25,7 +25,7 @@
(simply concatenate the names of the sets involved) and has the conclusion
@{text[display]"(?x \<in> even \<longrightarrow> ?P ?x) \<and> (?y \<in> odd \<longrightarrow> ?Q ?y)"}
-If we want to prove that all even numbers are divisible by 2, we have to
+If we want to prove that all even numbers are divisible by two, we have to
generalize the statement as follows:
*}
--- a/doc-src/TutorialI/Inductive/Star.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
section{*The Reflexive Transitive Closure*}
text{*\label{sec:rtc}
+\index{reflexive transitive closure!defining inductively|(}%
An inductive definition may accept parameters, so it can express
functions that yield sets.
Relations too can be defined inductively, since they are just sets of pairs.
@@ -21,7 +22,7 @@
text{*\noindent
The function @{term rtc} is annotated with concrete syntax: instead of
-@{text"rtc r"} we can read and write @{term"r*"}. The actual definition
+@{text"rtc r"} we can write @{term"r*"}. The actual definition
consists of two rules. Reflexivity is obvious and is immediately given the
@{text iff} attribute to increase automation. The
second rule, @{thm[source]rtc_step}, says that we can always add one more
@@ -65,9 +66,9 @@
apply(erule rtc.induct)
txt{*\noindent
-Unfortunately, even the resulting base case is a problem
+Unfortunately, even the base case is a problem:
@{subgoals[display,indent=0,goals_limit=1]}
-and maybe not what you had expected. We have to abandon this proof attempt.
+We have to abandon this proof attempt.
To understand what is going on, let us look again at @{thm[source]rtc.induct}.
In the above application of @{text erule}, the first premise of
@{thm[source]rtc.induct} is unified with the first suitable assumption, which
@@ -150,6 +151,7 @@
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough
anyway, we should always pick the simplest induction schema available.
Hence @{term rtc} is the definition of choice.
+\index{reflexive transitive closure!defining inductively|)}
\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of @{thm[source]rtc_step} also holds:
--- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Thu Aug 09 18:12:15 2001 +0200
@@ -7,6 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:CFG}
+\index{grammars!defining inductively|(}%
Grammars are nothing but shorthands for inductive definitions of nonterminals
which represent sets of strings. For example, the production
$A \to B c$ is short for
@@ -129,8 +130,7 @@
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split\ if{\isacharunderscore}splits{\isacharparenright}%
\begin{isamarkuptext}%
-Finally we come to the above mentioned lemma about cutting in half a word with two
-more elements of one sort than of the other sort:%
+Finally we come to the above-mentioned lemma about cutting in half a word with two more elements of one sort than of the other sort:%
\end{isamarkuptext}%
\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline
\ {\isachardoublequote}size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}\ {\isasymLongrightarrow}\isanewline
@@ -199,7 +199,7 @@
holds for all words shorter than \isa{w}.
The proof continues with a case distinction on \isa{w},
-i.e.\ if \isa{w} is empty or not.%
+on whether \isa{w} is empty or not.%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}%
@@ -266,7 +266,9 @@
\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}%
\begin{isamarkuptext}%
We conclude this section with a comparison of our proof with
-Hopcroft and Ullman's \cite[p.\ts81]{HopcroftUllman}. For a start, the textbook
+Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
+\cite[p.\ts81]{HopcroftUllman}.
+For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
@@ -283,8 +285,9 @@
thus is not at all similar to the other cases (which are automatic in
Isabelle). The authors are at least cavalier about this point and may
even have overlooked the slight difficulty lurking in the omitted
-cases. This is not atypical for pen-and-paper proofs, once analysed in
-detail.%
+cases. Such errors are found in many pen-and-paper proofs when they
+are scrutinized formally.%
+\index{grammars!defining inductively|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Thu Aug 09 18:12:15 2001 +0200
@@ -29,7 +29,7 @@
\ \ \ \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isacharquery}y\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isacharquery}Q\ {\isacharquery}y{\isacharparenright}%
\end{isabelle}
-If we want to prove that all even numbers are divisible by 2, we have to
+If we want to prove that all even numbers are divisible by two, we have to
generalize the statement as follows:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}m\ {\isasymin}\ even\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ m{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymin}\ odd\ {\isasymlongrightarrow}\ {\isadigit{2}}\ dvd\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
--- a/doc-src/TutorialI/Inductive/document/Star.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Thu Aug 09 18:12:15 2001 +0200
@@ -7,6 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:rtc}
+\index{reflexive transitive closure!defining inductively|(}%
An inductive definition may accept parameters, so it can express
functions that yield sets.
Relations too can be defined inductively, since they are just sets of pairs.
@@ -24,7 +25,7 @@
\begin{isamarkuptext}%
\noindent
The function \isa{rtc} is annotated with concrete syntax: instead of
-\isa{rtc\ r} we can read and write \isa{r{\isacharasterisk}}. The actual definition
+\isa{rtc\ r} we can write \isa{r{\isacharasterisk}}. The actual definition
consists of two rules. Reflexivity is obvious and is immediately given the
\isa{iff} attribute to increase automation. The
second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
@@ -68,11 +69,11 @@
\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-Unfortunately, even the resulting base case is a problem
+Unfortunately, even the base case is a problem:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}
-and maybe not what you had expected. We have to abandon this proof attempt.
+We have to abandon this proof attempt.
To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.
In the above application of \isa{erule}, the first premise of
\isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which
@@ -154,6 +155,7 @@
\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough
anyway, we should always pick the simplest induction schema available.
Hence \isa{rtc} is the definition of choice.
+\index{reflexive transitive closure!defining inductively|)}
\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
--- a/doc-src/TutorialI/Inductive/even-example.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/even-example.tex Thu Aug 09 18:12:15 2001 +0200
@@ -27,7 +27,7 @@
above states that 0 is even; the second states that if $n$ is even, then so
is~$n+2$. Given this declaration, Isabelle generates a fixed point
definition for \isa{even} and proves theorems about it,
-thus following the definitional approach (see \S\ref{sec:definitional}).
+thus following the definitional approach (see {\S}\ref{sec:definitional}).
These theorems
include the introduction rules specified in the declaration, an elimination
rule for case analysis and an induction rule. We can refer to these
@@ -300,9 +300,10 @@
dispensing with the lemma \isa{even_imp_even_minus_2}.
This example also justifies the terminology
\textbf{rule inversion}: the new rule inverts the introduction rule
-\isa{even.step}.
+\isa{even.step}. In general, a rule can be inverted when the set of elements
+it introduces is disjoint from those of the other introduction rules.
-For one-off applications of rule inversion, use the \isa{ind_cases} method.
+For one-off applications of rule inversion, use the \methdx{ind_cases} method.
Here is an example:
\begin{isabelle}
\isacommand{apply}\ (ind_cases\ "Suc(Suc\ n)\ \isasymin \ even")
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Aug 09 18:12:15 2001 +0200
@@ -4,7 +4,7 @@
text{*\noindent
Now that we have learned about rules and logic, we take another look at the
-finer points of induction. The two questions we answer are: what to do if the
+finer points of induction. We consider two questions: what to do if the
proposition to be proved is not directly amenable to induction
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
@@ -14,7 +14,7 @@
subsection{*Massaging the Proposition*};
text{*\label{sec:ind-var-in-prems}
-Often we have assumed that the theorem we want to prove is already in a form
+Often we have assumed that the theorem to be proved is already in a form
that is amenable to induction, but sometimes it isn't.
Here is an example.
Since @{term"hd"} and @{term"last"} return the first and last element of a
@@ -31,7 +31,7 @@
\end{quote}
and leads to the base case
@{subgoals[display,indent=0,goals_limit=1]}
-After simplification, it becomes
+Simplification reduces the base case to this:
\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
\end{isabelle}
@@ -41,7 +41,7 @@
We should not have ignored the warning. Because the induction
formula is only the conclusion, induction does not affect the occurrence of @{term xs} in the premises.
Thus the case that should have been trivial
-becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
+becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
@@ -49,7 +49,7 @@
\end{quote}
Thus we should state the lemma as an ordinary
implication~(@{text"\<longrightarrow>"}), letting
-@{text rule_format} (\S\ref{sec:forward}) convert the
+\attrdx{rule_format} (\S\ref{sec:forward}) convert the
result to the usual @{text"\<Longrightarrow>"} form:
*};
(*<*)oops;(*>*)
@@ -65,7 +65,7 @@
If there are multiple premises $A@1$, \dots, $A@n$ containing the
induction variable, you should turn the conclusion $C$ into
-\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
+\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
Additionally, you may also have to universally quantify some other variables,
which can yield a fairly complex conclusion. However, @{text rule_format}
can remove any number of occurrences of @{text"\<forall>"} and
@@ -82,15 +82,17 @@
*)
text{*
+\index{induction!on a term}%
A second reason why your proposition may not be amenable to induction is that
-you want to induct on a whole term, rather than an individual variable. In
-general, when inducting on some term $t$ you must rephrase the conclusion $C$
+you want to induct on a complex term, rather than a variable. In
+general, induction on a term~$t$ requires rephrasing the conclusion~$C$
as
\begin{equation}\label{eqn:ind-over-term}
-\forall y@1 \dots y@n.~ x = t \longrightarrow C
+\forall y@1 \dots y@n.~ x = t \longrightarrow C.
\end{equation}
-where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
-perform induction on $x$ afterwards. An example appears in
+where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
+Now you can perform
+perform induction on~$x$. An example appears in
\S\ref{sec:complete-ind} below.
The very same problem may occur in connection with rule induction. Remember
@@ -98,7 +100,7 @@
some inductively defined set and the $x@i$ are variables. If instead we have
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
-\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
+\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
For an example see \S\ref{sec:CTL-revisited} below.
Of course, all premises that share free variables with $t$ need to be pulled into
@@ -132,11 +134,12 @@
be helpful. We show how to apply such induction schemas by an example.
Structural induction on @{typ"nat"} is
-usually known as mathematical induction. There is also \emph{complete}
-induction, where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]nat_less_induct}:
+usually known as mathematical induction. There is also \textbf{complete}
+\index{induction!complete}%
+induction, where you prove $P(n)$ under the assumption that $P(m)$
+holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
@{thm[display]"nat_less_induct"[no_vars]}
-As an example of its application we prove a property of the following
+As an application, we prove a property of the following
function:
*};
@@ -169,7 +172,7 @@
apply(induct_tac k rule: nat_less_induct);
txt{*\noindent
-which leaves us with the following proof state:
+We get the following proof state:
@{subgoals[display,indent=0,margin=65]}
After stripping the @{text"\<forall>i"}, the proof continues with a case
distinction on @{term"i"}. The case @{prop"i = 0"} is trivial and we focus on
@@ -205,13 +208,12 @@
which, together with (2) yields @{prop"j < f (Suc j)"} (again by
@{thm[source]le_less_trans}).
-This last step shows both the power and the danger of automatic proofs: they
-will usually not tell you how the proof goes, because it can be very hard to
-translate the internal proof into a human-readable format. Therefore
-Chapter~\ref{sec:part2?} introduces a language for writing readable
-proofs.
+This last step shows both the power and the danger of automatic proofs. They
+will usually not tell you how the proof goes, because it can be hard to
+translate the internal proof into a human-readable format. Automatic
+proofs are easy to write but hard to read and understand.
-We can now derive the desired @{prop"i <= f i"} from @{thm[source]f_incr_lem}:
+The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
*};
lemmas f_incr = f_incr_lem[rule_format, OF refl];
@@ -254,11 +256,12 @@
subsection{*Derivation of New Induction Schemas*};
text{*\label{sec:derive-ind}
+\index{induction!deriving new schemas}%
Induction schemas are ordinary theorems and you can derive new ones
-whenever you wish. This section shows you how to, using the example
+whenever you wish. This section shows you how, using the example
of @{thm[source]nat_less_induct}. Assume we only have structural induction
-available for @{typ"nat"} and want to derive complete induction. This
-requires us to generalize the statement first:
+available for @{typ"nat"} and want to derive complete induction. We
+must generalize the statement as shown:
*};
lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
@@ -289,7 +292,7 @@
by(insert induct_lem, blast);
text{*
-Finally we should remind the reader that HOL already provides the mother of
+HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
example theorem @{thm[source]nat_less_induct} is
a special case of @{thm[source]wf_induct} where @{term r} is @{text"<"} on
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Aug 09 18:12:15 2001 +0200
@@ -5,7 +5,7 @@
\begin{isamarkuptext}%
\noindent
Now that we have learned about rules and logic, we take another look at the
-finer points of induction. The two questions we answer are: what to do if the
+finer points of induction. We consider two questions: what to do if the
proposition to be proved is not directly amenable to induction
(\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
@@ -17,7 +17,7 @@
%
\begin{isamarkuptext}%
\label{sec:ind-var-in-prems}
-Often we have assumed that the theorem we want to prove is already in a form
+Often we have assumed that the theorem to be proved is already in a form
that is amenable to induction, but sometimes it isn't.
Here is an example.
Since \isa{hd} and \isa{last} return the first and last element of a
@@ -35,7 +35,7 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
\end{isabelle}
-After simplification, it becomes
+Simplification reduces the base case to this:
\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
\end{isabelle}
@@ -45,7 +45,7 @@
We should not have ignored the warning. Because the induction
formula is only the conclusion, induction does not affect the occurrence of \isa{xs} in the premises.
Thus the case that should have been trivial
-becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
+becomes unprovable. Fortunately, the solution is easy:\footnote{A similar
heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
@@ -53,7 +53,7 @@
\end{quote}
Thus we should state the lemma as an ordinary
implication~(\isa{{\isasymlongrightarrow}}), letting
-\isa{rule{\isacharunderscore}format} (\S\ref{sec:forward}) convert the
+\attrdx{rule_format} (\S\ref{sec:forward}) convert the
result to the usual \isa{{\isasymLongrightarrow}} form:%
\end{isamarkuptxt}%
\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}%
@@ -67,7 +67,7 @@
If there are multiple premises $A@1$, \dots, $A@n$ containing the
induction variable, you should turn the conclusion $C$ into
-\[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
+\[ A@1 \longrightarrow \cdots A@n \longrightarrow C. \]
Additionally, you may also have to universally quantify some other variables,
which can yield a fairly complex conclusion. However, \isa{rule{\isacharunderscore}format}
can remove any number of occurrences of \isa{{\isasymforall}} and
@@ -75,15 +75,17 @@
\end{isamarkuptxt}%
%
\begin{isamarkuptext}%
+\index{induction!on a term}%
A second reason why your proposition may not be amenable to induction is that
-you want to induct on a whole term, rather than an individual variable. In
-general, when inducting on some term $t$ you must rephrase the conclusion $C$
+you want to induct on a complex term, rather than a variable. In
+general, induction on a term~$t$ requires rephrasing the conclusion~$C$
as
\begin{equation}\label{eqn:ind-over-term}
-\forall y@1 \dots y@n.~ x = t \longrightarrow C
+\forall y@1 \dots y@n.~ x = t \longrightarrow C.
\end{equation}
-where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and
-perform induction on $x$ afterwards. An example appears in
+where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
+Now you can perform
+perform induction on~$x$. An example appears in
\S\ref{sec:complete-ind} below.
The very same problem may occur in connection with rule induction. Remember
@@ -91,7 +93,7 @@
some inductively defined set and the $x@i$ are variables. If instead we have
a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
-\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
+\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C. \]
For an example see \S\ref{sec:CTL-revisited} below.
Of course, all premises that share free variables with $t$ need to be pulled into
@@ -127,13 +129,14 @@
be helpful. We show how to apply such induction schemas by an example.
Structural induction on \isa{nat} is
-usually known as mathematical induction. There is also \emph{complete}
-induction, where you must prove $P(n)$ under the assumption that $P(m)$
-holds for all $m<n$. In Isabelle, this is the theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}:
+usually known as mathematical induction. There is also \textbf{complete}
+\index{induction!complete}%
+induction, where you prove $P(n)$ under the assumption that $P(m)$
+holds for all $m<n$. In Isabelle, this is the theorem \tdx{nat_less_induct}:
\begin{isabelle}%
\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
\end{isabelle}
-As an example of its application we prove a property of the following
+As an application, we prove a property of the following
function:%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -162,7 +165,7 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ k\ rule{\isacharcolon}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-which leaves us with the following proof state:
+We get the following proof state:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ m\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
@@ -204,13 +207,12 @@
which, together with (2) yields \isa{j\ {\isacharless}\ f\ {\isacharparenleft}Suc\ j{\isacharparenright}} (again by
\isa{le{\isacharunderscore}less{\isacharunderscore}trans}).
-This last step shows both the power and the danger of automatic proofs: they
-will usually not tell you how the proof goes, because it can be very hard to
-translate the internal proof into a human-readable format. Therefore
-Chapter~\ref{sec:part2?} introduces a language for writing readable
-proofs.
+This last step shows both the power and the danger of automatic proofs. They
+will usually not tell you how the proof goes, because it can be hard to
+translate the internal proof into a human-readable format. Automatic
+proofs are easy to write but hard to read and understand.
-We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
+The desired result, \isa{i\ {\isasymle}\ f\ i}, follows from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
\end{isamarkuptext}%
\isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
\begin{isamarkuptext}%
@@ -255,11 +257,12 @@
%
\begin{isamarkuptext}%
\label{sec:derive-ind}
+\index{induction!deriving new schemas}%
Induction schemas are ordinary theorems and you can derive new ones
-whenever you wish. This section shows you how to, using the example
+whenever you wish. This section shows you how, using the example
of \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}. Assume we only have structural induction
-available for \isa{nat} and want to derive complete induction. This
-requires us to generalize the statement first:%
+available for \isa{nat} and want to derive complete induction. We
+must generalize the statement as shown:%
\end{isamarkuptext}%
\isacommand{lemma}\ induct{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
@@ -288,7 +291,7 @@
\isacommand{theorem}\ nat{\isacharunderscore}less{\isacharunderscore}induct{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isasymforall}m{\isacharless}n{\isachardot}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
-Finally we should remind the reader that HOL already provides the mother of
+HOL already provides the mother of
all inductions, well-founded induction (see \S\ref{sec:Well-founded}). For
example theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} is
a special case of \isa{wf{\isacharunderscore}induct} where \isa{r} is \isa{{\isacharless}} on
--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Thu Aug 09 18:12:15 2001 +0200
@@ -287,7 +287,7 @@
\isa{case}-expressions, as it does \isa{if}-expressions,
because with recursive datatypes it could lead to nontermination.
Instead, the simplifier has a modifier
-\isa{split}\index{*split (modified)}
+\isa{split}\index{*split (modifier)}
for adding splitting rules explicitly. The
lemma above can be proved in one step by%
\end{isamarkuptxt}%
--- a/doc-src/TutorialI/Misc/simp.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Thu Aug 09 18:12:15 2001 +0200
@@ -281,7 +281,7 @@
@{text"case"}-expressions, as it does @{text"if"}-expressions,
because with recursive datatypes it could lead to nontermination.
Instead, the simplifier has a modifier
-@{text split}\index{*split (modified)}
+@{text split}\index{*split (modifier)}
for adding splitting rules explicitly. The
lemma above can be proved in one step by
*}
--- a/doc-src/TutorialI/Recdef/Nested0.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested0.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
(*>*)
text{*
+\index{datatypes!nested}%
In \S\ref{sec:nested-datatype} we defined the datatype of terms
*}
--- a/doc-src/TutorialI/Recdef/Nested1.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Thu Aug 09 18:12:15 2001 +0200
@@ -25,15 +25,15 @@
where @{term set} returns the set of elements of a list
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle
-(while processing the declaration of @{text term}). First we have to understand why the
-recursive call of @{term trev} underneath @{term map} leads to the above
-condition. The reason is that \isacommand{recdef} ``knows'' that @{term map}
+(while processing the declaration of @{text term}). Why does the
+recursive call of @{term trev} lead to this
+condition? Because \isacommand{recdef} knows that @{term map}
will apply @{term trev} only to elements of @{term ts}. Thus the
condition expresses that the size of the argument @{prop"t : set ts"} of any
recursive call of @{term trev} is strictly less than @{term"size(App f ts)"},
which equals @{term"Suc(term_list_size ts)"}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
-\isacommand{recdef} ``knows'' about @{term map}.
+\isacommand{recdef} knows about @{term map}.
*};
(*<*)
--- a/doc-src/TutorialI/Recdef/Nested2.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy Thu Aug 09 18:12:15 2001 +0200
@@ -54,19 +54,19 @@
Let us now return to the question of how \isacommand{recdef} can come up with
sensible termination conditions in the presence of higher-order functions
-like @{term"map"}. For a start, if nothing were known about @{term"map"},
+like @{term"map"}. For a start, if nothing were known about @{term"map"}, then
@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
(term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
@{thm[source]map_cong}:
@{thm[display,margin=50]"map_cong"[no_vars]}
-Its second premise expresses (indirectly) that the first argument of
-@{term"map"} is only applied to elements of its second argument. Congruence
-rules for other higher-order functions on lists look very similar. If you get
+Its second premise expresses that in @{term"map f xs"},
+function @{term"f"} is only applied to elements of list @{term"xs"}. Congruence
+rules for other higher-order functions on lists are similar. If you get
into a situation where you need to supply \isacommand{recdef} with new
-congruence rules, you can either append a hint after the end of
-the recursion equations
+congruence rules, you can append a hint after the end of
+the recursion equations:
*}
(*<*)
consts dummy :: "nat => nat"
@@ -76,14 +76,14 @@
(hints recdef_cong: map_cong)
text{*\noindent
-or declare them globally
-by giving them the \attrdx{recdef_cong} attribute as in
+Or you can declare them globally
+by giving them the \attrdx{recdef_cong} attribute:
*}
declare map_cong[recdef_cong]
text{*
-Note that the @{text cong} and @{text recdef_cong} attributes are
+The @{text cong} and @{text recdef_cong} attributes are
intentionally kept apart because they control different activities, namely
simplification and making recursive definitions.
% The local @{text cong} in
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
\def\isabellecontext{Nested{\isadigit{0}}}%
%
\begin{isamarkuptext}%
+\index{datatypes!nested}%
In \S\ref{sec:nested-datatype} we defined the datatype of terms%
\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isachardoublequote}%
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Thu Aug 09 18:12:15 2001 +0200
@@ -27,15 +27,15 @@
where \isa{set} returns the set of elements of a list
and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary
function automatically defined by Isabelle
-(while processing the declaration of \isa{term}). First we have to understand why the
-recursive call of \isa{trev} underneath \isa{map} leads to the above
-condition. The reason is that \isacommand{recdef} ``knows'' that \isa{map}
+(while processing the declaration of \isa{term}). Why does the
+recursive call of \isa{trev} lead to this
+condition? Because \isacommand{recdef} knows that \isa{map}
will apply \isa{trev} only to elements of \isa{ts}. Thus the
condition expresses that the size of the argument \isa{t\ {\isasymin}\ set\ ts} of any
recursive call of \isa{trev} is strictly less than \isa{size\ {\isacharparenleft}App\ f\ ts{\isacharparenright}},
which equals \isa{Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}. We will now prove the termination condition and
continue with our definition. Below we return to the question of how
-\isacommand{recdef} ``knows'' about \isa{map}.%
+\isacommand{recdef} knows about \isa{map}.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Aug 09 18:12:15 2001 +0200
@@ -54,7 +54,7 @@
Let us now return to the question of how \isacommand{recdef} can come up with
sensible termination conditions in the presence of higher-order functions
-like \isa{map}. For a start, if nothing were known about \isa{map},
+like \isa{map}. For a start, if nothing were known about \isa{map}, then
\isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus
\isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
@@ -63,22 +63,22 @@
\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
\end{isabelle}
-Its second premise expresses (indirectly) that the first argument of
-\isa{map} is only applied to elements of its second argument. Congruence
-rules for other higher-order functions on lists look very similar. If you get
+Its second premise expresses that in \isa{map\ f\ xs},
+function \isa{f} is only applied to elements of list \isa{xs}. Congruence
+rules for other higher-order functions on lists are similar. If you get
into a situation where you need to supply \isacommand{recdef} with new
-congruence rules, you can either append a hint after the end of
-the recursion equations%
+congruence rules, you can append a hint after the end of
+the recursion equations:%
\end{isamarkuptext}%
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-or declare them globally
-by giving them the \attrdx{recdef_cong} attribute as in%
+Or you can declare them globally
+by giving them the \attrdx{recdef_cong} attribute:%
\end{isamarkuptext}%
\isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
\begin{isamarkuptext}%
-Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
+The \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
intentionally kept apart because they control different activities, namely
simplification and making recursive definitions.
% The local \isa{cong} in
--- a/doc-src/TutorialI/Rules/rules.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Aug 09 18:12:15 2001 +0200
@@ -1311,7 +1311,6 @@
\isacommand{by}\ (auto\ intro:\ order_antisym)
\end{isabelle}
-\REMARK{refer to \isa{Main_wo_AC} if we introduce it}
\subsection{Indefinite Descriptions}
--- a/doc-src/TutorialI/Sets/sets.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Aug 09 18:12:15 2001 +0200
@@ -913,7 +913,7 @@
((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
\rulenamedx{less_than_iff}\isanewline
wf\ less_than
-\rulename{wf_less_than}
+\rulenamedx{wf_less_than}
\end{isabelle}
The notion of measure generalizes to the
@@ -928,7 +928,7 @@
\isasymin\ r\isacharbraceright
\rulenamedx{inv_image_def}\isanewline
wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
-\rulename{wf_inv_image}
+\rulenamedx{wf_inv_image}
\end{isabelle}
A measure function involves the natural numbers. The relation \isa{measure
@@ -939,7 +939,7 @@
measure\ \isasymequiv\ inv_image\ less_than%
\rulenamedx{measure_def}\isanewline
wf\ (measure\ f)
-\rulename{wf_measure}
+\rulenamedx{wf_measure}
\end{isabelle}
Of the other constructions, the most important is the
@@ -957,7 +957,7 @@
\rulenamedx{lex_prod_def}%
\par\smallskip
\isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
-\rulename{wf_lex_prod}
+\rulenamedx{wf_lex_prod}
\end{isabelle}
These constructions can be used in a
--- a/doc-src/TutorialI/Types/Axioms.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,10 +3,10 @@
subsection{*Axioms*}
-text{*Now we want to attach axioms to our classes. Then we can reason on the
-level of classes and the results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our above ordering relations.
+text{*Attaching axioms to our classes lets us reason on the
+level of classes. The results will be applicable to all types in a class,
+just as in axiomatic mathematics. These ideas are demonstrated by means of
+our ordering relations.
*}
subsubsection{*Partial Orders*}
@@ -26,13 +26,13 @@
The first three axioms are the familiar ones, and the final one
requires that @{text"<<"} and @{text"<<="} are related as expected.
Note that behind the scenes, Isabelle has restricted the axioms to class
-@{text parord}. For example, this is what @{thm[source]refl} really looks like:
+@{text parord}. For example, the axiom @{thm[source]refl} really is
@{thm[show_sorts]refl}.
We have not made @{thm[source]less_le} a global definition because it would
fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of the above class is that
+asymmetry. The drawback of our choice is that
we need to define both @{text"<<="} and @{text"<<"} for each instance.
We can now prove simple theorems in this abstract setting, for example
@@ -42,14 +42,16 @@
lemma [simp]: "(x::'a::parord) << y \<Longrightarrow> (\<not> y << x) = True";
txt{*\noindent
-The conclusion is not simply @{prop"\<not> y << x"} because the preprocessor
-of the simplifier (see \S\ref{sec:simp-preprocessor})
-would turn this into @{prop"y << x = False"}, thus yielding
-a nonterminating rewrite rule. In the above form it is a generally useful
-rule.
+The conclusion is not just @{prop"\<not> y << x"} because the
+simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
+would turn it into @{prop"y << x = False"}, yielding
+a nonterminating rewrite rule.
+(It would be used to try to prove its own precondition \emph{ad
+ infinitum}.)
+In the form above, the rule is useful.
The type constraint is necessary because otherwise Isabelle would only assume
-@{text"'a::ordrel"} (as required in the type of @{text"<<"}), in
-which case the proposition is not a theorem. The proof is easy:
+@{text"'a::ordrel"} (as required in the type of @{text"<<"}),
+when the proposition is not a theorem. The proof is easy:
*}
by(simp add:less_le antisym);
@@ -67,8 +69,9 @@
This time @{text intro_classes} leaves us with the four axioms,
specialized to type @{typ bool}, as subgoals:
@{subgoals[display,show_types,indent=0]}
-Fortunately, the proof is easy for blast, once we have unfolded the definitions
-of @{text"<<"} and @{text"<<="} at @{typ bool}:
+Fortunately, the proof is easy for \isa{blast}
+once we have unfolded the definitions
+of @{text"<<"} and @{text"<<="} at type @{typ bool}:
*}
apply(simp_all (no_asm_use) only: le_bool_def less_bool_def);
@@ -85,16 +88,15 @@
text{*\noindent
The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules as well.
-It should be clear that the main advantage of the axiomatic method is that
-theorems can be proved in the abstract and one does not need to repeat the
-proof for each instance.
+that tools like the simplifier can deal with generic rules.
+The main advantage of the axiomatic method is that
+theorems can be proved in the abstract and freely reused for each instance.
*}
subsubsection{*Linear Orders*}
text{* If any two elements of a partial order are comparable it is a
-\emph{linear} or \emph{total} order: *}
+\textbf{linear} or \textbf{total} order: *}
axclass linord < parord
linear: "x <<= y \<or> y <<= x"
@@ -112,9 +114,10 @@
done
text{*
-Linear orders are an example of subclassing by construction, which is the most
-common case. It is also possible to prove additional subclass relationships
-later on, i.e.\ subclassing by proof. This is the topic of the following
+Linear orders are an example of subclassing\index{subclasses}
+by construction, which is the most
+common case. Subclass relationships can also be proved.
+This is the topic of the following
paragraph.
*}
@@ -122,7 +125,7 @@
text{*
An alternative axiomatization of partial orders takes @{text"<<"} rather than
-@{text"<<="} as the primary concept. The result is a \emph{strict} order:
+@{text"<<="} as the primary concept. The result is a \textbf{strict} order:
*}
axclass strord < ordrel
@@ -173,7 +176,7 @@
text{*
A class may inherit from more than one direct superclass. This is called
-multiple inheritance and is certainly permitted. For example we could define
+\bfindex{multiple inheritance}. For example, we could define
the classes of well-founded orderings and well-orderings:
*}
@@ -220,13 +223,12 @@
This concludes our demonstration of type classes based on orderings. We
remind our readers that \isa{Main} contains a theory of
orderings phrased in terms of the usual @{text"\<le>"} and @{text"<"}.
-It is recommended that, if possible,
-you base your own ordering relations on this theory.
+If possible, base your own ordering relations on this theory.
*}
subsubsection{*Inconsistencies*}
-text{* The reader may be wondering what happens if we, maybe accidentally,
+text{* The reader may be wondering what happens if we
attach an inconsistent set of axioms to a class. So far we have always
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
seems that we are throwing all caution to the wind. So why is there no
--- a/doc-src/TutorialI/Types/Overloading.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Thu Aug 09 18:12:15 2001 +0200
@@ -4,8 +4,9 @@
text{*\noindent
This \isacommand{instance} declaration can be read like the declaration of
-a function on types: the constructor @{text list} maps types of class @{text
-term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
+a function on types. The constructor @{text list} maps types of class @{text
+term} (all HOL types), to types of class @{text ordrel};
+in other words,
if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
Of course we should also define the meaning of @{text <<=} and
@{text <<} on lists:
--- a/doc-src/TutorialI/Types/Overloading0.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading0.thy Thu Aug 09 18:12:15 2001 +0200
@@ -34,10 +34,8 @@
However, there is nothing to prevent the user from forming terms such as
@{text"inverse []"} and proving theorems such as @{text"inverse []
-= inverse []"}, although we never defined inverse on lists. We hasten to say
-that there is nothing wrong with such terms and theorems. But it would be
-nice if we could prevent their formation, simply because it is very likely
-that the user did not mean to write what he did. Thus she had better not waste
-her time pursuing it further. This requires the use of type classes.
+= inverse []"} when inverse is not defined on lists. Proving theorems about
+undefined constants does not endanger soundness, but it is pointless.
+To prevent such terms from even being formed requires the use of type classes.
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading1.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading1.thy Thu Aug 09 18:12:15 2001 +0200
@@ -3,7 +3,7 @@
subsubsection{*Controlled Overloading with Type Classes*}
text{*
-We now start with the theory of ordering relations, which we want to phrase
+We now start with the theory of ordering relations, which we shall phrase
in terms of the two binary symbols @{text"<<"} and @{text"<<="}
to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
@@ -14,9 +14,9 @@
text{*\noindent
This introduces a new class @{text ordrel} and makes it a subclass of
-the predefined class @{text term}\footnote{The quotes around @{text term}
-simply avoid the clash with the command \isacommand{term}.} --- @{text term}
-is the class of all HOL types, like ``Object'' in Java.
+the predefined class @{text term}, which
+is the class of all HOL types.\footnote{The quotes around @{text term}
+simply avoid the clash with the command \isacommand{term}.}
This is a degenerate form of axiomatic type class without any axioms.
Its sole purpose is to restrict the use of overloaded constants to meaningful
instances:
@@ -30,7 +30,7 @@
constrained with a class; the constraint is propagated to the other
occurrences automatically.
-So far there is not a single type of class @{text ordrel}. To breathe life
+So far there are no types of class @{text ordrel}. To breathe life
into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
@{text ordrel}:
*}
@@ -41,7 +41,7 @@
Command \isacommand{instance} actually starts a proof, namely that
@{typ bool} satisfies all axioms of @{text ordrel}.
There are none, but we still need to finish that proof, which we do
-by invoking a fixed predefined method:
+by invoking the \methdx{intro_classes} method:
*}
by intro_classes
@@ -59,12 +59,13 @@
less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
text{*\noindent
-Now @{prop"False <<= P"} is provable
+Now @{prop"False <<= P"} is provable:
*}
lemma "False <<= P"
by(simp add: le_bool_def)
text{*\noindent
-whereas @{text"[] <<= []"} is not even well-typed. In order to make it well-typed
+At this point, @{text"[] <<= []"} is not even well-typed.
+To make it well-typed,
we need to make lists a type of class @{text ordrel}:*}(*<*)end(*>*)
--- a/doc-src/TutorialI/Types/Overloading2.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading2.thy Thu Aug 09 18:12:15 2001 +0200
@@ -16,6 +16,12 @@
text{*\noindent
The infix function @{text"!"} yields the nth element of a list.
+
+\begin{warn}
+A type constructor can be instantiated in only one way to
+a given type class. For example, our two instantiations of \isa{list} must
+reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+\end{warn}
*}
subsubsection{*Predefined Overloading*}
@@ -24,7 +30,7 @@
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
-@{text"-"}, @{text"\<le>"} and @{text"<"} on sets.
+$-$ and @{text"\<le>"} on sets.
In addition there is a special input syntax for bounded quantifiers:
\begin{center}
--- a/doc-src/TutorialI/Types/Pairs.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Pairs.thy Thu Aug 09 18:12:15 2001 +0200
@@ -6,8 +6,8 @@
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
repertoire of operations: pairing and the two projections @{term fst} and
@{term snd}. In any non-trivial application of pairs you will find that this
-quickly leads to unreadable formulae involving nests of projections. This
-section is concerned with introducing some syntactic sugar to overcome this
+quickly leads to unreadable nests of projections. This
+section introduces syntactic sugar to overcome this
problem: pattern matching with tuples.
*}
@@ -33,12 +33,11 @@
internal representation. Thus the internal and external form of a term may
differ, which can affect proofs. If you want to avoid this complication,
stick to @{term fst} and @{term snd} and write @{term"%p. fst p + snd p"}
-instead of @{text"\<lambda>(x,y). x+y"} (which denote the same function but are quite
-different terms).
+instead of @{text"\<lambda>(x,y). x+y"}. These terms are distinct even though they
+denote the same function.
Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
-@{term split}\indexbold{*split (constant)}
-is the uncurrying function of type @{text"('a \<Rightarrow> 'b
+\cdx{split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
\begin{center}
@{thm split_def}
@@ -64,16 +63,17 @@
approach is neither elegant nor very practical in large examples, although it
can be effective in small ones.
-If we step back and ponder why the above lemma presented a problem in the
-first place, we quickly realize that what we would like is to replace @{term
-p} with some concrete pair @{term"(a,b)"}, in which case both sides of the
-equation would simplify to @{term a} because of the simplification rules
-@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}. This is the
-key problem one faces when reasoning about pattern matching with pairs: how to
-convert some atomic term into a pair.
+If we consider why this lemma presents a problem,
+we quickly realize that we need to replace the variable~@{term
+p} by some pair @{term"(a,b)"}. Then both sides of the
+equation would simplify to @{term a} by the simplification rules
+@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.
+To reason about tuple patterns requires some way of
+converting a variable of product type into a pair.
In case of a subterm of the form @{term"split f p"} this is easy: the split
-rule @{thm[source]split_split} replaces @{term p} by a pair:
+rule @{thm[source]split_split} replaces @{term p} by a pair:%
+\index{*split (method)}
*}
lemma "(\<lambda>(x,y).y) p = snd p"
@@ -147,7 +147,7 @@
txt{*\noindent
@{subgoals[display,indent=0]}
-Again, @{text case_tac} is applicable because @{text"\<times>"} is a datatype.
+Again, \methdx{case_tac} is applicable because @{text"\<times>"} is a datatype.
The subgoal is easily proved by @{text simp}.
Splitting by @{text case_tac} also solves the previous examples and may thus
@@ -172,10 +172,13 @@
text{*\noindent
Note that we have intentionally included only @{thm[source]split_paired_all}
-in the first simplification step. This time the reason was not merely
+in the first simplification step, and then we simplify again.
+This time the reason was not merely
pedagogical:
-@{thm[source]split_paired_all} may interfere with certain congruence
-rules of the simplifier, i.e.
+@{thm[source]split_paired_all} may interfere with other functions
+of the simplifier.
+The following command could fail (here it does not)
+where two separate \isa{simp} applications succeed.
*}
(*<*)
@@ -184,18 +187,15 @@
apply(simp add:split_paired_all)
(*<*)done(*>*)
text{*\noindent
-may fail (here it does not) where the above two stages succeed.
-
-Finally, all @{text"\<forall>"} and @{text"\<exists>"}-quantified variables are split
-automatically by the simplifier:
+Finally, the simplifier automatically splits all @{text"\<forall>"} and
+@{text"\<exists>"}-quantified variables:
*}
lemma "\<forall>p. \<exists>q. swap p = swap q"
-apply simp;
-done
+by simp;
text{*\noindent
-In case you would like to turn off this automatic splitting, just disable the
+To turn off this automatic splitting, just disable the
responsible simplification rules:
\begin{center}
@{thm split_paired_All[no_vars]}
--- a/doc-src/TutorialI/Types/Typedef.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Typedef.thy Thu Aug 09 18:12:15 2001 +0200
@@ -5,8 +5,8 @@
text{*\label{sec:adv-typedef}
For most applications, a combination of predefined types like @{typ bool} and
@{text"\<Rightarrow>"} with recursive datatypes and records is quite sufficient. Very
-occasionally you may feel the need for a more advanced type. If you cannot do
-without that type, and you are certain that it is not definable by any of the
+occasionally you may feel the need for a more advanced type. If you
+are certain that your type is not definable by any of the
standard means, then read on.
\begin{warn}
Types in HOL must be non-empty; otherwise the quantifier rules would be
@@ -164,37 +164,25 @@
we merely need to prove that @{term A}, @{term B} and @{term C} are distinct
and that they exhaust the type.
-We start with a helpful version of injectivity of @{term Abs_three} on the
-representing subset:
-*}
-
-lemma [simp]:
- "\<lbrakk> x \<in> three; y \<in> three \<rbrakk> \<Longrightarrow> (Abs_three x = Abs_three y) = (x=y)";
-
-txt{*\noindent
-We prove each direction separately. From @{prop"Abs_three x = Abs_three y"}
-we use @{thm[source]arg_cong} to apply @{term Rep_three} to both sides,
-deriving @{prop[display]"Rep_three(Abs_three x) = Rep_three(Abs_three y)"}
-Thus we get the required @{prop"x =
-y"} by simplification with @{thm[source]Abs_three_inverse}.
-The other direction
-is trivial by simplification:
-*}
-
-apply(rule iffI);
- apply(drule_tac f = Rep_three in arg_cong);
- apply(simp add:Abs_three_inverse);
-by simp;
-
-text{*\noindent
-Analogous lemmas can be proved in the same way for arbitrary type definitions.
-
+In processing our \isacommand{typedef} declaration,
+Isabelle helpfully proves several lemmas.
+One, @{thm[source]Abs_three_inject},
+expresses that @{term Abs_three} is injective on the representing subset:
+\begin{center}
+@{thm Abs_three_inject[no_vars]}
+\end{center}
+Another, @{thm[source]Rep_three_inject}, expresses that the representation
+function is also injective:
+\begin{center}
+@{thm Rep_three_inject[no_vars]}
+\end{center}
Distinctness of @{term A}, @{term B} and @{term C} follows immediately
-if we expand their definitions and rewrite with the above simplification rule:
+if we expand their definitions and rewrite with the injectivity
+of @{term Abs_three}:
*}
lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B";
-by(simp add:A_def B_def C_def three_def);
+by(simp add: Abs_three_inject A_def B_def C_def three_def);
text{*\noindent
Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}.
@@ -221,7 +209,8 @@
done
text{*
-Now the case distinction lemma on type @{typ three} is easy to derive if you know how to:
+Now the case distinction lemma on type @{typ three} is easy to derive if you
+know how:
*}
lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x";
--- a/doc-src/TutorialI/Types/document/Axioms.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Thu Aug 09 18:12:15 2001 +0200
@@ -6,10 +6,10 @@
}
%
\begin{isamarkuptext}%
-Now we want to attach axioms to our classes. Then we can reason on the
-level of classes and the results will be applicable to all types in a class,
-just as in axiomatic mathematics. These ideas are demonstrated by means of
-our above ordering relations.%
+Attaching axioms to our classes lets us reason on the
+level of classes. The results will be applicable to all types in a class,
+just as in axiomatic mathematics. These ideas are demonstrated by means of
+our ordering relations.%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Partial Orders%
@@ -29,13 +29,13 @@
The first three axioms are the familiar ones, and the final one
requires that \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} are related as expected.
Note that behind the scenes, Isabelle has restricted the axioms to class
-\isa{parord}. For example, this is what \isa{refl} really looks like:
+\isa{parord}. For example, the axiom \isa{refl} really is
\isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
We have not made \isa{less{\isacharunderscore}le} a global definition because it would
fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
never the other way around. Below you will see why we want to avoid this
-asymmetry. The drawback of the above class is that
+asymmetry. The drawback of our choice is that
we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
We can now prove simple theorems in this abstract setting, for example
@@ -44,14 +44,16 @@
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-The conclusion is not simply \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the preprocessor
-of the simplifier (see \S\ref{sec:simp-preprocessor})
-would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding
-a nonterminating rewrite rule. In the above form it is a generally useful
-rule.
+The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the
+simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
+would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
+a nonterminating rewrite rule.
+(It would be used to try to prove its own precondition \emph{ad
+ infinitum}.)
+In the form above, the rule is useful.
The type constraint is necessary because otherwise Isabelle would only assume
-\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), in
-which case the proposition is not a theorem. The proof is easy:%
+\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}),
+when the proposition is not a theorem. The proof is easy:%
\end{isamarkuptxt}%
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}%
\begin{isamarkuptext}%
@@ -73,8 +75,9 @@
\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
\end{isabelle}
-Fortunately, the proof is easy for blast, once we have unfolded the definitions
-of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at \isa{bool}:%
+Fortunately, the proof is easy for \isa{blast}
+once we have unfolded the definitions
+of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}%
@@ -89,10 +92,9 @@
\begin{isamarkuptext}%
\noindent
The effect is not stunning, but it demonstrates the principle. It also shows
-that tools like the simplifier can deal with generic rules as well.
-It should be clear that the main advantage of the axiomatic method is that
-theorems can be proved in the abstract and one does not need to repeat the
-proof for each instance.%
+that tools like the simplifier can deal with generic rules.
+The main advantage of the axiomatic method is that
+theorems can be proved in the abstract and freely reused for each instance.%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Linear Orders%
@@ -100,7 +102,7 @@
%
\begin{isamarkuptext}%
If any two elements of a partial order are comparable it is a
-\emph{linear} or \emph{total} order:%
+\textbf{linear} or \textbf{total} order:%
\end{isamarkuptext}%
\isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline
linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}%
@@ -116,9 +118,10 @@
\isacommand{apply}\ blast\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-Linear orders are an example of subclassing by construction, which is the most
-common case. It is also possible to prove additional subclass relationships
-later on, i.e.\ subclassing by proof. This is the topic of the following
+Linear orders are an example of subclassing\index{subclasses}
+by construction, which is the most
+common case. Subclass relationships can also be proved.
+This is the topic of the following
paragraph.%
\end{isamarkuptext}%
%
@@ -127,7 +130,7 @@
%
\begin{isamarkuptext}%
An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
-\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \emph{strict} order:%
+\isa{{\isacharless}{\isacharless}{\isacharequal}} as the primary concept. The result is a \textbf{strict} order:%
\end{isamarkuptext}%
\isacommand{axclass}\ strord\ {\isacharless}\ ordrel\isanewline
irrefl{\isacharcolon}\ \ \ \ \ {\isachardoublequote}{\isasymnot}\ x\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
@@ -167,7 +170,7 @@
%
\begin{isamarkuptext}%
A class may inherit from more than one direct superclass. This is called
-multiple inheritance and is certainly permitted. For example we could define
+\bfindex{multiple inheritance}. For example, we could define
the classes of well-founded orderings and well-orderings:%
\end{isamarkuptext}%
\isacommand{axclass}\ wford\ {\isacharless}\ parord\isanewline
@@ -212,15 +215,14 @@
This concludes our demonstration of type classes based on orderings. We
remind our readers that \isa{Main} contains a theory of
orderings phrased in terms of the usual \isa{{\isasymle}} and \isa{{\isacharless}}.
-It is recommended that, if possible,
-you base your own ordering relations on this theory.%
+If possible, base your own ordering relations on this theory.%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Inconsistencies%
}
%
\begin{isamarkuptext}%
-The reader may be wondering what happens if we, maybe accidentally,
+The reader may be wondering what happens if we
attach an inconsistent set of axioms to a class. So far we have always
avoided to add new axioms to HOL for fear of inconsistencies and suddenly it
seems that we are throwing all caution to the wind. So why is there no
--- a/doc-src/TutorialI/Types/document/Overloading.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Thu Aug 09 18:12:15 2001 +0200
@@ -6,7 +6,8 @@
\begin{isamarkuptext}%
\noindent
This \isacommand{instance} declaration can be read like the declaration of
-a function on types: the constructor \isa{list} maps types of class \isa{term}, i.e.\ all HOL types, to types of class \isa{ordrel}, i.e.\
+a function on types. The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel};
+in other words,
if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
\isa{{\isacharless}{\isacharless}} on lists:%
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Thu Aug 09 18:12:15 2001 +0200
@@ -37,11 +37,9 @@
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say
-that there is nothing wrong with such terms and theorems. But it would be
-nice if we could prevent their formation, simply because it is very likely
-that the user did not mean to write what he did. Thus she had better not waste
-her time pursuing it further. This requires the use of type classes.%
+\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about
+undefined constants does not endanger soundness, but it is pointless.
+To prevent such terms from even being formed requires the use of type classes.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Thu Aug 09 18:12:15 2001 +0200
@@ -6,7 +6,7 @@
}
%
\begin{isamarkuptext}%
-We now start with the theory of ordering relations, which we want to phrase
+We now start with the theory of ordering relations, which we shall phrase
in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
introduce the class \isa{ordrel}:%
@@ -15,9 +15,9 @@
\begin{isamarkuptext}%
\noindent
This introduces a new class \isa{ordrel} and makes it a subclass of
-the predefined class \isa{term}\footnote{The quotes around \isa{term}
-simply avoid the clash with the command \isacommand{term}.} --- \isa{term}
-is the class of all HOL types, like ``Object'' in Java.
+the predefined class \isa{term}, which
+is the class of all HOL types.\footnote{The quotes around \isa{term}
+simply avoid the clash with the command \isacommand{term}.}
This is a degenerate form of axiomatic type class without any axioms.
Its sole purpose is to restrict the use of overloaded constants to meaningful
instances:%
@@ -30,7 +30,7 @@
constrained with a class; the constraint is propagated to the other
occurrences automatically.
-So far there is not a single type of class \isa{ordrel}. To breathe life
+So far there are no types of class \isa{ordrel}. To breathe life
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
\isa{ordrel}:%
\end{isamarkuptext}%
@@ -40,7 +40,7 @@
Command \isacommand{instance} actually starts a proof, namely that
\isa{bool} satisfies all axioms of \isa{ordrel}.
There are none, but we still need to finish that proof, which we do
-by invoking a fixed predefined method:%
+by invoking the \methdx{intro_classes} method:%
\end{isamarkuptxt}%
\isacommand{by}\ intro{\isacharunderscore}classes%
\begin{isamarkuptext}%
@@ -56,13 +56,14 @@
less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable%
+Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-whereas \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. In order to make it well-typed
+At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed.
+To make it well-typed,
we need to make lists a type of class \isa{ordrel}:%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Thu Aug 09 18:12:15 2001 +0200
@@ -16,7 +16,13 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.%
+The infix function \isa{{\isacharbang}} yields the nth element of a list.
+
+\begin{warn}
+A type constructor can be instantiated in only one way to
+a given type class. For example, our two instantiations of \isa{list} must
+reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+\end{warn}%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Predefined Overloading%
@@ -26,7 +32,7 @@
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
-\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
+$-$ and \isa{{\isasymle}} on sets.
In addition there is a special input syntax for bounded quantifiers:
\begin{center}
--- a/doc-src/TutorialI/Types/document/Pairs.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Thu Aug 09 18:12:15 2001 +0200
@@ -10,8 +10,8 @@
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
repertoire of operations: pairing and the two projections \isa{fst} and
\isa{snd}. In any non-trivial application of pairs you will find that this
-quickly leads to unreadable formulae involving nests of projections. This
-section is concerned with introducing some syntactic sugar to overcome this
+quickly leads to unreadable nests of projections. This
+section introduces syntactic sugar to overcome this
problem: pattern matching with tuples.%
\end{isamarkuptext}%
%
@@ -38,12 +38,11 @@
internal representation. Thus the internal and external form of a term may
differ, which can affect proofs. If you want to avoid this complication,
stick to \isa{fst} and \isa{snd} and write \isa{{\isasymlambda}p{\isachardot}\ fst\ p\ {\isacharplus}\ snd\ p}
-instead of \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharplus}y} (which denote the same function but are quite
-different terms).
+instead of \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharplus}y}. These terms are distinct even though they
+denote the same function.
Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
-\isa{split}\indexbold{*split (constant)}
-is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
+\cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
\begin{center}
\isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
\hfill(\isa{split{\isacharunderscore}def})
@@ -68,15 +67,16 @@
approach is neither elegant nor very practical in large examples, although it
can be effective in small ones.
-If we step back and ponder why the above lemma presented a problem in the
-first place, we quickly realize that what we would like is to replace \isa{p} with some concrete pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}, in which case both sides of the
-equation would simplify to \isa{a} because of the simplification rules
-\isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. This is the
-key problem one faces when reasoning about pattern matching with pairs: how to
-convert some atomic term into a pair.
+If we consider why this lemma presents a problem,
+we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the
+equation would simplify to \isa{a} by the simplification rules
+\isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.
+To reason about tuple patterns requires some way of
+converting a variable of product type into a pair.
In case of a subterm of the form \isa{split\ f\ p} this is easy: the split
rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:%
+\index{*split (method)}%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}%
@@ -142,7 +142,7 @@
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ swap\ {\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p%
\end{isabelle}
-Again, \isa{case{\isacharunderscore}tac} is applicable because \isa{{\isasymtimes}} is a datatype.
+Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype.
The subgoal is easily proved by \isa{simp}.
Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus
@@ -167,25 +167,25 @@
\begin{isamarkuptext}%
\noindent
Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all}
-in the first simplification step. This time the reason was not merely
+in the first simplification step, and then we simplify again.
+This time the reason was not merely
pedagogical:
-\isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with certain congruence
-rules of the simplifier, i.e.%
+\isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with other functions
+of the simplifier.
+The following command could fail (here it does not)
+where two separate \isa{simp} applications succeed.%
\end{isamarkuptext}%
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-may fail (here it does not) where the above two stages succeed.
-
-Finally, all \isa{{\isasymforall}} and \isa{{\isasymexists}}-quantified variables are split
-automatically by the simplifier:%
+Finally, the simplifier automatically splits all \isa{{\isasymforall}} and
+\isa{{\isasymexists}}-quantified variables:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline
-\isacommand{apply}\ simp\isanewline
-\isacommand{done}%
+\isacommand{by}\ simp%
\begin{isamarkuptext}%
\noindent
-In case you would like to turn off this automatic splitting, just disable the
+To turn off this automatic splitting, just disable the
responsible simplification rules:
\begin{center}
\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
--- a/doc-src/TutorialI/Types/document/Typedef.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Thu Aug 09 18:12:15 2001 +0200
@@ -9,8 +9,8 @@
\label{sec:adv-typedef}
For most applications, a combination of predefined types like \isa{bool} and
\isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very
-occasionally you may feel the need for a more advanced type. If you cannot do
-without that type, and you are certain that it is not definable by any of the
+occasionally you may feel the need for a more advanced type. If you
+are certain that your type is not definable by any of the
standard means, then read on.
\begin{warn}
Types in HOL must be non-empty; otherwise the quantifier rules would be
@@ -165,35 +165,24 @@
we merely need to prove that \isa{A}, \isa{B} and \isa{C} are distinct
and that they exhaust the type.
-We start with a helpful version of injectivity of \isa{Abs{\isacharunderscore}three} on the
-representing subset:%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
-\ {\isachardoublequote}{\isasymlbrakk}\ x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharequal}y{\isacharparenright}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-We prove each direction separately. From \isa{Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y}
-we use \isa{arg{\isacharunderscore}cong} to apply \isa{Rep{\isacharunderscore}three} to both sides,
-deriving \begin{isabelle}%
-Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
-\end{isabelle}
-Thus we get the required \isa{x\ {\isacharequal}\ y} by simplification with \isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse}.
-The other direction
-is trivial by simplification:%
-\end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Rep{\isacharunderscore}three\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Abs{\isacharunderscore}three{\isacharunderscore}inverse{\isacharparenright}\isanewline
-\isacommand{by}\ simp%
-\begin{isamarkuptext}%
-\noindent
-Analogous lemmas can be proved in the same way for arbitrary type definitions.
-
+In processing our \isacommand{typedef} declaration,
+Isabelle helpfully proves several lemmas.
+One, \isa{Abs{\isacharunderscore}three{\isacharunderscore}inject},
+expresses that \isa{Abs{\isacharunderscore}three} is injective on the representing subset:
+\begin{center}
+\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
+\end{center}
+Another, \isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}, expresses that the representation
+function is also injective:
+\begin{center}
+\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
+\end{center}
Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
-if we expand their definitions and rewrite with the above simplification rule:%
+if we expand their definitions and rewrite with the injectivity
+of \isa{Abs{\isacharunderscore}three}:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
@@ -220,7 +209,8 @@
\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
-Now the case distinction lemma on type \isa{three} is easy to derive if you know how to:%
+Now the case distinction lemma on type \isa{three} is easy to derive if you
+know how:%
\end{isamarkuptext}%
\isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}%
\begin{isamarkuptxt}%
--- a/doc-src/TutorialI/Types/numerics.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
\section{Numbers}
\label{sec:numbers}
+\index{numbers|(}%
Until now, our numerical examples have used the type of \textbf{natural
numbers},
\isa{nat}. This is a recursive datatype generated by the constructors
@@ -45,7 +46,7 @@
They begin
with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and
then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3}
-and \isa{\#441223334678}.
+and \isa{\#441223334678}.\REMARK{will need updating?}
Literals look like constants, but they abbreviate
terms, representing the number in a two's complement binary notation.
@@ -110,7 +111,7 @@
in a variety of additive types. The symbols \sdx{1} and \sdx{2} are
not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2} are
-syntactically different from \isa{0}, \isa{1} and \isa{2}. You will
+syntactically different from \isa{0}, \isa{1} and \isa{2}. You will\REMARK{will need updating?}
sometimes prefer one notation to the other. Literals are obviously
necessary to express large values, while \isa{0} and \isa{Suc} are needed
in order to match many theorems, including the rewrite rules for primitive
@@ -224,7 +225,7 @@
d))
\rulename{nat_diff_split}
\end{isabelle}
-For example, it proves the following fact, which lies outside the scope of
+For example, this splitting proves the following fact, which lies outside the scope of
linear arithmetic:\REMARK{replace by new example!}
\begin{isabelle}
\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
@@ -245,8 +246,10 @@
+\ z)
\rulename{add_left_commute}
\end{isabelle}
-The name \isa{add_ac} refers to the list of all three theorems, similarly
-there is \isa{mult_ac}. Here is an example of the sorting effect. Start
+The name \isa{add_ac}\index{*add_ac (theorems)}
+refers to the list of all three theorems; similarly
+there is \isa{mult_ac}.\index{*mult_ac (theorems)}
+Here is an example of the sorting effect. Start
with this goal:
\begin{isabelle}
\ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
@@ -297,9 +300,11 @@
Concerning simplifier tricks, we have no need to eliminate subtraction: it
is well-behaved. As with the natural numbers, the simplifier can sort the
-operands of sums and products. The name \isa{zadd_ac} refers to the
+operands of sums and products. The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
+refers to the
associativity and commutativity theorems for integer addition, while
-\isa{zmult_ac} has the analogous theorems for multiplication. The
+\isa{zmult_ac}\index{*zmult_ac (theorems)}
+has the analogous theorems for multiplication. The
prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
denote the set of integers.
@@ -450,4 +455,5 @@
about limits, differentiation and integration~\cite{fleuriot-jcm}. The
development defines an infinitely large number, \isa{omega} and an
infinitely small positive number, \isa{epsilon}. The
-relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.
+relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.%
+\index{numbers|)}
\ No newline at end of file
--- a/doc-src/TutorialI/Types/types.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/types.tex Thu Aug 09 18:12:15 2001 +0200
@@ -18,7 +18,8 @@
The material in this section goes beyond the needs of most novices. Serious
users should at least skim the sections on basic types and on type classes.
-The latter is fairly advanced: read the beginning to understand what it is
+The latter material is fairly advanced; read the beginning to understand what
+it is
about, but consult the rest only when necessary.
\input{Types/numerics}
@@ -44,8 +45,9 @@
an axiomatic specification of a class of types. Thus we can talk about a type
$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if
$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $D$ being a
-\textbf{subclass} of a class $C$, written $D < C$. This is the case if all
+organized in a hierarchy. Thus there is the notion of a class $D$ being a
+\textbf{subclass}\index{subclasses}
+of a class $C$, written $D < C$. This is the case if all
axioms of $C$ are also provable in $D$. We introduce these concepts
by means of a running example, ordering relations.
--- a/doc-src/TutorialI/tutorial.ind Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/tutorial.ind Thu Aug 09 18:12:15 2001 +0200
@@ -49,6 +49,7 @@
\item \texttt {abs}, \bold{189}
\item absolute value, 135
\item \isa {add} (modifier), 27
+ \item \isa {add_ac} (theorems), 134
\item \isa {add_assoc} (theorem), \bold{134}
\item \isa {add_commute} (theorem), \bold{134}
\item \isa {add_mult_distrib} (theorem), \bold{133}
@@ -133,13 +134,12 @@
\item converse
\subitem of a relation, \bold{96}
\item \isa {converse_iff} (theorem), \bold{96}
- \item CTL, 100--110
\indexspace
\item \isacommand {datatype} (command), 7, 36--41
\item datatypes, 15--20
- \subitem and nested recursion, 38
+ \subitem and nested recursion, 38, 42
\subitem mutually recursive, 36
\item \isacommand {defer} (command), 14, 84
\item Definitional Approach, 24
@@ -204,7 +204,7 @@
\indexspace
\item \isa {False} (constant), 3
- \item \isa {fast} (method), 76
+ \item \isa {fast} (method), 76, 108
\item Fibonacci function, 44
\item \isa {finite} (symbol), 93
\item \isa {Finites} (constant), 93
@@ -229,6 +229,8 @@
\item generalizing induction formulae, 32
\item Girard, Jean-Yves, \fnote{55}
\item Gordon, Mike, 1
+ \item grammars
+ \subitem defining inductively, 124--129
\item ground terms example, 119--124
\indexspace
@@ -237,6 +239,7 @@
\item higher-order pattern, \bold{159}
\item Hilbert's $\varepsilon$-operator, 70
\item HOLCF, 41
+ \item Hopcroft, J. E., 129
\item \isa {hypreal} (type), 137
\indexspace
@@ -249,7 +252,7 @@
\item identity relation, \bold{96}
\item \isa {if} expressions, 3, 4
\subitem simplification of, 31
- \subitem splitting of, 29
+ \subitem splitting of, 29, 47
\item if-and-only-if, 3
\item \isa {iff} (attribute), 74, 86, 114
\item \isa {iffD1} (theorem), \bold{78}
@@ -261,6 +264,7 @@
\item \isa {Image_iff} (theorem), \bold{96}
\item \isa {impI} (theorem), \bold{56}
\item implication, 56--57
+ \item \isa {ind_cases} (method), 115
\item \isa {induct_tac} (method), 10, 17, 50, 172
\item induction, 168--175
\subitem recursion, 49--50
@@ -339,7 +343,7 @@
\item \isa {Main} (theory), 2
\item major premise, \bold{59}
\item \isa {max} (constant), 21, 22
- \item measure function, \bold{45}, \bold{98}
+ \item measure functions, 45, 98
\item \isa {measure_def} (theorem), \bold{99}
\item meta-logic, \bold{64}
\item methods, \bold{14}
@@ -347,12 +351,14 @@
\item \isa {mod} (symbol), 21
\item \isa {mod_div_equality} (theorem), \bold{133}
\item \isa {mod_mult_distrib} (theorem), \bold{133}
+ \item model checking example, 100--110
\item \emph{modus ponens}, 51, 56
\item \isa {mono_def} (theorem), \bold{100}
\item monotone functions, \bold{100}, 123
\subitem and inductive definitions, 121--122
\item \isa {more} (constant), 140--142
\item \isa {mp} (theorem), \bold{56}
+ \item \isa {mult_ac} (theorems), 134
\item multiset ordering, \bold{99}
\indexspace
@@ -370,6 +376,7 @@
\item \isa {None} (constant), \bold{22}
\item \isa {notE} (theorem), \bold{57}
\item \isa {notI} (theorem), \bold{57}
+ \item numbers, 131--137
\item numeric literals, 132
\subitem for type \protect\isa{nat}, 133
\subitem for type \protect\isa{real}, 136
@@ -393,8 +400,10 @@
\item pairs and tuples, 22, 137--140
\item parent theories, \bold{2}
\item partial function, 164
+ \item pattern matching
+ \subitem and \isacommand{recdef}, 45
\item pattern, higher-order, \bold{159}
- \item PDL, 102--105
+ \item PDL, 102--104
\item permutative rewrite rule, \bold{158}
\item \isacommand {pr} (command), 14, 84
\item \isacommand {prefer} (command), 14, 84
@@ -445,6 +454,8 @@
\item recursion induction, 49--50
\item \isacommand {redo} (command), 14
\item reflexive and transitive closure, 96--98
+ \item reflexive transitive closure
+ \subitem defining inductively, 116--119
\item relations, 95--98
\subitem well-founded, 98--99
\item \isa {rename_tac} (method), 66--67
@@ -500,15 +511,15 @@
\item sorts, 150
\item \isa {spec} (theorem), \bold{64}
\item \isa {split} (attribute), 30
- \item \isa {split} (constant), \bold{137}
- \item \isa {split} (method), 29
- \item \isa {split} (method, attr.), 29--31
- \item \isa {split} (modified), 30
+ \item \isa {split} (constant), 137
+ \item \isa {split} (method), 29, 138
+ \item \isa {split} (modifier), 30
\item split rule, \bold{30}
\item \isa {split_if} (theorem), 30
\item \isa {split_if_asm} (theorem), 30
\item \isa {ssubst} (theorem), \bold{61}
\item structural induction, \see{induction, structural}{1}
+ \item subgoal numbering, 44
\item \isa {subgoal_tac} (method), 82
\item subgoals, 10
\item subset relation, \bold{90}
@@ -545,6 +556,7 @@
\item \isa {trace_simp} (flag), 31
\item tracing the simplifier, \bold{31}
\item \isa {trancl_trans} (theorem), \bold{97}
+ \item transition systems, 101
\item \isacommand {translations} (command), 24
\item tries, 41--44
\item \isa {True} (constant), 3
@@ -555,7 +567,7 @@
\item type inference, \bold{3}
\item type synonyms, 23
\item type variables, 3
- \item \isacommand {typedecl} (command), 150
+ \item \isacommand {typedecl} (command), 101, 150
\item \isacommand {typedef} (command), 151--155
\item types, 2--3
\subitem declaring, 150--151
@@ -564,6 +576,7 @@
\indexspace
+ \item Ullman, J. D., 129
\item \texttt {UN}, \bold{189}
\item \texttt {Un}, \bold{189}
\item \isa {UN_E} (theorem), \bold{92}
@@ -593,7 +606,16 @@
\item Wenzel, Markus, v
\item \isa {wf_induct} (theorem), \bold{99}
+ \item \isa {wf_inv_image} (theorem), \bold{99}
+ \item \isa {wf_less_than} (theorem), \bold{98}
+ \item \isa {wf_lex_prod} (theorem), \bold{99}
+ \item \isa {wf_measure} (theorem), \bold{99}
\item \isa {while} (constant), 167
\item \isa {While_Combinator} (theory), 167
+ \indexspace
+
+ \item \isa {zadd_ac} (theorems), 135
+ \item \isa {zmult_ac} (theorems), 135
+
\end{theindex}