|
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 |
|
99 definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) map" where |
|
100 "Tree t = Map (Tree.lookup t)" |
|
101 |
|
102 lemma [code, code del]: |
|
103 "(eq_class.eq :: (_, _) map \<Rightarrow> _) = eq_class.eq" .. |
|
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 |
|
118 lemma update_Tree [code]: |
|
119 "Mapping.update k v (Tree t) = Tree (update k v t)" |
|
120 by (simp add: Tree_def lookup_update) |
|
121 |
|
122 lemma keys_Tree [code]: |
|
123 "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))" |
|
124 by (simp add: Tree_def dom_lookup) |
|
125 |
|
126 lemma size_Tree [code]: |
|
127 "Mapping.size (Tree t) = size t" |
|
128 proof - |
|
129 have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))" |
|
130 unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def) |
|
131 then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def) |
|
132 qed |
|
133 |
|
134 lemma tabulate_Tree [code]: |
|
135 "Mapping.tabulate ks f = Tree (bulkload (sort ks) f)" |
|
136 proof - |
|
137 have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))" |
|
138 by (simp add: lookup_Tree lookup_bulkload lookup_tabulate) |
|
139 then show ?thesis by (simp add: lookup_inject) |
|
140 qed |
|
141 |
|
142 end |