--- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri Aug 03 18:04:55 2001 +0200
@@ -58,7 +58,7 @@
congruence rule for \isa{if}. Analogous rules control the evaluation of
\isa{case} expressions.
-You can declare your own congruence rules with the attribute \isa{cong},
+You can declare your own congruence rules with the attribute \attrdx{cong},
either globally, in the usual manner,
\begin{quote}
\isacommand{declare} \textit{theorem-name} \isa{{\isacharbrackleft}cong{\isacharbrackright}}
--- a/doc-src/TutorialI/Advanced/simp.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy Fri Aug 03 18:04:55 2001 +0200
@@ -45,7 +45,7 @@
congruence rule for @{text if}. Analogous rules control the evaluation of
@{text case} expressions.
-You can declare your own congruence rules with the attribute @{text cong},
+You can declare your own congruence rules with the attribute \attrdx{cong},
either globally, in the usual manner,
\begin{quote}
\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
--- a/doc-src/TutorialI/CTL/Base.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy Fri Aug 03 18:04:55 2001 +0200
@@ -10,7 +10,7 @@
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
-logic (PDL), which we then extend to the temporal logic CTL, which is
+logic (PDL)\@. We then proceed to the temporal logic CTL, which is
used in many real
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
recursive function @{term mc} that maps a formula into the set of all states of
@@ -21,8 +21,9 @@
\underscoreon
-Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
-transitions between them, as shown in this simple example:
+Our models are \emph{transition systems}:\index{transition systems}
+sets of \emph{states} with
+transitions between them. Here is a simple example:
\begin{center}
\unitlength.5mm
\thicklines
@@ -45,21 +46,20 @@
\put(91,21){\makebox(0,0)[bl]{$s_2$}}
\end{picture}
\end{center}
-Each state has a unique name or number ($s_0,s_1,s_2$), and in each
-state certain \emph{atomic propositions} ($p,q,r$) are true.
-The aim of temporal logic is to formalize statements such as ``there is no
-path starting from $s_2$ leading to a state where $p$ or $q$
-are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
-which is false.
+Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
+certain \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic
+is to formalize statements such as ``there is no path starting from $s_2$
+leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
+starting from $s_0$, $q$ always holds,'' which is false.
-Abstracting from this concrete example, we assume there is some type of
+Abstracting from this concrete example, we assume there is a type of
states:
*}
typedecl state
text{*\noindent
-Command \isacommand{typedecl} merely declares a new type but without
+Command \commdx{typedecl} merely declares a new type but without
defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because @{typ state} really is an implicit parameter of our model. Of
--- a/doc-src/TutorialI/CTL/PDL.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Fri Aug 03 18:04:55 2001 +0200
@@ -3,12 +3,13 @@
subsection{*Propositional Dynamic Logic --- PDL*}
text{*\index{PDL|(}
-The formulae of PDL\footnote{The customary definition of PDL
+The formulae of PDL are built up from atomic propositions via
+negation and conjunction and the two temporal
+connectives @{text AX} and @{text EF}\@. Since formulae are essentially
+syntax trees, they are naturally modelled as a datatype:%
+\footnote{The customary definition of PDL
\cite{HarelKT-DL} looks quite different from ours, but the two are easily
-shown to be equivalent.} are built up from atomic propositions via
-negation and conjunction and the two temporal
-connectives @{text AX} and @{text EF}. Since formulae are essentially
-syntax trees, they are naturally modelled as a datatype:
+shown to be equivalent.}
*}
datatype formula = Atom atom
@@ -18,11 +19,10 @@
| EF formula
text{*\noindent
-This is almost the same as in the boolean expression case study in
+This resembles the boolean expression case study in
\S\ref{sec:boolex}.
-
-The meaning of these formulae is given by saying which formula is true in
-which state:
+A validity relation between
+states and formulae specifies the semantics:
*}
consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
@@ -30,8 +30,6 @@
text{*\noindent
The syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of
\hbox{@{text"valid s f"}}.
-
-\smallskip
The definition of @{text"\<Turnstile>"} is by recursion over the syntax:
*}
@@ -50,8 +48,7 @@
closure. Because of reflexivity, the future includes the present.
Now we come to the model checker itself. It maps a formula into the set of
-states where the formula is true and is defined by recursion over the syntax,
-too:
+states where the formula is true. It too is defined by recursion over the syntax:
*}
consts mc :: "formula \<Rightarrow> state set";
@@ -111,13 +108,14 @@
(*pr(latex xsymbols symbols);*)
txt{*\noindent
Having disposed of the monotonicity subgoal,
-simplification leaves us with the following main goal
+simplification leaves us with the following goal:
\begin{isabelle}
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
\end{isabelle}
-which is proved by @{text blast} with the help of transitivity of @{text"\<^sup>*"}:
+It is proved by @{text blast}, using the transitivity of
+\isa{M\isactrlsup {\isacharasterisk}}.
*}
apply(blast intro: rtrancl_trans);
@@ -135,7 +133,7 @@
@{subgoals[display,indent=0,goals_limit=1]}
This goal is proved by induction on @{term"(s,t)\<in>M\<^sup>*"}. But since the model
checker works backwards (from @{term t} to @{term s}), we cannot use the
-induction theorem @{thm[source]rtrancl_induct} because it works in the
+induction theorem @{thm[source]rtrancl_induct}: it works in the
forward direction. Fortunately the converse induction theorem
@{thm[source]converse_rtrancl_induct} already exists:
@{thm[display,margin=60]converse_rtrancl_induct[no_vars]}
@@ -181,9 +179,11 @@
text{*
\begin{exercise}
-@{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
-as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
-(``there exists a next state such that'') with the intended semantics
+@{term AX} has a dual operator @{term EN}
+(``there exists a next state such that'')%
+\footnote{We cannot use the customary @{text EX}: it is reserved
+as the \textsc{ascii}-equivalent of @{text"\<exists>"}.}
+with the intended semantics
@{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
--- a/doc-src/TutorialI/CTL/ctl.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/ctl.tex Fri Aug 03 18:04:55 2001 +0200
@@ -1,6 +1,6 @@
-\index{CTL|(}
+\index{model checking example|(}%
\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
\input{CTL/document/Base.tex}
\input{CTL/document/PDL.tex}
\input{CTL/document/CTL.tex}
-\index{CTL|)}
+\index{model checking example|)}
--- a/doc-src/TutorialI/CTL/document/Base.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Aug 03 18:04:55 2001 +0200
@@ -14,7 +14,7 @@
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
-logic (PDL), which we then extend to the temporal logic CTL, which is
+logic (PDL)\@. We then proceed to the temporal logic CTL, which is
used in many real
model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a
recursive function \isa{mc} that maps a formula into the set of all states of
@@ -25,8 +25,9 @@
\underscoreon
-Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
-transitions between them, as shown in this simple example:
+Our models are \emph{transition systems}:\index{transition systems}
+sets of \emph{states} with
+transitions between them. Here is a simple example:
\begin{center}
\unitlength.5mm
\thicklines
@@ -49,20 +50,19 @@
\put(91,21){\makebox(0,0)[bl]{$s_2$}}
\end{picture}
\end{center}
-Each state has a unique name or number ($s_0,s_1,s_2$), and in each
-state certain \emph{atomic propositions} ($p,q,r$) are true.
-The aim of temporal logic is to formalize statements such as ``there is no
-path starting from $s_2$ leading to a state where $p$ or $q$
-are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
-which is false.
+Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
+certain \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic
+is to formalize statements such as ``there is no path starting from $s_2$
+leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
+starting from $s_0$, $q$ always holds,'' which is false.
-Abstracting from this concrete example, we assume there is some type of
+Abstracting from this concrete example, we assume there is a type of
states:%
\end{isamarkuptext}%
\isacommand{typedecl}\ state%
\begin{isamarkuptext}%
\noindent
-Command \isacommand{typedecl} merely declares a new type but without
+Command \commdx{typedecl} merely declares a new type but without
defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because \isa{state} really is an implicit parameter of our model. Of
--- a/doc-src/TutorialI/CTL/document/PDL.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Aug 03 18:04:55 2001 +0200
@@ -7,12 +7,13 @@
%
\begin{isamarkuptext}%
\index{PDL|(}
-The formulae of PDL\footnote{The customary definition of PDL
+The formulae of PDL are built up from atomic propositions via
+negation and conjunction and the two temporal
+connectives \isa{AX} and \isa{EF}\@. Since formulae are essentially
+syntax trees, they are naturally modelled as a datatype:%
+\footnote{The customary definition of PDL
\cite{HarelKT-DL} looks quite different from ours, but the two are easily
-shown to be equivalent.} are built up from atomic propositions via
-negation and conjunction and the two temporal
-connectives \isa{AX} and \isa{EF}. Since formulae are essentially
-syntax trees, they are naturally modelled as a datatype:%
+shown to be equivalent.}%
\end{isamarkuptext}%
\isacommand{datatype}\ formula\ {\isacharequal}\ Atom\ atom\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ formula\isanewline
@@ -21,19 +22,16 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ EF\ formula%
\begin{isamarkuptext}%
\noindent
-This is almost the same as in the boolean expression case study in
+This resembles the boolean expression case study in
\S\ref{sec:boolex}.
-
-The meaning of these formulae is given by saying which formula is true in
-which state:%
+A validity relation between
+states and formulae specifies the semantics:%
\end{isamarkuptext}%
\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ formula\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharparenleft}{\isacharunderscore}\ {\isasymTurnstile}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{8}}{\isadigit{0}}{\isacharcomma}{\isadigit{8}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{8}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
The syntax annotation allows us to write \isa{s\ {\isasymTurnstile}\ f} instead of
\hbox{\isa{valid\ s\ f}}.
-
-\smallskip
The definition of \isa{{\isasymTurnstile}} is by recursion over the syntax:%
\end{isamarkuptext}%
\isacommand{primrec}\isanewline
@@ -51,8 +49,7 @@
closure. Because of reflexivity, the future includes the present.
Now we come to the model checker itself. It maps a formula into the set of
-states where the formula is true and is defined by recursion over the syntax,
-too:%
+states where the formula is true. It too is defined by recursion over the syntax:%
\end{isamarkuptext}%
\isacommand{consts}\ mc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}formula\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
@@ -109,13 +106,14 @@
\begin{isamarkuptxt}%
\noindent
Having disposed of the monotonicity subgoal,
-simplification leaves us with the following main goal
+simplification leaves us with the following goal:
\begin{isabelle}
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
\end{isabelle}
-which is proved by \isa{blast} with the help of transitivity of \isa{\isactrlsup {\isacharasterisk}}:%
+It is proved by \isa{blast}, using the transitivity of
+\isa{M\isactrlsup {\isacharasterisk}}.%
\end{isamarkuptxt}%
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -132,7 +130,7 @@
\end{isabelle}
This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
checker works backwards (from \isa{t} to \isa{s}), we cannot use the
-induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the
+induction theorem \isa{rtrancl{\isacharunderscore}induct}: it works in the
forward direction. Fortunately the converse induction theorem
\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
\begin{isabelle}%
@@ -178,9 +176,11 @@
\isacommand{done}%
\begin{isamarkuptext}%
\begin{exercise}
-\isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
-as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}}
-(``there exists a next state such that'') with the intended semantics
+\isa{AX} has a dual operator \isa{EN}
+(``there exists a next state such that'')%
+\footnote{We cannot use the customary \isa{EX}: it is reserved
+as the \textsc{ascii}-equivalent of \isa{{\isasymexists}}.}
+with the intended semantics
\begin{isabelle}%
\ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
\end{isabelle}
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Aug 03 18:04:55 2001 +0200
@@ -5,6 +5,7 @@
section{*Case Study: Compiling Expressions*}
text{*\label{sec:ExprCompiler}
+\index{compiling expressions example|(}%
The task is to develop a compiler from a generic type of expressions (built
from variables, constants and binary operations) to a stack machine. This
generic type of expressions is a generalization of the boolean expressions in
@@ -64,7 +65,7 @@
text{*\noindent
Recall that @{term"hd"} and @{term"tl"}
return the first element and the remainder of a list.
-Because all functions are total, @{term"hd"} is defined even for the empty
+Because all functions are total, \cdx{hd} is defined even for the empty
list, although we do not know what the result is. Thus our model of the
machine always terminates properly, although the definition above does not
tell us much about the result in situations where @{term"Apply"} was executed
@@ -87,14 +88,14 @@
theorem "exec (comp e) s [] = [value e s]";
(*<*)oops;(*>*)
text{*\noindent
-This theorem needs to be generalized to
+This theorem needs to be generalized:
*}
theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
txt{*\noindent
-which is proved by induction on @{term"e"} followed by simplification, once
-we have the following lemma about executing the concatenation of two
+It will be proved by induction on @{term"e"} followed by simplification.
+First, we must prove a lemma about executing the concatenation of two
instruction sequences:
*}
(*<*)oops;(*>*)
@@ -105,7 +106,7 @@
This requires induction on @{term"xs"} and ordinary simplification for the
base cases. In the induction step, simplification leaves us with a formula
that contains two @{text"case"}-expressions over instructions. Thus we add
-automatic case splitting as well, which finishes the proof:
+automatic case splitting, which finishes the proof:
*}
apply(induct_tac xs, simp, simp split: instr.split);
(*<*)done(*>*)
@@ -126,7 +127,8 @@
We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
merely by simplification with the generalized version we just proved.
However, this is unnecessary because the generalized version fully subsumes
-its instance.
+its instance.%
+\index{compiling expressions example|)}
*}
(*<*)
theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Aug 03 18:04:55 2001 +0200
@@ -7,6 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:ExprCompiler}
+\index{compiling expressions example|(}%
The task is to develop a compiler from a generic type of expressions (built
from variables, constants and binary operations) to a stack machine. This
generic type of expressions is a generalization of the boolean expressions in
@@ -60,7 +61,7 @@
\noindent
Recall that \isa{hd} and \isa{tl}
return the first element and the remainder of a list.
-Because all functions are total, \isa{hd} is defined even for the empty
+Because all functions are total, \cdx{hd} is defined even for the empty
list, although we do not know what the result is. Thus our model of the
machine always terminates properly, although the definition above does not
tell us much about the result in situations where \isa{Apply} was executed
@@ -81,13 +82,13 @@
\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-This theorem needs to be generalized to%
+This theorem needs to be generalized:%
\end{isamarkuptext}%
\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-which is proved by induction on \isa{e} followed by simplification, once
-we have the following lemma about executing the concatenation of two
+It will be proved by induction on \isa{e} followed by simplification.
+First, we must prove a lemma about executing the concatenation of two
instruction sequences:%
\end{isamarkuptxt}%
\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
@@ -97,7 +98,7 @@
This requires induction on \isa{xs} and ordinary simplification for the
base cases. In the induction step, simplification leaves us with a formula
that contains two \isa{case}-expressions over instructions. Thus we add
-automatic case splitting as well, which finishes the proof:%
+automatic case splitting, which finishes the proof:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
@@ -115,6 +116,7 @@
merely by simplification with the generalized version we just proved.
However, this is unnecessary because the generalized version fully subsumes
its instance.%
+\index{compiling expressions example|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/ABexpr.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy Fri Aug 03 18:04:55 2001 +0200
@@ -3,12 +3,13 @@
(*>*)
text{*
+\index{datatypes!mutually recursive}%
Sometimes it is necessary to define two datatypes that depend on each
other. This is called \textbf{mutual recursion}. As an example consider a
language of arithmetic and boolean expressions where
\begin{itemize}
\item arithmetic expressions contain boolean expressions because there are
- conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
+ conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'',
and
\item boolean expressions contain arithmetic expressions because of
comparisons like ``$m<n$''.
@@ -31,14 +32,14 @@
fixed the values to be of type @{typ"nat"} and declared the two binary
operations @{text Sum} and @{term"Diff"}. Boolean
expressions can be arithmetic comparisons, conjunctions and negations.
-The semantics is fixed via two evaluation functions
+The semantics is given by two evaluation functions:
*}
consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool";
text{*\noindent
-that take an expression and an environment (a mapping from variables @{typ"'a"} to values
+Both take an expression and an environment (a mapping from variables @{typ"'a"} to values
@{typ"nat"}) and return its arithmetic/boolean
value. Since the datatypes are mutually recursive, so are functions that
operate on them. Hence they need to be defined in a single \isacommand{primrec}
@@ -117,13 +118,14 @@
\begin{exercise}
Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that
replaces @{term"IF"}s with complex boolean conditions by nested
- @{term"IF"}s where each condition is a @{term"Less"} --- @{term"And"} and
- @{term"Neg"} should be eliminated completely. Prove that @{text"norma"}
+ @{term"IF"}s; it should eliminate the constructors
+ @{term"And"} and @{term"Neg"}, leaving only @{term"Less"}.
+ Prove that @{text"norma"}
preserves the value of an expression and that the result of @{text"norma"}
is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
\end{exercise}
*}
-(*<*)
+(*<*)
end
(*>*)
--- a/doc-src/TutorialI/Datatype/Fundata.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy Fri Aug 03 18:04:55 2001 +0200
@@ -26,11 +26,11 @@
text{*\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of @{term"map_bt"} involve only subtrees obtained from
-@{term"F"}, i.e.\ the left-hand side. Thus termination is assured. The
-seasoned functional programmer might have written @{term"map_bt f o F"}
-instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by
-Isabelle because the termination proof is not as obvious since
-@{term"map_bt"} is only partially applied.
+@{term"F"}: the left-hand side. Thus termination is assured. The
+seasoned functional programmer might try expressing
+@{term"%i. map_bt f (F i)"} as @{term"map_bt f o F"}, which Isabelle
+however will reject. Applying @{term"map_bt"} to only one of its arguments
+makes the termination proof less obvious.
The following lemma has a simple proof by induction: *}
@@ -40,8 +40,8 @@
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
apply(induct_tac T, rename_tac[2] F)(*>*)
txt{*\noindent
-It is worth taking a look at the proof state after the induction step
-to understand what the presence of the function type entails.
+Because of the function type, the
+the proof state after induction looks unusual.
Notice the quantified induction hypothesis:
@{subgoals[display,indent=0]}
*}
--- a/doc-src/TutorialI/Datatype/Nested.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Aug 03 18:04:55 2001 +0200
@@ -3,8 +3,9 @@
(*>*)
text{*
+\index{datatypes!and nested recursion}%
So far, all datatypes had the property that on the right-hand side of their
-definition they occurred only at the top-level, i.e.\ directly below a
+definition they occurred only at the top-level: directly below a
constructor. Now we consider \emph{nested recursion}, where the recursive
datatype occurs nested in some other datatype (but not inside itself!).
Consider the following model of terms
@@ -55,7 +56,8 @@
"substs s (t # ts) = subst s t # substs s ts";
text{*\noindent
-Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.
+Individual equations in a \commdx{primrec} definition may be
+named as shown for @{thm[source]subst_App}.
The significance of this device will become apparent below.
Similarly, when proving a statement about terms inductively, we need
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Aug 03 18:04:55 2001 +0200
@@ -3,12 +3,13 @@
\def\isabellecontext{ABexpr}%
%
\begin{isamarkuptext}%
+\index{datatypes!mutually recursive}%
Sometimes it is necessary to define two datatypes that depend on each
other. This is called \textbf{mutual recursion}. As an example consider a
language of arithmetic and boolean expressions where
\begin{itemize}
\item arithmetic expressions contain boolean expressions because there are
- conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
+ conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'',
and
\item boolean expressions contain arithmetic expressions because of
comparisons like ``$m<n$''.
@@ -30,13 +31,13 @@
fixed the values to be of type \isa{nat} and declared the two binary
operations \isa{Sum} and \isa{Diff}. Boolean
expressions can be arithmetic comparisons, conjunctions and negations.
-The semantics is fixed via two evaluation functions%
+The semantics is given by two evaluation functions:%
\end{isamarkuptext}%
\isacommand{consts}\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-that take an expression and an environment (a mapping from variables \isa{{\isacharprime}a} to values
+Both take an expression and an environment (a mapping from variables \isa{{\isacharprime}a} to values
\isa{nat}) and return its arithmetic/boolean
value. Since the datatypes are mutually recursive, so are functions that
operate on them. Hence they need to be defined in a single \isacommand{primrec}
@@ -107,8 +108,9 @@
\begin{exercise}
Define a function \isa{norma} of type \isa{{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}a\ aexp} that
replaces \isa{IF}s with complex boolean conditions by nested
- \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
- \isa{Neg} should be eliminated completely. Prove that \isa{norma}
+ \isa{IF}s; it should eliminate the constructors
+ \isa{And} and \isa{Neg}, leaving only \isa{Less}.
+ Prove that \isa{norma}
preserves the value of an expression and that the result of \isa{norma}
is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Aug 03 18:04:55 2001 +0200
@@ -27,11 +27,11 @@
\begin{isamarkuptext}%
\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from
-\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
-seasoned functional programmer might have written \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}
-instead of \isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}}, but the former is not accepted by
-Isabelle because the termination proof is not as obvious since
-\isa{map{\isacharunderscore}bt} is only partially applied.
+\isa{F}: the left-hand side. Thus termination is assured. The
+seasoned functional programmer might try expressing
+\isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}} as \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}, which Isabelle
+however will reject. Applying \isa{map{\isacharunderscore}bt} to only one of its arguments
+makes the termination proof less obvious.
The following lemma has a simple proof by induction:%
\end{isamarkuptext}%
@@ -40,8 +40,8 @@
\isacommand{done}%
\begin{isamarkuptxt}%
\noindent
-It is worth taking a look at the proof state after the induction step
-to understand what the presence of the function type entails.
+Because of the function type, the
+the proof state after induction looks unusual.
Notice the quantified induction hypothesis:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri Aug 03 18:04:55 2001 +0200
@@ -3,8 +3,9 @@
\def\isabellecontext{Nested}%
%
\begin{isamarkuptext}%
+\index{datatypes!and nested recursion}%
So far, all datatypes had the property that on the right-hand side of their
-definition they occurred only at the top-level, i.e.\ directly below a
+definition they occurred only at the top-level: directly below a
constructor. Now we consider \emph{nested recursion}, where the recursive
datatype occurs nested in some other datatype (but not inside itself!).
Consider the following model of terms
@@ -52,7 +53,8 @@
\ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Individual equations in a primrec definition may be named as shown for \isa{subst{\isacharunderscore}App}.
+Individual equations in a \commdx{primrec} definition may be
+named as shown for \isa{subst{\isacharunderscore}App}.
The significance of this device will become apparent below.
Similarly, when proving a statement about terms inductively, we need
--- a/doc-src/TutorialI/Misc/Itrev.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 03 18:04:55 2001 +0200
@@ -5,6 +5,7 @@
section{*Induction Heuristics*}
text{*\label{sec:InductionHeuristics}
+\index{induction heuristics|(}%
The purpose of this section is to illustrate some simple heuristics for
inductive proofs. The first one we have already mentioned in our initial
example:
@@ -16,23 +17,29 @@
\emph{Do induction on argument number $i$ if the function is defined by
recursion in argument number $i$.}
\end{quote}
-When we look at the proof of @{term[source]"(xs @ ys) @ zs = xs @ (ys @ zs)"}
-in \S\ref{sec:intro-proof} we find (a) @{text"@"} is recursive in
-the first argument, (b) @{term xs} occurs only as the first argument of
-@{text"@"}, and (c) both @{term ys} and @{term zs} occur at least once as
-the second argument of @{text"@"}. Hence it is natural to perform induction
-on @{term xs}.
+When we look at the proof of @{text"(xs@ys) @ zs = xs @ (ys@zs)"}
+in \S\ref{sec:intro-proof} we find
+\begin{itemize}
+\item @{text"@"} is recursive in
+the first argument
+\item @{term xs} occurs only as the first argument of
+@{text"@"}
+\item both @{term ys} and @{term zs} occur at least once as
+the second argument of @{text"@"}
+\end{itemize}
+Hence it is natural to perform induction on~@{term xs}.
The key heuristic, and the main point of this section, is to
-generalize the goal before induction. The reason is simple: if the goal is
+\emph{generalize the goal before induction}.
+The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
step to go through. Let us illustrate the idea with an example.
-Function @{term"rev"} has quadratic worst-case running time
+Function \cdx{rev} has quadratic worst-case running time
because it calls function @{text"@"} for each element of the list and
@{text"@"} is linear in its first argument. A linear time version of
@{term"rev"} reqires an extra argument where the result is accumulated
-gradually, using only @{text"#"}:
+gradually, using only~@{text"#"}:
*}
consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
@@ -41,10 +48,10 @@
"itrev (x#xs) ys = itrev xs (x#ys)";
text{*\noindent
-The behaviour of @{term"itrev"} is simple: it reverses
+The behaviour of \cdx{itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
and returning that second argument when the first one becomes
-empty. Note that @{term"itrev"} is tail-recursive, i.e.\ it can be
+empty. Note that @{term"itrev"} is tail-recursive: it can be
compiled into a loop.
Naturally, we would like to show that @{term"itrev"} does indeed reverse
@@ -60,30 +67,30 @@
apply(induct_tac xs, simp_all);
txt{*\noindent
-Unfortunately, this is not a complete success:
+Unfortunately, this attempt does not prove
+the induction step:
@{subgoals[display,indent=0,margin=70]}
-Just as predicted above, the overall goal, and hence the induction
-hypothesis, is too weak to solve the induction step because of the fixed
-argument, @{term"[]"}. This suggests a heuristic:
-\begin{quote}
+The induction hypothesis is too weak. The fixed
+argument,~@{term"[]"}, prevents it from rewriting the conclusion.
+This example suggests a heuristic:
+\begin{quote}\index{generalizing induction formulae}%
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
-just not true --- the correct generalization is
+just not true. The correct generalization is
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
(*<*)apply(induct_tac xs, simp_all)(*>*)
txt{*\noindent
If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
-@{term"rev xs"}, just as required.
+@{term"rev xs"}, as required.
-In this particular instance it was easy to guess the right generalization,
-but in more complex situations a good deal of creativity is needed. This is
-the main source of complications in inductive proofs.
+In this instance it was easy to guess the right generalization.
+Other situations can require a good deal of creativity.
Although we now have two variables, only @{term"xs"} is suitable for
-induction, and we repeat our above proof attempt. Unfortunately, we are still
+induction, and we repeat our proof attempt. Unfortunately, we are still
not there:
@{subgoals[display,indent=0,goals_limit=1]}
The induction hypothesis is still too weak, but this time it takes no
@@ -105,12 +112,11 @@
\emph{Generalize goals for induction by universally quantifying all free
variables {\em(except the induction variable itself!)}.}
\end{quote}
-This prevents trivial failures like the above and does not change the
-provability of the goal. Because it is not always required, and may even
-complicate matters in some cases, this heuristic is often not
-applied blindly.
-The variables that require generalization are typically those that
-change in recursive calls.
+This prevents trivial failures like the one above and does not affect the
+validity of the goal. However, this heuristic should not be applied blindly.
+It is not always required, and the additional quantifiers can complicate
+matters in some cases, The variables that should be quantified are typically
+those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just
proved: the more complex notion (@{term itrev}) is on the left-hand
@@ -124,12 +130,13 @@
@{term"rev xs @ ys"} is simpler than @{term"itrev xs ys"}. But see what
happens if you try to prove @{prop"rev xs @ ys = itrev xs ys"}!
-In general, if you have tried the above heuristics and still find your
+If you have tried these heuristics and still find your
induction does not go through, and no obvious lemma suggests itself, you may
need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. You
-will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
-to learn about some advanced techniques for inductive proofs.
+the problem at hand and is beyond simple rules of thumb.
+Additionally, you can read \S\ref{sec:advanced-ind}
+to learn about some advanced techniques for inductive proofs.%
+\index{induction heuristics|)}
*}
(*<*)
end
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Fri Aug 03 18:04:55 2001 +0200
@@ -7,6 +7,7 @@
%
\begin{isamarkuptext}%
\label{sec:InductionHeuristics}
+\index{induction heuristics|(}%
The purpose of this section is to illustrate some simple heuristics for
inductive proofs. The first one we have already mentioned in our initial
example:
@@ -18,23 +19,29 @@
\emph{Do induction on argument number $i$ if the function is defined by
recursion in argument number $i$.}
\end{quote}
-When we look at the proof of \isa{{\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}}
-in \S\ref{sec:intro-proof} we find (a) \isa{{\isacharat}} is recursive in
-the first argument, (b) \isa{xs} occurs only as the first argument of
-\isa{{\isacharat}}, and (c) both \isa{ys} and \isa{zs} occur at least once as
-the second argument of \isa{{\isacharat}}. Hence it is natural to perform induction
-on \isa{xs}.
+When we look at the proof of \isa{{\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys{\isacharat}zs{\isacharparenright}}
+in \S\ref{sec:intro-proof} we find
+\begin{itemize}
+\item \isa{{\isacharat}} is recursive in
+the first argument
+\item \isa{xs} occurs only as the first argument of
+\isa{{\isacharat}}
+\item both \isa{ys} and \isa{zs} occur at least once as
+the second argument of \isa{{\isacharat}}
+\end{itemize}
+Hence it is natural to perform induction on~\isa{xs}.
The key heuristic, and the main point of this section, is to
-generalize the goal before induction. The reason is simple: if the goal is
+\emph{generalize the goal before induction}.
+The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
step to go through. Let us illustrate the idea with an example.
-Function \isa{rev} has quadratic worst-case running time
+Function \cdx{rev} has quadratic worst-case running time
because it calls function \isa{{\isacharat}} for each element of the list and
\isa{{\isacharat}} is linear in its first argument. A linear time version of
\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only \isa{{\isacharhash}}:%
+gradually, using only~\isa{{\isacharhash}}:%
\end{isamarkuptext}%
\isacommand{consts}\ itrev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
@@ -42,10 +49,10 @@
{\isachardoublequote}itrev\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ ys\ {\isacharequal}\ itrev\ xs\ {\isacharparenleft}x{\isacharhash}ys{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-The behaviour of \isa{itrev} is simple: it reverses
+The behaviour of \cdx{itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+empty. Note that \isa{itrev} is tail-recursive: it can be
compiled into a loop.
Naturally, we would like to show that \isa{itrev} does indeed reverse
@@ -59,32 +66,32 @@
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-Unfortunately, this is not a complete success:
+Unfortunately, this attempt does not prove
+the induction step:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }itrev\ list\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isasymLongrightarrow}\ itrev\ list\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ rev\ list\ {\isacharat}\ {\isacharbrackleft}a{\isacharbrackright}%
\end{isabelle}
-Just as predicted above, the overall goal, and hence the induction
-hypothesis, is too weak to solve the induction step because of the fixed
-argument, \isa{{\isacharbrackleft}{\isacharbrackright}}. This suggests a heuristic:
-\begin{quote}
+The induction hypothesis is too weak. The fixed
+argument,~\isa{{\isacharbrackleft}{\isacharbrackright}}, prevents it from rewriting the conclusion.
+This example suggests a heuristic:
+\begin{quote}\index{generalizing induction formulae}%
\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isacharequal}\ rev\ xs} is
-just not true --- the correct generalization is%
+just not true. The correct generalization is%
\end{isamarkuptxt}%
\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
If \isa{ys} is replaced by \isa{{\isacharbrackleft}{\isacharbrackright}}, the right-hand side simplifies to
-\isa{rev\ xs}, just as required.
+\isa{rev\ xs}, as required.
-In this particular instance it was easy to guess the right generalization,
-but in more complex situations a good deal of creativity is needed. This is
-the main source of complications in inductive proofs.
+In this instance it was easy to guess the right generalization.
+Other situations can require a good deal of creativity.
Although we now have two variables, only \isa{xs} is suitable for
-induction, and we repeat our above proof attempt. Unfortunately, we are still
+induction, and we repeat our proof attempt. Unfortunately, we are still
not there:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ list{\isachardot}\isanewline
@@ -106,12 +113,11 @@
\emph{Generalize goals for induction by universally quantifying all free
variables {\em(except the induction variable itself!)}.}
\end{quote}
-This prevents trivial failures like the above and does not change the
-provability of the goal. Because it is not always required, and may even
-complicate matters in some cases, this heuristic is often not
-applied blindly.
-The variables that require generalization are typically those that
-change in recursive calls.
+This prevents trivial failures like the one above and does not affect the
+validity of the goal. However, this heuristic should not be applied blindly.
+It is not always required, and the additional quantifiers can complicate
+matters in some cases, The variables that should be quantified are typically
+those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just
proved: the more complex notion (\isa{itrev}) is on the left-hand
@@ -125,12 +131,13 @@
\isa{rev\ xs\ {\isacharat}\ ys} is simpler than \isa{itrev\ xs\ ys}. But see what
happens if you try to prove \isa{rev\ xs\ {\isacharat}\ ys\ {\isacharequal}\ itrev\ xs\ ys}!
-In general, if you have tried the above heuristics and still find your
+If you have tried these heuristics and still find your
induction does not go through, and no obvious lemma suggests itself, you may
need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. You
-will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
+the problem at hand and is beyond simple rules of thumb.
+Additionally, you can read \S\ref{sec:advanced-ind}
to learn about some advanced techniques for inductive proofs.%
+\index{induction heuristics|)}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Aug 03 18:04:55 2001 +0200
@@ -70,9 +70,13 @@
\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-For efficiency's sake, this built-in prover ignores quantified formulae and all
-arithmetic operations apart from addition.
-
+For efficiency's sake, this built-in prover ignores quantified formulae,
+logical connectives, and all arithmetic operations apart from addition.
+In consequence, \isa{auto} cannot prove this slightly more complex goal:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
+\begin{isamarkuptext}%
+\noindent
The method \methdx{arith} is more general. It attempts to prove
the first subgoal provided it is a quantifier-free \textbf{linear arithmetic}
formula. Such formulas may involve the
--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Aug 03 18:04:55 2001 +0200
@@ -6,21 +6,24 @@
}
%
\begin{isamarkuptext}%
-\indexbold{simplification rule}
-To facilitate simplification, theorems can be declared to be simplification
-rules (by the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp
- (attribute)}), in which case proofs by simplification make use of these
-rules automatically. In addition the constructs \isacommand{datatype} and
-\isacommand{primrec} (and a few others) invisibly declare useful
-simplification rules. Explicit definitions are \emph{not} declared
+\index{simplification rules}
+To facilitate simplification,
+the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp (attribute)}
+declares theorems to be simplification rules, which the simplifier
+will use automatically. In addition, \isacommand{datatype} and
+\isacommand{primrec} declarations (and a few others)
+implicitly declare some simplification rules.
+Explicit definitions are \emph{not} declared as
simplification rules automatically!
-Not merely equations but pretty much any theorem can become a simplification
-rule. The simplifier will try to make sense of it. For example, a theorem
-\isa{{\isasymnot}\ P} is automatically turned into \isa{P\ {\isacharequal}\ False}. The details
+Nearly any theorem can become a simplification
+rule. The simplifier will try to transform it into an equation.
+For example, the theorem
+\isa{{\isasymnot}\ P} is turned into \isa{P\ {\isacharequal}\ False}. The details
are explained in \S\ref{sec:SimpHow}.
-The simplification attribute of theorems can be turned on and off as follows:
+The simplification attribute of theorems can be turned on and off:%
+\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
\begin{quote}
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
\isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
@@ -36,14 +39,14 @@
need to be disabled in certain proofs. Frequent changes in the simplification
status of a theorem may indicate an unwise use of defaults.
\begin{warn}
- Simplification may run forever, for example if both $f(x) = g(x)$ and
+ Simplification can run forever, for example if both $f(x) = g(x)$ and
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not
to include simplification rules that can lead to nontermination, either on
their own or in combination with other simplification rules.
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{The Simplification Method%
+\isamarkupsubsection{The {\tt\slshape simp} Method%
}
%
\begin{isamarkuptext}%
@@ -58,25 +61,25 @@
with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
only the first subgoal and may thus need to be repeated --- use
\methdx{simp_all} to simplify all subgoals.
-Note that \isa{simp} fails if nothing changes.%
+If nothing changes, \isa{simp} fails.%
\end{isamarkuptext}%
%
\isamarkupsubsection{Adding and Deleting Simplification Rules%
}
%
\begin{isamarkuptext}%
+\index{simplification rules!adding and deleting}%
If a certain theorem is merely needed in a few proofs by simplification,
we do not need to make it a global simplification rule. Instead we can modify
the set of simplification rules used in a simplification step by adding rules
to it and/or deleting rules from it. The two modifiers for this are
\begin{quote}
-\isa{add{\isacharcolon}} \textit{list of theorem names}\\
-\isa{del{\isacharcolon}} \textit{list of theorem names}
+\isa{add{\isacharcolon}} \textit{list of theorem names}\index{*add (modifier)}\\
+\isa{del{\isacharcolon}} \textit{list of theorem names}\index{*del (modifier)}
\end{quote}
-In case you want to use only a specific list of theorems and ignore all
-others:
+Or you can use a specific list of theorems and omit all others:
\begin{quote}
-\isa{only{\isacharcolon}} \textit{list of theorem names}
+\isa{only{\isacharcolon}} \textit{list of theorem names}\index{*only (modifier)}
\end{quote}
In this example, we invoke the simplifier, adding two distributive
laws:
@@ -102,36 +105,35 @@
simplifies the first assumption to \isa{zs\ {\isacharequal}\ ys}, thus reducing the
conclusion to \isa{ys\ {\isacharequal}\ ys} and hence to \isa{True}.
-In some cases this may be too much of a good thing and may lead to
-nontermination:%
+In some cases, using the assumptions can lead to nontermination:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ f\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-cannot be solved by an unmodified application of \isa{simp} because the
-simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}} extracted from the assumption
-does not terminate. Isabelle notices certain simple forms of
-nontermination but not this one. The problem can be circumvented by
-explicitly telling the simplifier to ignore the assumptions:%
+An unmodified application of \isa{simp} loops. The culprit is the
+simplification rule \isa{f\ x\ {\isacharequal}\ g\ {\isacharparenleft}f\ {\isacharparenleft}g\ x{\isacharparenright}{\isacharparenright}}, which is extracted from
+the assumption. (Isabelle notices certain simple forms of
+nontermination but not this one.) The problem can be circumvented by
+telling the simplifier to ignore the assumptions:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-There are three modifiers that influence the treatment of assumptions:
+Three modifiers influence the treatment of assumptions:
\begin{description}
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\indexbold{*no_asm}
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}}]\index{*no_asm (modifier)}
means that assumptions are completely ignored.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\indexbold{*no_asm_simp}
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}}]\index{*no_asm_simp (modifier)}
means that the assumptions are not simplified but
are used in the simplification of the conclusion.
-\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\indexbold{*no_asm_use}
+\item[\isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}}]\index{*no_asm_use (modifier)}
means that the assumptions are simplified but are not
used in the simplification of each other or the conclusion.
\end{description}
Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
the problematic subgoal above.
-Note that only one of the modifiers is allowed, and it must precede all
+Only one of the modifiers is allowed, and it must precede all
other modifiers.
\begin{warn}
@@ -150,13 +152,17 @@
%
\begin{isamarkuptext}%
\label{sec:Simp-with-Defs}\index{simplification!with definitions}
-Constant definitions (\S\ref{sec:ConstDefinitions}) can
-be used as simplification rules, but by default they are not. Hence the
-simplifier does not expand them automatically, just as it should be:
-definitions are introduced for the purpose of abbreviating complex
-concepts. Of course we need to expand the definitions initially to derive
-enough lemmas that characterize the concept sufficiently for us to forget the
-original definition. For example, given%
+Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
+simplification rules, but by default they are not: the simplifier does not
+expand them automatically. Definitions are intended for introducing abstract
+concepts and not merely as abbreviations. (Contrast with syntax
+translations, \S\ref{sec:def-translations}.) Of course, we need to expand
+the definition initially, but once we have proved enough abstract properties
+of the new constant, we can forget its original definition. This style makes
+proofs more robust: if the definition has to be changed,
+only the proofs of the abstract properties will be affected.
+
+For example, given%
\end{isamarkuptext}%
\isacommand{constdefs}\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ \ {\isachardoublequote}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}%
@@ -184,9 +190,6 @@
\noindent
Of course we can also unfold definitions in the middle of a proof.
-You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose.
-
\begin{warn}
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
occurrences of $f$ with at least two arguments. This may be helpful for unfolding
@@ -199,26 +202,27 @@
}
%
\begin{isamarkuptext}%
-\index{simplification!of let-expressions}
-Proving a goal containing \sdx{let}-expressions almost invariably
-requires the \isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant
-(called \isa{Let}), expanding \isa{let}-constructs means rewriting with
-\isa{Let{\isacharunderscore}def}:%
+\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
+Proving a goal containing \isa{let}-expressions almost invariably requires the
+\isa{let}-con\-structs to be expanded at some point. Since
+\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for
+the predefined constant \isa{Let}, expanding \isa{let}-constructs
+means rewriting with \tdx{Let_def}:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
If, in a particular context, there is no danger of a combinatorial explosion
-of nested \isa{let}s one could even simlify with \isa{Let{\isacharunderscore}def} by
+of nested \isa{let}s, you could even simplify with \isa{Let{\isacharunderscore}def} by
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsection{Conditional Equations%
+\isamarkupsubsection{Conditional Simplification Rules%
}
%
\begin{isamarkuptext}%
+\index{conditional simplification rules}%
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example%
\end{isamarkuptext}%
@@ -247,14 +251,15 @@
}
%
\begin{isamarkuptext}%
-\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
-Goals containing \isa{if}-expressions are usually proved by case
-distinction on the condition of the \isa{if}. For example the goal%
+\label{sec:AutoCaseSplits}\indexbold{case splits}%
+Goals containing \isa{if}-expressions\index{*if expressions!splitting of}
+are usually proved by case
+distinction on the boolean condition. Here is an example:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}xs{\isachardot}\ if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ else\ rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-can be split by a special method \isa{split}:%
+The goal can be split by a special method, \methdx{split}:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -264,12 +269,12 @@
\end{isabelle}
where \tdx{split_if} is a theorem that expresses splitting of
\isa{if}s. Because
-case-splitting on \isa{if}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
+splitting the \isa{if}s is usually the right proof strategy, the
+simplifier does it automatically. Try \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}}
on the initial goal above.
This splitting idea generalizes from \isa{if} to \sdx{case}.
-Let us simplify a case analysis over lists:%
+Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
\end{isamarkuptxt}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}split\ list{\isachardot}split{\isacharparenright}%
@@ -278,20 +283,22 @@
\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}\ {\isasymand}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isacharparenleft}{\isasymforall}a\ list{\isachardot}\ xs\ {\isacharequal}\ a\ {\isacharhash}\ list\ {\isasymlongrightarrow}\ a\ {\isacharhash}\ list\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ zs{\isacharparenright}%
\end{isabelle}
-In contrast to \isa{if}-expressions, the simplifier does not split
-\isa{case}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Therefore the simplifier has a modifier
-\isa{split} for adding further splitting rules explicitly. This means the
-above lemma can be proved in one step by%
+The simplifier does not split
+\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)}
+for adding splitting rules explicitly. The
+lemma above can be proved in one step by%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
whereas \isacommand{apply}\isa{{\isacharparenleft}simp{\isacharparenright}} alone will not succeed.
-In general, every datatype $t$ comes with a theorem
+Every datatype $t$ comes with a theorem
$t$\isa{{\isachardot}split} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the \isa{split} attribute globally:%
+locally as above, or by giving it the \attrdx{split} attribute globally:%
\end{isamarkuptext}%
\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split{\isacharbrackright}%
\begin{isamarkuptext}%
@@ -306,22 +313,23 @@
\end{isamarkuptext}%
\isacommand{declare}\ list{\isachardot}split\ {\isacharbrackleft}split\ del{\isacharbrackright}%
\begin{isamarkuptext}%
-In polished proofs the \isa{split} method is rarely used on its own
-but always as part of the simplifier. However, if a goal contains
-multiple splittable constructs, the \isa{split} method can be
+Polished proofs typically perform splitting within \isa{simp} rather than
+invoking the \isa{split} method. However, if a goal contains
+several \isa{if} and \isa{case} expressions,
+the \isa{split} method can be
helpful in selectively exploring the effects of splitting.
-The above split rules intentionally only affect the conclusion of a
-subgoal. If you want to split an \isa{if} or \isa{case}-expression in
-the assumptions, you have to apply \isa{split{\isacharunderscore}if{\isacharunderscore}asm} or
+The split rules shown above are intended to affect only the subgoal's
+conclusion. If you want to split an \isa{if} or \isa{case}-expression
+in the assumptions, you have to apply \tdx{split_if_asm} or
$t$\isa{{\isachardot}split{\isacharunderscore}asm}:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ else\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by \isa{simp{\isacharunderscore}all}):
+Unlike splitting the conclusion, this step creates two
+separate subgoals, which here can be solved by \isa{simp{\isacharunderscore}all}:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\ ys\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ xs\ {\isacharat}\ ys\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}%
@@ -331,36 +339,16 @@
$t$\isa{{\isachardot}split{\isacharunderscore}asm}. Analogously, there is \isa{if{\isacharunderscore}splits}.
\begin{warn}
- The simplifier merely simplifies the condition of an \isa{if} but not the
+ The simplifier merely simplifies the condition of an
+ \isa{if}\index{*if expressions!simplification of} but not the
\isa{then} or \isa{else} parts. The latter are simplified only after the
condition reduces to \isa{True} or \isa{False}, or after splitting. The
same is true for \sdx{case}-expressions: only the selector is
simplified at first, until either the expression reduces to one of the
cases or it is split.
-\end{warn}\index{*split (method, attr.)|)}%
+\end{warn}%
\end{isamarkuptxt}%
%
-\isamarkupsubsection{Arithmetic%
-}
-%
-\begin{isamarkuptext}%
-\index{linear arithmetic}
-The simplifier routinely solves a small class of linear arithmetic formulae
-(over type \isa{nat} and other numeric types): it only takes into account
-assumptions and conclusions that are relations
-($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-is proved by simplification, whereas the only slightly more complex%
-\end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
-\begin{isamarkuptext}%
-\noindent
-is not proved by simplification and requires \isa{arith}.%
-\end{isamarkuptext}%
-%
\isamarkupsubsection{Tracing%
}
%
@@ -403,9 +391,9 @@
each of the rule's conditions. Many other hints about the simplifier's
actions will appear.
-In more complicated cases, the trace can be quite lengthy, especially since
-invocations of the simplifier are often nested (e.g.\ when solving conditions
-of rewrite rules). Thus it is advisable to reset it:%
+In more complicated cases, the trace can be quite lengthy. Invocations of the
+simplifier are often nested, for instance when solving conditions of rewrite
+rules. Thus it is advisable to reset it:%
\end{isamarkuptext}%
\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
\end{isabellebody}%
--- a/doc-src/TutorialI/Misc/natsum.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy Fri Aug 03 18:04:55 2001 +0200
@@ -70,9 +70,15 @@
(*<*)by(auto)(*>*)
text{*\noindent
-For efficiency's sake, this built-in prover ignores quantified formulae and all
-arithmetic operations apart from addition.
+For efficiency's sake, this built-in prover ignores quantified formulae,
+logical connectives, and all arithmetic operations apart from addition.
+In consequence, @{text auto} cannot prove this slightly more complex goal:
+*}
+lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
+(*<*)by(arith)(*>*)
+
+text{*\noindent
The method \methdx{arith} is more general. It attempts to prove
the first subgoal provided it is a quantifier-free \textbf{linear arithmetic}
formula. Such formulas may involve the
--- a/doc-src/TutorialI/Misc/simp.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy Fri Aug 03 18:04:55 2001 +0200
@@ -4,21 +4,24 @@
subsection{*Simplification Rules*}
-text{*\indexbold{simplification rule}
-To facilitate simplification, theorems can be declared to be simplification
-rules (by the attribute @{text"[simp]"}\index{*simp
- (attribute)}), in which case proofs by simplification make use of these
-rules automatically. In addition the constructs \isacommand{datatype} and
-\isacommand{primrec} (and a few others) invisibly declare useful
-simplification rules. Explicit definitions are \emph{not} declared
+text{*\index{simplification rules}
+To facilitate simplification,
+the attribute @{text"[simp]"}\index{*simp (attribute)}
+declares theorems to be simplification rules, which the simplifier
+will use automatically. In addition, \isacommand{datatype} and
+\isacommand{primrec} declarations (and a few others)
+implicitly declare some simplification rules.
+Explicit definitions are \emph{not} declared as
simplification rules automatically!
-Not merely equations but pretty much any theorem can become a simplification
-rule. The simplifier will try to make sense of it. For example, a theorem
-@{prop"~P"} is automatically turned into @{prop"P = False"}. The details
+Nearly any theorem can become a simplification
+rule. The simplifier will try to transform it into an equation.
+For example, the theorem
+@{prop"~P"} is turned into @{prop"P = False"}. The details
are explained in \S\ref{sec:SimpHow}.
-The simplification attribute of theorems can be turned on and off as follows:
+The simplification attribute of theorems can be turned on and off:%
+\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
\begin{quote}
\isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
\isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
@@ -34,14 +37,14 @@
need to be disabled in certain proofs. Frequent changes in the simplification
status of a theorem may indicate an unwise use of defaults.
\begin{warn}
- Simplification may run forever, for example if both $f(x) = g(x)$ and
+ Simplification can run forever, for example if both $f(x) = g(x)$ and
$g(x) = f(x)$ are simplification rules. It is the user's responsibility not
to include simplification rules that can lead to nontermination, either on
their own or in combination with other simplification rules.
\end{warn}
-*}
+*}
-subsection{*The Simplification Method*}
+subsection{*The {\tt\slshape simp} Method*}
text{*\index{*simp (method)|bold}
The general format of the simplification method is
@@ -54,24 +57,24 @@
with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
only the first subgoal and may thus need to be repeated --- use
\methdx{simp_all} to simplify all subgoals.
-Note that @{text simp} fails if nothing changes.
+If nothing changes, @{text simp} fails.
*}
subsection{*Adding and Deleting Simplification Rules*}
text{*
+\index{simplification rules!adding and deleting}%
If a certain theorem is merely needed in a few proofs by simplification,
we do not need to make it a global simplification rule. Instead we can modify
the set of simplification rules used in a simplification step by adding rules
to it and/or deleting rules from it. The two modifiers for this are
\begin{quote}
-@{text"add:"} \textit{list of theorem names}\\
-@{text"del:"} \textit{list of theorem names}
+@{text"add:"} \textit{list of theorem names}\index{*add (modifier)}\\
+@{text"del:"} \textit{list of theorem names}\index{*del (modifier)}
\end{quote}
-In case you want to use only a specific list of theorems and ignore all
-others:
+Or you can use a specific list of theorems and omit all others:
\begin{quote}
-@{text"only:"} \textit{list of theorem names}
+@{text"only:"} \textit{list of theorem names}\index{*only (modifier)}
\end{quote}
In this example, we invoke the simplifier, adding two distributive
laws:
@@ -96,38 +99,37 @@
simplifies the first assumption to @{term"zs = ys"}, thus reducing the
conclusion to @{term"ys = ys"} and hence to @{term"True"}.
-In some cases this may be too much of a good thing and may lead to
-nontermination:
+In some cases, using the assumptions can lead to nontermination:
*}
lemma "\<forall>x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []";
txt{*\noindent
-cannot be solved by an unmodified application of @{text"simp"} because the
-simplification rule @{term"f x = g (f (g x))"} extracted from the assumption
-does not terminate. Isabelle notices certain simple forms of
-nontermination but not this one. The problem can be circumvented by
-explicitly telling the simplifier to ignore the assumptions:
+An unmodified application of @{text"simp"} loops. The culprit is the
+simplification rule @{term"f x = g (f (g x))"}, which is extracted from
+the assumption. (Isabelle notices certain simple forms of
+nontermination but not this one.) The problem can be circumvented by
+telling the simplifier to ignore the assumptions:
*}
apply(simp (no_asm));
done
text{*\noindent
-There are three modifiers that influence the treatment of assumptions:
+Three modifiers influence the treatment of assumptions:
\begin{description}
-\item[@{text"(no_asm)"}]\indexbold{*no_asm}
+\item[@{text"(no_asm)"}]\index{*no_asm (modifier)}
means that assumptions are completely ignored.
-\item[@{text"(no_asm_simp)"}]\indexbold{*no_asm_simp}
+\item[@{text"(no_asm_simp)"}]\index{*no_asm_simp (modifier)}
means that the assumptions are not simplified but
are used in the simplification of the conclusion.
-\item[@{text"(no_asm_use)"}]\indexbold{*no_asm_use}
+\item[@{text"(no_asm_use)"}]\index{*no_asm_use (modifier)}
means that the assumptions are simplified but are not
used in the simplification of each other or the conclusion.
\end{description}
Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
the problematic subgoal above.
-Note that only one of the modifiers is allowed, and it must precede all
+Only one of the modifiers is allowed, and it must precede all
other modifiers.
\begin{warn}
@@ -144,14 +146,17 @@
subsection{*Rewriting with Definitions*}
text{*\label{sec:Simp-with-Defs}\index{simplification!with definitions}
-Constant definitions (\S\ref{sec:ConstDefinitions}) can
-be used as simplification rules, but by default they are not. Hence the
-simplifier does not expand them automatically, just as it should be:
-definitions are introduced for the purpose of abbreviating complex
-concepts. Of course we need to expand the definitions initially to derive
-enough lemmas that characterize the concept sufficiently for us to forget the
-original definition. For example, given
-*}
+Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
+simplification rules, but by default they are not: the simplifier does not
+expand them automatically. Definitions are intended for introducing abstract
+concepts and not merely as abbreviations. (Contrast with syntax
+translations, \S\ref{sec:def-translations}.) Of course, we need to expand
+the definition initially, but once we have proved enough abstract properties
+of the new constant, we can forget its original definition. This style makes
+proofs more robust: if the definition has to be changed,
+only the proofs of the abstract properties will be affected.
+
+For example, given *}
constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
@@ -179,9 +184,6 @@
text{*\noindent
Of course we can also unfold definitions in the middle of a proof.
-You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose.
-
\begin{warn}
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
occurrences of $f$ with at least two arguments. This may be helpful for unfolding
@@ -192,13 +194,12 @@
subsection{*Simplifying {\tt\slshape let}-Expressions*}
-text{*\index{simplification!of let-expressions}
-Proving a goal containing \sdx{let}-expressions almost invariably
-requires the @{text"let"}-con\-structs to be expanded at some point. Since
-@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant
-(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
-@{thm[source]Let_def}:
-*}
+text{*\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
+Proving a goal containing \isa{let}-expressions almost invariably requires the
+@{text"let"}-con\-structs to be expanded at some point. Since
+@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for
+the predefined constant @{term"Let"}, expanding @{text"let"}-constructs
+means rewriting with \tdx{Let_def}: *}
lemma "(let xs = [] in xs@ys@xs) = ys";
apply(simp add: Let_def);
@@ -206,14 +207,15 @@
text{*
If, in a particular context, there is no danger of a combinatorial explosion
-of nested @{text"let"}s one could even simlify with @{thm[source]Let_def} by
+of nested @{text"let"}s, you could even simplify with @{thm[source]Let_def} by
default:
*}
declare Let_def [simp]
-subsection{*Conditional Equations*}
+subsection{*Conditional Simplification Rules*}
text{*
+\index{conditional simplification rules}%
So far all examples of rewrite rules were equations. The simplifier also
accepts \emph{conditional} equations, for example
*}
@@ -245,15 +247,16 @@
subsection{*Automatic Case Splits*}
-text{*\label{sec:AutoCaseSplits}\indexbold{case splits}\index{*split (method, attr.)|(}
-Goals containing @{text"if"}-expressions are usually proved by case
-distinction on the condition of the @{text"if"}. For example the goal
+text{*\label{sec:AutoCaseSplits}\indexbold{case splits}%
+Goals containing @{text"if"}-expressions\index{*if expressions!splitting of}
+are usually proved by case
+distinction on the boolean condition. Here is an example:
*}
lemma "\<forall>xs. if xs = [] then rev xs = [] else rev xs \<noteq> []";
txt{*\noindent
-can be split by a special method @{text split}:
+The goal can be split by a special method, \methdx{split}:
*}
apply(split split_if)
@@ -262,23 +265,25 @@
@{subgoals[display,indent=0]}
where \tdx{split_if} is a theorem that expresses splitting of
@{text"if"}s. Because
-case-splitting on @{text"if"}s is almost always the right proof strategy, the
-simplifier performs it automatically. Try \isacommand{apply}@{text"(simp)"}
+splitting the @{text"if"}s is usually the right proof strategy, the
+simplifier does it automatically. Try \isacommand{apply}@{text"(simp)"}
on the initial goal above.
This splitting idea generalizes from @{text"if"} to \sdx{case}.
-Let us simplify a case analysis over lists:
+Let us simplify a case analysis over lists:\index{*list.split (theorem)}
*}(*<*)by simp(*>*)
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
apply(split list.split);
txt{*
@{subgoals[display,indent=0]}
-In contrast to @{text"if"}-expressions, the simplifier does not split
-@{text"case"}-expressions by default because this can lead to nontermination
-in case of recursive datatypes. Therefore the simplifier has a modifier
-@{text split} for adding further splitting rules explicitly. This means the
-above lemma can be proved in one step by
+The simplifier does not split
+@{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)}
+for adding splitting rules explicitly. The
+lemma above can be proved in one step by
*}
(*<*)oops;
lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs";
@@ -288,9 +293,9 @@
text{*\noindent
whereas \isacommand{apply}@{text"(simp)"} alone will not succeed.
-In general, every datatype $t$ comes with a theorem
+Every datatype $t$ comes with a theorem
$t$@{text".split"} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the @{text"split"} attribute globally:
+locally as above, or by giving it the \attrdx{split} attribute globally:
*}
declare list.split [split]
@@ -312,65 +317,42 @@
declare list.split [split del]
text{*
-In polished proofs the @{text split} method is rarely used on its own
-but always as part of the simplifier. However, if a goal contains
-multiple splittable constructs, the @{text split} method can be
+Polished proofs typically perform splitting within @{text simp} rather than
+invoking the @{text split} method. However, if a goal contains
+several @{text if} and @{text case} expressions,
+the @{text split} method can be
helpful in selectively exploring the effects of splitting.
-The above split rules intentionally only affect the conclusion of a
-subgoal. If you want to split an @{text"if"} or @{text"case"}-expression in
-the assumptions, you have to apply @{thm[source]split_if_asm} or
-$t$@{text".split_asm"}:
-*}
+The split rules shown above are intended to affect only the subgoal's
+conclusion. If you want to split an @{text"if"} or @{text"case"}-expression
+in the assumptions, you have to apply \tdx{split_if_asm} or
+$t$@{text".split_asm"}: *}
lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
apply(split split_if_asm)
txt{*\noindent
-In contrast to splitting the conclusion, this actually creates two
-separate subgoals (which are solved by @{text"simp_all"}):
+Unlike splitting the conclusion, this step creates two
+separate subgoals, which here can be solved by @{text"simp_all"}:
@{subgoals[display,indent=0]}
If you need to split both in the assumptions and the conclusion,
use $t$@{text".splits"} which subsumes $t$@{text".split"} and
$t$@{text".split_asm"}. Analogously, there is @{thm[source]if_splits}.
\begin{warn}
- The simplifier merely simplifies the condition of an \isa{if} but not the
+ The simplifier merely simplifies the condition of an
+ \isa{if}\index{*if expressions!simplification of} but not the
\isa{then} or \isa{else} parts. The latter are simplified only after the
condition reduces to \isa{True} or \isa{False}, or after splitting. The
same is true for \sdx{case}-expressions: only the selector is
simplified at first, until either the expression reduces to one of the
cases or it is split.
-\end{warn}\index{*split (method, attr.)|)}
+\end{warn}
*}
(*<*)
by(simp_all)
(*>*)
-subsection{*Arithmetic*}
-
-text{*\index{linear arithmetic}
-The simplifier routinely solves a small class of linear arithmetic formulae
-(over type \isa{nat} and other numeric types): it only takes into account
-assumptions and conclusions that are relations
-($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus
-*}
-
-lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"
-(*<*)by(auto)(*>*)
-
-text{*\noindent
-is proved by simplification, whereas the only slightly more complex
-*}
-
-lemma "\<not> m < n \<and> m < n+1 \<Longrightarrow> m = n";
-(*<*)by(arith)(*>*)
-
-text{*\noindent
-is not proved by simplification and requires @{text arith}.
-*}
-
-
subsection{*Tracing*}
text{*\indexbold{tracing the simplifier}
Using the simplifier effectively may take a bit of experimentation. Set the
@@ -412,9 +394,9 @@
each of the rule's conditions. Many other hints about the simplifier's
actions will appear.
-In more complicated cases, the trace can be quite lengthy, especially since
-invocations of the simplifier are often nested (e.g.\ when solving conditions
-of rewrite rules). Thus it is advisable to reset it:
+In more complicated cases, the trace can be quite lengthy. Invocations of the
+simplifier are often nested, for instance when solving conditions of rewrite
+rules. Thus it is advisable to reset it:
*}
ML "reset trace_simp";
--- a/doc-src/TutorialI/Recdef/Induction.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy Fri Aug 03 18:04:55 2001 +0200
@@ -52,17 +52,18 @@
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
-induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
+induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
~~{\isasymAnd}a~x.~P~a~[x];\isanewline
~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
{\isasymLongrightarrow}~P~u~v%
\end{isabelle}
-merely says that in order to prove a property @{term"P"} of @{term"u"} and
+It merely says that in order to prove a property @{term"P"} of @{term"u"} and
@{term"v"} you need to prove it for the three cases where @{term"v"} is the
-empty list, the singleton list, and the list with at least two elements
-(in which case you may assume it holds for the tail of that list).
+empty list, the singleton list, and the list with at least two elements.
+The final case has an induction hypothesis: you may assume that @{term"P"}
+holds for the tail of that list.
*}
(*<*)
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Fri Aug 03 18:04:55 2001 +0200
@@ -54,17 +54,18 @@
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
name of a function that takes an $n$-tuple. Usually the subgoal will
contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
-induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct}
+induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
\begin{isabelle}
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
~~{\isasymAnd}a~x.~P~a~[x];\isanewline
~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
{\isasymLongrightarrow}~P~u~v%
\end{isabelle}
-merely says that in order to prove a property \isa{P} of \isa{u} and
+It merely says that in order to prove a property \isa{P} of \isa{u} and
\isa{v} you need to prove it for the three cases where \isa{v} is the
-empty list, the singleton list, and the list with at least two elements
-(in which case you may assume it holds for the tail of that list).%
+empty list, the singleton list, and the list with at least two elements.
+The final case has an induction hypothesis: you may assume that \isa{P}
+holds for the tail of that list.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/examples.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Fri Aug 03 18:04:55 2001 +0200
@@ -3,7 +3,7 @@
\def\isabellecontext{examples}%
%
\begin{isamarkuptext}%
-Here is a simple example, the Fibonacci function:%
+Here is a simple example, the \rmindex{Fibonacci function}:%
\end{isamarkuptext}%
\isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
@@ -12,7 +12,8 @@
\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-The definition of \isa{fib} is accompanied by a \bfindex{measure function}
+\index{measure functions}%
+The definition of \isa{fib} is accompanied by a \textbf{measure function}
\isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
@@ -36,7 +37,8 @@
The details of tupled $\lambda$-abstractions \isa{{\isasymlambda}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlsub n{\isacharparenright}} are
explained in \S\ref{sec:products}, but for now your intuition is all you need.
-Pattern matching need not be exhaustive:%
+Pattern matching\index{pattern matching!and \isacommand{recdef}}
+need not be exhaustive:%
\end{isamarkuptext}%
\isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
\isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 03 18:04:55 2001 +0200
@@ -3,11 +3,12 @@
\def\isabellecontext{simplification}%
%
\begin{isamarkuptext}%
-Once we have succeeded in proving all termination conditions, the recursion
-equations become simplification rules, just as with
+Once we have proved all the termination conditions, the \isacommand{recdef}
+recursion equations become simplification rules, just as with
\isacommand{primrec}. In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not
terminate because of automatic splitting of \isa{if}.
+\index{*if expressions!splitting of}
Let us look at an example:%
\end{isamarkuptext}%
\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -25,8 +26,9 @@
rule. Of course the equation is nonterminating if we are allowed to unfold
the recursive call inside the \isa{else} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
-something else which leads to the same problem: it splits \isa{if}s if the
-condition simplifies to neither \isa{True} nor \isa{False}. For
+something else that leads to the same problem: it splits
+each \isa{if}-expression unless its
+condition simplifies to \isa{True} or \isa{False}. For
example, simplification reduces
\begin{isabelle}%
\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
@@ -44,9 +46,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending \isa{split{\isacharunderscore}if}
+The most radical solution is to disable the offending theorem
+\isa{split{\isacharunderscore}if},
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
-because it means you will often have to invoke the rule explicitly when
+approach: you will often have to invoke the rule explicitly when
\isa{if} is involved.
If possible, the definition should be given by pattern matching on the left
@@ -59,19 +62,20 @@
\ \ {\isachardoublequote}gcd{\isadigit{1}}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isadigit{1}}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-Note that the order of equations is important and hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
+The order of equations is important: it hides the side condition
+\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
may not be expressible by pattern matching.
-A very simple alternative is to replace \isa{if} by \isa{case}, which
-is also available for \isa{bool} but is not split automatically:%
+A simple alternative is to replace \isa{if} by \isa{case},
+which is also available for \isa{bool} and is not split automatically:%
\end{isamarkuptext}%
\isacommand{consts}\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ gcd{\isadigit{2}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}gcd{\isadigit{2}}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-In fact, this is probably the neatest solution next to pattern matching.
+This is probably the neatest solution next to pattern matching, and it is
+always available.
A final alternative is to replace the offending simplification rules by
derived conditional ones. For \isa{gcd} it means we have to prove
@@ -80,11 +84,13 @@
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isacommand{done}\isanewline
+\isanewline
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
+Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}.
Now we can disable the original simplification rule:%
\end{isamarkuptext}%
\isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
--- a/doc-src/TutorialI/Recdef/document/termination.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Aug 03 18:04:55 2001 +0200
@@ -13,16 +13,16 @@
the same function. What is more, those equations are automatically declared as
simplification rules.
-Isabelle may fail to prove some termination conditions
-(there is one for each recursive call). For example,
-termination of the following artificial function%
+Isabelle may fail to prove the termination condition for some
+recursive call. Let us try the following artificial function:%
\end{isamarkuptext}%
\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-is not proved automatically. Isabelle prints a
+Isabelle prints a
+\REMARK{error or warning? change this part? rename g to f?}
message showing you what it was unable to prove. You will then
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:%
@@ -30,8 +30,8 @@
\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
-It was not proved automatically because of the special nature of subtraction
-on \isa{nat}. This requires more arithmetic than is tried by default:%
+It was not proved automatically because of the awkward behaviour of subtraction
+on type \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
\isacommand{done}%
@@ -49,8 +49,8 @@
\begin{isamarkuptext}%
\noindent
This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{g} and they are simplification
-rules. Thus we can automatically prove%
+the stated recursion equation for \isa{g}, which has been stored as a
+simplification rule. Thus we can automatically prove results such as this one:%
\end{isamarkuptext}%
\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
@@ -70,13 +70,14 @@
fail, and thus we could not define it a second time. However, all theorems
about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
the unproved termination condition. Moreover, the theorems
-\isa{f{\isachardot}simps} are not simplification rules. However, this mechanism
+\isa{f{\isachardot}simps} are not stored as simplification rules.
+However, this mechanism
allows a delayed proof of termination: instead of proving
\isa{termi{\isacharunderscore}lem} up front, we could prove
it later on and then use it to remove the preconditions from the theorems
about \isa{f}. In most cases this is more cumbersome than proving things
up front.
-%FIXME, with one exception: nested recursion.%
+\REMARK{FIXME, with one exception: nested recursion.}%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/examples.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Fri Aug 03 18:04:55 2001 +0200
@@ -3,7 +3,7 @@
(*>*)
text{*
-Here is a simple example, the Fibonacci function:
+Here is a simple example, the \rmindex{Fibonacci function}:
*}
consts fib :: "nat \<Rightarrow> nat";
@@ -13,7 +13,8 @@
"fib (Suc(Suc x)) = fib x + fib (Suc x)";
text{*\noindent
-The definition of @{term"fib"} is accompanied by a \bfindex{measure function}
+\index{measure functions}%
+The definition of @{term"fib"} is accompanied by a \textbf{measure function}
@{term"%n. n"} which maps the argument of @{term"fib"} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
@@ -38,7 +39,8 @@
The details of tupled $\lambda$-abstractions @{text"\<lambda>(x\<^sub>1,\<dots>,x\<^sub>n)"} are
explained in \S\ref{sec:products}, but for now your intuition is all you need.
-Pattern matching need not be exhaustive:
+Pattern matching\index{pattern matching!and \isacommand{recdef}}
+need not be exhaustive:
*}
consts last :: "'a list \<Rightarrow> 'a";
--- a/doc-src/TutorialI/Recdef/simplification.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy Fri Aug 03 18:04:55 2001 +0200
@@ -3,11 +3,12 @@
(*>*)
text{*
-Once we have succeeded in proving all termination conditions, the recursion
-equations become simplification rules, just as with
+Once we have proved all the termination conditions, the \isacommand{recdef}
+recursion equations become simplification rules, just as with
\isacommand{primrec}. In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not
terminate because of automatic splitting of @{text if}.
+\index{*if expressions!splitting of}
Let us look at an example:
*}
@@ -24,8 +25,9 @@
rule. Of course the equation is nonterminating if we are allowed to unfold
the recursive call inside the @{text else} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
-something else which leads to the same problem: it splits @{text if}s if the
-condition simplifies to neither @{term True} nor @{term False}. For
+something else that leads to the same problem: it splits
+each @{text if}-expression unless its
+condition simplifies to @{term True} or @{term False}. For
example, simplification reduces
@{term[display]"gcd(m,n) = k"}
in one step to
@@ -37,9 +39,10 @@
simplification steps. Fortunately, this problem can be avoided in many
different ways.
-The most radical solution is to disable the offending @{thm[source]split_if}
+The most radical solution is to disable the offending theorem
+@{thm[source]split_if},
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
-because it means you will often have to invoke the rule explicitly when
+approach: you will often have to invoke the rule explicitly when
@{text if} is involved.
If possible, the definition should be given by pattern matching on the left
@@ -54,12 +57,12 @@
text{*\noindent
-Note that the order of equations is important and hides the side condition
-@{prop"n ~= 0"}. Unfortunately, in general the case distinction
+The order of equations is important: it hides the side condition
+@{prop"n ~= 0"}. Unfortunately, in general the case distinction
may not be expressible by pattern matching.
-A very simple alternative is to replace @{text if} by @{text case}, which
-is also available for @{typ bool} but is not split automatically:
+A simple alternative is to replace @{text if} by @{text case},
+which is also available for @{typ bool} and is not split automatically:
*}
consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
@@ -67,7 +70,8 @@
"gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
text{*\noindent
-In fact, this is probably the neatest solution next to pattern matching.
+This is probably the neatest solution next to pattern matching, and it is
+always available.
A final alternative is to replace the offending simplification rules by
derived conditional ones. For @{term gcd} it means we have to prove
@@ -77,11 +81,14 @@
lemma [simp]: "gcd (m, 0) = m";
apply(simp);
done
+
lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
apply(simp);
done
text{*\noindent
+Simplification terminates for these proofs because the condition of the @{text
+if} simplifies to @{term True} or @{term False}.
Now we can disable the original simplification rule:
*}
--- a/doc-src/TutorialI/Recdef/termination.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Fri Aug 03 18:04:55 2001 +0200
@@ -13,17 +13,16 @@
the same function. What is more, those equations are automatically declared as
simplification rules.
-Isabelle may fail to prove some termination conditions
-(there is one for each recursive call). For example,
-termination of the following artificial function
-*}
+Isabelle may fail to prove the termination condition for some
+recursive call. Let us try the following artificial function:*}
consts f :: "nat\<times>nat \<Rightarrow> nat";
recdef f "measure(\<lambda>(x,y). x-y)"
"f(x,y) = (if x \<le> y then x else f(x,y+1))";
text{*\noindent
-is not proved automatically. Isabelle prints a
+Isabelle prints a
+\REMARK{error or warning? change this part? rename g to f?}
message showing you what it was unable to prove. You will then
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:
@@ -32,8 +31,8 @@
lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
txt{*\noindent
-It was not proved automatically because of the special nature of subtraction
-on @{typ"nat"}. This requires more arithmetic than is tried by default:
+It was not proved automatically because of the awkward behaviour of subtraction
+on type @{typ"nat"}. This requires more arithmetic than is tried by default:
*}
apply(arith);
@@ -53,8 +52,8 @@
text{*\noindent
This time everything works fine. Now @{thm[source]g.simps} contains precisely
-the stated recursion equation for @{term g} and they are simplification
-rules. Thus we can automatically prove
+the stated recursion equation for @{term g}, which has been stored as a
+simplification rule. Thus we can automatically prove results such as this one:
*}
theorem "g(1,0) = g(1,1)";
@@ -75,13 +74,14 @@
fail, and thus we could not define it a second time. However, all theorems
about @{term f}, for example @{thm[source]f.simps}, carry as a precondition
the unproved termination condition. Moreover, the theorems
-@{thm[source]f.simps} are not simplification rules. However, this mechanism
+@{thm[source]f.simps} are not stored as simplification rules.
+However, this mechanism
allows a delayed proof of termination: instead of proving
@{thm[source]termi_lem} up front, we could prove
it later on and then use it to remove the preconditions from the theorems
about @{term f}. In most cases this is more cumbersome than proving things
up front.
-%FIXME, with one exception: nested recursion.
+\REMARK{FIXME, with one exception: nested recursion.}
*}
(*<*)
--- a/doc-src/TutorialI/Rules/Basic.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Fri Aug 03 18:04:55 2001 +0200
@@ -277,6 +277,9 @@
Hilbert-epsilon theorems*}
text{*
+@{thm[display] the_equality[no_vars]}
+\rulename{the_equality}
+
@{thm[display] some_equality[no_vars]}
\rulename{some_equality}
@@ -311,7 +314,7 @@
"\<lbrakk> P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
apply (simp add: Least_def)
-txt{*omit maybe?
+txt{*
@{subgoals[display,indent=0,margin=65]}
*};
--- a/doc-src/TutorialI/Rules/rules.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Fri Aug 03 18:04:55 2001 +0200
@@ -1232,30 +1232,38 @@
-\section{Hilbert's $\varepsilon$-Operator}
+\section{Description Operators}
\label{sec:SOME}
-\index{Hilbert's $\varepsilon$-operator|(}%
-HOL provides Hilbert's $\varepsilon$-operator. The term $\varepsilon x.
-P(x)$ denotes some $x$ such that $P(x)$ is true, provided such a value
-exists. In \textsc{ascii}, we write \sdx{SOME} for the Greek
-letter~$\varepsilon$.
+\index{description operators|(}%
+HOL provides two description operators.
+A \textbf{definite description} formalizes the word ``the,'' as in
+``the greatest divisior of~$n$.''
+It returns an arbitrary value unless the formula has a unique solution.
+An \textbf{indefinite description} formalizes the word ``some,'' as in
+``some member of~$S$.'' It differs from a definition description in not
+requiring the solution to be unique: it uses the axiom of choice to pick any
+solution.
\begin{warn}
-Hilbert's $\varepsilon$-operator can be hard to reason about. New users
-should try to avoid it. Fortunately, situations that require it are rare.
+Description operators can be hard to reason about. Novices
+should try to avoid them. Fortunately, descriptions are seldom required.
\end{warn}
\subsection{Definite Descriptions}
\index{descriptions!definite}%
-The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
-description}: when \isa{P} is satisfied by a unique value,~\isa{a}.
-We reason using this rule:\REMARK{update if we add iota}
+A definite description is traditionally written $\iota x. P(x)$. It denotes
+the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$;
+otherwise, it returns an arbitrary value of the expected type.
+Isabelle uses \sdx{THE} for the Greek letter~$\iota$. (The
+traditional notation could be provided, but it is not legible on screen.)
+
+We reason using this rule, where \isa{a} is the unique solution:
\begin{isabelle}
\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
-\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
-\rulenamedx{some_equality}
+\isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a%
+\rulenamedx{the_equality}
\end{isabelle}
For instance, we can define the
cardinality of a finite set~$A$ to be that
@@ -1267,21 +1275,22 @@
operator, which denotes the least \isa{x} satisfying~\isa{P}:%
\index{least number operator|see{\protect\isa{LEAST}}}
\begin{isabelle}
-(LEAST\ x.\ P\ x)\ = (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
+(LEAST\ x.\ P\ x)\ = (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\
P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))
\end{isabelle}
%
-Let us prove the counterpart of \isa{some_equality} for \sdx{LEAST}\@.
-The first step merely unfolds the definitions (\isa{LeastM} is a
-auxiliary operator):
+Let us prove the analogue of \isa{the_equality} for \sdx{LEAST}\@.
\begin{isabelle}
\isacommand{theorem}\ Least_equality:\isanewline
\ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline
-\isacommand{apply}\ (simp\ add:\ Least_def\ LeastM_def)\isanewline
-%\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
-%\isasymle \ x\isasymrbrakk \isanewline
-%\ \ \ \ \isasymLongrightarrow \ (SOME\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
-\isacommand{apply}\ (rule\ some_equality)\isanewline
+\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline
+\isanewline
+\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \isanewline
+\isaindent{\ 1.\ }\isasymLongrightarrow \ (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k%
+\end{isabelle}
+The first step has merely unfolded the definition.
+\begin{isabelle}
+\isacommand{apply}\ (rule\ the_equality)\isanewline
\isanewline
\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\
\isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \
@@ -1289,32 +1298,40 @@
\ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline
\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k%
\end{isabelle}
-As always with \isa{some_equality}, we must show existence and
+As always with \isa{the_equality}, we must show existence and
uniqueness of the claimed solution,~\isa{k}. Existence, the first
subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry:
\begin{isabelle}
\isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y%
\rulename{order_antisym}
\end{isabelle}
-The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One call
-to \isa{auto} does it all:
+The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One
+call to \isa{auto} does it all:
\begin{isabelle}
\isacommand{by}\ (auto\ intro:\ order_antisym)
\end{isabelle}
+\REMARK{refer to \isa{Main_wo_AC} if we introduce it}
\subsection{Indefinite Descriptions}
+\index{Hilbert's $\varepsilon$-operator}%
\index{descriptions!indefinite}%
-Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
-description}, when it makes an arbitrary selection from the values
-satisfying~\isa{P}\@. Here is the definition
-of~\cdx{inv}, which expresses inverses of
+An indefinite description is traditionally written $\varepsilon x. P(x)$ and is
+known as Hilbert's $\varepsilon$-operator. It denotes
+some $x$ such that $P(x)$ is true, provided one exists.
+Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$.
+
+Here is the definition of~\cdx{inv}, which expresses inverses of
functions:
\begin{isabelle}
inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
\rulename{inv_def}
\end{isabelle}
+Using \isa{SOME} rather than \isa{THE} makes \isa{inv~f} behave well
+even if \isa{f} is not injective. As it happens, most useful theorems about
+\isa{inv} do assume the function to be injective.
+
The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that
\isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse
of the \isa{Suc} function
@@ -1332,7 +1349,14 @@
We know nothing about what
\isa{inv~Suc} returns when applied to zero. The proof above still treats
\isa{SOME} as a definite description, since it only reasons about
-situations in which the value is described uniquely. To go further is
+situations in which the value is described uniquely. Indeed, \isa{SOME}
+satisfies this rule:
+\begin{isabelle}
+\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \
+\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
+\rulenamedx{some_equality}
+\end{isabelle}
+To go further is
tricky and requires rules such as these:
\begin{isabelle}
P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
@@ -1382,7 +1406,7 @@
This rule is seldom used for that purpose --- it can cause exponential
blow-up --- but it is occasionally used as an introduction rule
for~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%%
-\index{Hilbert's $\varepsilon$-operator|)}
+\index{description operators|)}
\section{Some Proofs That Fail}
--- a/doc-src/TutorialI/Sets/sets.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Fri Aug 03 18:04:55 2001 +0200
@@ -892,7 +892,8 @@
formulations are all complicated. However, often a relation
is well-founded by construction. HOL provides
theorems concerning ways of constructing a well-founded relation. The
-most familiar way is to specify a \bfindex{measure function}~\isa{f} into
+most familiar way is to specify a
+\index{measure functions}\textbf{measure function}~\isa{f} into
the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$;
we write this particular relation as
\isa{measure~f}.
--- a/doc-src/TutorialI/Trie/Trie.thy Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/Trie/Trie.thy Fri Aug 03 18:04:55 2001 +0200
@@ -12,6 +12,7 @@
datatype ('a,'v)trie = Trie "'v option" "('a * ('a,'v)trie)list";
text{*\noindent
+\index{datatypes!and nested recursion}%
The first component is the optional value, the second component the
association list of subtries. This is an example of nested recursion involving products,
which is fine because products are datatypes as well.
@@ -100,11 +101,11 @@
txt{*\noindent
Our plan is to induct on @{term as}; hence the remaining variables are
quantified. From the definitions it is clear that induction on either
-@{term as} or @{term bs} is required. The choice of @{term as} is merely
+@{term as} or @{term bs} is required. The choice of @{term as} is
guided by the intuition that simplification of @{term lookup} might be easier
if @{term update} has already been simplified, which can only happen if
@{term as} is instantiated.
-The start of the proof is completely conventional:
+The start of the proof is conventional:
*};
apply(induct_tac as, auto);
@@ -123,6 +124,7 @@
done
text{*\noindent
+\index{subgoal numbering}%
All methods ending in @{text tac} take an optional first argument that
specifies the range of subgoals they are applied to, where @{text"[!]"} means
all subgoals, i.e.\ @{text"[1-3]"} in our case. Individual subgoal numbers,
@@ -133,8 +135,7 @@
proof states are invisible, and we rely on the (possibly brittle) magic of
@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
of the induction up in such a way that case distinction on @{term bs} makes
-sense and solves the proof. Chapter~\ref{ch:Isar} shows you how to write readable
-and stable proofs.
+sense and solves the proof.
\begin{exercise}
Modify @{term update} (and its type) such that it allows both insertion and
--- a/doc-src/TutorialI/fp.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/fp.tex Fri Aug 03 18:04:55 2001 +0200
@@ -155,7 +155,7 @@
\index{datatypes|(}%
Inductive datatypes are part of almost every non-trivial application of HOL.
-First we take another look at a very important example, the datatype of
+First we take another look at an important example, the datatype of
lists, before we turn to datatypes in general. The section closes with a
case study.
@@ -307,18 +307,19 @@
\chapter{More Functional Programming}
-The purpose of this chapter is to deepen the reader's understanding of the
+The purpose of this chapter is to deepen your understanding of the
concepts encountered so far and to introduce advanced forms of datatypes and
recursive functions. The first two sections give a structured presentation of
theorem proving by simplification ({\S}\ref{sec:Simplification}) and discuss
-important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). They can
-be skipped by readers less interested in proofs. They are followed by a case
-study, a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
+important heuristics for induction ({\S}\ref{sec:InductionHeuristics}). You can
+skip them if you are not planning to perform proofs yourself.
+We then present a case
+study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
datatypes, including those involving function spaces, are covered in
-{\S}\ref{sec:advanced-datatypes}, which closes with another case study, search
-trees (``tries''). Finally we introduce \isacommand{recdef}, a very general
-form of recursive function definition which goes well beyond what
-\isacommand{primrec} allows ({\S}\ref{sec:recdef}).
+{\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
+trees (``tries''). Finally we introduce \isacommand{recdef}, a general
+form of recursive function definition that goes well beyond
+\isacommand{primrec} ({\S}\ref{sec:recdef}).
\section{Simplification}
@@ -326,21 +327,21 @@
\index{simplification|(}
So far we have proved our theorems by \isa{auto}, which simplifies
-\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
-that it did not need to so far. However, when you go beyond toy examples, you
+all subgoals. In fact, \isa{auto} can do much more than that.
+To go beyond toy examples, you
need to understand the ingredients of \isa{auto}. This section covers the
method that \isa{auto} always applies first, simplification.
Simplification is one of the central theorem proving tools in Isabelle and
-many other systems. The tool itself is called the \bfindex{simplifier}. The
-purpose of this section is to introduce the many features of the simplifier.
-Anybody intending to perform proofs in HOL should read this section. Later on
-({\S}\ref{sec:simplification-II}) we explain some more advanced features and a
+many other systems. The tool itself is called the \textbf{simplifier}.
+This section introduces the many features of the simplifier
+and is required reading if you intend to perform proofs. Later on,
+{\S}\ref{sec:simplification-II} explains some more advanced features and a
little bit of how the simplifier works. The serious student should read that
-section as well, in particular in order to understand what happened if things
-do not simplify as expected.
+section as well, in particular to understand why the simplifier did
+something unexpected.
-\subsection{What is Simplification}
+\subsection{What is Simplification?}
In its most basic form, simplification means repeated application of
equations from left to right. For example, taking the rules for \isa{\at}
@@ -350,10 +351,16 @@
(0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[]
\end{ttbox}
This is also known as \bfindex{term rewriting}\indexbold{rewriting} and the
-equations are referred to as \textbf{rewrite rules}\indexbold{rewrite rule}.
+equations are referred to as \bfindex{rewrite rules}.
``Rewriting'' is more honest than ``simplification'' because the terms do not
necessarily become simpler in the process.
+The simplifier proves arithmetic goals as described in
+{\S}\ref{sec:nat} above. Arithmetic expressions are simplified using built-in
+procedures that go beyond mere rewrite rules. New simplification procedures
+can be coded and installed, but they are definitely not a matter for this
+tutorial.
+
\input{Misc/document/simp.tex}
\index{simplification|)}
@@ -407,16 +414,16 @@
Fortunately, a limited form of recursion
involving function spaces is permitted: the recursive type may occur on the
right of a function arrow, but never on the left. Hence the above can of worms
-is ruled out but the following example of a potentially infinitely branching tree is
-accepted:
+is ruled out but the following example of a potentially
+\index{infinitely branching trees}%
+infinitely branching tree is accepted:
\smallskip
\input{Datatype/document/Fundata.tex}
-\bigskip
If you need nested recursion on the left of a function arrow, there are
alternatives to pure HOL\@. In the Logic for Computable Functions
-(LCF), types like
+(\rmindex{LCF}), types like
\begin{isabelle}
\isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
\end{isabelle}
@@ -424,7 +431,7 @@
\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
expressing the type of \emph{continuous} functions.
There is even a version of LCF on top of HOL,
-called HOLCF~\cite{MuellerNvOS99}.
+called \rmindex{HOLCF}~\cite{MuellerNvOS99}.
\index{datatype@\isacommand {datatype} (command)|)}
\index{primrec@\isacommand {primrec} (command)|)}
@@ -432,6 +439,7 @@
\subsection{Case Study: Tries}
\label{sec:Trie}
+\index{tries|(}%
Tries are a classic search tree data structure~\cite{Knuth3-75} for fast
indexing with strings. Figure~\ref{fig:trie} gives a graphical example of a
trie containing the words ``all'', ``an'', ``ape'', ``can'', ``car'' and
@@ -482,6 +490,7 @@
nodes do not carry any value. This distinction is modeled with the help
of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
\input{Trie/document/Trie.tex}
+\index{tries|)}
\section{Total Recursive Functions}
\label{sec:recdef}
@@ -503,12 +512,12 @@
\input{Recdef/document/termination.tex}
-\subsection{Simplification with Recdef}
+\subsection{Simplification and Recursive Functions}
\label{sec:recdef-simplification}
\input{Recdef/document/simplification.tex}
-\subsection{Induction}
+\subsection{Induction and Recursive Functions}
\index{induction!recursion|(}
\index{recursion induction|(}
--- a/doc-src/TutorialI/tutorial.ind Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/tutorial.ind Fri Aug 03 18:04:55 2001 +0200
@@ -48,6 +48,7 @@
\item \isa {abs} (constant), 135
\item \texttt {abs}, \bold{189}
\item absolute value, 135
+ \item \isa {add} (modifier), 27
\item \isa {add_assoc} (theorem), \bold{134}
\item \isa {add_commute} (theorem), \bold{134}
\item \isa {add_mult_distrib} (theorem), \bold{133}
@@ -68,7 +69,7 @@
\subitem of subgoal, 10
\subitem renaming, 66--67
\subitem reusing, 67
- \item \isa {auto} (method), 36, 76
+ \item \isa {auto} (method), 35, 76
\item \isa {axclass}, 144--150
\item axiom of choice, 70
\item axiomatic type classes, 144--150
@@ -78,7 +79,7 @@
\item \isacommand {back} (command), 62
\item \isa {Ball} (constant), 93
\item \isa {ballI} (theorem), \bold{92}
- \item \isa {best} (method), 75, 76
+ \item \isa {best} (method), 76
\item \isa {Bex} (constant), 93
\item \isa {bexE} (theorem), \bold{92}
\item \isa {bexI} (theorem), \bold{92}
@@ -87,7 +88,7 @@
\item binary trees, 16
\item binomial coefficients, 93
\item bisimulations, 100
- \item \isa {blast} (method), 72--75
+ \item \isa {blast} (method), 73--74, 76
\item \isa {bool} (type), 2, 3
\item boolean expressions example, 18--20
\item \isa {bspec} (theorem), \bold{92}
@@ -104,12 +105,13 @@
\item case distinctions, 17
\item case splits, \bold{29}
\item \isa {case_tac} (method), 17, 85
- \item \isa {clarify} (method), 74, 76
+ \item \isa {clarify} (method), 75, 76
\item \isa {clarsimp} (method), 75, 76
\item \isa {classical} (theorem), \bold{57}
\item coinduction, \bold{100}
\item \isa {Collect} (constant), 93
\item \isa {comp_def} (theorem), \bold{96}
+ \item compiling expressions example, 34--36
\item \isa {Compl_iff} (theorem), \bold{90}
\item complement
\subitem of a set, 89
@@ -119,6 +121,8 @@
\item conclusion
\subitem of subgoal, 10
\item conditional expressions, \see{\isa{if} expressions}{1}
+ \item conditional simplification rules, 29
+ \item \isa {cong} (attribute), 158
\item congruence rules, \bold{157}
\item \isa {conjE} (theorem), \bold{55}
\item \isa {conjI} (theorem), \bold{52}
@@ -133,13 +137,17 @@
\indexspace
- \item \isacommand {datatype} (command), 7, 36--42
+ \item \isacommand {datatype} (command), 7, 36--41
\item datatypes, 15--20
+ \subitem and nested recursion, 38
+ \subitem mutually recursive, 36
\item \isacommand {defer} (command), 14, 84
\item Definitional Approach, 24
\item definitions, \bold{23}
\subitem unfolding, \bold{28}
\item \isacommand {defs} (command), 23
+ \item \isa {del} (modifier), 27
+ \item description operators, 69--71
\item descriptions
\subitem definite, 69
\subitem indefinite, 70
@@ -151,7 +159,7 @@
\item \isa {disjCI} (theorem), \bold{58}
\item \isa {disjE} (theorem), \bold{54}
\item \isa {div} (symbol), 21
- \item divides relation, 68, 78, 85--87, 134
+ \item divides relation, 68, 79, 85--88, 134
\item division
\subitem by negative numbers, 135
\subitem by zero, 134
@@ -179,7 +187,7 @@
\item \isa {equalityI} (theorem), \bold{90}
\item \isa {erule} (method), 54
\item \isa {erule_tac} (method), 60
- \item Euclid's algorithm, 85--87
+ \item Euclid's algorithm, 85--88
\item even numbers
\subitem defining inductively, 111--115
\item \texttt {EX}, \bold{189}
@@ -196,7 +204,8 @@
\indexspace
\item \isa {False} (constant), 3
- \item \isa {fast} (method), 75, 76
+ \item \isa {fast} (method), 76
+ \item Fibonacci function, 44
\item \isa {finite} (symbol), 93
\item \isa {Finites} (constant), 93
\item fixed points, 100
@@ -210,22 +219,24 @@
\item \isa {fst} (constant), 22
\item function types, 3
\item functions, 93--95
- \subitem total, 9, 45--50
+ \subitem total, 9, 44--50
\subitem underdefined, 165
\indexspace
- \item \isa {gcd} (constant), 76--78, 85--87
+ \item \isa {gcd} (constant), 77--78, 85--88
\item generalizing for induction, 113
+ \item generalizing induction formulae, 32
\item Girard, Jean-Yves, \fnote{55}
\item Gordon, Mike, 1
\item ground terms example, 119--124
\indexspace
- \item \isa {hd} (constant), 15
+ \item \isa {hd} (constant), 15, 35
\item higher-order pattern, \bold{159}
- \item Hilbert's $\varepsilon$-operator, 69--71
+ \item Hilbert's $\varepsilon$-operator, 70
+ \item HOLCF, 41
\item \isa {hypreal} (type), 137
\indexspace
@@ -237,8 +248,10 @@
\item identity function, \bold{94}
\item identity relation, \bold{96}
\item \isa {if} expressions, 3, 4
+ \subitem simplification of, 31
+ \subitem splitting of, 29
\item if-and-only-if, 3
- \item \isa {iff} (attribute), 73, 74, 86, 114
+ \item \isa {iff} (attribute), 74, 86, 114
\item \isa {iffD1} (theorem), \bold{78}
\item \isa {iffD2} (theorem), \bold{78}
\item image
@@ -253,16 +266,18 @@
\subitem recursion, 49--50
\subitem structural, 17
\subitem well-founded, 99
+ \item induction heuristics, 31--33
\item \isacommand {inductive} (command), 111
\item inductive definition
\subitem simultaneous, 125
\item inductive definitions, 111--129
\item \isacommand {inductive\_cases} (command), 115, 123
+ \item infinitely branching trees, 40
\item \isacommand{infixr} (annotation), 8
\item \isa {inj_on_def} (theorem), \bold{94}
\item injections, 94
\item \isa {insert} (constant), 91
- \item \isa {insert} (method), 80--82
+ \item \isa {insert} (method), 81--82
\item instance, \bold{145}
\item \texttt {INT}, \bold{189}
\item \texttt {Int}, \bold{189}
@@ -288,6 +303,7 @@
\item inverse image
\subitem of a function, 95
\subitem of a relation, 98
+ \item \isa {itrev} (constant), 32
\indexspace
@@ -296,6 +312,7 @@
\indexspace
\item $\lambda$ expressions, 3
+ \item LCF, 41
\item \isa {LEAST} (symbol), 21, 69
\item least number operator, \see{\protect\isa{LEAST}}{69}
\item \isacommand {lemma} (command), 11
@@ -304,15 +321,16 @@
\item \isa {length_induct}, \bold{172}
\item \isa {less_than} (constant), 98
\item \isa {less_than_iff} (theorem), \bold{98}
- \item \isa {let} (symbol), 29
- \item \isa {let} expressions, 3, 4
+ \item \isa {let} expressions, 3, 4, 29
+ \item \isa {Let_def} (theorem), 29
\item \isa {lex_prod_def} (theorem), \bold{99}
\item lexicographic product, \bold{99}, 160
\item {\texttt{lfp}}
\subitem applications of, \see{CTL}{100}
- \item linear arithmetic, 20--22, 31, 131
+ \item linear arithmetic, 20--22, 131
\item \isa {List} (theory), 15
\item \isa {list} (type), 2, 7, 15
+ \item \isa {list.split} (theorem), 30
\item \isa {lists_mono} (theorem), \bold{121}
\item Lowe, Gavin, 178--179
@@ -345,9 +363,9 @@
\item Needham-Schroeder protocol, 177--179
\item negation, 57--59
\item \isa {Nil} (constant), 7
- \item \isa {no_asm}, \bold{27}
- \item \isa {no_asm_simp}, \bold{27}
- \item \isa {no_asm_use}, \bold{28}
+ \item \isa {no_asm} (modifier), 27
+ \item \isa {no_asm_simp} (modifier), 27
+ \item \isa {no_asm_use} (modifier), 27
\item non-standard reals, 137
\item \isa {None} (constant), \bold{22}
\item \isa {notE} (theorem), \bold{57}
@@ -361,8 +379,9 @@
\item \isa {O} (symbol), 96
\item \texttt {o}, \bold{189}
\item \isa {o_def} (theorem), \bold{94}
- \item \isa {OF} (attribute), 78--79
- \item \isa {of} (attribute), 77, 79
+ \item \isa {OF} (attribute), 79--80
+ \item \isa {of} (attribute), 77, 80
+ \item \isa {only} (modifier), 27
\item \isacommand {oops} (command), 11
\item \isa {option} (type), \bold{22}
\item ordered rewriting, \bold{158}
@@ -377,16 +396,16 @@
\item pattern, higher-order, \bold{159}
\item PDL, 102--105
\item permutative rewrite rule, \bold{158}
- \item \isacommand {pr} (command), 14, 83
+ \item \isacommand {pr} (command), 14, 84
\item \isacommand {prefer} (command), 14, 84
\item primitive recursion, \see{recursion, primitive}{1}
- \item \isacommand {primrec} (command), 8, 16, 36--42
+ \item \isacommand {primrec} (command), 8, 16, 36--41
\item product type, \see{pairs and tuples}{1}
\item Proof General, \bold{5}
\item proof state, 10
\item proofs
\subitem abandoning, \bold{11}
- \subitem examples of failing, 71--72
+ \subitem examples of failing, 71--73
\item protocols
\subitem security, 177--187
@@ -411,10 +430,10 @@
\item \isa {Real} (theory), 137
\item \isa {real} (type), 136--137
\item real numbers, 136--137
- \item \isacommand {recdef} (command), 45--50, 98, 160--168
+ \item \isacommand {recdef} (command), 44--50, 98, 160--168
\subitem and numeric literals, 132
\item \isa {recdef_cong} (attribute), 164
- \item \isa {recdef_simp} (attribute), 47
+ \item \isa {recdef_simp} (attribute), 46
\item \isa {recdef_wf} (attribute), 162
\item \isacommand {record} (command), 140
\item \isa {record_split} (method), 143
@@ -429,10 +448,11 @@
\item relations, 95--98
\subitem well-founded, 98--99
\item \isa {rename_tac} (method), 66--67
- \item \isa {rev} (constant), 8--12
- \item rewrite rule, \bold{26}
+ \item \isa {rev} (constant), 8--12, 32
+ \item rewrite rule
\subitem permutative, \bold{158}
- \item rewriting, \bold{26}
+ \item rewrite rules, \bold{25}
+ \item rewriting, \bold{25}
\subitem ordered, \bold{158}
\item \isa {rotate_tac} (method), 28
\item \isa {rtrancl_refl} (theorem), \bold{96}
@@ -445,7 +465,7 @@
\indexspace
\item \isa {safe} (method), 75, 76
- \item safe rules, \bold{73}
+ \item safe rules, \bold{74}
\item \isa {set} (type), 2, 89
\item set comprehensions, 91--92
\item \isa {set_ext} (theorem), \bold{90}
@@ -457,33 +477,39 @@
\item \isa {show_types} (flag), 3, 14
\item \isa {simp} (attribute), 9, 26
\item \isa {simp} (method), \bold{26}
- \item \isa {simp_all} (method), 26, 36
- \item simplification, 25--32, 157--160
- \subitem of let-expressions, 29
+ \item \isa {simp} del (attribute), 26
+ \item \isa {simp_all} (method), 26, 35
+ \item simplification, 25--31, 157--160
+ \subitem of \isa{let}-expressions, 29
\subitem ordered, \bold{158}
\subitem with definitions, 28
\subitem with/of assumptions, 27
- \item simplification rule, \bold{26}, 159--160
- \item \isa {simplified} (attribute), 77, 79
- \item simplifier, \bold{25}
+ \item simplification rule, 159--160
+ \item simplification rules, 26
+ \subitem adding and deleting, 27
+ \item \isa {simplified} (attribute), 77, 80
\item \isa {size} (constant), 15
\item \isa {snd} (constant), 22
- \item \isa {SOME} (symbol), 69
+ \item \isa {SOME} (symbol), 70
\item \texttt {SOME}, \bold{189}
\item \isa {Some} (constant), \bold{22}
- \item \isa {some_equality} (theorem), \bold{69}
+ \item \isa {some_equality} (theorem), \bold{70}
\item \isa {someI} (theorem), \bold{70}
\item \isa {someI2} (theorem), \bold{70}
\item \isa {someI_ex} (theorem), \bold{71}
\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 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 \isa {subgoal_tac} (method), 81, 82
+ \item \isa {subgoal_tac} (method), 82
\item subgoals, 10
\item subset relation, \bold{90}
\item \isa {subsetD} (theorem), \bold{90}
@@ -493,19 +519,21 @@
\item \isa {Suc} (constant), 20
\item \isa {surj_def} (theorem), \bold{94}
\item surjections, 94
- \item \isa {sym} (theorem), \bold{77}
+ \item \isa {sym} (theorem), \bold{78}
\item syntax, 4, 9
\item syntax translations, 24
\indexspace
- \item tacticals, 82--83
+ \item tacticals, 83
\item tactics, 10
\item \isacommand {term} (command), 14
- \item term rewriting, \bold{26}
+ \item term rewriting, \bold{25}
\item termination, \see{functions, total}{1}
\item terms, 3
- \item \isa {THEN} (attribute), \bold{77}, 79, 86
+ \item \isa {THE} (symbol), 69
+ \item \isa {the_equality} (theorem), \bold{69}
+ \item \isa {THEN} (attribute), \bold{78}, 80, 86
\item \isacommand {theorem} (command), \bold{9}, 11
\item theories, 2
\subitem abandoning, \bold{14}
@@ -518,6 +546,7 @@
\item tracing the simplifier, \bold{31}
\item \isa {trancl_trans} (theorem), \bold{97}
\item \isacommand {translations} (command), 24
+ \item tries, 41--44
\item \isa {True} (constant), 3
\item tuples, \see{pairs and tuples}{1}
\item \isacommand {typ} (command), 14
@@ -550,7 +579,7 @@
\item \isa {Union_iff} (theorem), \bold{92}
\item \isa {unit} (type), 22
\item unknowns, 4, \bold{52}
- \item unsafe rules, \bold{73}
+ \item unsafe rules, \bold{74}
\item updating a function, \bold{93}
\indexspace
--- a/doc-src/TutorialI/tutorial.tex Thu Jul 26 18:23:38 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex Fri Aug 03 18:04:55 2001 +0200
@@ -30,7 +30,7 @@
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
-\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
+\author{Tobias Nipkow and Lawrence C. Paulson\\[1ex]
Technische Universit{\"a}t M{\"u}nchen \\
Institut f{\"u}r Informatik \\[1ex]
University of Cambridge\\