1.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex Sun Oct 21 19:48:19 2001 +0200
1.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Sun Oct 21 19:49:29 2001 +0200
1.3 @@ -1,9 +1,11 @@
1.4 %
1.5 \begin{isabellebody}%
1.6 \def\isabellecontext{Star}%
1.7 +\isamarkupfalse%
1.8 %
1.9 \isamarkupsection{The Reflexive Transitive Closure%
1.10 }
1.11 +\isamarkuptrue%
1.12 %
1.13 \begin{isamarkuptext}%
1.14 \label{sec:rtc}
1.15 @@ -17,11 +19,14 @@
1.16 defined as a least fixed point because inductive definitions were not yet
1.17 available. But now they are:%
1.18 \end{isamarkuptext}%
1.19 +\isamarkuptrue%
1.20 \isacommand{consts}\ rtc\ {\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
1.21 +\isamarkupfalse%
1.22 \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline
1.23 \isakeyword{intros}\isanewline
1.24 rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
1.25 -rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
1.26 +rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse%
1.27 +%
1.28 \begin{isamarkuptext}%
1.29 \noindent
1.30 The function \isa{rtc} is annotated with concrete syntax: instead of
1.31 @@ -39,8 +44,11 @@
1.32 The rest of this section is devoted to proving that it is equivalent to
1.33 the standard definition. We start with a simple lemma:%
1.34 \end{isamarkuptext}%
1.35 +\isamarkuptrue%
1.36 \isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
1.37 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
1.38 +\isamarkupfalse%
1.39 +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isamarkupfalse%
1.40 +%
1.41 \begin{isamarkuptext}%
1.42 \noindent
1.43 Although the lemma itself is an unremarkable consequence of the basic rules,
1.44 @@ -65,8 +73,11 @@
1.45
1.46 Now we turn to the inductive proof of transitivity:%
1.47 \end{isamarkuptext}%
1.48 +\isamarkuptrue%
1.49 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
1.50 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
1.51 +\isamarkupfalse%
1.52 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.53 +%
1.54 \begin{isamarkuptxt}%
1.55 \noindent
1.56 Unfortunately, even the base case is a problem:
1.57 @@ -91,8 +102,11 @@
1.58 weak. Fortunately, it can easily be strengthened:
1.59 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
1.60 \end{isamarkuptxt}%
1.61 +\isamarkuptrue%
1.62 +\isamarkupfalse%
1.63 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
1.64 -\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}%
1.65 +\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse%
1.66 +%
1.67 \begin{isamarkuptxt}%
1.68 \noindent
1.69 This is not an obscure trick but a generally applicable heuristic:
1.70 @@ -106,7 +120,9 @@
1.71 \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
1.72 statement of our lemma.%
1.73 \end{isamarkuptxt}%
1.74 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
1.75 +\isamarkuptrue%
1.76 +\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.77 +%
1.78 \begin{isamarkuptxt}%
1.79 \noindent
1.80 Now induction produces two subgoals which are both proved automatically:
1.81 @@ -117,37 +133,56 @@
1.82 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
1.83 \end{isabelle}%
1.84 \end{isamarkuptxt}%
1.85 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.86 +\ \isamarkuptrue%
1.87 +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.88 +\isamarkupfalse%
1.89 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
1.90 -\isacommand{done}%
1.91 +\isamarkupfalse%
1.92 +\isacommand{done}\isamarkupfalse%
1.93 +%
1.94 \begin{isamarkuptext}%
1.95 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
1.96 of \isa{r}, i.e.\ the least reflexive and transitive
1.97 relation containing \isa{r}. The latter is easily formalized%
1.98 \end{isamarkuptext}%
1.99 +\isamarkuptrue%
1.100 \isacommand{consts}\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
1.101 +\isamarkupfalse%
1.102 \isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
1.103 \isakeyword{intros}\isanewline
1.104 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
1.105 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
1.106 -{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}%
1.107 +{\isachardoublequote}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isamarkupfalse%
1.108 +%
1.109 \begin{isamarkuptext}%
1.110 \noindent
1.111 and the equivalence of the two definitions is easily shown by the obvious rule
1.112 inductions:%
1.113 \end{isamarkuptext}%
1.114 +\isamarkuptrue%
1.115 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
1.116 +\isamarkupfalse%
1.117 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
1.118 -\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.119 -\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.120 +\ \ \isamarkupfalse%
1.121 +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.122 +\ \isamarkupfalse%
1.123 +\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.124 +\isamarkupfalse%
1.125 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline
1.126 +\isamarkupfalse%
1.127 \isacommand{done}\isanewline
1.128 \isanewline
1.129 +\isamarkupfalse%
1.130 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
1.131 +\isamarkupfalse%
1.132 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
1.133 -\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
1.134 +\ \isamarkupfalse%
1.135 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
1.136 -\isacommand{done}%
1.137 +\isamarkupfalse%
1.138 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
1.139 +\isamarkupfalse%
1.140 +\isacommand{done}\isamarkupfalse%
1.141 +%
1.142 \begin{isamarkuptext}%
1.143 So why did we start with the first definition? Because it is simpler. It
1.144 contains only two rules, and the single step rule is simpler than
1.145 @@ -169,6 +204,13 @@
1.146 in exercise~\ref{ex:converse-rtc-step}.
1.147 \end{exercise}%
1.148 \end{isamarkuptext}%
1.149 +\isamarkuptrue%
1.150 +\isamarkupfalse%
1.151 +\isamarkupfalse%
1.152 +\isamarkupfalse%
1.153 +\isamarkupfalse%
1.154 +\isamarkupfalse%
1.155 +\isamarkupfalse%
1.156 \end{isabellebody}%
1.157 %%% Local Variables:
1.158 %%% mode: latex