doc-src/TutorialI/document/Fundata.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Fundata.tex	Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,115 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Fundata}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}i{\isaliteral{29}{\isacharparenright}}bigtree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Br\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}i{\isaliteral{29}{\isacharparenright}}bigtree{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+Parameter \isa{{\isaliteral{27}{\isacharprime}}a} is the type of values stored in
+the \isa{Br}anches of the tree, whereas \isa{{\isaliteral{27}{\isacharprime}}i} is the index
+type over which the tree branches. If \isa{{\isaliteral{27}{\isacharprime}}i} is instantiated to
+\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 term
+\begin{isabelle}%
+\ \ \ \ \ Br\ {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ Br\ i\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}n{\isaliteral{2E}{\isachardot}}\ Tip{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}
+of type \isa{{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{2C}{\isacharcomma}}\ nat{\isaliteral{29}{\isacharparenright}}\ 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{\isaliteral{5F}{\isacharunderscore}}bt} applies a function to all labels in a \isa{bigtree}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{primrec}\isamarkupfalse%
+\ map{\isaliteral{5F}{\isacharunderscore}}bt\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}i{\isaliteral{29}{\isacharparenright}}bigtree\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}i{\isaliteral{29}{\isacharparenright}}bigtree{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ Tip\ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ Tip{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{28}{\isacharparenleft}}Br\ a\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Br\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{28}{\isacharparenleft}}F\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent This is a valid \isacommand{primrec} definition because the
+recursive calls of \isa{map{\isaliteral{5F}{\isacharunderscore}}bt} involve only subtrees of
+\isa{F}, which is itself a subterm of the left-hand side. Thus termination
+is assured.  The seasoned functional programmer might try expressing
+\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}i{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{28}{\isacharparenleft}}F\ i{\isaliteral{29}{\isacharparenright}}} as \isa{map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ F}, which Isabelle 
+however will reject.  Applying \isa{map{\isaliteral{5F}{\isacharunderscore}}bt} to only one of its arguments
+makes the termination proof less obvious.
+
+The following lemma has a simple proof by induction:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}map{\isaliteral{5F}{\isacharunderscore}}bt\ {\isaliteral{28}{\isacharparenleft}}g\ o\ f{\isaliteral{29}{\isacharparenright}}\ T\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ T{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ T{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{5F}{\isacharunderscore}}all{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{done}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{isamarkuptxt}%
+\noindent
+Because of the function type, the proof state after induction looks unusual.
+Notice the quantified induction hypothesis:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ Tip\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ Tip{\isaliteral{29}{\isacharparenright}}\isanewline
+\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ F{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}F\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{28}{\isacharparenleft}}F\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
+\isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ F{\isaliteral{2E}{\isachardot}}\ }map{\isaliteral{5F}{\isacharunderscore}}bt\ {\isaliteral{28}{\isacharparenleft}}g\ {\isaliteral{5C3C636972633E}{\isasymcirc}}\ f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Br\ a\ F{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ map{\isaliteral{5F}{\isacharunderscore}}bt\ g\ {\isaliteral{28}{\isacharparenleft}}map{\isaliteral{5F}{\isacharunderscore}}bt\ f\ {\isaliteral{28}{\isacharparenleft}}Br\ a\ F{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: