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 \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
nipkow@10225
    15
inductive "r*"
nipkow@10225
    16
intros
nipkow@10242
    17
rtc_refl[iff]:  "(x,x) \<in> r*"
nipkow@10242
    18
rtc_step:       "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> 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 \<Longrightarrow> (x,y) \<in> 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) \<in>
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: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> 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) \<in> r*"} rather than @{term"(y,z) \<in> 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) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> 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"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}. 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 \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
nipkow@10237
   120
inductive "rtc2 r"
nipkow@10225
   121
intros
nipkow@10237
   122
"(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"
nipkow@10237
   123
"(x,x) \<in> rtc2 r"
nipkow@10237
   124
"\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> 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) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> 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) \<in> r* \<Longrightarrow> (x,y) \<in> 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* \<Longrightarrow> (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
(*>*)