datatype  tree = Leaf of int | Node of  tree * tree
  
datatype path = H | L of path | R of path

(* subtree (p, t) = t'
 
   Invariant:
   If p is a valid path in t then t' is the subtree at p 
*)
fun subtree (H, t) = t
  | subtree (L p, Node (left, right)) = subtree (p, left)
  | subtree (R p, Node (left, right)) = subtree (p, right) 

(* mirror p = p'
  
   Invariant:
   If p  is a path then p' is its mirror path
*)
fun mirror H = H
  | mirror (L p) = R (mirror p)
  | mirror (R p) = L (mirror p)

(* reflect t = t'
  
   Invariant:
   If  t is a tree then t' is a tree where all 
   each subtree has been hereditarily switched
*)
fun reflect (Leaf i) = (Leaf i)
  | reflect (Node (left, right)) =
      Node (reflect (right), reflect (left))