equal
deleted
inserted
replaced
|
1 (*<*) |
|
2 theory Tree = Main: |
|
3 (*>*) |
|
4 |
|
5 text{*\noindent |
|
6 Define the datatype of binary trees |
|
7 *} |
|
8 |
|
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) |
|
10 |
|
11 consts mirror :: "'a tree \\<Rightarrow> 'a tree"; |
|
12 primrec |
|
13 "mirror Tip = Tip" |
|
14 "mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*) |
|
15 |
|
16 text{*\noindent |
|
17 and a function \isa{mirror} that mirrors a binary tree |
|
18 by swapping subtrees (recursively). Prove |
|
19 *} |
|
20 |
|
21 lemma mirror_mirror: "mirror(mirror t) = t"; |
|
22 (*<*) |
|
23 apply(induct_tac t); |
|
24 apply(auto).; |
|
25 |
|
26 end |
|
27 (*>*) |