nipkow@10225: %
nipkow@10225: \begin{isabellebody}%
nipkow@10225: \def\isabellecontext{Star}%
nipkow@10225: %
nipkow@10225: \isamarkupsection{The transitive and reflexive closure}
nipkow@10225: %
nipkow@10225: \begin{isamarkuptext}%
nipkow@10225: A perfect example of an inductive definition is the transitive, reflexive
nipkow@10225: closure of a relation. This concept was already introduced in
nipkow@10225: \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
nipkow@10225: the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
nipkow@10225: fixpoint because at that point in the theory hierarchy
nipkow@10225: inductive definitions are not yet available. But now they are:%
nipkow@10225: \end{isamarkuptext}%
nipkow@10225: \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: \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
nipkow@10225: \isakeyword{intros}\isanewline
nipkow@10225: trc{\isacharunderscore}refl{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
nipkow@10225: 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: \isanewline
nipkow@10225: \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: \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
nipkow@10225: \isanewline
nipkow@10225: \isacommand{lemma}\ step{\isadigit{2}}{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
nipkow@10225: \ \ {\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: \isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10225: \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10225: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}step{\isacharparenright}\isanewline
nipkow@10225: \isacommand{done}\isanewline
nipkow@10225: \isanewline
nipkow@10225: \isacommand{lemma}\ trc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
nipkow@10225: \ \ {\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: \isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10225: \ \isacommand{apply}\ blast\isanewline
nipkow@10225: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ step{\isadigit{2}}{\isacharparenright}\isanewline
nipkow@10225: \isacommand{done}\isanewline
nipkow@10225: \isanewline
nipkow@10225: \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: \isacommand{inductive}\ {\isachardoublequote}trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
nipkow@10225: \isakeyword{intros}\isanewline
nipkow@10225: {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
nipkow@10225: {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ trc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
nipkow@10225: {\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: \isanewline
nipkow@10225: \isanewline
nipkow@10225: \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: \isacommand{apply}{\isacharparenleft}rule\ iffI{\isacharparenright}\isanewline
nipkow@10225: \ \isacommand{apply}{\isacharparenleft}erule\ trc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10225: \ \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10225: \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
nipkow@10225: \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isacharunderscore}trans{\isacharparenright}\isanewline
nipkow@10225: \isacommand{apply}{\isacharparenleft}erule\ trc{\isachardot}induct{\isacharparenright}\isanewline
nipkow@10225: \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
nipkow@10225: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
nipkow@10225: \isacommand{done}\isanewline
nipkow@10225: \end{isabellebody}%
nipkow@10225: %%% Local Variables:
nipkow@10225: %%% mode: latex
nipkow@10225: %%% TeX-master: "root"
nipkow@10225: %%% End: