--- a/doc-src/TutorialI/Misc/Tree.thy Tue Aug 01 18:26:34 2000 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy Wed Aug 02 11:30:38 2000 +0200
@@ -11,7 +11,7 @@
consts mirror :: "'a tree \\<Rightarrow> 'a tree";
primrec
"mirror Tip = Tip"
-"mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*)
+"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
text{*\noindent
and a function \isa{mirror} that mirrors a binary tree
@@ -23,5 +23,21 @@
apply(induct_tac t);
by(auto);
+consts flatten :: "'a tree => 'a list"
+primrec
+"flatten Tip = []"
+"flatten (Node l x r) = flatten l @ [x] @ flatten r";
+(*>*)
+
+text{*\noindent
+Define a function \isa{flatten} that flattens a tree into a list
+by traversing it in infix order. Prove
+*}
+
+lemma "flatten(mirror t) = rev(flatten t)";
+(*<*)
+apply(induct_tac t);
+by(auto);
+
end
(*>*)