(*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);