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 

64973

30 
fun ltree :: "'a lheap \<Rightarrow> bool" where


31 
"ltree Leaf = True" 


32 
"ltree (Node n l a r) =


33 
(n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"

62706

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 

64976

43 
function merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where


44 
"merge Leaf t2 = t2" 


45 
"merge t1 Leaf = t1" 


46 
"merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =


47 
(if a1 \<le> a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2))


48 
else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))"

62706

49 
by pat_completeness auto


50 
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto


51 

64976

52 
lemma merge_code: "merge t1 t2 = (case (t1,t2) of

62706

53 
(Leaf, _) \<Rightarrow> t2 


54 
(_, Leaf) \<Rightarrow> t1 


55 
(Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>

64976

56 
if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"


57 
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)

62706

58 


59 
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where

64976

60 
"insert x t = merge (Node 1 Leaf x Leaf) t"

62706

61 


62 
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where


63 
"del_min Leaf = Leaf" 

64976

64 
"del_min (Node n l x r) = merge l r"

62706

65 


66 


67 
subsection "Lemmas"


68 


69 
declare Let_def [simp]


70 

64973

71 
lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"

62706

72 
by(cases t) auto


73 

64973

74 
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"

62706

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"

64975

86 
and is_empty :: "'q \<Rightarrow> bool"

64971

87 
and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"


88 
and get_min :: "'q \<Rightarrow> 'a"


89 
and del_min :: "'q \<Rightarrow> 'q"


90 
and invar :: "'q \<Rightarrow> bool"


91 
and mset :: "'q \<Rightarrow> 'a multiset"

62706

92 
assumes mset_empty: "mset empty = {#}"

64975

93 
and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"

64971

94 
and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"


95 
and mset_del_min: "invar q \<Longrightarrow> mset (del_min q) = mset q  {#get_min q#}"


96 
and get_min: "invar q \<Longrightarrow> q \<noteq> empty \<Longrightarrow>


97 
get_min q \<in> set_mset(mset q) \<and> (\<forall>x \<in># mset q. get_min q \<le> x)"


98 
and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"


99 
and invar_del_min: "invar q \<Longrightarrow> invar (del_min q)"

62706

100 


101 

64976

102 
lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"


103 
by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)

62706

104 

64968

105 
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"

64976

106 
by (auto simp add: insert_def mset_merge)

62706

107 

64968

108 
lemma get_min:


109 
"heap h \<Longrightarrow> h \<noteq> Leaf \<Longrightarrow>


110 
get_min h \<in> set_mset(mset_tree h) \<and> (\<forall>x \<in># mset_tree h. get_min h \<le> x)"


111 
by (induction h) (auto)


112 

62706

113 
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h  {# get_min h #}"

64976

114 
by (cases h) (auto simp: mset_merge)

62706

115 

64976

116 
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"


117 
proof(induction l r rule: merge.induct)

62706

118 
case (3 n1 l1 a1 r1 n2 l2 a2 r2)

64976

119 
show ?case (is "ltree(merge ?t1 ?t2)")

62706

120 
proof cases


121 
assume "a1 \<le> a2"

64976

122 
hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp


123 
also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"

64973

124 
by(simp add: ltree_node)

62706

125 
also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)


126 
finally show ?thesis .


127 
next (* analogous but automatic *)


128 
assume "\<not> a1 \<le> a2"

64973

129 
thus ?thesis using 3 by(simp)(auto simp: ltree_node)

62706

130 
qed


131 
qed simp_all


132 

64976

133 
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"


134 
proof(induction l r rule: merge.induct)


135 
case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)

64968

136 
qed simp_all


137 

64973

138 
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"

64976

139 
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)

62706

140 

64968

141 
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"

64976

142 
by(simp add: insert_def heap_merge del: merge.simps split: tree.split)

64968

143 

64973

144 
lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"

64976

145 
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)

62706

146 

64968

147 
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"

64976

148 
by(cases t)(auto simp add: heap_merge simp del: merge.simps)

64968

149 

62706

150 


151 
interpretation lheap: Priority_Queue

64975

152 
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"


153 
and insert = insert and del_min = del_min

64973

154 
and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h"

64968

155 
and mset = mset_tree

62706

156 
proof(standard, goal_cases)


157 
case 1 show ?case by simp


158 
next

64975

159 
case (2 q) show ?case by (cases q) auto

62706

160 
next

64975

161 
case 3 show ?case by(rule mset_insert)


162 
next


163 
case 4 show ?case by(rule mset_del_min)

62706

164 
next

64975

165 
case 5 thus ?case by(simp add: get_min)

62706

166 
next

64975

167 
case 6 thus ?case by(simp add: heap_insert ltree_insert)

64968

168 
next

64975

169 
case 7 thus ?case by(simp add: heap_del_min ltree_del_min)

62706

170 
qed


171 


172 


173 
subsection "Complexity"


174 

64973

175 
lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t"

62706

176 
proof(induction t)


177 
case Leaf show ?case by simp


178 
next


179 
case (Node n l a r)


180 
hence "rank r \<le> rank l" by simp


181 
hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp


182 
have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r"


183 
by(simp add: mult_2)


184 
also have "\<dots> \<le> size1 l + size1 r"


185 
using Node * by (simp del: power_increasing_iff)


186 
also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp


187 
finally show ?case .


188 
qed


189 

64976

190 
function t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where


191 
"t_merge Leaf t2 = 1" 


192 
"t_merge t2 Leaf = 1" 


193 
"t_merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =


194 
(if a1 \<le> a2 then 1 + t_merge r1 (Node n2 l2 a2 r2)


195 
else 1 + t_merge r2 (Node n1 l1 a1 r1))"

62706

196 
by pat_completeness auto


197 
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto


198 


199 
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where

64976

200 
"t_insert x t = t_merge (Node 1 Leaf x Leaf) t"

62706

201 


202 
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where


203 
"t_del_min Leaf = 1" 

64976

204 
"t_del_min (Node n l a r) = t_merge l r"

62706

205 

64976

206 
lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"


207 
proof(induction l r rule: merge.induct)

62706

208 
case 3 thus ?case

64976

209 
by(simp)(fastforce split: tree.splits simp del: t_merge.simps)

62706

210 
qed simp_all


211 

64976

212 
corollary t_merge_log: assumes "ltree l" "ltree r"


213 
shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"

62706

214 
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]

64976

215 
le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r]

62706

216 
by linarith


217 

64973

218 
corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"

64976

219 
using t_merge_log[of "Node 1 Leaf x Leaf" t]

62706

220 
by(simp add: t_insert_def split: tree.split)


221 


222 
lemma ld_ld_1_less:


223 
assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)"


224 
proof 


225 
have 1: "2*x*y < (x+y)^2" using assms


226 
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)


227 
show ?thesis


228 
apply(rule powr_less_cancel_iff[of 2, THEN iffD1])


229 
apply simp


230 
using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)


231 
qed


232 

64973

233 
corollary t_del_min_log: assumes "ltree t"

62706

234 
shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"


235 
proof(cases t)


236 
case Leaf thus ?thesis using assms by simp


237 
next


238 
case [simp]: (Node _ t1 _ t2)

64976

239 
have "t_del_min t = t_merge t1 t2" by simp

62706

240 
also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"

64976

241 
using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)

62706

242 
also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"


243 
using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)


244 
finally show ?thesis .


245 
qed


246 


247 
end
