|
nipkow@10225
|
1 |
%
|
|
nipkow@10225
|
2 |
\begin{isabellebody}%
|
|
nipkow@10225
|
3 |
\def\isabellecontext{Star}%
|
|
nipkow@10225
|
4 |
%
|
|
nipkow@10225
|
5 |
\isamarkupsection{The transitive and reflexive closure}
|
|
nipkow@10225
|
6 |
%
|
|
nipkow@10225
|
7 |
\begin{isamarkuptext}%
|
|
nipkow@10225
|
8 |
A perfect example of an inductive definition is the transitive, reflexive
|
|
nipkow@10225
|
9 |
closure of a relation. This concept was already introduced in
|
|
nipkow@10225
|
10 |
\S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
|
|
nipkow@10225
|
11 |
the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
|
|
nipkow@10225
|
12 |
fixpoint because at that point in the theory hierarchy
|
|
nipkow@10225
|
13 |
inductive definitions are not yet available. But now they are:%
|
|
nipkow@10225
|
14 |
\end{isamarkuptext}%
|
|
nipkow@10225
|
15 |
\isacommand{consts}\ trc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
|
|
nipkow@10225
|
16 |
\isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
17 |
\isakeyword{intros}\isanewline
|
|
nipkow@10225
|
18 |
trc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
19 |
trc{\isacharunderscore}step{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
20 |
\isanewline
|
|
nipkow@10225
|
21 |
\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
22 |
\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
|
|
nipkow@10225
|
23 |
\isanewline
|
|
nipkow@10225
|
24 |
\isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
|
|
nipkow@10225
|
25 |
\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
26 |
\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
|
|
nipkow@10225
|
27 |
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
|
nipkow@10225
|
28 |
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
|
|
nipkow@10225
|
29 |
\isacommand{done}\isanewline
|
|
nipkow@10225
|
30 |
\isanewline
|
|
nipkow@10225
|
31 |
\isacommand{lemma}\ trc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
|
|
nipkow@10225
|
32 |
\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ \ {\isasymLongrightarrow}\ {\isasymforall}z{\isachardot}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
33 |
\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
|
|
nipkow@10225
|
34 |
\ \isacommand{apply}\ blast\isanewline
|
|
nipkow@10225
|
35 |
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\isanewline
|
|
nipkow@10225
|
36 |
\isacommand{done}\isanewline
|
|
nipkow@10225
|
37 |
\isanewline
|
|
nipkow@10225
|
38 |
\isacommand{consts}\ trc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
39 |
\isacommand{inductive}\ {\isachardoublequote}trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
40 |
\isakeyword{intros}\isanewline
|
|
nipkow@10225
|
41 |
{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
42 |
{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
43 |
{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
44 |
\isanewline
|
|
nipkow@10225
|
45 |
\isanewline
|
|
nipkow@10225
|
46 |
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharparenright}{\isachardoublequote}\isanewline
|
|
nipkow@10225
|
47 |
\isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
|
|
nipkow@10225
|
48 |
\ \isacommand{apply}{\isacharparenleft}erule\ trc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
|
|
nipkow@10225
|
49 |
\ \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
|
nipkow@10225
|
50 |
\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
|
nipkow@10225
|
51 |
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}trans{\isacharparenright}\isanewline
|
|
nipkow@10225
|
52 |
\isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
|
|
nipkow@10225
|
53 |
\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
|
|
nipkow@10225
|
54 |
\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
|
|
nipkow@10225
|
55 |
\isacommand{done}\isanewline
|
|
nipkow@10225
|
56 |
\end{isabellebody}%
|
|
nipkow@10225
|
57 |
%%% Local Variables:
|
|
nipkow@10225
|
58 |
%%% mode: latex
|
|
nipkow@10225
|
59 |
%%% TeX-master: "root"
|
|
nipkow@10225
|
60 |
%%% End:
|