8745
|
1 |
(*<*)
|
16417
|
2 |
theory Fundata imports Main begin
|
8745
|
3 |
(*>*)
|
10420
|
4 |
datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
|
8745
|
5 |
|
9792
|
6 |
text{*\noindent
|
|
7 |
Parameter @{typ"'a"} is the type of values stored in
|
10420
|
8 |
the @{term Br}anches of the tree, whereas @{typ"'i"} is the index
|
9792
|
9 |
type over which the tree branches. If @{typ"'i"} is instantiated to
|
|
10 |
@{typ"bool"}, the result is a binary tree; if it is instantiated to
|
|
11 |
@{typ"nat"}, we have an infinitely branching tree because each node
|
8745
|
12 |
has as many subtrees as there are natural numbers. How can we possibly
|
9541
|
13 |
write down such a tree? Using functional notation! For example, the term
|
12631
|
14 |
@{term[display]"Br (0::nat) (\<lambda>i. Br i (\<lambda>n. Tip))"}
|
9541
|
15 |
of type @{typ"(nat,nat)bigtree"} is the tree whose
|
8771
|
16 |
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
|
9792
|
17 |
has merely @{term"Tip"}s as further subtrees.
|
8745
|
18 |
|
9792
|
19 |
Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
|
8745
|
20 |
*}
|
|
21 |
|
27015
|
22 |
primrec map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
|
|
23 |
where
|
|
24 |
"map_bt f Tip = Tip" |
|
10420
|
25 |
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
|
8745
|
26 |
|
|
27 |
text{*\noindent This is a valid \isacommand{primrec} definition because the
|
14188
|
28 |
recursive calls of @{term"map_bt"} involve only subtrees of
|
|
29 |
@{term"F"}, which is itself a subterm of the left-hand side. Thus termination
|
|
30 |
is assured. The seasoned functional programmer might try expressing
|
11458
|
31 |
@{term"%i. map_bt f (F i)"} as @{term"map_bt f o F"}, which Isabelle
|
|
32 |
however will reject. Applying @{term"map_bt"} to only one of its arguments
|
|
33 |
makes the termination proof less obvious.
|
8745
|
34 |
|
11309
|
35 |
The following lemma has a simple proof by induction: *}
|
8745
|
36 |
|
8771
|
37 |
lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
|
10171
|
38 |
apply(induct_tac T, simp_all)
|
|
39 |
done
|
10420
|
40 |
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
|
|
41 |
apply(induct_tac T, rename_tac[2] F)(*>*)
|
|
42 |
txt{*\noindent
|
13439
|
43 |
Because of the function type, the proof state after induction looks unusual.
|
10795
|
44 |
Notice the quantified induction hypothesis:
|
10420
|
45 |
@{subgoals[display,indent=0]}
|
8745
|
46 |
*}
|
|
47 |
(*<*)
|
10420
|
48 |
oops
|
8745
|
49 |
end
|
|
50 |
(*>*)
|