section ‹Augmented Tree (Tree2)
›
theory Tree2
imports "HOL-Library.Tree"
begin
text ‹This
theory provides the basic infrastructure
for the type @{
typ ‹(
'a * 'b) tree
›}
of augmented trees
where @{
typ 'a} is the key and @{typ 'b} some additional information.
›
text ‹IMPORTANT: Inductions
and cases analyses on augmented trees need
to use the following
two rules explicitly. They generate nodes of the form @{
term "Node l (a,b) r"}
rather than @{
term "Node l a r"}
for trees of type @{
typ "'a tree"}.
›
lemmas tree2_induct = tree.induct[
where 'a = "'a *
'b", split_format(complete)]
lemmas tree2_cases = tree.exhaust[
where 'a = "'a *
'b", split_format(complete)]
fun inorder ::
"('a*'b)tree \ 'a list" where
"inorder Leaf = []" |
"inorder (Node l (a,_) r) = inorder l @ a # inorder r"
fun set_tree ::
"('a*'b) tree \ 'a set" where
"set_tree Leaf = {}" |
"set_tree (Node l (a,_) r) = {a} \ set_tree l \ set_tree r"
fun bst ::
"('a::linorder*'b) tree \ bool" where
"bst Leaf = True" |
"bst (Node l (a, _) r) = ((\x \ set_tree l. x < a) \ (\x \ set_tree r. a < x) \ bst l \ bst r)"
lemma finite_set_tree[simp]:
"finite(set_tree t)"
by(
induction t) auto
lemma eq_set_tree_empty[simp]:
"set_tree t = {} \ t = Leaf"
by (cases t) auto
lemma set_inorder[simp]:
"set (inorder t) = set_tree t"
by (
induction t) auto
lemma length_inorder[simp]:
"length (inorder t) = size t"
by (
induction t) auto
end
