src/HOL/Library/Tree.thy
author nipkow
Thu, 12 Jun 2014 21:23:28 +0200
changeset 57250 cddaf5b93728
child 57449 f81da03b9ebd
permissions -rw-r--r--
new theory of binary trees
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     1
(* Author: Tobias Nipkow *)
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     2
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     3
header {* Binary Tree *}
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     4
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     5
theory Tree
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     6
imports Main
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     7
begin
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     8
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
     9
datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    10
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    11
fun set_tree :: "'a tree \<Rightarrow> 'a set" where
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    12
"set_tree Leaf = {}" |
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    13
"set_tree (Node l x r) = insert x (set_tree l \<union> set_tree r)"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    14
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    15
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    16
"subtrees Leaf = {Leaf}" |
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    17
"subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    18
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    19
fun inorder :: "'a tree \<Rightarrow> 'a list" where
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    20
"inorder Leaf = []" |
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    21
"inorder (Node l x r) = inorder l @ [x] @ inorder r"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    22
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    23
text{* Binary Search Tree predicate: *}
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    24
fun bst :: "'a::linorder tree \<Rightarrow> bool" where
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    25
"bst Leaf = True" |
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    26
"bst (Node l a r) =
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    27
  (bst l & bst r & (\<forall>x \<in> set_tree l. x < a)  & (\<forall>x \<in> set_tree r. a < x))"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    28
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    29
lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    30
by (cases t) auto
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    31
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    32
lemma set_inorder[simp]: "set(inorder t) = set_tree t"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    33
by (induction t) auto
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    34
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    35
lemma set_treeE: "a : set_tree t \<Longrightarrow> \<exists>l r. Node l a r \<in> subtrees t"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    36
by(induction t)(auto)
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    37
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    38
lemma Node_notin_subtrees_if[simp]:
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    39
  "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    40
by (induction t) auto
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    41
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    42
lemma in_set_tree_if:
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    43
  "Node l a r \<in> subtrees t \<Longrightarrow> a \<in> set_tree t"
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    44
by (metis Node_notin_subtrees_if)
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    45
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    46
end