(*<*)

 theory Tree imports Main begin

 (*>*)

 text{*\noindent

 Define the datatype of \rmindex{binary trees}:

 *}

 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)

 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where

 "mirror Tip = Tip" |

 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)

 text{*\noindent

 Define a function @{term"mirror"} that mirrors a binary tree

 by swapping subtrees recursively. Prove

 *}

 lemma mirror_mirror: "mirror(mirror t) = t";

 (*<*)

 apply(induct_tac t);

 by(auto);

 primrec flatten :: "'a tree => 'a list" where

 "flatten Tip = []" |

 "flatten (Node l x r) = flatten l @ [x] @ flatten r";

 (*>*)

 text{*\noindent

 Define a function @{term"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

 (*>*)