use_thy "AVL";
(* testing 'isin' *)
(* standard example: empty tree 'contains' nothing *)
Goal "\\ isin 0 Leaf";
auto();
qed "std1";
(* just another standard example, which refers to the
difference between a label and the tree *)
Goal "\\ isin Leaf Leaf";
auto();
qed "std2";
(* an example which refers to the root label
note: Peter is in ;) *)
Goal "isin Peter (Node Peter Leaf Leaf)";
auto();
qed "PeterIsIn";
(* analogous example with Leafs, looks funny *)
Goal "isin Leaf (Node Leaf Leaf Leaf)";
auto();
qed "LeafIsIn";
(* let's look in to the left subtree *)
Goal "l = Y \\ isin l (Node X (Node Y Leaf Leaf) (Node Z Leaf Leaf))";
auto();
qed "left_subtree";
(* \\ and now in to the right *)
Goal "l = Z \\ isin l (Node X (Node Y Leaf Leaf) (Node Z Leaf Leaf))";
auto();
qed "right_subtree";
(* testing 'isord' *)
(* an empty tree is ordered *)
Goal "isord Leaf";
auto();
qed "empty";
(* let's look at an example with numbers *)
Goal "isord (Node 2 (Node 1 Leaf Leaf) (Node 3 Leaf Leaf))";
auto();
(* well okay, but that's not enough
we have to make the type of our 'numbers' explicit *)
Goal "isord (Node (2::nat) (Node 1 Leaf Leaf) (Node 3 Leaf Leaf))";
auto();
qed "ordered";
Goal "\\ isord (Node (1::nat) (Node 3 Leaf Leaf) (Node 2 Leaf Leaf))";
auto();
qed "not_ordered";