author | haftmann |
Sun, 28 Sep 2014 20:27:46 +0200 | |
changeset 58467 | 6a3da58f7233 |
parent 58438 | 566117a31cc0 |
child 58881 | b9556a055632 |
permissions | -rw-r--r-- |
57250 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header {* Binary Tree *} |
|
4 |
||
5 |
theory Tree |
|
6 |
imports Main |
|
7 |
begin |
|
8 |
||
58424 | 9 |
datatype 'a tree = |
10 |
Leaf ("\<langle>\<rangle>") | |
|
11 |
Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>") |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
12 |
where |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
13 |
"left Leaf = Leaf" |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
14 |
| "right Leaf = Leaf" |
57569
e20a999f7161
register tree with datatype_compat ot support QuickCheck
hoelzl
parents:
57530
diff
changeset
|
15 |
datatype_compat tree |
57250 | 16 |
|
58438 | 17 |
text{* Can be seen as counting the number of leaves rather than nodes: *} |
18 |
||
19 |
definition size1 :: "'a tree \<Rightarrow> nat" where |
|
20 |
"size1 t = size t + 1" |
|
21 |
||
22 |
lemma size1_simps[simp]: |
|
23 |
"size1 \<langle>\<rangle> = 1" |
|
24 |
"size1 \<langle>l, x, r\<rangle> = size1 l + size1 r" |
|
25 |
by (simp_all add: size1_def) |
|
26 |
||
58424 | 27 |
lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)" |
28 |
by (cases t) auto |
|
57530 | 29 |
|
57687 | 30 |
lemma finite_set_tree[simp]: "finite(set_tree t)" |
31 |
by(induction t) auto |
|
32 |
||
33 |
||
34 |
subsection "The set of subtrees" |
|
35 |
||
57250 | 36 |
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where |
58424 | 37 |
"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" | |
38 |
"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)" |
|
57250 | 39 |
|
58424 | 40 |
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t" |
41 |
by (induction t)(auto) |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
42 |
|
57450 | 43 |
lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t" |
58424 | 44 |
by (induction t) auto |
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
45 |
|
58424 | 46 |
lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" |
47 |
by (metis Node_notin_subtrees_if) |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
48 |
|
57687 | 49 |
|
50 |
subsection "Inorder list of entries" |
|
51 |
||
57250 | 52 |
fun inorder :: "'a tree \<Rightarrow> 'a list" where |
58424 | 53 |
"inorder \<langle>\<rangle> = []" | |
54 |
"inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r" |
|
57250 | 55 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
56 |
lemma set_inorder[simp]: "set (inorder t) = set_tree t" |
58424 | 57 |
by (induction t) auto |
57250 | 58 |
|
57687 | 59 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
60 |
subsection {* Binary Search Tree predicate *} |
57250 | 61 |
|
57450 | 62 |
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where |
58424 | 63 |
"bst \<langle>\<rangle> \<longleftrightarrow> True" | |
64 |
"bst \<langle>l, a, r\<rangle> \<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 | 65 |
|
57450 | 66 |
lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" |
58424 | 67 |
by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
57250 | 68 |
|
57687 | 69 |
|
70 |
subsection "Deletion of the rightmost entry" |
|
71 |
||
72 |
fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where |
|
58424 | 73 |
"del_rightmost \<langle>l, a, \<langle>\<rangle>\<rangle> = (l,a)" | |
74 |
"del_rightmost \<langle>l, a, r\<rangle> = (let (r',x) = del_rightmost r in (\<langle>l, a, r'\<rangle>, x))" |
|
57687 | 75 |
|
76 |
lemma del_rightmost_set_tree_if_bst: |
|
77 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> |
|
78 |
\<Longrightarrow> x \<in> set_tree t \<and> set_tree t' = set_tree t - {x}" |
|
79 |
apply(induction t arbitrary: t' rule: del_rightmost.induct) |
|
80 |
apply (fastforce simp: ball_Un split: prod.splits)+ |
|
81 |
done |
|
82 |
||
83 |
lemma del_rightmost_set_tree: |
|
58424 | 84 |
"\<lbrakk> del_rightmost t = (t',x); t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> set_tree t = insert x (set_tree t')" |
57687 | 85 |
apply(induction t arbitrary: t' rule: del_rightmost.induct) |
86 |
by (auto split: prod.splits) auto |
|
87 |
||
88 |
lemma del_rightmost_bst: |
|
58424 | 89 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> bst t'" |
57687 | 90 |
proof(induction t arbitrary: t' rule: del_rightmost.induct) |
91 |
case (2 l a rl b rr) |
|
92 |
let ?r = "Node rl b rr" |
|
93 |
from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'" |
|
94 |
by(simp split: prod.splits) |
|
95 |
from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH") |
|
96 |
qed auto |
|
97 |
||
98 |
||
58424 | 99 |
lemma del_rightmost_greater: "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> |
57687 | 100 |
\<Longrightarrow> \<forall>a\<in>set_tree t'. a < x" |
101 |
proof(induction t arbitrary: t' rule: del_rightmost.induct) |
|
102 |
case (2 l a rl b rr) |
|
103 |
from "2.prems"(1) obtain r' |
|
104 |
where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'" |
|
105 |
by(simp split: prod.splits) |
|
106 |
show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm] |
|
107 |
by (fastforce simp add: ball_Un) |
|
108 |
qed simp_all |
|
109 |
||
110 |
lemma del_rightmost_Max: |
|
58424 | 111 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> x = Max(set_tree t)" |
58467 | 112 |
by (metis Max_insert2 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le) |
57687 | 113 |
|
57250 | 114 |
end |