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