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 


9 
type_synonym 'a lheap = "('a,nat)tree"


10 


11 
fun rank :: "'a lheap \<Rightarrow> nat" where


12 
"rank Leaf = 0" 


13 
"rank (Node _ _ _ r) = rank r + 1"


14 


15 
fun rk :: "'a lheap \<Rightarrow> nat" where


16 
"rk Leaf = 0" 


17 
"rk (Node n _ _ _) = n"


18 


19 
text{* The invariant: *}


20 


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


22 
"lheap Leaf = True" 


23 
"lheap (Node n l a r) =


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


25 


26 
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where


27 
"node l a r =


28 
(let rl = rk l; rr = rk r


29 
in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"


30 


31 
fun get_min :: "'a lheap \<Rightarrow> 'a" where


32 
"get_min(Node n l a r) = a"


33 


34 
function meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where


35 
"meld Leaf t2 = t2" 


36 
"meld t1 Leaf = t1" 


37 
"meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =


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


39 
else node l2 a2 (meld r2 (Node n1 l1 a1 r1)))"


40 
by pat_completeness auto


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


42 


43 
lemma meld_code: "meld t1 t2 = (case (t1,t2) of


44 
(Leaf, _) \<Rightarrow> t2 


45 
(_, Leaf) \<Rightarrow> t1 


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


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


48 
by(induction t1 t2 rule: meld.induct) (simp_all split: tree.split)


49 


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


51 
"insert x t = meld (Node 1 Leaf x Leaf) t"


52 


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


54 
"del_min Leaf = Leaf" 


55 
"del_min (Node n l x r) = meld l r"


56 


57 


58 
subsection "Lemmas"


59 


60 
declare Let_def [simp]


61 


62 
lemma rk_eq_rank[simp]: "lheap t \<Longrightarrow> rk t = rank t"


63 
by(cases t) auto


64 


65 
lemma lheap_node: "lheap (node l a r) \<longleftrightarrow> lheap l \<and> lheap r"


66 
by(auto simp add: node_def)


67 


68 


69 
subsection "Functional Correctness"


70 


71 
locale Priority_Queue =


72 
fixes empty :: "'pq"


73 
and insert :: "'a \<Rightarrow> 'pq \<Rightarrow> 'pq"


74 
and get_min :: "'pq \<Rightarrow> 'a"


75 
and del_min :: "'pq \<Rightarrow> 'pq"


76 
and invar :: "'pq \<Rightarrow> bool"


77 
and mset :: "'pq \<Rightarrow> 'a multiset"


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


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


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


81 
and invar_insert: "invar pq \<Longrightarrow> invar (insert x pq)"


82 
and invar_del_min: "invar pq \<Longrightarrow> invar (del_min pq)"


83 


84 


85 
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where


86 
"mset_tree Leaf = {#}" 


87 
"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"


88 


89 


90 
lemma mset_meld: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2"


91 
by (induction h1 h2 rule: meld.induct) (auto simp add: node_def ac_simps)


92 


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


94 
by (auto simp add: insert_def mset_meld)


95 


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


97 
by (cases h) (auto simp: mset_meld ac_simps subset_mset.diff_add_assoc)


98 


99 


100 
lemma lheap_meld: "\<lbrakk> lheap l; lheap r \<rbrakk> \<Longrightarrow> lheap (meld l r)"


101 
proof(induction l r rule: meld.induct)


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


103 
show ?case (is "lheap(meld ?t1 ?t2)")


104 
proof cases


105 
assume "a1 \<le> a2"


106 
hence "lheap (meld ?t1 ?t2) = lheap (node l1 a1 (meld r1 ?t2))" by simp


107 
also have "\<dots> = (lheap l1 \<and> lheap(meld r1 ?t2))"


108 
by(simp add: lheap_node)


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


110 
finally show ?thesis .


111 
next (* analogous but automatic *)


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


113 
thus ?thesis using 3 by(simp)(auto simp: lheap_node)


114 
qed


115 
qed simp_all


116 


117 
lemma lheap_insert: "lheap t \<Longrightarrow> lheap(insert x t)"


118 
by(simp add: insert_def lheap_meld del: meld.simps split: tree.split)


119 


120 
lemma lheap_del_min: "lheap t \<Longrightarrow> lheap(del_min t)"


121 
by(cases t)(auto simp add: lheap_meld simp del: meld.simps)


122 


123 


124 
interpretation lheap: Priority_Queue


125 
where empty = Leaf and insert = insert and del_min = del_min


126 
and get_min = get_min and invar = lheap and mset = mset_tree


127 
proof(standard, goal_cases)


128 
case 1 show ?case by simp


129 
next


130 
case 2 show ?case by(rule mset_insert)


131 
next


132 
case 3 show ?case by(rule mset_del_min)


133 
next


134 
case 4 thus ?case by(rule lheap_insert)


135 
next


136 
case 5 thus ?case by(rule lheap_del_min)


137 
qed


138 


139 


140 
subsection "Complexity"


141 


142 
lemma pow2_rank_size1: "lheap t \<Longrightarrow> 2 ^ rank t \<le> size1 t"


143 
proof(induction t)


144 
case Leaf show ?case by simp


145 
next


146 
case (Node n l a r)


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


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


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


150 
by(simp add: mult_2)


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


152 
using Node * by (simp del: power_increasing_iff)


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


154 
finally show ?case .


155 
qed


156 


157 
function t_meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where


158 
"t_meld Leaf t2 = 1" 


159 
"t_meld t2 Leaf = 1" 


160 
"t_meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =


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


162 
else 1 + t_meld r2 (Node n1 l1 a1 r1))"


163 
by pat_completeness auto


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


165 


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


167 
"t_insert x t = t_meld (Node 1 Leaf x Leaf) t"


168 


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


170 
"t_del_min Leaf = 1" 


171 
"t_del_min (Node n l a r) = t_meld l r"


172 


173 
lemma t_meld_rank: "t_meld l r \<le> rank l + rank r + 1"


174 
proof(induction l r rule: meld.induct)


175 
case 3 thus ?case


176 
by(simp)(fastforce split: tree.splits simp del: t_meld.simps)


177 
qed simp_all


178 


179 
corollary t_meld_log: assumes "lheap l" "lheap r"


180 
shows "t_meld l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"


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


182 
le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_meld_rank[of l r]


183 
by linarith


184 


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


186 
using t_meld_log[of "Node 1 Leaf x Leaf" t]


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


188 


189 
lemma ld_ld_1_less:


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


191 
proof 


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


193 
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)


194 
show ?thesis


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


196 
apply simp


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


198 
qed


199 


200 
corollary t_del_min_log: assumes "lheap t"


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


202 
proof(cases t)


203 
case Leaf thus ?thesis using assms by simp


204 
next


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


206 
have "t_del_min t = t_meld t1 t2" by simp


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


208 
using \<open>lheap t\<close> by (auto simp: t_meld_log simp del: t_meld.simps)


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


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


211 
finally show ?thesis .


212 
qed


213 


214 
end
