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 ***
     1 (*<*)theory Star = Main:(*>*)

     2

     3 section{*The reflexive transitive closure*}

     4

     5 text{*\label{sec:rtc}

     6 Many inductive definitions define proper relations rather than merely set

     7 like @{term even}. A perfect example is the

     8 reflexive transitive closure of a relation. This concept was already

     9 introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was

    10 defined as a least fixed point because inductive definitions were not yet

    11 available. But now they are:

    12 *}

    13

    14 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)

    15 inductive "r*"

    16 intros

    17 rtc_refl[iff]:  "(x,x) \<in> r*"

    18 rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

    19

    20 text{*\noindent

    21 The function @{term rtc} is annotated with concrete syntax: instead of

    22 @{text"rtc r"} we can read and write @{term"r*"}. The actual definition

    23 consists of two rules. Reflexivity is obvious and is immediately given the

    24 @{text iff} attribute to increase automation. The

    25 second rule, @{thm[source]rtc_step}, says that we can always add one more

    26 @{term r}-step to the left. Although we could make @{thm[source]rtc_step} an

    27 introduction rule, this is dangerous: the recursion in the second premise

    28 slows down and may even kill the automatic tactics.

    29

    30 The above definition of the concept of reflexive transitive closure may

    31 be sufficiently intuitive but it is certainly not the only possible one:

    32 for a start, it does not even mention transitivity explicitly.

    33 The rest of this section is devoted to proving that it is equivalent to

    34 the standard'' definition. We start with a simple lemma:

    35 *}

    36

    37 lemma [intro]: "(x,y) : r \<Longrightarrow> (x,y) \<in> r*"

    38 by(blast intro: rtc_step);

    39

    40 text{*\noindent

    41 Although the lemma itself is an unremarkable consequence of the basic rules,

    42 it has the advantage that it can be declared an introduction rule without the

    43 danger of killing the automatic tactics because @{term"r*"} occurs only in

    44 the conclusion and not in the premise. Thus some proofs that would otherwise

    45 need @{thm[source]rtc_step} can now be found automatically. The proof also

    46 shows that @{text blast} is quite able to handle @{thm[source]rtc_step}. But

    47 some of the other automatic tactics are more sensitive, and even @{text

    48 blast} can be lead astray in the presence of large numbers of rules.

    49

    50 To prove transitivity, we need rule induction, i.e.\ theorem

    51 @{thm[source]rtc.induct}:

    52 @{thm[display]rtc.induct}

    53 It says that @{text"?P"} holds for an arbitrary pair @{text"(?xb,?xa) \<in>

    54 ?r*"} if @{text"?P"} is preserved by all rules of the inductive definition,

    55 i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the

    56 premises. In general, rule induction for an $n$-ary inductive relation $R$

    57 expects a premise of the form $(x@1,\dots,x@n) \in R$.

    58

    59 Now we turn to the inductive proof of transitivity:

    60 *}

    61

    62 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"

    63 apply(erule rtc.induct)

    64

    65 txt{*\noindent

    66 Unfortunately, even the resulting base case is a problem

    67 @{subgoals[display,indent=0,goals_limit=1]}

    68 and maybe not what you had expected. We have to abandon this proof attempt.

    69 To understand what is going on, let us look again at @{thm[source]rtc.induct}.

    70 In the above application of @{text erule}, the first premise of

    71 @{thm[source]rtc.induct} is unified with the first suitable assumption, which

    72 is @{term"(x,y) \<in> r*"} rather than @{term"(y,z) \<in> r*"}. Although that

    73 is what we want, it is merely due to the order in which the assumptions occur

    74 in the subgoal, which it is not good practice to rely on. As a result,

    75 @{text"?xb"} becomes @{term x}, @{text"?xa"} becomes

    76 @{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus

    77 yielding the above subgoal. So what went wrong?

    78

    79 When looking at the instantiation of @{text"?P"} we see that it does not

    80 depend on its second parameter at all. The reason is that in our original

    81 goal, of the pair @{term"(x,y)"} only @{term x} appears also in the

    82 conclusion, but not @{term y}. Thus our induction statement is too

    83 weak. Fortunately, it can easily be strengthened:

    84 transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*}

    85 (*<*)oops(*>*)

    86 lemma rtc_trans[rule_format]:

    87   "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"

    88

    89 txt{*\noindent

    90 This is not an obscure trick but a generally applicable heuristic:

    91 \begin{quote}\em

    92 Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,

    93 pull all other premises containing any of the $x@i$ into the conclusion

    94 using $\longrightarrow$.

    95 \end{quote}

    96 A similar heuristic for other kinds of inductions is formulated in

    97 \S\ref{sec:ind-var-in-prems}. The @{text rule_format} directive turns

    98 @{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. Thus in the end we obtain the original

    99 statement of our lemma.

   100 *}

   101

   102 apply(erule rtc.induct)

   103

   104 txt{*\noindent

   105 Now induction produces two subgoals which are both proved automatically:

   106 @{subgoals[display,indent=0]}

   107 *}

   108

   109  apply(blast);

   110 apply(blast intro: rtc_step);

   111 done

   112

   113 text{*

   114 Let us now prove that @{term"r*"} is really the reflexive transitive closure

   115 of @{term r}, i.e.\ the least reflexive and transitive

   116 relation containing @{term r}. The latter is easily formalized

   117 *}

   118

   119 consts rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"

   120 inductive "rtc2 r"

   121 intros

   122 "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"

   123 "(x,x) \<in> rtc2 r"

   124 "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"

   125

   126 text{*\noindent

   127 and the equivalence of the two definitions is easily shown by the obvious rule

   128 inductions:

   129 *}

   130

   131 lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"

   132 apply(erule rtc2.induct);

   133   apply(blast);

   134  apply(blast);

   135 apply(blast intro: rtc_trans);

   136 done

   137

   138 lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"

   139 apply(erule rtc.induct);

   140  apply(blast intro: rtc2.intros);

   141 apply(blast intro: rtc2.intros);

   142 done

   143

   144 text{*

   145 So why did we start with the first definition? Because it is simpler. It

   146 contains only two rules, and the single step rule is simpler than

   147 transitivity.  As a consequence, @{thm[source]rtc.induct} is simpler than

   148 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should

   149 certainly pick the simplest induction schema available for any concept.

   150 Hence @{term rtc} is the definition of choice.

   151

   152 \begin{exercise}\label{ex:converse-rtc-step}

   153 Show that the converse of @{thm[source]rtc_step} also holds:

   154 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}

   155 \end{exercise}

   156 \begin{exercise}

   157 Repeat the development of this section, but starting with a definition of

   158 @{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown

   159 in exercise~\ref{ex:converse-rtc-step}.

   160 \end{exercise}

   161 *}

   162 (*<*)

   163 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"

   164 apply(erule rtc.induct);

   165  apply blast;

   166 apply(blast intro:rtc_step)

   167 done

   168

   169 end

   170 (*>*)