theory BSTHW imports BSTInClass begin lemma BST_in_tree: "\ in_tree t x; is_BST t lo hi \ \ lo \ x \ x \ hi" apply (induct t arbitrary: lo hi x) apply simp apply force done -- "lookup finds items in the tree" theorem in_tree_implies_lookup: assumes bst: "is_BST t lo hi" and intree: "in_tree t x" shows "lookup t x" using bst intree proof (induct t arbitrary: lo hi x) fix lo hi x assume "in_tree Tip x" from this have "False" by simp from this show "lookup Tip x" .. next fix t1 y t2 lo hi x assume IH1: "\lo hi x. \is_BST t1 lo hi; in_tree t1 x\ \ lookup t1 x" and IH2: "\lo hi x. \is_BST t2 lo hi; in_tree t2 x\ \ lookup t2 x" and bst_node: "is_BST (Node t1 y t2) lo hi" and in_tree_node: "in_tree (Node t1 y t2) x" from bst_node have bst_t1: "is_BST t1 lo y" by simp from bst_node have bst_t2: "is_BST t2 y hi" by simp from in_tree_node have "x = y \ in_tree t1 x \ in_tree t2 x" by simp moreover { assume "x = y" hence "lookup (Node t1 y t2) x" by simp } moreover { assume in_t1: "in_tree t1 x" from bst_t1 in_t1 IH1 have lt1: "lookup t1 x" by blast from in_t1 bst_t1 have "lo \ x \ x \ y" by (rule BST_in_tree) with lt1 have "lookup (Node t1 y t2) x" by simp } moreover { assume in_t2: "in_tree t2 x" from bst_t2 in_t2 IH2 have lt2: "lookup t2 x" by blast from in_t2 bst_t2 have "y \ x \ x \ hi" by (rule BST_in_tree) with lt2 have "lookup (Node t1 y t2) x" by simp } ultimately show "lookup (Node t1 y t2) x" by blast qed -- "same theorem, but using tactics" theorem in_tree_implies_lookup_tactics: "\ is_BST t lo hi; in_tree t x \ \ lookup t x" apply (induct t arbitrary: lo hi x) apply simp apply simp apply clarify apply (erule disjE) apply simp apply (erule disjE) apply simp apply (frule BST_in_tree) apply simp apply simp apply simp apply (frule BST_in_tree) apply simp apply simp done theorem lookup_equiv_in_tree: "is_BST t lo hi \ lookup t x = in_tree t x" using in_tree_implies_lookup lookup_implies_in_tree by blast end