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