equal
deleted
inserted
replaced
12 primrec |
12 primrec |
13 "mirror Tip = Tip" |
13 "mirror Tip = Tip" |
14 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*) |
14 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*) |
15 |
15 |
16 text{*\noindent |
16 text{*\noindent |
17 and a function \isa{mirror} that mirrors a binary tree |
17 and a function @{term"mirror"} that mirrors a binary tree |
18 by swapping subtrees (recursively). Prove |
18 by swapping subtrees (recursively). Prove |
19 *} |
19 *} |
20 |
20 |
21 lemma mirror_mirror: "mirror(mirror t) = t"; |
21 lemma mirror_mirror: "mirror(mirror t) = t"; |
22 (*<*) |
22 (*<*) |
28 "flatten Tip = []" |
28 "flatten Tip = []" |
29 "flatten (Node l x r) = flatten l @ [x] @ flatten r"; |
29 "flatten (Node l x r) = flatten l @ [x] @ flatten r"; |
30 (*>*) |
30 (*>*) |
31 |
31 |
32 text{*\noindent |
32 text{*\noindent |
33 Define a function \isa{flatten} that flattens a tree into a list |
33 Define a function @{term"flatten"} that flattens a tree into a list |
34 by traversing it in infix order. Prove |
34 by traversing it in infix order. Prove |
35 *} |
35 *} |
36 |
36 |
37 lemma "flatten(mirror t) = rev(flatten t)"; |
37 lemma "flatten(mirror t) = rev(flatten t)"; |
38 (*<*) |
38 (*<*) |