doc-src/TutorialI/Inductive/Star.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10520 bb9dfcc87951 child 10898 b086f4e1722f permissions -rw-r--r--
*** empty log message ***
 nipkow@10225  1 (*<*)theory Star = Main:(*>*)  nipkow@10225  2 nipkow@10237  3 section{*The reflexive transitive closure*}  nipkow@10225  4 nipkow@10242  5 text{*\label{sec:rtc}  nipkow@10520  6 Many inductive definitions define proper relations rather than merely set  nipkow@10520  7 like @{term even}. A perfect example is the  nipkow@10520  8 reflexive transitive closure of a relation. This concept was already  nipkow@10520  9 introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was  nipkow@10520  10 defined as a least fixed point because inductive definitions were not yet  nipkow@10520  11 available. But now they are:  nipkow@10225  12 *}  nipkow@10225  13 nipkow@10242  14 consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999)  nipkow@10225  15 inductive "r*"  nipkow@10225  16 intros  nipkow@10242  17 rtc_refl[iff]: "(x,x) \ r*"  nipkow@10242  18 rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*"  nipkow@10242  19 nipkow@10242  20 text{*\noindent  nipkow@10242  21 The function @{term rtc} is annotated with concrete syntax: instead of  nipkow@10520  22 @{text"rtc r"} we can read and write @{term"r*"}. The actual definition  nipkow@10520  23 consists of two rules. Reflexivity is obvious and is immediately given the  nipkow@10520  24 @{text iff} attribute to increase automation. The  nipkow@10363  25 second rule, @{thm[source]rtc_step}, says that we can always add one more  nipkow@10363  26 @{term r}-step to the left. Although we could make @{thm[source]rtc_step} an  nipkow@10520  27 introduction rule, this is dangerous: the recursion in the second premise  nipkow@10520  28 slows down and may even kill the automatic tactics.  nipkow@10242  29 nipkow@10242  30 The above definition of the concept of reflexive transitive closure may  nipkow@10242  31 be sufficiently intuitive but it is certainly not the only possible one:  nipkow@10242  32 for a start, it does not even mention transitivity explicitly.  nipkow@10242  33 The rest of this section is devoted to proving that it is equivalent to  nipkow@10242  34 the standard'' definition. We start with a simple lemma:  nipkow@10242  35 *}  nipkow@10225  36 nipkow@10225  37 lemma [intro]: "(x,y) : r \ (x,y) \ r*"  nipkow@10237  38 by(blast intro: rtc_step);  nipkow@10225  39 nipkow@10242  40 text{*\noindent  nipkow@10242  41 Although the lemma itself is an unremarkable consequence of the basic rules,  nipkow@10242  42 it has the advantage that it can be declared an introduction rule without the  nipkow@10242  43 danger of killing the automatic tactics because @{term"r*"} occurs only in  nipkow@10242  44 the conclusion and not in the premise. Thus some proofs that would otherwise  nipkow@10242  45 need @{thm[source]rtc_step} can now be found automatically. The proof also  nipkow@10520  46 shows that @{text blast} is quite able to handle @{thm[source]rtc_step}. But  nipkow@10242  47 some of the other automatic tactics are more sensitive, and even @{text  nipkow@10242  48 blast} can be lead astray in the presence of large numbers of rules.  nipkow@10242  49 nipkow@10520  50 To prove transitivity, we need rule induction, i.e.\ theorem  nipkow@10520  51 @{thm[source]rtc.induct}:  nipkow@10520  52 @{thm[display]rtc.induct}  nipkow@10520  53 It says that @{text"?P"} holds for an arbitrary pair @{text"(?xb,?xa) \  nipkow@10520  54 ?r*"} if @{text"?P"} is preserved by all rules of the inductive definition,  nipkow@10520  55 i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the  nipkow@10520  56 premises. In general, rule induction for an $n$-ary inductive relation $R$  nipkow@10520  57 expects a premise of the form $(x@1,\dots,x@n) \in R$.  nipkow@10520  58 nipkow@10520  59 Now we turn to the inductive proof of transitivity:  nipkow@10242  60 *}  nipkow@10242  61 nipkow@10520  62 lemma rtc_trans: "\ (x,y) \ r*; (y,z) \ r* \ \ (x,z) \ r*"  nipkow@10363  63 apply(erule rtc.induct)  nipkow@10363  64 nipkow@10363  65 txt{*\noindent  nipkow@10520  66 Unfortunately, even the resulting base case is a problem  nipkow@10363  67 @{subgoals[display,indent=0,goals_limit=1]}  nipkow@10242  68 and maybe not what you had expected. We have to abandon this proof attempt.  nipkow@10520  69 To understand what is going on, let us look again at @{thm[source]rtc.induct}.  nipkow@10520  70 In the above application of @{text erule}, the first premise of  nipkow@10520  71 @{thm[source]rtc.induct} is unified with the first suitable assumption, which  nipkow@10520  72 is @{term"(x,y) \ r*"} rather than @{term"(y,z) \ r*"}. Although that  nipkow@10520  73 is what we want, it is merely due to the order in which the assumptions occur  nipkow@10520  74 in the subgoal, which it is not good practice to rely on. As a result,  nipkow@10520  75 @{text"?xb"} becomes @{term x}, @{text"?xa"} becomes  nipkow@10520  76 @{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus  nipkow@10242  77 yielding the above subgoal. So what went wrong?  nipkow@10242  78 nipkow@10520  79 When looking at the instantiation of @{text"?P"} we see that it does not  nipkow@10520  80 depend on its second parameter at all. The reason is that in our original  nipkow@10520  81 goal, of the pair @{term"(x,y)"} only @{term x} appears also in the  nipkow@10520  82 conclusion, but not @{term y}. Thus our induction statement is too  nipkow@10520  83 weak. Fortunately, it can easily be strengthened:  nipkow@10363  84 transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*}  nipkow@10363  85 (*<*)oops(*>*)  nipkow@10242  86 lemma rtc_trans[rule_format]:  nipkow@10242  87  "(x,y) \ r* \ (y,z) \ r* \ (x,z) \ r*"  nipkow@10242  88 nipkow@10242  89 txt{*\noindent  nipkow@10242  90 This is not an obscure trick but a generally applicable heuristic:  nipkow@10242  91 \begin{quote}\em  nipkow@10242  92 Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,  nipkow@10242  93 pull all other premises containing any of the $x@i$ into the conclusion  nipkow@10242  94 using $\longrightarrow$.  nipkow@10242  95 \end{quote}  nipkow@10242  96 A similar heuristic for other kinds of inductions is formulated in  nipkow@10242  97 \S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns  nipkow@10242  98 @{text"\"} back into @{text"\"}. Thus in the end we obtain the original  nipkow@10242  99 statement of our lemma.  nipkow@10242  100 *}  nipkow@10242  101 nipkow@10363  102 apply(erule rtc.induct)  nipkow@10363  103 nipkow@10363  104 txt{*\noindent  nipkow@10363  105 Now induction produces two subgoals which are both proved automatically:  nipkow@10363  106 @{subgoals[display,indent=0]}  nipkow@10363  107 *}  nipkow@10363  108 nipkow@10225  109  apply(blast);  nipkow@10237  110 apply(blast intro: rtc_step);  nipkow@10225  111 done  nipkow@10225  112 nipkow@10242  113 text{*  nipkow@10242  114 Let us now prove that @{term"r*"} is really the reflexive transitive closure  nipkow@10242  115 of @{term r}, i.e.\ the least reflexive and transitive  nipkow@10242  116 relation containing @{term r}. The latter is easily formalized  nipkow@10242  117 *}  nipkow@10225  118 nipkow@10237  119 consts rtc2 :: "('a \ 'a)set \ ('a \ 'a)set"  nipkow@10237  120 inductive "rtc2 r"  nipkow@10225  121 intros  nipkow@10237  122 "(x,y) \ r \ (x,y) \ rtc2 r"  nipkow@10237  123 "(x,x) \ rtc2 r"  nipkow@10237  124 "\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ rtc2 r"  nipkow@10225  125 nipkow@10242  126 text{*\noindent  nipkow@10242  127 and the equivalence of the two definitions is easily shown by the obvious rule  nipkow@10237  128 inductions:  nipkow@10237  129 *}  nipkow@10225  130 nipkow@10237  131 lemma "(x,y) \ rtc2 r \ (x,y) \ r*"  nipkow@10237  132 apply(erule rtc2.induct);  nipkow@10225  133  apply(blast);  nipkow@10237  134  apply(blast);  nipkow@10237  135 apply(blast intro: rtc_trans);  nipkow@10237  136 done  nipkow@10237  137 nipkow@10237  138 lemma "(x,y) \ r* \ (x,y) \ rtc2 r"  nipkow@10237  139 apply(erule rtc.induct);  nipkow@10237  140  apply(blast intro: rtc2.intros);  nipkow@10237  141 apply(blast intro: rtc2.intros);  nipkow@10225  142 done  nipkow@10225  143 nipkow@10242  144 text{*  nipkow@10242  145 So why did we start with the first definition? Because it is simpler. It  nipkow@10242  146 contains only two rules, and the single step rule is simpler than  nipkow@10242  147 transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than  nipkow@10242  148 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should  nipkow@10242  149 certainly pick the simplest induction schema available for any concept.  nipkow@10242  150 Hence @{term rtc} is the definition of choice.  nipkow@10242  151 nipkow@10520  152 \begin{exercise}\label{ex:converse-rtc-step}  nipkow@10242  153 Show that the converse of @{thm[source]rtc_step} also holds:  nipkow@10242  154 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}  nipkow@10242  155 \end{exercise}  nipkow@10520  156 \begin{exercise}  nipkow@10520  157 Repeat the development of this section, but starting with a definition of  nipkow@10520  158 @{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown  nipkow@10520  159 in exercise~\ref{ex:converse-rtc-step}.  nipkow@10520  160 \end{exercise}  nipkow@10242  161 *}  nipkow@10242  162 (*<*)  nipkow@10242  163 lemma rtc_step2[rule_format]: "(x,y) : r* \ (y,z) : r --> (x,z) : r*"  nipkow@10242  164 apply(erule rtc.induct);  nipkow@10242  165  apply blast;  nipkow@10242  166 apply(blast intro:rtc_step)  nipkow@10242  167 done  nipkow@10242  168 nipkow@10242  169 end  nipkow@10242  170 (*>*)