(*Exercise sheet 3, model solution*)

(*AVL Trees*)
use_thy "AVL";

(*Sheet 3, Exercise 1*)
(* testing 'isin' *)
(* standard example: empty tree 'contains' nothing *)
Goal "\\<not> isin 0 Leaf";
auto();
qed "std1";


(* just another standard example, which refers to the
   difference between a label and the tree *)
Goal "\\<not> 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 \\<Longrightarrow> isin l (Node X (Node Y Leaf Leaf) (Node Z Leaf Leaf))";
auto();
qed "left_subtree";


(* \\<dots> and now in to the right *)
Goal "l = Z \\<Longrightarrow> 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 "\\<not> 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) \\<longrightarrow> x < n \\<longrightarrow> isin x (Node n l r) \\<longrightarrow> isin x l";
auto();
qed_spec_mp "isin_ord_l";

Goal "isord (Node n l r) \\<longrightarrow> n < x \\<longrightarrow> isin x (Node n l r) \\<longrightarrow> isin x r";
auto();
qed_spec_mp "isin_ord_r";

Goal "isord t \\<longrightarrow> (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";