author | nipkow |
Tue, 15 Aug 2017 09:29:35 +0200 | |
changeset 66425 | 8756322dc5de |
parent 66419 | 8194ed7cf2cb |
child 66491 | 78a009ac91d2 |
permissions | -rw-r--r-- |
62706 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section \<open>Leftist Heap\<close> |
|
4 |
||
5 |
theory Leftist_Heap |
|
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
6 |
imports |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
7 |
Tree2 |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
8 |
Priority_Queue |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
9 |
Complex_Main |
62706 | 10 |
begin |
11 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
12 |
(* FIXME mv Base *) |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
13 |
lemma size_prod_measure[measure_function]: |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
14 |
"is_measure f \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
15 |
by (rule is_measure_trivial) |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
16 |
|
64968 | 17 |
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where |
18 |
"mset_tree Leaf = {#}" | |
|
19 |
"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r" |
|
20 |
||
62706 | 21 |
type_synonym 'a lheap = "('a,nat)tree" |
22 |
||
23 |
fun rank :: "'a lheap \<Rightarrow> nat" where |
|
24 |
"rank Leaf = 0" | |
|
25 |
"rank (Node _ _ _ r) = rank r + 1" |
|
26 |
||
27 |
fun rk :: "'a lheap \<Rightarrow> nat" where |
|
28 |
"rk Leaf = 0" | |
|
29 |
"rk (Node n _ _ _) = n" |
|
30 |
||
64968 | 31 |
text{* The invariants: *} |
32 |
||
33 |
fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where |
|
34 |
"heap Leaf = True" | |
|
35 |
"heap (Node _ l m r) = |
|
36 |
(heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))" |
|
62706 | 37 |
|
64973 | 38 |
fun ltree :: "'a lheap \<Rightarrow> bool" where |
39 |
"ltree Leaf = True" | |
|
40 |
"ltree (Node n l a r) = |
|
41 |
(n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)" |
|
62706 | 42 |
|
43 |
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where |
|
44 |
"node l a r = |
|
45 |
(let rl = rk l; rr = rk r |
|
46 |
in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)" |
|
47 |
||
48 |
fun get_min :: "'a lheap \<Rightarrow> 'a" where |
|
49 |
"get_min(Node n l a r) = a" |
|
50 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
51 |
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where |
64976 | 52 |
"merge Leaf t2 = t2" | |
53 |
"merge t1 Leaf = t1" | |
|
54 |
"merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) = |
|
55 |
(if a1 \<le> a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2)) |
|
56 |
else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))" |
|
62706 | 57 |
|
64976 | 58 |
lemma merge_code: "merge t1 t2 = (case (t1,t2) of |
62706 | 59 |
(Leaf, _) \<Rightarrow> t2 | |
60 |
(_, Leaf) \<Rightarrow> t1 | |
|
61 |
(Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow> |
|
64976 | 62 |
if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))" |
63 |
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split) |
|
62706 | 64 |
|
65 |
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where |
|
64976 | 66 |
"insert x t = merge (Node 1 Leaf x Leaf) t" |
62706 | 67 |
|
68 |
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where |
|
69 |
"del_min Leaf = Leaf" | |
|
64976 | 70 |
"del_min (Node n l x r) = merge l r" |
62706 | 71 |
|
72 |
||
73 |
subsection "Lemmas" |
|
74 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
75 |
(* FIXME mv DS_Base *) |
62706 | 76 |
declare Let_def [simp] |
77 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
78 |
lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
79 |
by(cases t) auto |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
80 |
|
64973 | 81 |
lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t" |
62706 | 82 |
by(cases t) auto |
83 |
||
64973 | 84 |
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r" |
62706 | 85 |
by(auto simp add: node_def) |
86 |
||
64968 | 87 |
lemma heap_node: "heap (node l a r) \<longleftrightarrow> |
88 |
heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)" |
|
89 |
by(auto simp add: node_def) |
|
90 |
||
62706 | 91 |
|
92 |
subsection "Functional Correctness" |
|
93 |
||
64976 | 94 |
lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2" |
95 |
by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps) |
|
62706 | 96 |
|
64968 | 97 |
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}" |
64976 | 98 |
by (auto simp add: insert_def mset_merge) |
62706 | 99 |
|
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
100 |
lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)" |
66425 | 101 |
by (induction h) (auto simp add: eq_Min_iff) |
64968 | 102 |
|
62706 | 103 |
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}" |
64976 | 104 |
by (cases h) (auto simp: mset_merge) |
62706 | 105 |
|
64976 | 106 |
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)" |
107 |
proof(induction l r rule: merge.induct) |
|
62706 | 108 |
case (3 n1 l1 a1 r1 n2 l2 a2 r2) |
64976 | 109 |
show ?case (is "ltree(merge ?t1 ?t2)") |
62706 | 110 |
proof cases |
111 |
assume "a1 \<le> a2" |
|
64976 | 112 |
hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp |
113 |
also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))" |
|
64973 | 114 |
by(simp add: ltree_node) |
62706 | 115 |
also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp) |
116 |
finally show ?thesis . |
|
117 |
next (* analogous but automatic *) |
|
118 |
assume "\<not> a1 \<le> a2" |
|
64973 | 119 |
thus ?thesis using 3 by(simp)(auto simp: ltree_node) |
62706 | 120 |
qed |
121 |
qed simp_all |
|
122 |
||
64976 | 123 |
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)" |
124 |
proof(induction l r rule: merge.induct) |
|
125 |
case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un) |
|
64968 | 126 |
qed simp_all |
127 |
||
64973 | 128 |
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)" |
64976 | 129 |
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split) |
62706 | 130 |
|
64968 | 131 |
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)" |
64976 | 132 |
by(simp add: insert_def heap_merge del: merge.simps split: tree.split) |
64968 | 133 |
|
64973 | 134 |
lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)" |
64976 | 135 |
by(cases t)(auto simp add: ltree_merge simp del: merge.simps) |
62706 | 136 |
|
64968 | 137 |
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)" |
64976 | 138 |
by(cases t)(auto simp add: heap_merge simp del: merge.simps) |
64968 | 139 |
|
62706 | 140 |
|
141 |
interpretation lheap: Priority_Queue |
|
64975 | 142 |
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf" |
143 |
and insert = insert and del_min = del_min |
|
64973 | 144 |
and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h" |
64968 | 145 |
and mset = mset_tree |
62706 | 146 |
proof(standard, goal_cases) |
147 |
case 1 show ?case by simp |
|
148 |
next |
|
64975 | 149 |
case (2 q) show ?case by (cases q) auto |
62706 | 150 |
next |
64975 | 151 |
case 3 show ?case by(rule mset_insert) |
152 |
next |
|
153 |
case 4 show ?case by(rule mset_del_min) |
|
62706 | 154 |
next |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
155 |
case 5 thus ?case by(simp add: get_min mset_tree_empty) |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
156 |
next |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
157 |
case 6 thus ?case by(simp) |
62706 | 158 |
next |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
159 |
case 7 thus ?case by(simp add: heap_insert ltree_insert) |
64968 | 160 |
next |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
161 |
case 8 thus ?case by(simp add: heap_del_min ltree_del_min) |
62706 | 162 |
qed |
163 |
||
164 |
||
165 |
subsection "Complexity" |
|
166 |
||
64973 | 167 |
lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t" |
62706 | 168 |
proof(induction t) |
169 |
case Leaf show ?case by simp |
|
170 |
next |
|
171 |
case (Node n l a r) |
|
172 |
hence "rank r \<le> rank l" by simp |
|
173 |
hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp |
|
174 |
have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r" |
|
175 |
by(simp add: mult_2) |
|
176 |
also have "\<dots> \<le> size1 l + size1 r" |
|
177 |
using Node * by (simp del: power_increasing_iff) |
|
178 |
also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp |
|
179 |
finally show ?case . |
|
180 |
qed |
|
181 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
182 |
fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where |
64976 | 183 |
"t_merge Leaf t2 = 1" | |
184 |
"t_merge t2 Leaf = 1" | |
|
185 |
"t_merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) = |
|
186 |
(if a1 \<le> a2 then 1 + t_merge r1 (Node n2 l2 a2 r2) |
|
187 |
else 1 + t_merge r2 (Node n1 l1 a1 r1))" |
|
62706 | 188 |
|
189 |
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where |
|
64976 | 190 |
"t_insert x t = t_merge (Node 1 Leaf x Leaf) t" |
62706 | 191 |
|
192 |
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where |
|
193 |
"t_del_min Leaf = 1" | |
|
64976 | 194 |
"t_del_min (Node n l a r) = t_merge l r" |
62706 | 195 |
|
64976 | 196 |
lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1" |
197 |
proof(induction l r rule: merge.induct) |
|
62706 | 198 |
case 3 thus ?case |
64976 | 199 |
by(simp)(fastforce split: tree.splits simp del: t_merge.simps) |
62706 | 200 |
qed simp_all |
201 |
||
64976 | 202 |
corollary t_merge_log: assumes "ltree l" "ltree r" |
203 |
shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1" |
|
62706 | 204 |
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]] |
64976 | 205 |
le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r] |
62706 | 206 |
by linarith |
207 |
||
64973 | 208 |
corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2" |
64976 | 209 |
using t_merge_log[of "Node 1 Leaf x Leaf" t] |
62706 | 210 |
by(simp add: t_insert_def split: tree.split) |
211 |
||
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
212 |
(* FIXME mv Lemmas_log *) |
62706 | 213 |
lemma ld_ld_1_less: |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
214 |
assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)" |
62706 | 215 |
proof - |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset
|
216 |
have "2 powr (log 2 x + log 2 y + 1) = 2*x*y" |
64977 | 217 |
using assms by(simp add: powr_add) |
218 |
also have "\<dots> < (x+y)^2" using assms |
|
62706 | 219 |
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos) |
64977 | 220 |
also have "\<dots> = 2 powr (2 * log 2 (x+y))" |
221 |
using assms by(simp add: powr_add log_powr[symmetric] powr_numeral) |
|
222 |
finally show ?thesis by simp |
|
62706 | 223 |
qed |
224 |
||
64973 | 225 |
corollary t_del_min_log: assumes "ltree t" |
62706 | 226 |
shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1" |
227 |
proof(cases t) |
|
228 |
case Leaf thus ?thesis using assms by simp |
|
229 |
next |
|
230 |
case [simp]: (Node _ t1 _ t2) |
|
64976 | 231 |
have "t_del_min t = t_merge t1 t2" by simp |
62706 | 232 |
also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1" |
64976 | 233 |
using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps) |
62706 | 234 |
also have "\<dots> \<le> 2 * log 2 (size1 t) + 1" |
235 |
using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp) |
|
236 |
finally show ?thesis . |
|
237 |
qed |
|
238 |
||
239 |
end |