--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
\begin{isabelle}%
-\isacommand{datatype}~('a,'i)bigtree~=~Tip~|~Branch~'a~{"}'i~{\isasymRightarrow}~('a,'i)bigtree{"}%
+\isacommand{datatype}\ ('a,'i)bigtree\ =\ Tip\ |\ Branch\ 'a\ {"}'i\ {\isasymRightarrow}\ ('a,'i)bigtree{"}%
\begin{isamarkuptext}%
\noindent Parameter \isa{'a} is the type of values stored in
the \isa{Branch}es of the tree, whereas \isa{'i} is the index
@@ -7,33 +7,37 @@
\isa{bool}, the result is a binary tree; if it is instantiated to
\isa{nat}, we have an infinitely branching tree because each node
has as many subtrees as there are natural numbers. How can we possibly
-write down such a tree? Using functional notation! For example, the%
-\end{isamarkuptext}%
-\isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}%
-\begin{isamarkuptext}%
-\noindent of type \isa{(nat,nat)bigtree} is the tree whose
+write down such a tree? Using functional notation! For example, the term
+\begin{quote}
+
+\begin{isabelle}%
+Branch\ 0\ ({\isasymlambda}i.\ Branch\ i\ ({\isasymlambda}n.\ Tip))
+\end{isabelle}%
+
+\end{quote}
+of type \isa{(nat,\ nat)\ bigtree} is the tree whose
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
has merely \isa{Tip}s as further subtrees.
Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:%
\end{isamarkuptext}%
-\isacommand{consts}~map\_bt~::~{"}('a~{\isasymRightarrow}~'b)~{\isasymRightarrow}~('a,'i)bigtree~{\isasymRightarrow}~('b,'i)bigtree{"}\isanewline
+\isacommand{consts}\ map\_bt\ ::\ {"}('a\ {\isasymRightarrow}\ 'b)\ {\isasymRightarrow}\ ('a,'i)bigtree\ {\isasymRightarrow}\ ('b,'i)bigtree{"}\isanewline
\isacommand{primrec}\isanewline
-{"}map\_bt~f~Tip~~~~~~~~~~=~Tip{"}\isanewline
-{"}map\_bt~f~(Branch~a~F)~=~Branch~(f~a)~({\isasymlambda}i.~map\_bt~f~(F~i)){"}%
+{"}map\_bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ =\ Tip{"}\isanewline
+{"}map\_bt\ f\ (Branch\ a\ F)\ =\ Branch\ (f\ a)\ ({\isasymlambda}i.\ map\_bt\ f\ (F\ i)){"}%
\begin{isamarkuptext}%
\noindent This is a valid \isacommand{primrec} definition because the
recursive calls of \isa{map_bt} involve only subtrees obtained from
\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
-seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
-of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
+seasoned functional programmer might have written \isa{map\_bt\ f\ {\isasymcirc}\ F}
+instead of \isa{{\isasymlambda}i.\ map\_bt\ f\ (F\ i)}, but the former is not accepted by
Isabelle because the termination proof is not as obvious since
\isa{map_bt} is only partially applied.
The following lemma has a canonical proof%
\end{isamarkuptext}%
-\isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline
-\isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}%
+\isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline
+\isacommand{apply}(induct\_tac\ {"}T{"},\ auto)\isacommand{.}%
\begin{isamarkuptext}%
\noindent
but it is worth taking a look at the proof state after the induction step