equal
deleted
inserted
replaced
15 "rev (x # xs) = (rev xs) @ (x # [])" |
15 "rev (x # xs) = (rev xs) @ (x # [])" |
16 |
16 |
17 theorem rev_rev [simp]: "rev(rev xs) = xs" |
17 theorem rev_rev [simp]: "rev(rev xs) = xs" |
18 (*<*)oops(*>*) |
18 (*<*)oops(*>*) |
19 |
19 |
20 |
|
21 text{* |
20 text{* |
22 \begin{exercise} |
21 \begin{exercise} |
23 Define a datatype of binary trees and a function @{term mirror} |
22 Define a datatype of binary trees and a function @{term mirror} |
24 that mirrors a binary tree by swapping subtrees recursively. Prove |
23 that mirrors a binary tree by swapping subtrees recursively. Prove |
25 @{prop"mirror(mirror t) = t"}. |
24 @{prop"mirror(mirror t) = t"}. |
27 Define a function @{term flatten} that flattens a tree into a list |
26 Define a function @{term flatten} that flattens a tree into a list |
28 by traversing it in infix order. Prove |
27 by traversing it in infix order. Prove |
29 @{prop"flatten(mirror t) = rev(flatten t)"}. |
28 @{prop"flatten(mirror t) = rev(flatten t)"}. |
30 \end{exercise} |
29 \end{exercise} |
31 *} |
30 *} |
32 |
|
33 end |
31 end |