| author | nipkow |
| Fri, 28 Jul 2000 16:02:51 +0200 | |
| changeset 9458 | c613cd06d5cf |
| parent 8745 | 13b32661dde4 |
| child 9493 | 494f8cd34df7 |
| permissions | -rw-r--r-- |
1 (*<*)
2 theory Tree = Main:
3 (*>*)
5 text{*\noindent
6 Define the datatype of binary trees
7 *}
9 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
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)";(*>*)
16 text{*\noindent
17 and a function \isa{mirror} that mirrors a binary tree
18 by swapping subtrees (recursively). Prove
19 *}
21 lemma mirror_mirror: "mirror(mirror t) = t";
22 (*<*)
23 apply(induct_tac t);
24 by(auto);
26 end
27 (*>*)