equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Tree = Main: |
2 theory Tree = Main: |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent |
5 text{*\noindent |
6 Define the datatype of binary trees |
6 Define the datatype of \rmindex{binary trees}: |
7 *} |
7 *} |
8 |
8 |
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) |
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) |
10 |
10 |
11 consts mirror :: "'a tree \<Rightarrow> 'a tree"; |
11 consts mirror :: "'a tree \<Rightarrow> 'a tree"; |
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 @{term"mirror"} that mirrors a binary tree |
17 Define 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 (*<*) |