--- a/doc-src/TutorialI/CTL/CTL.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Wed Oct 18 17:19:18 2000 +0200
@@ -67,7 +67,7 @@
text{*\noindent
Because @{term af} is monotone in its second argument (and also its first, but
-that is irrelevant) @{term"af A"} has a least fixpoint:
+that is irrelevant) @{term"af A"} has a least fixed point:
*};
lemma mono_af: "mono(af A)";
@@ -108,7 +108,7 @@
txt{*\noindent
In contrast to the analogous property for @{term EF}, and just
-for a change, we do not use fixpoint induction but a weaker theorem,
+for a change, we do not use fixed point induction but a weaker theorem,
@{thm[source]lfp_lowerbound}:
@{thm[display]lfp_lowerbound[of _ "S",no_vars]}
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
@@ -403,7 +403,7 @@
set operations are easily implemented. Only @{term lfp} requires a little thought.
Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
@{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
-a fixpoint is reached. It is actually possible to generate executable functional programs
+a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.
*}
(*<*)end(*>*)
--- a/doc-src/TutorialI/CTL/PDL.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/CTL/PDL.thy Wed Oct 18 17:19:18 2000 +0200
@@ -65,7 +65,7 @@
postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
converse of a relation and the application of a relation to a set. Thus
@{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least
-fixpoint (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set
+fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set
@{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
find it hard to see that @{term"mc(EF f)"} contains exactly those states from
which there is a path to a state where @{term f} is true, do not worry---that
@@ -80,7 +80,7 @@
done
text{*\noindent
-in order to make sure it really has a least fixpoint.
+in order to make sure it really has a least fixed point.
Now we can relate model checking and semantics. For the @{text EF} case we need
a separate lemma:
--- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 18 17:19:18 2000 +0200
@@ -44,7 +44,7 @@
\begin{isamarkuptext}%
\noindent
Because \isa{af} is monotone in its second argument (and also its first, but
-that is irrelevant) \isa{af\ A} has a least fixpoint:%
+that is irrelevant) \isa{af\ A} has a least fixed point:%
\end{isamarkuptext}%
\isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -60,7 +60,7 @@
\begin{isamarkuptxt}%
\noindent
In contrast to the analogous property for \isa{EF}, and just
-for a change, we do not use fixpoint induction but a weaker theorem,
+for a change, we do not use fixed point induction but a weaker theorem,
\isa{lfp{\isacharunderscore}lowerbound}:
\begin{isabelle}%
\ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
@@ -310,7 +310,7 @@
set operations are easily implemented. Only \isa{lfp} requires a little thought.
Fortunately the HOL library proves that in the case of finite sets and a monotone \isa{F},
\isa{lfp\ F} can be computed by iterated application of \isa{F} to \isa{{\isacharbraceleft}{\isacharbraceright}} until
-a fixpoint is reached. It is actually possible to generate executable functional programs
+a fixed point is reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\end{isamarkuptext}%
\end{isabellebody}%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Wed Oct 18 17:19:18 2000 +0200
@@ -64,7 +64,7 @@
postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the
converse of a relation and the application of a relation to a set. Thus
\isa{M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
-fixpoint (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
+fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
which there is a path to a state where \isa{f} is true, do not worry---that
@@ -78,7 +78,7 @@
\isacommand{done}%
\begin{isamarkuptext}%
\noindent
-in order to make sure it really has a least fixpoint.
+in order to make sure it really has a least fixed point.
Now we can relate model checking and semantics. For the \isa{EF} case we need
a separate lemma:%
--- a/doc-src/TutorialI/Inductive/AB.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy Wed Oct 18 17:19:18 2000 +0200
@@ -1,8 +1,8 @@
(*<*)theory AB = Main:(*>*)
-section{*A context free grammar*}
+section{*Case study: A context free grammar*}
-text{*
+text{*\label{sec:CFG}
Grammars are nothing but shorthands for inductive definitions of nonterminals
which represent sets of strings. For example, the production
$A \to B c$ is short for
@@ -43,7 +43,8 @@
text{*\noindent
The above productions are recast as a \emph{simultaneous} inductive
-definition of @{term S}, @{term A} and @{term B}:
+definition\index{inductive definition!simultaneous}
+of @{term S}, @{term A} and @{term B}:
*}
inductive S A B
--- a/doc-src/TutorialI/Inductive/Star.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy Wed Oct 18 17:19:18 2000 +0200
@@ -2,37 +2,120 @@
section{*The reflexive transitive closure*}
-text{*
+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:rtrancl}, but it was not shown how it is defined. In fact,
the operator @{text"^*"} is not defined inductively but via a least
-fixpoint because at that point in the theory hierarchy
+fixed point because at that point in the theory hierarchy
inductive definitions are not yet available. But now they are:
*}
-consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
+consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
inductive "r*"
intros
-rtc_refl[intro!]: "(x,x) \<in> r*"
-rtc_step: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+rtc_refl[iff]: "(x,x) \<in> r*"
+rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
+
+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
+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.
+
+The above definition of the concept of reflexive transitive closure may
+be sufficiently intuitive but it is certainly not the only possible one:
+for a start, it does not even mention transitivity explicitly.
+The rest of this section is devoted to proving that it is equivalent to
+the ``standard'' definition. We start with a simple lemma:
+*}
lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"
by(blast intro: rtc_step);
-lemma step2[rule_format]:
- "(y,z) \<in> r* \<Longrightarrow> (x,y) \<in> r \<longrightarrow> (x,z) \<in> r*"
-apply(erule rtc.induct)
+text{*\noindent
+Although the lemma itself is an unremarkable consequence of the basic rules,
+it has the advantage that it can be declared an introduction rule without the
+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
+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.
+*}
+
+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:
+*}
+
+apply(erule rtc.induct)(*pr(latex xsymbols symbols);*)(*<*)oops(*>*)
+text{*\noindent
+However, 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 @{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
+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:
+transfer the additional premise @{prop"(y,z):r*"} into the conclusion:
+*}
+
+lemma rtc_trans[rule_format]:
+ "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
+
+txt{*\noindent
+This is not an obscure trick but a generally applicable heuristic:
+\begin{quote}\em
+Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
+pull all other premises containing any of the $x@i$ into the conclusion
+using $\longrightarrow$.
+\end{quote}
+A similar heuristic for other kinds of inductions is formulated in
+\S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns
+@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original
+statement of our lemma.
+
+Now induction produces two subgoals which are both proved automatically:
+\begin{isabelle}
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
+\end{isabelle}
+*}
+
+apply(erule rtc.induct)(*pr(latex xsymbols symbols);*)
apply(blast);
apply(blast intro: rtc_step);
done
-lemma rtc_trans[rule_format]:
- "(x,y) \<in> r* \<Longrightarrow> \<forall>z. (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
-apply(erule rtc.induct)
- apply blast;
-apply(blast intro: step2);
-done
+text{*
+Let us now prove that @{term"r*"} is really the reflexive transitive closure
+of @{term r}, i.e.\ the least reflexive and transitive
+relation containing @{term r}. The latter is easily formalized
+*}
consts rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
inductive "rtc2 r"
@@ -41,8 +124,8 @@
"(x,x) \<in> rtc2 r"
"\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"
-text{*
-The equivalence of the two definitions is easily shown by the obvious rule
+text{*\noindent
+and the equivalence of the two definitions is easily shown by the obvious rule
inductions:
*}
@@ -59,4 +142,25 @@
apply(blast intro: rtc2.intros);
done
-(*<*)end(*>*)
+text{*
+So why did we start with the first definition? Because it is simpler. It
+contains only two rules, and the single step rule is simpler than
+transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than
+@{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should
+certainly pick the simplest induction schema available for any concept.
+Hence @{term rtc} is the definition of choice.
+
+\begin{exercise}
+Show that the converse of @{thm[source]rtc_step} also holds:
+@{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
+\end{exercise}
+*}
+(*<*)
+lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
+apply(erule rtc.induct);
+ apply blast;
+apply(blast intro:rtc_step)
+done
+
+end
+(*>*)
--- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Oct 18 17:19:18 2000 +0200
@@ -2,9 +2,10 @@
\begin{isabellebody}%
\def\isabellecontext{AB}%
%
-\isamarkupsection{A context free grammar}
+\isamarkupsection{Case study: A context free grammar}
%
\begin{isamarkuptext}%
+\label{sec:CFG}
Grammars are nothing but shorthands for inductive definitions of nonterminals
which represent sets of strings. For example, the production
$A \to B c$ is short for
@@ -42,7 +43,8 @@
\begin{isamarkuptext}%
\noindent
The above productions are recast as a \emph{simultaneous} inductive
-definition of \isa{S}, \isa{A} and \isa{B}:%
+definition\index{inductive definition!simultaneous}
+of \isa{S}, \isa{A} and \isa{B}:%
\end{isamarkuptext}%
\isacommand{inductive}\ S\ A\ B\isanewline
\isakeyword{intros}\isanewline
--- a/doc-src/TutorialI/Inductive/document/Star.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Wed Oct 18 17:19:18 2000 +0200
@@ -5,36 +5,113 @@
\isamarkupsection{The reflexive transitive closure}
%
\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:rtrancl}, but it was not shown how it is defined. In fact,
the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
-fixpoint because at that point in the theory hierarchy
+fixed point because at that point in the theory hierarchy
inductive definitions are 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{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
\isakeyword{intros}\isanewline
-rtc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
-rtc{\isacharunderscore}step{\isacharcolon}\ {\isachardoublequote}{\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}{\isachardoublequote}\isanewline
-\isanewline
+rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
+rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
+\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
+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.
+
+The above definition of the concept of reflexive transitive closure may
+be sufficiently intuitive but it is certainly not the only possible one:
+for a start, it does not even mention transitivity explicitly.
+The rest of this section is devoted to proving that it is equivalent to
+the ``standard'' definition. We start with a simple lemma:%
+\end{isamarkuptext}%
\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
-\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
-\isanewline
-\isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+Although the lemma itself is an unremarkable consequence of the basic rules,
+it has the advantage that it can be declared an introduction rule without the
+danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in
+the conclusion and not in the premise. Thus some proofs that would otherwise
+need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also
+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.%
+\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{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+However, 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
+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:
+transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
+\begin{isamarkuptxt}%
+\noindent
+This is not an obscure trick but a generally applicable heuristic:
+\begin{quote}\em
+Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
+pull all other premises containing any of the $x@i$ into the conclusion
+using $\longrightarrow$.
+\end{quote}
+A similar heuristic for other kinds of inductions is formulated in
+\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
+\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
+statement of our lemma.
+
+Now induction produces two subgoals which are both proved automatically:
+\begin{isabelle}
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
+\ \ \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
+\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
+\end{isabelle}%
+\end{isamarkuptxt}%
\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
-\isacommand{done}\isanewline
-\isanewline
-\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isasymforall}z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
-\ \isacommand{apply}\ blast\isanewline
-\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\isanewline
-\isacommand{done}\isanewline
-\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
+of \isa{r}, i.e.\ the least reflexive and transitive
+relation containing \isa{r}. The latter is easily formalized%
+\end{isamarkuptext}%
\isacommand{consts}\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
\isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
\isakeyword{intros}\isanewline
@@ -42,7 +119,8 @@
{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}%
\begin{isamarkuptext}%
-The equivalence of the two definitions is easily shown by the obvious rule
+\noindent
+and the equivalence of the two definitions is easily shown by the obvious rule
inductions:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
@@ -56,7 +134,22 @@
\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
-\isacommand{done}\isanewline
+\isacommand{done}%
+\begin{isamarkuptext}%
+So why did we start with the first definition? Because it is simpler. It
+contains only two rules, and the single step rule is simpler than
+transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than
+\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should
+certainly pick the simplest induction schema available for any concept.
+Hence \isa{rtc} is the definition of choice.
+
+\begin{exercise}
+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}%
+\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Inductive/inductive.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Inductive/inductive.tex Wed Oct 18 17:19:18 2000 +0200
@@ -1,4 +1,21 @@
\chapter{Inductively Defined Sets}
+\index{inductive definition|(}
+\index{*inductive|(}
+
+This chapter is dedicated to the most important definition principle after
+recursive functions and datatypes: inductively defined sets.
+
+We start with a simple example \ldots . A slightly more complicated example, the
+reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,
+some standard induction heuristics are discussed. To demonstrate the
+versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study
+from the realm of context-free grammars. The chapter closes with a discussion
+of advanced forms of inductive definitions.
\input{Inductive/document/Star}
\input{Inductive/document/AB}
+
+\index{inductive definition|)}
+\index{*inductive|)}
+
+\section{Advanced inductive definitions}
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Wed Oct 18 17:19:18 2000 +0200
@@ -34,13 +34,14 @@
\begin{isabelle}
\ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
\end{isabelle}
-We cannot prove this equality because we do not know what @{term"hd"} and
-@{term"last"} return when applied to @{term"[]"}.
+We cannot prove this equality because we do not know what @{term hd} and
+@{term last} return when applied to @{term"[]"}.
The point is that we have violated the above warning. Because the induction
-formula is only the conclusion, the occurrence of @{term"xs"} in the premises is
+formula is only the conclusion, the occurrence of @{term xs} in the premises is
not modified by induction. Thus the case that should have been trivial
-becomes unprovable. Fortunately, the solution is easy:
+becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
+heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
using @{text"\<longrightarrow>"}.}
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Oct 18 17:19:18 2000 +0200
@@ -41,7 +41,8 @@
The point is that we have violated the above warning. Because the induction
formula is only the conclusion, the occurrence of \isa{xs} in the premises is
not modified by induction. Thus the case that should have been trivial
-becomes unprovable. Fortunately, the solution is easy:
+becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar
+heuristic applies to rule inductions; see \S\ref{sec:rtc}.}
\begin{quote}
\emph{Pull all occurrences of the induction variable into the conclusion
using \isa{{\isasymlongrightarrow}}.}
@@ -268,18 +269,18 @@
\isacommand{by}{\isacharparenleft}insert\ induct{\isacharunderscore}lem{\isacharcomma}\ blast{\isacharparenright}%
\begin{isamarkuptext}%
Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{wellfounded
-induction}\indexbold{induction!wellfounded}\index{wellfounded
-induction|see{induction, wellfounded}} (\isa{wf{\isacharunderscore}induct}):
+inductions, \textbf{well-founded
+induction}\indexbold{induction!well-founded}\index{well-founded
+induction|see{induction, well-founded}} (\isa{wf{\isacharunderscore}induct}):
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}
-where \isa{wf\ r} means that the relation \isa{r} is wellfounded
-(see \S\ref{sec:wellfounded}).
+where \isa{wf\ r} means that the relation \isa{r} is well-founded
+(see \S\ref{sec:well-founded}).
For example, theorem \isa{nat{\isacharunderscore}less{\isacharunderscore}induct} can be viewed (and
derived) as a special case of \isa{wf{\isacharunderscore}induct} where
\isa{r} is \isa{{\isacharless}} on \isa{nat}. The details can be found in the HOL library.
-For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.%
+For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/Nested1.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Wed Oct 18 17:19:18 2000 +0200
@@ -21,7 +21,7 @@
Remember that function @{term size} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
-@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
+@{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"}
where @{term set} returns the set of elements of a list
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle
--- a/doc-src/TutorialI/appendix.tex Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/appendix.tex Wed Oct 18 17:19:18 2000 +0200
@@ -64,25 +64,26 @@
\indexboldpos{\isasymtimes}{$IsaFun}&
\ttindexboldpos{*}{$HOL2arithfun} &
\verb$\<times>$\\
-\indexboldpos{\isasymin}{$HOL3Set}&
-\ttindexboldpos{:}{$HOL3Set} &
+\indexboldpos{\isasymin}{$HOL3Set0a}&
+\ttindexboldpos{:}{$HOL3Set0b} &
\verb$\<in>$\\
-? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
-\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
+\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
+\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
\verb$\<notin>$\\
-\indexboldpos{\isasymsubseteq}{$HOL3Set}&
-\verb$<=$ &
-\verb$\<subseteq>$\\
-\indexboldpos{\isasymunion}{$HOL3Set}&
+\indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
+\verb$<=$ & \verb$\<subseteq>$\\
+\indexboldpos{\isasymsubset}{$HOL3Set0f}&
+\verb$<$ & \verb$\<subset>$\\
+\indexboldpos{\isasymunion}{$HOL3Set1}&
\ttindexbold{Un} &
\verb$\<union>$\\
-\indexboldpos{\isasyminter}{$HOL3Set}&
+\indexboldpos{\isasyminter}{$HOL3Set1}&
\ttindexbold{Int} &
\verb$\<inter>$\\
-\indexboldpos{\isasymUnion}{$HOL3Set}&
+\indexboldpos{\isasymUnion}{$HOL3Set2}&
\ttindexbold{UN}, \ttindexbold{Union} &
\verb$\<Union>$\\
-\indexboldpos{\isasymInter}{$HOL3Set}&
+\indexboldpos{\isasymInter}{$HOL3Set2}&
\ttindexbold{INT}, \ttindexbold{Inter} &
\verb$\<Inter>$\\
\hline
--- a/doc-src/TutorialI/todo.tobias Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/todo.tobias Wed Oct 18 17:19:18 2000 +0200
@@ -21,8 +21,6 @@
Add map_cong?? (upto 10% slower)
But we should install UN_cong and INT_cong too.
-recdef: funny behaviour with map (see email to Konrad.Slind, Recdef/Nested1)
-
defs with = and pattern matching
use arith_tac in recdef to solve termination conditions?
@@ -90,8 +88,8 @@
clarify, clarsimp (intro, elim?)
Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
-Where explained?
-Inductive also needs rule_format!
+Where explained? Should go into a separate section as Inductive needs it as
+well.
Where is "simplified" explained? Needed by Inductive/AB.thy
@@ -189,44 +187,6 @@
==============================================================
-Nested inductive datatypes: better recursion and induction
-
-Show how to derive simpler primrec functions using eg map. Text:
-
-Returning to the definition of \texttt{subst}, we have to admit that it does
-not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
-can directly be expressed as
-\begin{ttbox}
-\input{Datatype/appmap}\end{ttbox}
-Although Isabelle insists on the more verbose version, we can easily {\em
- prove} that the \texttt{map}-equation holds: simply by induction on
-\texttt{ts} followed by \texttt{Auto_tac}.
-lemma "subst s (App f ts) = App f (map (subst s) ts)";
-by(induct_tac ts, auto);
-
-Now explain how to remove old eqns from simpset by naming them.
-But: the new eqn only helps if the induction schema is also modified
-accordingly:
-
-val prems =
-Goal "[| !!v. P(Var v); !!f ts. (!!t. t : set ts ==> P t) ==> P(App f ts) |] \
-\ ==> P t & (!t: set ts. P t)";
-by(induct_tac "t ts" 1);
-brs prems 1;
-brs prems 1;
-by(Blast_tac 1);
-by(Simp_tac 1);
-by(Asm_simp_tac 1);
-
-Now the following exercise has an easy proof:
-
-\begin{exercise}
- Define a function \texttt{rev_term} of type \texttt{term -> term} that
- recursively reverses the order of arguments of all function symbols in a
- term. Prove that \texttt{rev_term(rev_term t) = t}.
-\end{exercise}
-
-==============================================================
Recdef:
nested recursion
@@ -237,10 +197,6 @@
Trie?
a case study?
-A separate subsection on recdef beyond measure, eg <*lex*> and psubset.
-Example: some finite fixpoint computation? MC, Grammar?
-How to modify wf-prover?
-
----------
Partial rekursive functions / Nontermination