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