1.1 --- a/doc-src/TutorialI/IsaMakefile Tue Aug 01 18:26:34 2000 +0200
1.2 +++ b/doc-src/TutorialI/IsaMakefile Wed Aug 02 11:30:38 2000 +0200
1.3 @@ -92,7 +92,7 @@
1.4
1.5 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
1.6
1.7 -$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \
1.8 +$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
1.9 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \
1.10 Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
1.11 Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \
2.1 --- a/doc-src/TutorialI/Misc/Itrev.thy Tue Aug 01 18:26:34 2000 +0200
2.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Aug 02 11:30:38 2000 +0200
2.3 @@ -2,23 +2,25 @@
2.4 theory Itrev = Main:;
2.5 (*>*)
2.6
2.7 -text{*
2.8 -We define a tail-recursive version of list-reversal,
2.9 -i.e.\ one that can be compiled into a loop:
2.10 -*};
2.11 +text{* Function \isa{rev} has quadratic worst-case running time
2.12 +because it calls function \isa{\at} for each element of the list and
2.13 +\isa{\at} is linear in its first argument. A linear time version of
2.14 +\isa{rev} reqires an extra argument where the result is accumulated
2.15 +gradually, using only \isa{\#}:*}
2.16
2.17 consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
2.18 primrec
2.19 "itrev [] ys = ys"
2.20 "itrev (x#xs) ys = itrev xs (x#ys)";
2.21
2.22 -text{*\noindent
2.23 -The behaviour of \isa{itrev} is simple: it reverses its first argument by
2.24 -stacking its elements onto the second argument, and returning that second
2.25 -argument when the first one becomes empty.
2.26 -We need to show that \isa{itrev} does indeed reverse its first argument
2.27 -provided the second one is empty:
2.28 -*};
2.29 +text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
2.30 +its first argument by stacking its elements onto the second argument,
2.31 +and returning that second argument when the first one becomes
2.32 +empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
2.33 +compiled into a loop.
2.34 +
2.35 +Naturally, we would like to show that \isa{itrev} does indeed reverse
2.36 +its first argument provided the second one is empty: *};
2.37
2.38 lemma "itrev xs [] = rev xs";
2.39
3.1 --- a/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 01 18:26:34 2000 +0200
3.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML Wed Aug 02 11:30:38 2000 +0200
3.3 @@ -1,4 +1,5 @@
3.4 use_thy "Tree";
3.5 +use_thy "Tree2";
3.6 use_thy "cases";
3.7 use_thy "fakenat";
3.8 use_thy "natsum";
4.1 --- a/doc-src/TutorialI/Misc/Tree.thy Tue Aug 01 18:26:34 2000 +0200
4.2 +++ b/doc-src/TutorialI/Misc/Tree.thy Wed Aug 02 11:30:38 2000 +0200
4.3 @@ -11,7 +11,7 @@
4.4 consts mirror :: "'a tree \\<Rightarrow> 'a tree";
4.5 primrec
4.6 "mirror Tip = Tip"
4.7 -"mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*)
4.8 +"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
4.9
4.10 text{*\noindent
4.11 and a function \isa{mirror} that mirrors a binary tree
4.12 @@ -23,5 +23,21 @@
4.13 apply(induct_tac t);
4.14 by(auto);
4.15
4.16 +consts flatten :: "'a tree => 'a list"
4.17 +primrec
4.18 +"flatten Tip = []"
4.19 +"flatten (Node l x r) = flatten l @ [x] @ flatten r";
4.20 +(*>*)
4.21 +
4.22 +text{*\noindent
4.23 +Define a function \isa{flatten} that flattens a tree into a list
4.24 +by traversing it in infix order. Prove
4.25 +*}
4.26 +
4.27 +lemma "flatten(mirror t) = rev(flatten t)";
4.28 +(*<*)
4.29 +apply(induct_tac t);
4.30 +by(auto);
4.31 +
4.32 end
4.33 (*>*)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/TutorialI/Misc/Tree2.thy Wed Aug 02 11:30:38 2000 +0200
5.3 @@ -0,0 +1,30 @@
5.4 +(*<*)
5.5 +theory Tree2 = Tree:
5.6 +(*>*)
5.7 +
5.8 +text{*\noindent In Exercise~\ref{ex:Tree} we defined a function
5.9 +\isa{flatten} from trees to lists. The straightforward version of
5.10 +\isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic.
5.11 +A linear time version of \isa{flatten} again reqires an extra
5.12 +argument, the accumulator: *}
5.13 +
5.14 +consts flatten2 :: "'a tree => 'a list => 'a list"
5.15 +(*<*)
5.16 +primrec
5.17 +"flatten2 Tip xs = xs"
5.18 +"flatten2 (Node l x r) xs = flatten2 l (x#(flatten2 r xs))"
5.19 +(*>*)
5.20 +
5.21 +text{*\noindent Define \isa{flatten2} and prove
5.22 +*}
5.23 +(*<*)
5.24 +lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs";
5.25 +apply(induct_tac t);
5.26 +by(auto);
5.27 +(*>*)
5.28 +lemma "flatten2 t [] = flatten t";
5.29 +(*<*)
5.30 +by(simp);
5.31 +
5.32 +end
5.33 +(*>*)
6.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 01 18:26:34 2000 +0200
6.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Aug 02 11:30:38 2000 +0200
6.3 @@ -1,20 +1,25 @@
6.4 \begin{isabelle}%
6.5 %
6.6 \begin{isamarkuptext}%
6.7 -We define a tail-recursive version of list-reversal,
6.8 -i.e.\ one that can be compiled into a loop:%
6.9 +Function \isa{rev} has quadratic worst-case running time
6.10 +because it calls function \isa{\at} for each element of the list and
6.11 +\isa{\at} is linear in its first argument. A linear time version of
6.12 +\isa{rev} reqires an extra argument where the result is accumulated
6.13 +gradually, using only \isa{\#}:%
6.14 \end{isamarkuptext}%
6.15 \isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline
6.16 \isacommand{primrec}\isanewline
6.17 {"}itrev~[]~~~~~ys~=~ys{"}\isanewline
6.18 {"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}%
6.19 \begin{isamarkuptext}%
6.20 -\noindent
6.21 -The behaviour of \isa{itrev} is simple: it reverses its first argument by
6.22 -stacking its elements onto the second argument, and returning that second
6.23 -argument when the first one becomes empty.
6.24 -We need to show that \isa{itrev} does indeed reverse its first argument
6.25 -provided the second one is empty:%
6.26 +\noindent The behaviour of \isa{itrev} is simple: it reverses
6.27 +its first argument by stacking its elements onto the second argument,
6.28 +and returning that second argument when the first one becomes
6.29 +empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
6.30 +compiled into a loop.
6.31 +
6.32 +Naturally, we would like to show that \isa{itrev} does indeed reverse
6.33 +its first argument provided the second one is empty:%
6.34 \end{isamarkuptext}%
6.35 \isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}%
6.36 \begin{isamarkuptxt}%
7.1 --- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 01 18:26:34 2000 +0200
7.2 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Wed Aug 02 11:30:38 2000 +0200
7.3 @@ -10,7 +10,13 @@
7.4 and a function \isa{mirror} that mirrors a binary tree
7.5 by swapping subtrees (recursively). Prove%
7.6 \end{isamarkuptext}%
7.7 -\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}\end{isabelle}%
7.8 +\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}%
7.9 +\begin{isamarkuptext}%
7.10 +\noindent
7.11 +Define a function \isa{flatten} that flattens a tree into a list
7.12 +by traversing it in infix order. Prove%
7.13 +\end{isamarkuptext}%
7.14 +\isacommand{lemma}~{"}flatten(mirror~t)~=~rev(flatten~t){"}\end{isabelle}%
7.15 %%% Local Variables:
7.16 %%% mode: latex
7.17 %%% TeX-master: "root"
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Aug 02 11:30:38 2000 +0200
8.3 @@ -0,0 +1,18 @@
8.4 +\begin{isabelle}%
8.5 +%
8.6 +\begin{isamarkuptext}%
8.7 +\noindent In Exercise~\ref{ex:Tree} we defined a function
8.8 +\isa{flatten} from trees to lists. The straightforward version of
8.9 +\isa{flatten} is based on \isa{\at} and is thus, like \isa{rev}, quadratic.
8.10 +A linear time version of \isa{flatten} again reqires an extra
8.11 +argument, the accumulator:%
8.12 +\end{isamarkuptext}%
8.13 +\isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}%
8.14 +\begin{isamarkuptext}%
8.15 +\noindent Define \isa{flatten2} and prove%
8.16 +\end{isamarkuptext}%
8.17 +\isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}%
8.18 +%%% Local Variables:
8.19 +%%% mode: latex
8.20 +%%% TeX-master: "root"
8.21 +%%% End:
9.1 --- a/doc-src/TutorialI/fp.tex Tue Aug 01 18:26:34 2000 +0200
9.2 +++ b/doc-src/TutorialI/fp.tex Wed Aug 02 11:30:38 2000 +0200
9.3 @@ -197,7 +197,7 @@
9.4 A more general method for defining total recursive functions is introduced in
9.5 \S\ref{sec:recdef}.
9.6
9.7 -\begin{exercise}
9.8 +\begin{exercise}\label{ex:Tree}
9.9 \input{Misc/document/Tree.tex}%
9.10 \end{exercise}
9.11
9.12 @@ -679,6 +679,9 @@
9.13 \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
9.14 happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
9.15
9.16 +\begin{exercise}
9.17 +\input{Misc/document/Tree2.tex}%
9.18 +\end{exercise}
9.19
9.20 \section{Case study: compiling expressions}
9.21 \label{sec:ExprCompiler}