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 +(*>*)