(*Exercise sheet no. 15*)
use_thy "AVL";
(*tests on pruning*)
(*Exercise 4*)
(*remark: the first two trees are correct, the other ones are not*)
Goal "prune (ENode Just 2 ELeaf ELeaf) = ?t";
by (Simp_tac 1);
Goal "prune (ENode Left 2 (ENode Just 1 ELeaf ELeaf) ELeaf) = ?t";
by (Simp_tac 1);
Goal "prune (ENode Just 1 (ENode Left 0 ELeaf ELeaf) (ENode Just 2 ELeaf ELeaf)) = ?t";
by (Simp_tac 1);
Goal "prune (ENode Just 1 (ENode Right 0 ELeaf (ENode Just 0 ELeaf ELeaf)) (ENode Just 2 ELeaf ELeaf)) = ?t";
by (Simp_tac 1);
(*tests on correct*)
(*Exercise 5*)
(*I use the same trees as in Exercise 4*)
(*correct*)
Goal "correct (ENode Just 2 ELeaf ELeaf)";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
(*correct*)
Goal "correct (ENode Left 2 (ENode Just 1 ELeaf ELeaf) ELeaf)";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
(*not correct*)
Goal "~correct (ENode Just 1 (ENode Left 0 ELeaf ELeaf) (ENode Just 2 ELeaf ELeaf))";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
(*not correct*)
Goal "~correct (ENode Just 1 (ENode Right 0 ELeaf (ENode Just 0 ELeaf ELeaf)) (ENode Just 2 ELeaf ELeaf))";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
(*Exercise 7*)
(*I do this in analogy to Exercise 5, i.e. essentially I reverse the
calls I had there. Obviously, I get the corrected versions of the
incorrect trees above*)
Goal "label (Node 2 Leaf Leaf) = ?t";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
Goal "label (Node 2 (Node 1 Leaf Leaf) Leaf) = ?t";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
Goal "label (Node 1 (Node 0 Leaf Leaf) (Node 2 Leaf Leaf)) = ?t";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);
Goal "label (Node 1 (Node 0 Leaf (Node 0 Leaf Leaf)) (Node 2 Leaf Leaf)) = ?t";
by (asm_simp_tac (simpset() addsimps [bal_def]) 1);