text\<open>This theory provides the basic infrastructure for the type @{typ \<open>('a * 'b) tree\<close>}
of augmented trees where @{typ'a} is the key and @{typ 'b} some additional information.\<close>
text\<open>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"}.\<close>
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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
