--- a/doc-src/TutorialI/IsaMakefile Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Wed Aug 02 11:30:38 2000 +0200
@@ -92,7 +92,7 @@
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
-$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \
+$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
--- a/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Aug 02 11:30:38 2000 +0200
@@ -2,23 +2,25 @@
theory Itrev = Main:;
(*>*)
-text{*
-We define a tail-recursive version of list-reversal,
-i.e.\ one that can be compiled into a loop:
-*};
+text{* Function \isa{rev} has quadratic worst-case running time
+because it calls function \isa{\at} for each element of the list and
+\isa{\at} is linear in its first argument. A linear time version of
+\isa{rev} reqires an extra argument where the result is accumulated
+gradually, using only \isa{\#}:*}
consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)";
-text{*\noindent
-The behaviour of \isa{itrev} is simple: it reverses its first argument by
-stacking its elements onto the second argument, and returning that second
-argument when the first one becomes empty.
-We need to show that \isa{itrev} does indeed reverse its first argument
-provided the second one is empty:
-*};
+text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
+its first argument by stacking its elements onto the second argument,
+and returning that second argument when the first one becomes
+empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+compiled into a loop.
+
+Naturally, we would like to show that \isa{itrev} does indeed reverse
+its first argument provided the second one is empty: *};
lemma "itrev xs [] = rev xs";
--- a/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML Wed Aug 02 11:30:38 2000 +0200
@@ -1,4 +1,5 @@
use_thy "Tree";
+use_thy "Tree2";
use_thy "cases";
use_thy "fakenat";
use_thy "natsum";
--- a/doc-src/TutorialI/Misc/Tree.thy Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Wed Aug 02 11:30:38 2000 +0200
@@ -11,7 +11,7 @@
consts mirror :: "'a tree \\<Rightarrow> 'a tree";
primrec
"mirror Tip = Tip"
-"mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*)
+"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
and a function \isa{mirror} that mirrors a binary tree
@@ -23,5 +23,21 @@
apply(induct_tac t);
by(auto);
+consts flatten :: "'a tree => 'a list"
+primrec
+"flatten Tip = []"
+"flatten (Node l x r) = flatten l @ [x] @ flatten r";
+(*>*)
+
+text{*\noindent
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+*}
+
+lemma "flatten(mirror t) = rev(flatten t)";
+(*<*)
+apply(induct_tac t);
+by(auto);
+
end
(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Tree2.thy Wed Aug 02 11:30:38 2000 +0200
@@ -0,0 +1,30 @@
+(*<*)
+theory Tree2 = Tree:
+(*>*)
+
+text{*\noindent In Exercise~\ref{ex:Tree} we defined a function
+\isa{flatten} from trees to lists. The straightforward version of
+\isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic.
+A linear time version of \isa{flatten} again reqires an extra
+argument, the accumulator: *}
+
+consts flatten2 :: "'a tree => 'a list => 'a list"
+(*<*)
+primrec
+"flatten2 Tip xs = xs"
+"flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))"
+(*>*)
+
+text{*\noindent Define \isa{flatten2} and prove
+*}
+(*<*)
+lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs";
+apply(induct_tac t);
+by(auto);
+(*>*)
+lemma "flatten2 t [] = flatten t";
+(*<*)
+by(simp);
+
+end
+(*>*)
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Aug 02 11:30:38 2000 +0200
@@ -1,20 +1,25 @@
\begin{isabelle}%
%
\begin{isamarkuptext}%
-We define a tail-recursive version of list-reversal,
-i.e.\ one that can be compiled into a loop:%
+Function \isa{rev} has quadratic worst-case running time
+because it calls function \isa{\at} for each element of the list and
+\isa{\at} is linear in its first argument. A linear time version of
+\isa{rev} reqires an extra argument where the result is accumulated
+gradually, using only \isa{\#}:%
\end{isamarkuptext}%
\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
\isacommand{primrec}\isanewline
{"}itrev~[]~~~~~ys~=~ys{"}\isanewline
{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
\begin{isamarkuptext}%
-\noindent
-The behaviour of \isa{itrev} is simple: it reverses its first argument by
-stacking its elements onto the second argument, and returning that second
-argument when the first one becomes empty.
-We need to show that \isa{itrev} does indeed reverse its first argument
-provided the second one is empty:%
+\noindent The behaviour of \isa{itrev} is simple: it reverses
+its first argument by stacking its elements onto the second argument,
+and returning that second argument when the first one becomes
+empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+compiled into a loop.
+
+Naturally, we would like to show that \isa{itrev} does indeed reverse
+its first argument provided the second one is empty:%
\end{isamarkuptext}%
\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
\begin{isamarkuptxt}%
--- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Wed Aug 02 11:30:38 2000 +0200
@@ -10,7 +10,13 @@
and a function \isa{mirror} that mirrors a binary tree
by swapping subtrees (recursively). Prove%
\end{isamarkuptext}%
-\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}\end{isabelle}%
+\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}%
+\begin{isamarkuptext}%
+\noindent
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove%
+\end{isamarkuptext}%
+\isacommand{lemma}~{"}flatten(mirror~t)~=~rev(flatten~t){"}\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Aug 02 11:30:38 2000 +0200
@@ -0,0 +1,18 @@
+\begin{isabelle}%
+%
+\begin{isamarkuptext}%
+\noindent In Exercise~\ref{ex:Tree} we defined a function
+\isa{flatten} from trees to lists. The straightforward version of
+\isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic.
+A linear time version of \isa{flatten} again reqires an extra
+argument, the accumulator:%
+\end{isamarkuptext}%
+\isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}%
+\begin{isamarkuptext}%
+\noindent Define \isa{flatten2} and prove%
+\end{isamarkuptext}%
+\isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/TutorialI/fp.tex Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/fp.tex Wed Aug 02 11:30:38 2000 +0200
@@ -197,7 +197,7 @@
A more general method for defining total recursive functions is introduced in
\S\ref{sec:recdef}.
-\begin{exercise}
+\begin{exercise}\label{ex:Tree}
\input{Misc/document/Tree.tex}%
\end{exercise}
@@ -679,6 +679,9 @@
\isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
+\begin{exercise}
+\input{Misc/document/Tree2.tex}%
+\end{exercise}
\section{Case study: compiling expressions}
\label{sec:ExprCompiler}