(*Exercise sheet 3, model solution*)
(*AVL Trees*)
use_thy "AVL";
(*Sheet 3, Exercise 1*)
(* 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";
(*Exercise 2*)
(* 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";
open AVL;
tree.cases;
tree.distinct;
tree.induct;
tree.recs;
tree.exhaust;
bal_def;
(*NEW LEMMAS NOT CONSIDERED BY PUSCH AND NIPKOW*)
(*lemmas about efficient isin. Sheet 3 Exercise ???*)
Goal "isord (Node n l r) \\ x < n \\ isin x (Node n l r) \\ isin x l";
auto();
qed_spec_mp "isin_ord_l";
Goal "isord (Node n l r) \\ n < x \\ isin x (Node n l r) \\ isin x r";
auto();
qed_spec_mp "isin_ord_r";
Goal "isord t \\ (isin k t = isin_eff k t)";
by (induct_tac "t" 1);
by (Simp_tac 1);
by (case_tac "k = a" 1);
by (asm_simp_tac (simpset() addsimps [isin_eff_branch,isin_branch]) 1);
by (case_tac "k < a" 1);
by (asm_simp_tac (simpset() addsimps [isin_eff_branch,isin_branch]) 1);
auto();
qed_spec_mp "isin_eff_correct";