doc-src/TutorialI/Datatype/Fundata.thy
author nipkow
Wed, 19 Apr 2000 11:56:31 +0200
changeset 8745 13b32661dde4
child 8771 026f37a86ea7
permissions -rw-r--r--
I wonder which files i forgot.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     2
theory Fundata = Main:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     3
(*>*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     4
datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     6
text{*\noindent Parameter \isa{'a} is the type of values stored in
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     7
the \isa{Branch}es of the tree, whereas \isa{'i} is the index
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     8
type over which the tree branches. If \isa{'i} is instantiated to
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     9
\isa{bool}, the result is a binary tree; if it is instantiated to
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    10
\isa{nat}, we have an infinitely branching tree because each node
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    11
has as many subtrees as there are natural numbers. How can we possibly
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    12
write down such a tree? Using functional notation! For example, the *}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    13
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    14
term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    15
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    16
text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    17
root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
has merely \isa{Tip}s as further subtrees.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    19
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    20
Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    22
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    23
consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    24
primrec
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    25
"map_bt f Tip          = Tip"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    28
text{*\noindent This is a valid \isacommand{primrec} definition because the
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    29
recursive calls of \isa{map_bt} involve only subtrees obtained from
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    30
\isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    31
seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    32
of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    33
Isabelle because the termination proof is not as obvious since
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
\isa{map_bt} is only partially applied.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    35
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
The following lemma has a canonical proof  *}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    37
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    38
lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    39
apply(induct_tac "T", auto).
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    40
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    41
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    42
but it is worth taking a look at the proof state after the induction step
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
to understand what the presence of the function type entails:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    44
\begin{isabellepar}%
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    45
~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    46
~2.~{\isasymAnd}a~F.\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    48
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
\end{isabellepar}%
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    52
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    53
(*>*)