src/Doc/Tutorial/Inductive/Star.thy
author desharna
Thu, 05 Aug 2021 17:43:16 +0200
changeset 74393 b9837b07684d
parent 69609 ff784d5a5bfb
permissions -rw-r--r--
fixed $ite syntax in TPTP THX generation
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
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    12
introduced in \S\ref{sec:Relations}, where the operator \<open>\<^sup>*\<close> 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
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    25
The function \<^term>\<open>rtc\<close> is annotated with concrete syntax: instead of
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    26
\<open>rtc r\<close> we can write \<^term>\<open>r*\<close>. 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
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    28
\<open>iff\<close> 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
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    30
\<^term>\<open>r\<close>-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
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    47
danger of killing the automatic tactics because \<^term>\<open>r*\<close> occurs only in
10242
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
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    50
shows that \<open>blast\<close> is able to handle @{thm[source]rtc_step}. But
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    51
some of the other automatic tactics are more sensitive, and even \<open>blast\<close> can be lead astray in the presence of large numbers of rules.
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    52
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    53
To prove transitivity, we need rule induction, i.e.\ theorem
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    54
@{thm[source]rtc.induct}:
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    55
@{thm[display]rtc.induct}
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    56
It says that \<open>?P\<close> holds for an arbitrary pair @{thm (prem 1) rtc.induct}
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    57
if \<open>?P\<close> is preserved by all rules of the inductive definition,
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    58
i.e.\ if \<open>?P\<close> holds for the conclusion provided it holds for the
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    59
premises. In general, rule induction for an $n$-ary inductive relation $R$
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    60
expects a premise of the form $(x@1,\dots,x@n) \in R$.
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    61
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    62
Now we turn to the inductive proof of transitivity:
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    63
\<close>
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    64
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    65
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
    66
apply(erule rtc.induct)
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
    67
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    68
txt\<open>\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11308
diff changeset
    69
Unfortunately, even the base case is a problem:
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
    70
@{subgoals[display,indent=0,goals_limit=1]}
11494
23a118849801 revisions and indexing
paulson
parents: 11308
diff changeset
    71
We have to abandon this proof attempt.
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    72
To understand what is going on, let us look again at @{thm[source]rtc.induct}.
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    73
In the above application of \<open>erule\<close>, the first premise of
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    74
@{thm[source]rtc.induct} is unified with the first suitable assumption, which
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    75
is \<^term>\<open>(x,y) \<in> r*\<close> rather than \<^term>\<open>(y,z) \<in> r*\<close>. Although that
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    76
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
    77
in the subgoal, which it is not good practice to rely on. As a result,
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    78
\<open>?xb\<close> becomes \<^term>\<open>x\<close>, \<open>?xa\<close> becomes
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    79
\<^term>\<open>y\<close> and \<open>?P\<close> becomes \<^term>\<open>\<lambda>u v. (u,z) \<in> r*\<close>, thus
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    80
yielding the above subgoal. So what went wrong?
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    81
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
    82
When looking at the instantiation of \<open>?P\<close> we see that it does not
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
    83
depend on its second parameter at all. The reason is that in our original
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    84
goal, of the pair \<^term>\<open>(x,y)\<close> only \<^term>\<open>x\<close> appears also in the
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    85
conclusion, but not \<^term>\<open>y\<close>. Thus our induction statement is too
27172
8236f13be95b correction
nipkow
parents: 23847
diff changeset
    86
general. Fortunately, it can easily be specialized:
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
    87
transfer the additional premise \<^prop>\<open>(y,z)\<in>r*\<close> into the conclusion:\<close>
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
    88
(*<*)oops(*>*)
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    89
lemma rtc_trans[rule_format]:
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    90
  "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    91
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    92
txt\<open>\noindent
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    93
This is not an obscure trick but a generally applicable heuristic:
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    94
\begin{quote}\em
11257
622331bbdb7f *** empty log message ***
nipkow
parents: 11147
diff changeset
    95
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
    96
pull all other premises containing any of the $x@i$ into the conclusion
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    97
using $\longrightarrow$.
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    98
\end{quote}
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
    99
A similar heuristic for other kinds of inductions is formulated in
69517
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
   100
\S\ref{sec:ind-var-in-prems}. The \<open>rule_format\<close> directive turns
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67613
diff changeset
   101
\<open>\<longrightarrow>\<close> back into \<open>\<Longrightarrow>\<close>: in the end we obtain the original
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   102
statement of our lemma.
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   103
\<close>
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   104
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
   105
apply(erule rtc.induct)
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
   106
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   107
txt\<open>\noindent
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
   108
Now induction produces two subgoals which are both proved automatically:
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
   109
@{subgoals[display,indent=0]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   110
\<close>
10363
6e8002c1790e *** empty log message ***
nipkow
parents: 10243
diff changeset
   111
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   112
 apply(blast)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   113
apply(blast intro: rtc_step)
10225
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   114
done
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   115
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   116
text\<open>
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
   117
Let us now prove that \<^term>\<open>r*\<close> is really the reflexive transitive closure
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
   118
of \<^term>\<open>r\<close>, i.e.\ the least reflexive and transitive
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
   119
relation containing \<^term>\<open>r\<close>. The latter is easily formalized
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   120
\<close>
10225
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   121
23733
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   122
inductive_set
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   123
  rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   124
  for r :: "('a \<times> 'a)set"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   125
where
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   126
  "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   127
| "(x,x) \<in> rtc2 r"
3f8ad7418e55 Adapted to new inductive definition package.
berghofe
parents: 17914
diff changeset
   128
| "\<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
   129
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   130
text\<open>\noindent
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   131
and the equivalence of the two definitions is easily shown by the obvious rule
10237
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   132
inductions:
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   133
\<close>
10225
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   134
10237
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   135
lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   136
apply(erule rtc2.induct)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   137
  apply(blast)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   138
 apply(blast)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   139
apply(blast intro: rtc_trans)
10237
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   140
done
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   141
875bf54b5d74 *** empty log message ***
nipkow
parents: 10225
diff changeset
   142
lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   143
apply(erule rtc.induct)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   144
 apply(blast intro: rtc2.intros)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   145
apply(blast intro: rtc2.intros)
10225
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   146
done
b9fd52525b69 *** empty log message ***
nipkow
parents:
diff changeset
   147
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   148
text\<open>
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   149
So why did we start with the first definition? Because it is simpler. It
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   150
contains only two rules, and the single step rule is simpler than
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   151
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
   152
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough
11147
d848c6693185 *** empty log message ***
nipkow
parents: 10898
diff changeset
   153
anyway, we should always pick the simplest induction schema available.
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
   154
Hence \<^term>\<open>rtc\<close> is the definition of choice.
11494
23a118849801 revisions and indexing
paulson
parents: 11308
diff changeset
   155
\index{reflexive transitive closure!defining inductively|)}
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   156
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
   157
\begin{exercise}\label{ex:converse-rtc-step}
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   158
Show that the converse of @{thm[source]rtc_step} also holds:
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67406
diff changeset
   159
@{prop[display]"[| (x,y) \<in> r*; (y,z) \<in> r |] ==> (x,z) \<in> r*"}
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   160
\end{exercise}
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
   161
\begin{exercise}
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
   162
Repeat the development of this section, but starting with a definition of
69609
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69517
diff changeset
   163
\<^term>\<open>rtc\<close> where @{thm[source]rtc_step} is replaced by its converse as shown
10520
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
   164
in exercise~\ref{ex:converse-rtc-step}.
bb9dfcc87951 *** empty log message ***
nipkow
parents: 10396
diff changeset
   165
\end{exercise}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
   166
\<close>
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   167
(*<*)
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 67406
diff changeset
   168
lemma rtc_step2[rule_format]: "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r \<longrightarrow> (x,z) \<in> r*"
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   169
apply(erule rtc.induct)
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
   170
 apply blast
12815
wenzelm
parents: 11494
diff changeset
   171
apply(blast intro: rtc_step)
10242
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   172
done
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   173
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   174
end
028f54cd2cc9 *** empty log message ***
nipkow
parents: 10237
diff changeset
   175
(*>*)