author | blanchet |
Thu, 11 Sep 2014 19:32:36 +0200 | |
changeset 58310 | 91ea607a34d8 |
parent 57687 | cca7e8788481 |
child 58424 | cbbba613b6ab |
permissions | -rw-r--r-- |
57250 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
header {* Binary Tree *} |
|
4 |
||
5 |
theory Tree |
|
6 |
imports Main |
|
7 |
begin |
|
8 |
||
58310 | 9 |
datatype 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree") |
57449
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 | 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 | 16 |
by (cases t) auto |
57250 | 17 |
|
57530 | 18 |
lemma set_tree_Node2: "set_tree(Node l x r) = insert x (set_tree l \<union> set_tree r)" |
19 |
by auto |
|
20 |
||
57687 | 21 |
lemma finite_set_tree[simp]: "finite(set_tree t)" |
22 |
by(induction t) auto |
|
23 |
||
24 |
||
25 |
subsection "The set of subtrees" |
|
26 |
||
57250 | 27 |
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where |
57450 | 28 |
"subtrees Leaf = {Leaf}" | |
29 |
"subtrees (Node l a r) = insert (Node l a r) (subtrees l \<union> subtrees r)" |
|
57250 | 30 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
31 |
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
|
32 |
by (induction t)(auto) |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
33 |
|
57450 | 34 |
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
|
35 |
by (induction t) auto |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
36 |
|
57450 | 37 |
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
|
38 |
by (metis Node_notin_subtrees_if) |
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
39 |
|
57687 | 40 |
|
41 |
subsection "Inorder list of entries" |
|
42 |
||
57250 | 43 |
fun inorder :: "'a tree \<Rightarrow> 'a list" where |
57450 | 44 |
"inorder Leaf = []" | |
45 |
"inorder (Node l x r) = inorder l @ [x] @ inorder r" |
|
57250 | 46 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
47 |
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
|
48 |
by (induction t) auto |
57250 | 49 |
|
57687 | 50 |
|
57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset
|
51 |
subsection {* Binary Search Tree predicate *} |
57250 | 52 |
|
57450 | 53 |
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where |
54 |
"bst Leaf \<longleftrightarrow> True" | |
|
55 |
"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 | 56 |
|
57450 | 57 |
lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" |
58 |
by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
|
57250 | 59 |
|
57687 | 60 |
|
61 |
subsection "Deletion of the rightmost entry" |
|
62 |
||
63 |
fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where |
|
64 |
"del_rightmost (Node l a Leaf) = (l,a)" | |
|
65 |
"del_rightmost (Node l a r) = (let (r',x) = del_rightmost r in (Node l a r', x))" |
|
66 |
||
67 |
lemma del_rightmost_set_tree_if_bst: |
|
68 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> |
|
69 |
\<Longrightarrow> x \<in> set_tree t \<and> set_tree t' = set_tree t - {x}" |
|
70 |
apply(induction t arbitrary: t' rule: del_rightmost.induct) |
|
71 |
apply (fastforce simp: ball_Un split: prod.splits)+ |
|
72 |
done |
|
73 |
||
74 |
lemma del_rightmost_set_tree: |
|
75 |
"\<lbrakk> del_rightmost t = (t',x); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> set_tree t = insert x (set_tree t')" |
|
76 |
apply(induction t arbitrary: t' rule: del_rightmost.induct) |
|
77 |
by (auto split: prod.splits) auto |
|
78 |
||
79 |
lemma del_rightmost_bst: |
|
80 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> bst t'" |
|
81 |
proof(induction t arbitrary: t' rule: del_rightmost.induct) |
|
82 |
case (2 l a rl b rr) |
|
83 |
let ?r = "Node rl b rr" |
|
84 |
from "2.prems"(1) obtain r' where 1: "del_rightmost ?r = (r',x)" and [simp]: "t' = Node l a r'" |
|
85 |
by(simp split: prod.splits) |
|
86 |
from "2.prems"(2) 1 del_rightmost_set_tree[OF 1] show ?case by(auto)(simp add: "2.IH") |
|
87 |
qed auto |
|
88 |
||
89 |
||
90 |
lemma del_rightmost_greater: "\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> |
|
91 |
\<Longrightarrow> \<forall>a\<in>set_tree t'. a < x" |
|
92 |
proof(induction t arbitrary: t' rule: del_rightmost.induct) |
|
93 |
case (2 l a rl b rr) |
|
94 |
from "2.prems"(1) obtain r' |
|
95 |
where dm: "del_rightmost (Node rl b rr) = (r',x)" and [simp]: "t' = Node l a r'" |
|
96 |
by(simp split: prod.splits) |
|
97 |
show ?case using "2.prems"(2) "2.IH"[OF dm] del_rightmost_set_tree_if_bst[OF dm] |
|
98 |
by (fastforce simp add: ball_Un) |
|
99 |
qed simp_all |
|
100 |
||
101 |
(* should be moved but metis not available in much of Main *) |
|
102 |
lemma Max_insert1: "\<lbrakk> finite A; \<forall>a\<in>A. a \<le> x \<rbrakk> \<Longrightarrow> Max(insert x A) = x" |
|
103 |
by (metis Max_in Max_insert Max_singleton antisym max_def) |
|
104 |
||
105 |
lemma del_rightmost_Max: |
|
106 |
"\<lbrakk> del_rightmost t = (t',x); bst t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> x = Max(set_tree t)" |
|
107 |
by (metis Max_insert1 del_rightmost_greater del_rightmost_set_tree finite_set_tree less_le_not_le) |
|
108 |
||
57250 | 109 |
end |