src/HOL/Library/Tree.thy
author hoelzl
Thu, 17 Jul 2014 14:55:56 +0200
changeset 57569 e20a999f7161
parent 57530 439f881c8744
child 57687 cca7e8788481
permissions -rw-r--r--
register tree with datatype_compat ot support QuickCheck
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
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
     9
datatype_new 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree")
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    10
  where
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    11
    "left Leaf = Leaf"
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    12
  | "right Leaf = Leaf"
57569
e20a999f7161 register tree with datatype_compat ot support QuickCheck
hoelzl
parents: 57530
diff changeset
    13
datatype_compat tree
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    14
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    15
lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)"
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    16
  by (cases t) auto
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    17
57530
439f881c8744 added lemma
nipkow
parents: 57450
diff changeset
    18
lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)"
439f881c8744 added lemma
nipkow
parents: 57450
diff changeset
    19
by auto
439f881c8744 added lemma
nipkow
parents: 57450
diff changeset
    20
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    21
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    22
  "subtrees Leaf = {Leaf}" |
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    23
  "subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)"
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    24
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    25
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. Node l a r \<in> subtrees t"
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    26
  by (induction t)(auto)
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    27
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    28
lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t"
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    29
  by (induction t) auto
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    30
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    31
lemma in_set_tree_if: "Node l a r \<in> subtrees t \<Longrightarrow> a \<in> set_tree t"
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    32
  by (metis Node_notin_subtrees_if)
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    33
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    34
fun inorder :: "'a tree \<Rightarrow> 'a list" where
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    35
  "inorder Leaf = []" |
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    36
  "inorder (Node l x r) = inorder l @ [x] @ inorder r"
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    37
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    38
lemma set_inorder[simp]: "set (inorder t) = set_tree t"
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    39
  by (induction t) auto
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    40
57449
f81da03b9ebd Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents: 57250
diff changeset
    41
subsection {* Binary Search Tree predicate *}
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    42
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    43
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    44
  "bst Leaf \<longleftrightarrow> True" |
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    45
  "bst (Node l a r) \<longleftrightarrow> bst l \<and> bst r \<and> (\<forall>x\<in>set_tree l. x < a) \<and> (\<forall>x\<in>set_tree r. a < x)"
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    46
57450
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    47
lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)"
2baecef3207f Library/Tree: bst is preferred to be a function
hoelzl
parents: 57449
diff changeset
    48
  by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
57250
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    49
cddaf5b93728 new theory of binary trees
nipkow
parents:
diff changeset
    50
end