author | hoelzl |
Tue, 01 Jul 2014 15:25:27 +0200 | |
changeset 57449 | f81da03b9ebd |
parent 57250 | cddaf5b93728 |
child 57450 | 2baecef3207f |
permissions | -rw-r--r-- |
57250 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header {* Binary Tree *} |
|
4 |
||
5 |
theory Tree |
|
6 |
imports Main |
|
7 |
begin |
|
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" |
57250 | 13 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
14 |
lemma neq_Leaf_iff: "(t \<noteq> Leaf) = (\<exists>l a r. t = Node l a r)" |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
15 |
by (cases t) auto |
57250 | 16 |
|
17 |
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where |
|
18 |
"subtrees Leaf = {Leaf}" | |
|
19 |
"subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)" |
|
20 |
||
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
21 |
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
|
22 |
by (induction t)(auto) |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
23 |
|
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
24 |
lemma Node_notin_subtrees_if[simp]: |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
25 |
"a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> 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 |
|
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
28 |
lemma in_set_tree_if: |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
29 |
"Node l a r \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
30 |
by (metis Node_notin_subtrees_if) |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
31 |
|
57250 | 32 |
fun inorder :: "'a tree \<Rightarrow> 'a list" where |
33 |
"inorder Leaf = []" | |
|
34 |
"inorder (Node l x r) = inorder l @ [x] @ inorder r" |
|
35 |
||
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
36 |
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
|
37 |
by (induction t) auto |
57250 | 38 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
39 |
subsection {* Binary Search Tree predicate *} |
57250 | 40 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
41 |
inductive bst :: "'a::linorder tree \<Rightarrow> bool" where |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
42 |
Leaf[intro!, simp]: "bst Leaf" | |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
43 |
Node: "bst l \<Longrightarrow> bst r \<Longrightarrow> (\<And>x. x \<in> set_tree l \<Longrightarrow> x < a) \<Longrightarrow> (\<And>x. x \<in> set_tree r \<Longrightarrow> a < x) \<Longrightarrow> |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
44 |
bst (Node l a r)" |
57250 | 45 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
46 |
lemma bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
47 |
by (induction rule: bst.induct) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
57250 | 48 |
|
49 |
end |