# HG changeset patch
# User nipkow
# Date 965208638 -7200
# Node ID 494f8cd34df74ee49b1b3ec1adf2468633346e64
# Parent  72e429c666087060c4cecc697310e1a780b28779
*** empty log message ***

diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/IsaMakefile
--- 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 \
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/Itrev.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";
 
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/ROOT.ML
--- 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";
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/Tree.thy
--- 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
 (*>*)
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/Tree2.thy
--- /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
+(*>*)
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/document/Itrev.tex
--- 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}%
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/document/Tree.tex
--- 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"
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/Misc/document/Tree2.tex
--- /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:
diff -r 72e429c66608 -r 494f8cd34df7 doc-src/TutorialI/fp.tex
--- 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}