doc-src/TutorialI/Inductive/Star.thy

 (*<*)theory Star = Main:(*>*)
 
 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"
 intros
 "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"
 "(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:
 *}
 
 lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
 apply(erule rtc2.induct);

 apply(erule rtc.induct);
  apply(blast intro: rtc2.intros);
 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
+(*>*)