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