# HG changeset patch # User nipkow # Date 967557913 -7200 # Node ID a977245dfc8a24445856884088eb2b4cd3cc2ecf # Parent a5f86aed785b82b20ddcf9d73580fb4124690275 *** empty log message *** diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Datatype/Fundata.thy --- a/doc-src/TutorialI/Datatype/Fundata.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Tue Aug 29 16:05:13 2000 +0200 @@ -41,12 +41,12 @@ text{*\noindent but it is worth taking a look at the proof state after the induction step to understand what the presence of the function type entails: -\begin{isabellepar}% +\begin{isabelle} ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline ~2.~{\isasymAnd}a~F.\isanewline ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)% -\end{isabellepar}% +\end{isabelle} *} (*<*) end diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 16:05:13 2000 +0200 @@ -43,12 +43,12 @@ \noindent but it is worth taking a look at the proof state after the induction step to understand what the presence of the function type entails: -\begin{isabellepar}% +\begin{isabelle} ~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline ~2.~{\isasymAnd}a~F.\isanewline ~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)% -\end{isabellepar}%% +\end{isabelle}% \end{isamarkuptext}% \end{isabellebody}% %%% Local Variables: diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Tue Aug 29 16:05:13 2000 +0200 @@ -28,13 +28,13 @@ Induction variable occurs also among premises! \end{quote} and leads to the base case -\begin{isabellepar}% +\begin{isabelle} \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} which, after simplification, becomes -\begin{isabellepar}% +\begin{isabelle} \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} We cannot prove this equality because we do not know what \isa{hd} and \isa{last} return when applied to \isa{[]}. @@ -56,9 +56,9 @@ text{*\noindent This time, induction leaves us with the following base case -\begin{isabellepar}% +\begin{isabelle} \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} which is trivial, and \isa{auto} finishes the whole proof. If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you @@ -169,18 +169,18 @@ (*>*) txt{*\noindent which leaves us with the following proof state: -\begin{isabellepar}% +\begin{isabelle} \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} -\end{isabellepar}% +\end{isabelle} After stripping the \isa{\isasymforall i}, the proof continues with a case distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the other case: -\begin{isabellepar}% +\begin{isabelle} \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} -\end{isabellepar}% +\end{isabelle} *}; by(blast intro!: f_ax Suc_leI intro:le_less_trans); diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 29 16:05:13 2000 +0200 @@ -32,9 +32,9 @@ txt{*\noindent Unfortunately, this is not a complete success: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% -\end{isabellepar}% +\end{isabelle} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed \isa{[]}. The corresponding heuristic: @@ -59,11 +59,11 @@ Although we now have two variables, only \isa{xs} is suitable for induction, and we repeat our above proof attempt. Unfortunately, we are still not there: -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymAnd}a~list.\isanewline ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys% -\end{isabellepar}% +\end{isabelle} The induction hypothesis is still too weak, but this time it takes no intuition to generalize: the problem is that \isa{ys} is fixed throughout the subgoal, but the induction hypothesis needs to be applied with diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/case_splits.thy --- a/doc-src/TutorialI/Misc/case_splits.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/case_splits.thy Tue Aug 29 16:05:13 2000 +0200 @@ -11,9 +11,9 @@ txt{*\noindent can be split into -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])% -\end{isabellepar}% +\end{isabelle} by a degenerate form of simplification *} @@ -34,10 +34,10 @@ lemma "(case xs of [] \\ zs | y#ys \\ y#(ys@zs)) = xs@zs"; txt{*\noindent becomes -\begin{isabellepar}% +\begin{isabelle} ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)% -\end{isabellepar}% +\end{isabelle} by typing *} diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/def_rewr.thy --- a/doc-src/TutorialI/Misc/def_rewr.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/def_rewr.thy Tue Aug 29 16:05:13 2000 +0200 @@ -28,9 +28,9 @@ txt{*\noindent In this particular case, the resulting goal -\begin{isabellepar}% +\begin{isabelle} ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% -\end{isabellepar}% +\end{isabelle} can be proved by simplification. Thus we could have proved the lemma outright *}(*<*)oops;lemma "exor A (\\A)";(*>*) by(simp add: exor_def) diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 16:05:13 2000 +0200 @@ -27,13 +27,13 @@ Induction variable occurs also among premises! \end{quote} and leads to the base case -\begin{isabellepar}% +\begin{isabelle} \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} which, after simplification, becomes -\begin{isabellepar}% +\begin{isabelle} \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} We cannot prove this equality because we do not know what \isa{hd} and \isa{last} return when applied to \isa{[]}. @@ -51,9 +51,9 @@ \begin{isamarkuptext}% \noindent This time, induction leaves us with the following base case -\begin{isabellepar}% +\begin{isabelle} \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ [] -\end{isabellepar}% +\end{isabelle} which is trivial, and \isa{auto} finishes the whole proof. If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you @@ -151,18 +151,18 @@ \begin{isamarkuptxt}% \noindent which leaves us with the following proof state: -\begin{isabellepar}% +\begin{isabelle} \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} -\end{isabellepar}% +\end{isabelle} After stripping the \isa{\isasymforall i}, the proof continues with a case distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the other case: -\begin{isabellepar}% +\begin{isabelle} \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i} -\end{isabellepar}%% +\end{isabelle}% \end{isamarkuptxt}% \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}% \begin{isamarkuptext}% diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 16:05:13 2000 +0200 @@ -31,9 +31,9 @@ \begin{isamarkuptxt}% \noindent Unfortunately, this is not a complete success: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% -\end{isabellepar}% +\end{isabelle} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed \isa{[]}. The corresponding heuristic: @@ -57,11 +57,11 @@ Although we now have two variables, only \isa{xs} is suitable for induction, and we repeat our above proof attempt. Unfortunately, we are still not there: -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymAnd}a~list.\isanewline ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline ~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys% -\end{isabellepar}% +\end{isabelle} The induction hypothesis is still too weak, but this time it takes no intuition to generalize: the problem is that \isa{ys} is fixed throughout the subgoal, but the induction hypothesis needs to be applied with diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/document/case_splits.tex --- a/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 16:05:13 2000 +0200 @@ -9,9 +9,9 @@ \begin{isamarkuptxt}% \noindent can be split into -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])% -\end{isabellepar}% +\end{isabelle} by a degenerate form of simplification% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% @@ -30,10 +30,10 @@ \begin{isamarkuptxt}% \noindent becomes -\begin{isabellepar}% +\begin{isabelle} ~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline ~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)% -\end{isabellepar}% +\end{isabelle} by typing% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/document/def_rewr.tex --- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 16:05:13 2000 +0200 @@ -26,9 +26,9 @@ \begin{isamarkuptxt}% \noindent In this particular case, the resulting goal -\begin{isabellepar}% +\begin{isabelle} ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A% -\end{isabellepar}% +\end{isabelle} can be proved by simplification. Thus we could have proved the lemma outright% \end{isamarkuptxt}% \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}% diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Recdef/Induction.thy --- a/doc-src/TutorialI/Recdef/Induction.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Aug 29 16:05:13 2000 +0200 @@ -31,13 +31,13 @@ txt{*\noindent The resulting proof state has three subgoals corresponding to the three clauses for \isa{sep}: -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline ~3.~{\isasymAnd}a~x~y~zs.\isanewline ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% -\end{isabellepar}% +\end{isabelle} The rest is pure simplification: *} @@ -57,12 +57,12 @@ name of a function that takes an $n$-tuple. Usually the subgoal will contain the term $f~x@1~\dots~x@n$ but this need not be the case. The induction rules do not mention $f$ at all. For example \isa{sep.induct} -\begin{isabellepar}% +\begin{isabelle} {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline ~~{\isasymAnd}a~x.~P~a~[x];\isanewline ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline {\isasymLongrightarrow}~P~u~v% -\end{isabellepar}% +\end{isabelle} merely says that in order to prove a property \isa{P} of \isa{u} and \isa{v} you need to prove it for the three cases where \isa{v} is the empty list, the singleton list, and the list with at least two elements diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 16:05:13 2000 +0200 @@ -28,13 +28,13 @@ \noindent The resulting proof state has three subgoals corresponding to the three clauses for \isa{sep}: -\begin{isabellepar}% +\begin{isabelle} ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline ~3.~{\isasymAnd}a~x~y~zs.\isanewline ~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline ~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))% -\end{isabellepar}% +\end{isabelle} The rest is pure simplification:% \end{isamarkuptxt}% \isacommand{by}\ simp{\isacharunderscore}all% @@ -52,12 +52,12 @@ name of a function that takes an $n$-tuple. Usually the subgoal will contain the term $f~x@1~\dots~x@n$ but this need not be the case. The induction rules do not mention $f$ at all. For example \isa{sep.induct} -\begin{isabellepar}% +\begin{isabelle} {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline ~~{\isasymAnd}a~x.~P~a~[x];\isanewline ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline {\isasymLongrightarrow}~P~u~v% -\end{isabellepar}% +\end{isabelle} merely says that in order to prove a property \isa{P} of \isa{u} and \isa{v} you need to prove it for the three cases where \isa{v} is the empty list, the singleton list, and the list with at least two elements diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Aug 29 16:05:13 2000 +0200 @@ -137,24 +137,24 @@ The name and the simplification attribute are optional. \end{itemize} Isabelle's response is to print -\begin{isabellepar}% +\begin{isabelle} proof(prove):~step~0\isanewline \isanewline goal~(theorem~rev\_rev):\isanewline rev~(rev~xs)~=~xs\isanewline ~1.~rev~(rev~xs)~=~xs -\end{isabellepar}% +\end{isabelle} The first three lines tell us that we are 0 steps into the proof of theorem \isa{rev_rev}; for compactness reasons we rarely show these initial lines in this tutorial. The remaining lines display the current proof state. Until we have finished a proof, the proof state always looks like this: -\begin{isabellepar}% +\begin{isabelle} $G$\isanewline ~1.~$G\sb{1}$\isanewline ~~\vdots~~\isanewline ~$n$.~$G\sb{n}$ -\end{isabellepar}% +\end{isabelle} where $G$ is the overall goal that we are trying to prove, and the numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to @@ -175,15 +175,15 @@ By default, induction acts on the first subgoal. The new proof state contains two subgoals, namely the base case (\isa{Nil}) and the induction step (\isa{Cons}): -\begin{isabellepar}% +\begin{isabelle} ~1.~rev~(rev~[])~=~[]\isanewline ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list% -\end{isabellepar}% +\end{isabelle} The induction step is an example of the general format of a subgoal: -\begin{isabellepar}% +\begin{isabelle} ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} -\end{isabellepar}% +\end{isabelle} The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be ignored most of the time, or simply treated as a list of variables local to this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}. @@ -208,18 +208,18 @@ ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks to the equation \isa{rev [] = []}) and disappears; the simplified version of subgoal~2 becomes the new subgoal~1: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list -\end{isabellepar}% +\end{isabelle} In order to simplify this subgoal further, a lemma suggests itself. *} (*<*) oops (*>*) +subsubsection{*First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}*} + text{* -\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} - After abandoning the above proof attempt\indexbold{abandon proof}\indexbold{proof!abandon} (at the shell level type \isacommand{oops}\indexbold{*oops}) we start a new proof: @@ -247,10 +247,10 @@ apply(auto); txt{* -\begin{isabellepar}% +\begin{isabelle} ~1.~rev~ys~=~rev~ys~@~[]\isanewline ~2. \dots -\end{isabellepar}% +\end{isabelle} Again, we need to abandon this proof attempt and prove another simple lemma first. In the future the step of abandoning an incomplete proof before embarking on the proof of a lemma usually remains implicit. @@ -259,9 +259,9 @@ oops (*>*) +subsubsection{*Second lemma: \texttt{xs \at~[] = xs}*} + text{* -\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}} - This time the canonical proof procedure *} @@ -272,10 +272,10 @@ txt{* \noindent leads to the desired message \isa{No subgoals!}: -\begin{isabellepar}% +\begin{isabelle} xs~@~[]~=~xs\isanewline No~subgoals! -\end{isabellepar}% +\end{isabelle} We still need to confirm that the proof is now finished: *} @@ -302,29 +302,27 @@ \noindent we find that this time \isa{auto} solves the base case, but the induction step merely simplifies to -\begin{isabellepar} +\begin{isabelle} ~1.~{\isasymAnd}a~list.\isanewline ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[] -\end{isabellepar}% +\end{isabelle} Now we need to remember that \isa{\at} associates to the right, and that \isa{\#} and \isa{\at} have the same priority (namely the \isa{65} in their \isacommand{infixr} annotation). Thus the conclusion really is -\begin{isabellepar}% +\begin{isabelle} ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))% -\end{isabellepar}% +\end{isabelle} and the missing lemma is associativity of \isa{\at}. +*} +(*<*)oops(*>*) -\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}} +subsubsection{*Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}*} +text{* Abandoning the previous proof, the canonical proof procedure *} - -txt_raw{*\begin{comment}*} -oops -text_raw{*\end{comment}*} - lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; apply(induct_tac xs); by(auto); @@ -332,7 +330,6 @@ text{* \noindent succeeds without further ado. - Now we can go back and prove the first lemma *} diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 16:05:13 2000 +0200 @@ -132,24 +132,24 @@ The name and the simplification attribute are optional. \end{itemize} Isabelle's response is to print -\begin{isabellepar}% +\begin{isabelle} proof(prove):~step~0\isanewline \isanewline goal~(theorem~rev\_rev):\isanewline rev~(rev~xs)~=~xs\isanewline ~1.~rev~(rev~xs)~=~xs -\end{isabellepar}% +\end{isabelle} The first three lines tell us that we are 0 steps into the proof of theorem \isa{rev_rev}; for compactness reasons we rarely show these initial lines in this tutorial. The remaining lines display the current proof state. Until we have finished a proof, the proof state always looks like this: -\begin{isabellepar}% +\begin{isabelle} $G$\isanewline ~1.~$G\sb{1}$\isanewline ~~\vdots~~\isanewline ~$n$.~$G\sb{n}$ -\end{isabellepar}% +\end{isabelle} where $G$ is the overall goal that we are trying to prove, and the numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to @@ -169,15 +169,15 @@ By default, induction acts on the first subgoal. The new proof state contains two subgoals, namely the base case (\isa{Nil}) and the induction step (\isa{Cons}): -\begin{isabellepar}% +\begin{isabelle} ~1.~rev~(rev~[])~=~[]\isanewline ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list% -\end{isabellepar}% +\end{isabelle} The induction step is an example of the general format of a subgoal: -\begin{isabellepar}% +\begin{isabelle} ~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} -\end{isabellepar}% +\end{isabelle} The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be ignored most of the time, or simply treated as a list of variables local to this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}. @@ -200,15 +200,15 @@ ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks to the equation \isa{rev [] = []}) and disappears; the simplified version of subgoal~2 becomes the new subgoal~1: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list -\end{isabellepar}% +\end{isabelle} In order to simplify this subgoal further, a lemma suggests itself.% \end{isamarkuptxt}% % +\isamarkupsubsubsection{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} +% \begin{isamarkuptext}% -\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} - After abandoning the above proof attempt\indexbold{abandon proof}\indexbold{proof!abandon} (at the shell level type \isacommand{oops}\indexbold{*oops}) we start a new proof:% @@ -232,18 +232,18 @@ \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptxt}% -\begin{isabellepar}% +\begin{isabelle} ~1.~rev~ys~=~rev~ys~@~[]\isanewline ~2. \dots -\end{isabellepar}% +\end{isabelle} Again, we need to abandon this proof attempt and prove another simple lemma first. In the future the step of abandoning an incomplete proof before embarking on the proof of a lemma usually remains implicit.% \end{isamarkuptxt}% % +\isamarkupsubsubsection{Second lemma: \texttt{xs \at~[] = xs}} +% \begin{isamarkuptext}% -\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}} - This time the canonical proof procedure% \end{isamarkuptext}% \isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline @@ -252,10 +252,10 @@ \begin{isamarkuptxt}% \noindent leads to the desired message \isa{No subgoals!}: -\begin{isabellepar}% +\begin{isabelle} xs~@~[]~=~xs\isanewline No~subgoals! -\end{isabellepar}% +\end{isabelle} We still need to confirm that the proof is now finished:% \end{isamarkuptxt}% @@ -279,34 +279,31 @@ \noindent we find that this time \isa{auto} solves the base case, but the induction step merely simplifies to -\begin{isabellepar} +\begin{isabelle} ~1.~{\isasymAnd}a~list.\isanewline ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[] -\end{isabellepar}% +\end{isabelle} Now we need to remember that \isa{\at} associates to the right, and that \isa{\#} and \isa{\at} have the same priority (namely the \isa{65} in their \isacommand{infixr} annotation). Thus the conclusion really is -\begin{isabellepar}% +\begin{isabelle} ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))% -\end{isabellepar}% -and the missing lemma is associativity of \isa{\at}. - -\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}} - -Abandoning the previous proof, the canonical proof procedure% +\end{isabelle} +and the missing lemma is associativity of \isa{\at}.% \end{isamarkuptxt}% % -\begin{comment} -\isacommand{oops}% -\end{comment} +\isamarkupsubsubsection{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}} +% +\begin{isamarkuptext}% +Abandoning the previous proof, the canonical proof procedure% +\end{isamarkuptext}% \isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptext}% \noindent succeeds without further ado. - Now we can go back and prove the first lemma% \end{isamarkuptext}% \isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Tue Aug 29 16:05:13 2000 +0200 @@ -109,11 +109,11 @@ txt{*\noindent Unfortunately, this time we are left with three intimidating looking subgoals: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs% -\end{isabellepar}% +\end{isabelle} Clearly, if we want to make headway we have to instantiate \isa{bs} as well now. It turns out that instead of induction, case distinction suffices: diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 16:05:13 2000 +0200 @@ -98,11 +98,11 @@ \begin{isamarkuptxt}% \noindent Unfortunately, this time we are left with three intimidating looking subgoals: -\begin{isabellepar}% +\begin{isabelle} ~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs% -\end{isabellepar}% +\end{isabelle} Clearly, if we want to make headway we have to instantiate \isa{bs} as well now. It turns out that instead of induction, case distinction suffices:% diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/tutorial.tex --- a/doc-src/TutorialI/tutorial.tex Tue Aug 29 15:43:29 2000 +0200 +++ b/doc-src/TutorialI/tutorial.tex Tue Aug 29 16:05:13 2000 +0200 @@ -4,8 +4,6 @@ \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} \usepackage{../pdfsetup} %last package! -\newcommand\Out[1]{\texttt{\textsl{#1}}} %% for output from terminal sessions - %\newtheorem{theorem}{Theorem}[section] \newtheorem{Exercise}{Exercise}[section] \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} @@ -22,7 +20,6 @@ \newcommand{\isasymFun}{\isasymRightarrow} \newcommand{\isasymuniqex}{\emph{$\exists!\,$}} -\newenvironment{isabellepar}{\medskip\begin{isabelle}}{\end{isabelle}\medskip} \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} %%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}