--- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Sun Nov 26 10:48:38 2000 +0100
@@ -21,7 +21,7 @@
\noindent
This is almost the same as in the boolean expression case study in
\S\ref{sec:boolex}, except that what used to be called \isa{Var} is now
-called \isa{formula{\isachardot}Atom}.
+called \isa{Atom}.
The meaning of these formulae is given by saying which formula is true in
which state:%
--- a/doc-src/TutorialI/Inductive/AB.thy Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy Sun Nov 26 10:48:38 2000 +0100
@@ -303,6 +303,6 @@
similar to the other cases (which are automatic in Isabelle). We conclude
that the authors are at least cavalier about this point and may even have
overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pencil-and-paper proofs, once analysed in detail. *}
+atypical for pen-and-paper proofs, once analysed in detail. *}
(*<*)end(*>*)
--- a/doc-src/TutorialI/Inductive/Even.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Even.tex Sun Nov 26 10:48:38 2000 +0100
@@ -157,6 +157,7 @@
\end{isabelle}
\subsection{Generalization and rule induction}
+\label{sec:gen-rule-induction}
Everybody knows that when before applying induction we often must generalize
the induction formula. This step is just as important with rule induction,
--- a/doc-src/TutorialI/Inductive/Star.thy Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Star.thy Sun Nov 26 10:48:38 2000 +0100
@@ -3,14 +3,12 @@
section{*The reflexive transitive closure*}
text{*\label{sec:rtc}
-{\bf Say something about inductive relations as opposed to sets? Or has that
-been said already? If not, explain induction!}
-
-A perfect example of an inductive definition is the reflexive transitive
-closure of a relation. This concept was already introduced in
-\S\ref{sec:Relations}, where the operator @{text"^*"} was
-defined as a least fixed point because
-inductive definitions were not yet available. But now they are:
+Many inductive definitions define proper relations rather than merely set
+like @{term even}. A perfect example is the
+reflexive transitive closure of a relation. This concept was already
+introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was
+defined as a least fixed point because inductive definitions were not yet
+available. But now they are:
*}
consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
@@ -21,13 +19,13 @@
text{*\noindent
The function @{term rtc} is annotated with concrete syntax: instead of
-@{text"rtc r"} we can read and write {term"r*"}. The actual definition
-consists of two rules. Reflexivity is obvious and is immediately declared an
-equivalence rule. Thus the automatic tools will apply it automatically. The
+@{text"rtc r"} we can read and write @{term"r*"}. The actual definition
+consists of two rules. Reflexivity is obvious and is immediately given the
+@{text iff} attribute to increase automation. The
second rule, @{thm[source]rtc_step}, says that we can always add one more
@{term r}-step to the left. Although we could make @{thm[source]rtc_step} an
-introduction rule, this is dangerous: the recursion slows down and may
-even kill the automatic tactics.
+introduction rule, this is dangerous: the recursion in the second premise
+slows down and may even kill the automatic tactics.
The above definition of the concept of reflexive transitive closure may
be sufficiently intuitive but it is certainly not the only possible one:
@@ -45,38 +43,44 @@
danger of killing the automatic tactics because @{term"r*"} occurs only in
the conclusion and not in the premise. Thus some proofs that would otherwise
need @{thm[source]rtc_step} can now be found automatically. The proof also
-shows that @{term blast} is quite able to handle @{thm[source]rtc_step}. But
+shows that @{text blast} is quite able to handle @{thm[source]rtc_step}. But
some of the other automatic tactics are more sensitive, and even @{text
blast} can be lead astray in the presence of large numbers of rules.
-Let us now turn to transitivity. It should be a consequence of the definition.
+To prove transitivity, we need rule induction, i.e.\ theorem
+@{thm[source]rtc.induct}:
+@{thm[display]rtc.induct}
+It says that @{text"?P"} holds for an arbitrary pair @{text"(?xb,?xa) \<in>
+?r*"} if @{text"?P"} is preserved by all rules of the inductive definition,
+i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the
+premises. In general, rule induction for an $n$-ary inductive relation $R$
+expects a premise of the form $(x@1,\dots,x@n) \in R$.
+
+Now we turn to the inductive proof of transitivity:
*}
-lemma rtc_trans:
- "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
-
-txt{*\noindent
-The proof starts canonically by rule induction:
-*}
-
+lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
apply(erule rtc.induct)
txt{*\noindent
-However, even the resulting base case is a problem
+Unfortunately, even the resulting base case is a problem
@{subgoals[display,indent=0,goals_limit=1]}
and maybe not what you had expected. We have to abandon this proof attempt.
-To understand what is going on,
-let us look at the induction rule @{thm[source]rtc.induct}:
-\[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]
-When applying this rule, $x$ becomes @{term x}, $y$ becomes
-@{term y} and $P~x~y$ becomes @{prop"(x,z) : r*"}, thus
+To understand what is going on, let us look again at @{thm[source]rtc.induct}.
+In the above application of @{text erule}, the first premise of
+@{thm[source]rtc.induct} is unified with the first suitable assumption, which
+is @{term"(x,y) \<in> r*"} rather than @{term"(y,z) \<in> r*"}. Although that
+is what we want, it is merely due to the order in which the assumptions occur
+in the subgoal, which it is not good practice to rely on. As a result,
+@{text"?xb"} becomes @{term x}, @{text"?xa"} becomes
+@{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus
yielding the above subgoal. So what went wrong?
-When looking at the instantiation of $P~x~y$ we see
-that $P$ does not depend on its second parameter at
-all. The reason is that in our original goal, of the pair @{term"(x,y)"} only
-@{term x} appears also in the conclusion, but not @{term y}. Thus our
-induction statement is too weak. Fortunately, it can easily be strengthened:
+When looking at the instantiation of @{text"?P"} we see that it does not
+depend on its second parameter at all. The reason is that in our original
+goal, of the pair @{term"(x,y)"} only @{term x} appears also in the
+conclusion, but not @{term y}. Thus our induction statement is too
+weak. Fortunately, it can easily be strengthened:
transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*}
(*<*)oops(*>*)
lemma rtc_trans[rule_format]:
@@ -145,10 +149,15 @@
certainly pick the simplest induction schema available for any concept.
Hence @{term rtc} is the definition of choice.
-\begin{exercise}
+\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of @{thm[source]rtc_step} also holds:
@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
\end{exercise}
+\begin{exercise}
+Repeat the development of this section, but starting with a definition of
+@{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown
+in exercise~\ref{ex:converse-rtc-step}.
+\end{exercise}
*}
(*<*)
lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
--- a/doc-src/TutorialI/Inductive/document/AB.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Sun Nov 26 10:48:38 2000 +0100
@@ -276,7 +276,7 @@
similar to the other cases (which are automatic in Isabelle). We conclude
that the authors are at least cavalier about this point and may even have
overlooked the slight difficulty lurking in the omitted cases. This is not
-atypical for pencil-and-paper proofs, once analysed in detail.%
+atypical for pen-and-paper proofs, once analysed in detail.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Star.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Sun Nov 26 10:48:38 2000 +0100
@@ -7,14 +7,12 @@
%
\begin{isamarkuptext}%
\label{sec:rtc}
-{\bf Say something about inductive relations as opposed to sets? Or has that
-been said already? If not, explain induction!}
-
-A perfect example of an inductive definition is the reflexive transitive
-closure of a relation. This concept was already introduced in
-\S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
-defined as a least fixed point because
-inductive definitions were not yet available. But now they are:%
+Many inductive definitions define proper relations rather than merely set
+like \isa{even}. A perfect example is the
+reflexive transitive closure of a relation. This concept was already
+introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
+defined as a least fixed point because inductive definitions were not yet
+available. But now they are:%
\end{isamarkuptext}%
\isacommand{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
\isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
@@ -24,13 +22,13 @@
\begin{isamarkuptext}%
\noindent
The function \isa{rtc} is annotated with concrete syntax: instead of
-\isa{rtc\ r} we can read and write {term"r*"}. The actual definition
-consists of two rules. Reflexivity is obvious and is immediately declared an
-equivalence rule. Thus the automatic tools will apply it automatically. The
+\isa{rtc\ r} we can read and write \isa{r{\isacharasterisk}}. The actual definition
+consists of two rules. Reflexivity is obvious and is immediately given the
+\isa{iff} attribute to increase automation. The
second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
-introduction rule, this is dangerous: the recursion slows down and may
-even kill the automatic tactics.
+introduction rule, this is dangerous: the recursion in the second premise
+slows down and may even kill the automatic tactics.
The above definition of the concept of reflexive transitive closure may
be sufficiently intuitive but it is certainly not the only possible one:
@@ -50,34 +48,44 @@
shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But
some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules.
-Let us now turn to transitivity. It should be a consequence of the definition.%
+To prove transitivity, we need rule induction, i.e.\ theorem
+\isa{rtc{\isachardot}induct}:
+\begin{isabelle}%
+\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ {\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%
+\end{isabelle}
+It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
+i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the
+premises. In general, rule induction for an $n$-ary inductive relation $R$
+expects a premise of the form $(x@1,\dots,x@n) \in R$.
+
+Now we turn to the inductive proof of transitivity:%
\end{isamarkuptext}%
-\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
-\begin{isamarkuptxt}%
-\noindent
-The proof starts canonically by rule induction:%
-\end{isamarkuptxt}%
+\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
-However, even the resulting base case is a problem
+Unfortunately, even the resulting base case is a problem
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}
and maybe not what you had expected. We have to abandon this proof attempt.
-To understand what is going on,
-let us look at the induction rule \isa{rtc{\isachardot}induct}:
-\[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]
-When applying this rule, $x$ becomes \isa{x}, $y$ becomes
-\isa{y} and $P~x~y$ becomes \isa{{\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
+To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.
+In the above application of \isa{erule}, the first premise of
+\isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which
+is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that
+is what we want, it is merely due to the order in which the assumptions occur
+in the subgoal, which it is not good practice to rely on. As a result,
+\isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes
+\isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
yielding the above subgoal. So what went wrong?
-When looking at the instantiation of $P~x~y$ we see
-that $P$ does not depend on its second parameter at
-all. The reason is that in our original goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only
-\isa{x} appears also in the conclusion, but not \isa{y}. Thus our
-induction statement is too weak. Fortunately, it can easily be strengthened:
+When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not
+depend on its second parameter at all. The reason is that in our original
+goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the
+conclusion, but not \isa{y}. Thus our induction statement is too
+weak. Fortunately, it can easily be strengthened:
transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
\end{isamarkuptxt}%
\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
@@ -145,11 +153,16 @@
certainly pick the simplest induction schema available for any concept.
Hence \isa{rtc} is the definition of choice.
-\begin{exercise}
+\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}
+\end{exercise}
+\begin{exercise}
+Repeat the development of this section, but starting with a definition of
+\isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown
+in exercise~\ref{ex:converse-rtc-step}.
\end{exercise}%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/Inductive/inductive.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/Inductive/inductive.tex Sun Nov 26 10:48:38 2000 +0100
@@ -15,10 +15,11 @@
\input{Inductive/Even}
\input{Inductive/document/Star}
-\input{Inductive/document/AB}
\section{Advanced inductive definitions}
\input{Inductive/Advanced}
+\input{Inductive/document/AB}
+
\index{inductive definition|)}
\index{*inductive|)}
--- a/doc-src/TutorialI/todo.tobias Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/todo.tobias Sun Nov 26 10:48:38 2000 +0100
@@ -1,7 +1,6 @@
Implementation
==============
-Hide global names like Node.
Why is comp needed in addition to op O?
Explain in syntax section!
@@ -31,7 +30,9 @@
Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?
-defs with = and pattern matching
+proper mutual simplification
+
+defs with = and pattern matching??
Minor fixes in the tutorial
@@ -48,7 +49,7 @@
Explain typographic conventions?
Orderings on numbers (with hint that it is overloaded):
->, >=, and bounded quantifers ALL x<y, <=, todo: x>y, x>=y.
+bounded quantifers ALL x<y, <=.
an example of induction: !y. A --> B --> C ??
@@ -71,6 +72,10 @@
Appendix with list functions.
+Move section on rule inversion further to the front, and combine
+\subsection{Universal quantifiers in introduction rules}
+\subsection{Continuing the `ground terms' example}
+
Minor additions to the tutorial, unclear where
==============================================
--- a/doc-src/TutorialI/tutorial.tex Fri Nov 24 16:49:27 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex Sun Nov 26 10:48:38 2000 +0100
@@ -1,6 +1,6 @@
\documentclass{article}
\newif\ifremarks
-\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
+\remarksfalse %TRUE causes remarks to be displayed (as marginal notes)
\usepackage{cl2emono-modified,isabelle,isabellesym}
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
\usepackage{proof,amsmath}