# HG changeset patch # User nipkow # Date 971882358 -7200 # Node ID 028f54cd2cc9691ff5a25a2062c2a1f457b0109c # Parent e0428c2778f1c43c13e812180bf0157e3fb48bdf *** empty log message *** diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/CTL/CTL.thy --- 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 \ 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(*>*) diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/CTL/PDL.thy --- 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"\T. mc f \ M^-1 ^^ T"} is the least set +fixed point (@{term lfp}) of @{term"\T. mc f \ 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: diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/CTL/document/CTL.tex --- 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}% diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/CTL/document/PDL.tex --- 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:% diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/AB.thy --- 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 diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/Star.thy --- 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 \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) +consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) inductive "r*" intros -rtc_refl[intro!]: "(x,x) \ r*" -rtc_step: "\ (x,y) \ r*; (y,z) \ r \ \ (x,z) \ r*" +rtc_refl[iff]: "(x,x) \ r*" +rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ 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 \ (x,y) \ r*" by(blast intro: rtc_step); -lemma step2[rule_format]: - "(y,z) \ r* \ (x,y) \ r \ (x,z) \ 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: + "\ (x,y) \ r*; (y,z) \ r* \ \ (x,z) \ 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) \ r* \ (y,z) \ r* \ (x,z) \ 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"\"} back into @{text"\"}. 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) \ r* \ \z. (y,z) \ r* \ (x,z) \ 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 \ 'a)set \ ('a \ 'a)set" inductive "rtc2 r" @@ -41,8 +124,8 @@ "(x,x) \ rtc2 r" "\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ 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* \ (y,z) : r --> (x,z) : r*" +apply(erule rtc.induct); + apply blast; +apply(blast intro:rtc_step) +done + +end +(*>*) diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/document/AB.tex --- 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 diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/document/Star.tex --- 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 diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Inductive/inductive.tex --- 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} diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Misc/AdvancedInd.thy --- 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"\"}.} diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- 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: diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/Recdef/Nested1.thy --- 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 \ nat"} is an auxiliary function automatically defined by Isabelle diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/appendix.tex --- 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$\$\\ -\indexboldpos{\isasymin}{$HOL3Set}& -\ttindexboldpos{:}{$HOL3Set} & +\indexboldpos{\isasymin}{$HOL3Set0a}& +\ttindexboldpos{:}{$HOL3Set0b} & \verb$\$\\ -? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason -\verb$~:$\index{$HOL3Set@\verb$~:$|bold} & +\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} & +\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} & \verb$\$\\ -\indexboldpos{\isasymsubseteq}{$HOL3Set}& -\verb$<=$ & -\verb$\$\\ -\indexboldpos{\isasymunion}{$HOL3Set}& +\indexboldpos{\isasymsubseteq}{$HOL3Set0e}& +\verb$<=$ & \verb$\$\\ +\indexboldpos{\isasymsubset}{$HOL3Set0f}& +\verb$<$ & \verb$\$\\ +\indexboldpos{\isasymunion}{$HOL3Set1}& \ttindexbold{Un} & \verb$\$\\ -\indexboldpos{\isasyminter}{$HOL3Set}& +\indexboldpos{\isasyminter}{$HOL3Set1}& \ttindexbold{Int} & \verb$\$\\ -\indexboldpos{\isasymUnion}{$HOL3Set}& +\indexboldpos{\isasymUnion}{$HOL3Set2}& \ttindexbold{UN}, \ttindexbold{Union} & \verb$\$\\ -\indexboldpos{\isasymInter}{$HOL3Set}& +\indexboldpos{\isasymInter}{$HOL3Set2}& \ttindexbold{INT}, \ttindexbold{Inter} & \verb$\$\\ \hline diff -r e0428c2778f1 -r 028f54cd2cc9 doc-src/TutorialI/todo.tobias --- 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