--- 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
--- 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:
--- 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);
--- 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
--- 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 [] \\<Rightarrow> zs | y#ys \\<Rightarrow> 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
*}
--- 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 (\\<not>A)";(*>*)
by(simp add: exor_def)
--- 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}%
--- 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
--- 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}%
--- 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}%
--- 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
--- 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
--- 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
*}
--- 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
--- 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:
--- 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:%
--- 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}