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