equal
deleted
inserted
replaced
10 write down such a tree? Using functional notation! For example, the% |
10 write down such a tree? Using functional notation! For example, the% |
11 \end{isamarkuptext}% |
11 \end{isamarkuptext}% |
12 \isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}% |
12 \isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}% |
13 \begin{isamarkuptext}% |
13 \begin{isamarkuptext}% |
14 \noindent of type \isa{(nat,nat)bigtree} is the tree whose |
14 \noindent of type \isa{(nat,nat)bigtree} is the tree whose |
15 root is labeled with 0 and whose $n$th subtree is labeled with $n$ and |
15 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
16 has merely \isa{Tip}s as further subtrees. |
16 has merely \isa{Tip}s as further subtrees. |
17 |
17 |
18 Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:% |
18 Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
20 \isacommand{consts}~map\_bt~::~{"}('a~{\isasymRightarrow}~'b)~{\isasymRightarrow}~('a,'i)bigtree~{\isasymRightarrow}~('b,'i)bigtree{"}\isanewline |
20 \isacommand{consts}~map\_bt~::~{"}('a~{\isasymRightarrow}~'b)~{\isasymRightarrow}~('a,'i)bigtree~{\isasymRightarrow}~('b,'i)bigtree{"}\isanewline |
30 Isabelle because the termination proof is not as obvious since |
30 Isabelle because the termination proof is not as obvious since |
31 \isa{map_bt} is only partially applied. |
31 \isa{map_bt} is only partially applied. |
32 |
32 |
33 The following lemma has a canonical proof% |
33 The following lemma has a canonical proof% |
34 \end{isamarkuptext}% |
34 \end{isamarkuptext}% |
35 \isacommand{lemma}~{"}map\_bt~g~(map\_bt~f~T)~=~map\_bt~(g~o~f)~T{"}\isanewline |
35 \isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline |
36 \isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}% |
36 \isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}% |
37 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
38 \noindent |
38 \noindent |
39 but it is worth taking a look at the proof state after the induction step |
39 but it is worth taking a look at the proof state after the induction step |
40 to understand what the presence of the function type entails: |
40 to understand what the presence of the function type entails: |