Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Impl.java Sprache: Isabelle

Original von: Isabelle^©

section \<open>Augmented Tree (Tree2)\<close>

theory Tree2
imports "HOL-Library.Tree"
begin

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>

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

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.