31459
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
|
2 |
|
|
3 |
header {* Trees implementing mappings. *}
|
|
4 |
|
|
5 |
theory Tree
|
|
6 |
imports Mapping
|
|
7 |
begin
|
|
8 |
|
|
9 |
subsection {* Type definition and operations *}
|
|
10 |
|
|
11 |
datatype ('a, 'b) tree = Empty
|
|
12 |
| Branch 'b 'a "('a, 'b) tree" "('a, 'b) tree"
|
|
13 |
|
|
14 |
primrec lookup :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a \<rightharpoonup> 'b" where
|
|
15 |
"lookup Empty = (\<lambda>_. None)"
|
|
16 |
| "lookup (Branch v k l r) = (\<lambda>k'. if k' = k then Some v
|
|
17 |
else if k' \<le> k then lookup l k' else lookup r k')"
|
|
18 |
|
|
19 |
primrec update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) tree \<Rightarrow> ('a, 'b) tree" where
|
|
20 |
"update k v Empty = Branch v k Empty Empty"
|
|
21 |
| "update k' v' (Branch v k l r) = (if k' = k then
|
|
22 |
Branch v' k l r else if k' \<le> k
|
|
23 |
then Branch v k (update k' v' l) r
|
|
24 |
else Branch v k l (update k' v' r))"
|
|
25 |
|
|
26 |
primrec keys :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a list" where
|
|
27 |
"keys Empty = []"
|
|
28 |
| "keys (Branch _ k l r) = k # keys l @ keys r"
|
|
29 |
|
|
30 |
definition size :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> nat" where
|
|
31 |
"size t = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
|
|
32 |
|
|
33 |
fun bulkload :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) tree" where
|
|
34 |
[simp del]: "bulkload ks f = (case ks of [] \<Rightarrow> Empty | _ \<Rightarrow> let
|
|
35 |
mid = length ks div 2;
|
|
36 |
ys = take mid ks;
|
|
37 |
x = ks ! mid;
|
|
38 |
zs = drop (Suc mid) ks
|
|
39 |
in Branch (f x) x (bulkload ys f) (bulkload zs f))"
|
|
40 |
|
|
41 |
|
|
42 |
subsection {* Properties *}
|
|
43 |
|
|
44 |
lemma dom_lookup:
|
|
45 |
"dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
|
|
46 |
proof -
|
|
47 |
have "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (keys t))"
|
|
48 |
by (induct t) (auto simp add: dom_if)
|
|
49 |
also have "\<dots> = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
|
|
50 |
by simp
|
|
51 |
finally show ?thesis .
|
|
52 |
qed
|
|
53 |
|
|
54 |
lemma lookup_finite:
|
|
55 |
"finite (dom (lookup t))"
|
|
56 |
unfolding dom_lookup by simp
|
|
57 |
|
|
58 |
lemma lookup_update:
|
|
59 |
"lookup (update k v t) = (lookup t)(k \<mapsto> v)"
|
|
60 |
by (induct t) (simp_all add: expand_fun_eq)
|
|
61 |
|
|
62 |
lemma lookup_bulkload:
|
|
63 |
"sorted ks \<Longrightarrow> lookup (bulkload ks f) = (Some o f) |` set ks"
|
|
64 |
proof (induct ks f rule: bulkload.induct)
|
|
65 |
case (1 ks f) show ?case proof (cases ks)
|
|
66 |
case Nil then show ?thesis by (simp add: bulkload.simps)
|
|
67 |
next
|
|
68 |
case (Cons w ws)
|
|
69 |
then have case_simp: "\<And>w v::('a, 'b) tree. (case ks of [] \<Rightarrow> v | _ \<Rightarrow> w) = w"
|
|
70 |
by (cases ks) auto
|
|
71 |
from Cons have "ks \<noteq> []" by simp
|
|
72 |
then have "0 < length ks" by simp
|
|
73 |
let ?mid = "length ks div 2"
|
|
74 |
let ?ys = "take ?mid ks"
|
|
75 |
let ?x = "ks ! ?mid"
|
|
76 |
let ?zs = "drop (Suc ?mid) ks"
|
|
77 |
from `ks \<noteq> []` have ks_split: "ks = ?ys @ [?x] @ ?zs"
|
|
78 |
by (simp add: id_take_nth_drop)
|
|
79 |
then have in_ks: "\<And>x. x \<in> set ks \<longleftrightarrow> x \<in> set (?ys @ [?x] @ ?zs)"
|
|
80 |
by simp
|
|
81 |
with ks_split have ys_x: "\<And>y. y \<in> set ?ys \<Longrightarrow> y \<le> ?x"
|
|
82 |
and x_zs: "\<And>z. z \<in> set ?zs \<Longrightarrow> ?x \<le> z"
|
|
83 |
using `sorted ks` sorted_append [of "?ys" "[?x] @ ?zs"] sorted_append [of "[?x]" "?zs"]
|
|
84 |
by simp_all
|
|
85 |
have ys: "lookup (bulkload ?ys f) = (Some o f) |` set ?ys"
|
|
86 |
by (rule "1.hyps"(1)) (auto intro: Cons sorted_take `sorted ks`)
|
|
87 |
have zs: "lookup (bulkload ?zs f) = (Some o f) |` set ?zs"
|
|
88 |
by (rule "1.hyps"(2)) (auto intro: Cons sorted_drop `sorted ks`)
|
|
89 |
show ?thesis using `0 < length ks`
|
|
90 |
by (simp add: bulkload.simps)
|
|
91 |
(auto simp add: restrict_map_def in_ks case_simp Let_def ys zs expand_fun_eq
|
|
92 |
dest: in_set_takeD in_set_dropD ys_x x_zs)
|
|
93 |
qed
|
|
94 |
qed
|
|
95 |
|
|
96 |
|
|
97 |
subsection {* Trees as mappings *}
|
|
98 |
|
35158
|
99 |
definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) mapping" where
|
|
100 |
"Tree t = Mapping (Tree.lookup t)"
|
31459
|
101 |
|
|
102 |
lemma [code, code del]:
|
35158
|
103 |
"(eq_class.eq :: (_, _) mapping \<Rightarrow> _) = eq_class.eq" ..
|
31459
|
104 |
|
|
105 |
lemma [code, code del]:
|
|
106 |
"Mapping.delete k m = Mapping.delete k m" ..
|
|
107 |
|
|
108 |
code_datatype Tree
|
|
109 |
|
|
110 |
lemma empty_Tree [code]:
|
|
111 |
"Mapping.empty = Tree Empty"
|
|
112 |
by (simp add: Tree_def Mapping.empty_def)
|
|
113 |
|
|
114 |
lemma lookup_Tree [code]:
|
|
115 |
"Mapping.lookup (Tree t) = lookup t"
|
|
116 |
by (simp add: Tree_def)
|
|
117 |
|
35158
|
118 |
lemma is_empty_Tree [code]:
|
|
119 |
"Mapping.is_empty (Tree Empty) \<longleftrightarrow> True"
|
|
120 |
"Mapping.is_empty (Tree (Branch v k l r)) \<longleftrightarrow> False"
|
|
121 |
by (simp_all only: is_empty_def lookup_Tree dom_lookup) auto
|
|
122 |
|
31459
|
123 |
lemma update_Tree [code]:
|
|
124 |
"Mapping.update k v (Tree t) = Tree (update k v t)"
|
|
125 |
by (simp add: Tree_def lookup_update)
|
|
126 |
|
|
127 |
lemma keys_Tree [code]:
|
|
128 |
"Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
|
35158
|
129 |
by (simp add: Mapping.keys_def lookup_Tree dom_lookup)
|
31459
|
130 |
|
|
131 |
lemma size_Tree [code]:
|
|
132 |
"Mapping.size (Tree t) = size t"
|
|
133 |
proof -
|
|
134 |
have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
|
|
135 |
unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def)
|
|
136 |
then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def)
|
|
137 |
qed
|
|
138 |
|
|
139 |
lemma tabulate_Tree [code]:
|
|
140 |
"Mapping.tabulate ks f = Tree (bulkload (sort ks) f)"
|
|
141 |
proof -
|
|
142 |
have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))"
|
35158
|
143 |
by (simp add: lookup_bulkload lookup_Tree)
|
|
144 |
then show ?thesis by (simp only: lookup_inject)
|
31459
|
145 |
qed
|
|
146 |
|
35158
|
147 |
hide (open) const Empty Branch lookup update keys size bulkload Tree
|
|
148 |
|
31459
|
149 |
end
|