1.1 --- a/doc-src/TutorialI/Inductive/document/Star.tex Sun Jan 30 20:48:50 2005 +0100
1.2 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Tue Feb 01 18:01:57 2005 +0100
1.3 @@ -47,7 +47,7 @@
1.4 \isamarkuptrue%
1.5 \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.6 \isamarkupfalse%
1.7 -\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isamarkupfalse%
1.8 +\isamarkupfalse%
1.9 %
1.10 \begin{isamarkuptext}%
1.11 \noindent
1.12 @@ -76,69 +76,17 @@
1.13 \isamarkuptrue%
1.14 \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.15 \isamarkupfalse%
1.16 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.17 -%
1.18 -\begin{isamarkuptxt}%
1.19 -\noindent
1.20 -Unfortunately, even the base case is a problem:
1.21 -\begin{isabelle}%
1.22 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
1.23 -\end{isabelle}
1.24 -We have to abandon this proof attempt.
1.25 -To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.
1.26 -In the above application of \isa{erule}, the first premise of
1.27 -\isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which
1.28 -is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that
1.29 -is what we want, it is merely due to the order in which the assumptions occur
1.30 -in the subgoal, which it is not good practice to rely on. As a result,
1.31 -\isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes
1.32 -\isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
1.33 -yielding the above subgoal. So what went wrong?
1.34 -
1.35 -When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not
1.36 -depend on its second parameter at all. The reason is that in our original
1.37 -goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the
1.38 -conclusion, but not \isa{y}. Thus our induction statement is too
1.39 -weak. Fortunately, it can easily be strengthened:
1.40 -transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
1.41 -\end{isamarkuptxt}%
1.42 +\isamarkupfalse%
1.43 \isamarkuptrue%
1.44 \isamarkupfalse%
1.45 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
1.46 \ \ {\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.47 -%
1.48 -\begin{isamarkuptxt}%
1.49 -\noindent
1.50 -This is not an obscure trick but a generally applicable heuristic:
1.51 -\begin{quote}\em
1.52 -When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
1.53 -pull all other premises containing any of the $x@i$ into the conclusion
1.54 -using $\longrightarrow$.
1.55 -\end{quote}
1.56 -A similar heuristic for other kinds of inductions is formulated in
1.57 -\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
1.58 -\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
1.59 -statement of our lemma.%
1.60 -\end{isamarkuptxt}%
1.61 \isamarkuptrue%
1.62 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse%
1.63 -%
1.64 -\begin{isamarkuptxt}%
1.65 -\noindent
1.66 -Now induction produces two subgoals which are both proved automatically:
1.67 -\begin{isabelle}%
1.68 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
1.69 -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
1.70 -\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
1.71 -\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
1.72 -\end{isabelle}%
1.73 -\end{isamarkuptxt}%
1.74 -\ \isamarkuptrue%
1.75 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.76 \isamarkupfalse%
1.77 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
1.78 +\isamarkuptrue%
1.79 \isamarkupfalse%
1.80 -\isacommand{done}\isamarkupfalse%
1.81 +\isamarkupfalse%
1.82 +\isamarkupfalse%
1.83 %
1.84 \begin{isamarkuptext}%
1.85 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
1.86 @@ -162,26 +110,19 @@
1.87 \isamarkuptrue%
1.88 \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.89 \isamarkupfalse%
1.90 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
1.91 -\ \ \isamarkupfalse%
1.92 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.93 -\ \isamarkupfalse%
1.94 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
1.95 \isamarkupfalse%
1.96 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline
1.97 \isamarkupfalse%
1.98 -\isacommand{done}\isanewline
1.99 +\isamarkupfalse%
1.100 +\isamarkupfalse%
1.101 +\isanewline
1.102 \isanewline
1.103 \isamarkupfalse%
1.104 \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.105 \isamarkupfalse%
1.106 -\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
1.107 -\ \isamarkupfalse%
1.108 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
1.109 \isamarkupfalse%
1.110 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
1.111 \isamarkupfalse%
1.112 -\isacommand{done}\isamarkupfalse%
1.113 +\isamarkupfalse%
1.114 +\isamarkupfalse%
1.115 %
1.116 \begin{isamarkuptext}%
1.117 So why did we start with the first definition? Because it is simpler. It