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›}
  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
  rules explicitly. They generate nodes of the form @{term "Node l (a,b) r"}
  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