doc-src/TutorialI/Datatype/Fundata.thy
author nipkow
Wed, 08 Nov 2000 14:38:04 +0100
changeset 10420 ef006735bee8
parent 10171 59d6633835fa
child 10795 9e888d60d3e5
permissions -rw-r--r--
*** empty log message ***
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
(*>*)
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
     4
datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
     6
text{*\noindent
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
     7
Parameter @{typ"'a"} is the type of values stored in
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
     8
the @{term Br}anches of the tree, whereas @{typ"'i"} is the index
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
     9
type over which the tree branches. If @{typ"'i"} is instantiated to
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    10
@{typ"bool"}, the result is a binary tree; if it is instantiated to
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    11
@{typ"nat"}, we have an infinitely branching tree because each node
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    12
has as many subtrees as there are natural numbers. How can we possibly
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8771
diff changeset
    13
write down such a tree? Using functional notation! For example, the term
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    14
@{term[display]"Br 0 (%i. Br i (%n. Tip))"}
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8771
diff changeset
    15
of type @{typ"(nat,nat)bigtree"} is the tree whose
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8745
diff changeset
    16
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    17
has merely @{term"Tip"}s as further subtrees.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    19
Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    20
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
9933
9feb1e0c4cb3 *** empty log message ***
nipkow
parents: 9834
diff changeset
    22
consts map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    23
primrec
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    24
"map_bt f Tip      = Tip"
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    25
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
text{*\noindent This is a valid \isacommand{primrec} definition because the
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    28
recursive calls of @{term"map_bt"} involve only subtrees obtained from
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    29
@{term"F"}, i.e.\ the left-hand side. Thus termination is assured.  The
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8771
diff changeset
    30
seasoned functional programmer might have written @{term"map_bt f o F"}
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8771
diff changeset
    31
instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    32
Isabelle because the termination proof is not as obvious since
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
    33
@{term"map_bt"} is only partially applied.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    35
The following lemma has a canonical proof  *}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8745
diff changeset
    37
lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    38
apply(induct_tac T, simp_all)
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    39
done
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    40
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    41
apply(induct_tac T, rename_tac[2] F)(*>*)
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    42
txt{*\noindent
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
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
    44
to understand what the presence of the function type entails:
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    45
@{subgoals[display,indent=0]}
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    46
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
(*<*)
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    48
oops
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
(*>*)