author  nipkow 
Sat, 21 Apr 2018 11:13:35 +0200  
changeset 68021  b91a043c0dcb 
parent 68020  6aade817bee5 
child 68414  b56ed5010e69 
permissions  rwrr 
62706  1 
(* Author: Tobias Nipkow *) 
2 

3 
section \<open>Leftist Heap\<close> 

4 

5 
theory Leftist_Heap 

66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

6 
imports 
66492  7 
Base_FDS 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

8 
Tree2 
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

9 
Priority_Queue 
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

10 
Complex_Main 
62706  11 
begin 
12 

64969  13 
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where 
14 
"mset_tree Leaf = {#}"  

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

16 

62706  17 
type_synonym 'a lheap = "('a,nat)tree" 
18 

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

20 
"rank Leaf = 0"  

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

22 

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

24 
"rk Leaf = 0"  

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

26 

67406  27 
text\<open>The invariants:\<close> 
64969  28 

29 
fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where 

30 
"heap Leaf = True"  

31 
"heap (Node _ l m r) = 

32 
(heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))" 

62706  33 

64973  34 
fun ltree :: "'a lheap \<Rightarrow> bool" where 
35 
"ltree Leaf = True"  

36 
"ltree (Node n l a r) = 

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

62706  38 

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

40 
"node l a r = 

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

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

43 

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

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

46 

66502  47 
text \<open>For function \<open>merge\<close>:\<close> 
48 
unbundle pattern_aliases 

49 
declare size_prod_measure[measure_function] 

66492  50 

66502  51 
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where 
64976  52 
"merge Leaf t2 = t2"  
53 
"merge t1 Leaf = t1"  

66492  54 
"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) = 
55 
(if a1 \<le> a2 then node l1 a1 (merge r1 t2) 

56 
else node l2 a2 (merge r2 t1))" 

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 

66524  65 
hide_const (open) insert 
66 

62706  67 
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where 
64976  68 
"insert x t = merge (Node 1 Leaf x Leaf) t" 
62706  69 

68021  70 
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where 
71 
"del_min Leaf = Leaf"  

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

62706  73 

74 

75 
subsection "Lemmas" 

76 

66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

77 
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

78 
by(cases t) auto 
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

79 

64973  80 
lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t" 
62706  81 
by(cases t) auto 
82 

64973  83 
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r" 
62706  84 
by(auto simp add: node_def) 
85 

64969  86 
lemma heap_node: "heap (node l a r) \<longleftrightarrow> 
87 
heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)" 

88 
by(auto simp add: node_def) 

89 

62706  90 

91 
subsection "Functional Correctness" 

92 

64976  93 
lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2" 
94 
by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps) 

62706  95 

64969  96 
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}" 
64976  97 
by (auto simp add: insert_def mset_merge) 
62706  98 

66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

99 
lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)" 
66424  100 
by (induction h) (auto simp add: eq_Min_iff) 
64969  101 

68021  102 
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h  {# get_min h #}" 
64976  103 
by (cases h) (auto simp: mset_merge) 
62706  104 

64976  105 
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)" 
106 
proof(induction l r rule: merge.induct) 

62706  107 
case (3 n1 l1 a1 r1 n2 l2 a2 r2) 
64976  108 
show ?case (is "ltree(merge ?t1 ?t2)") 
62706  109 
proof cases 
110 
assume "a1 \<le> a2" 

64976  111 
hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp 
112 
also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))" 

64973  113 
by(simp add: ltree_node) 
67406  114 
also have "..." using "3.prems" "3.IH"(1)[OF \<open>a1 \<le> a2\<close>] by (simp) 
62706  115 
finally show ?thesis . 
116 
next (* analogous but automatic *) 

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

64973  118 
thus ?thesis using 3 by(simp)(auto simp: ltree_node) 
62706  119 
qed 
120 
qed simp_all 

121 

64976  122 
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)" 
123 
proof(induction l r rule: merge.induct) 

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

64969  125 
qed simp_all 
126 

64973  127 
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)" 
64976  128 
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split) 
62706  129 

64969  130 
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)" 
64976  131 
by(simp add: insert_def heap_merge del: merge.simps split: tree.split) 
64969  132 

68021  133 
lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)" 
64976  134 
by(cases t)(auto simp add: ltree_merge simp del: merge.simps) 
62706  135 

68021  136 
lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)" 
64976  137 
by(cases t)(auto simp add: heap_merge simp del: merge.simps) 
64969  138 

66564  139 
text \<open>Last step of functional correctness proof: combine all the above lemmas 
140 
to show that leftist heaps satisfy the specification of priority queues with merge.\<close> 

62706  141 

66564  142 
interpretation lheap: Priority_Queue_Merge 
64975  143 
where empty = Leaf and is_empty = "\<lambda>h. h = Leaf" 
68021  144 
and insert = insert and del_min = del_min 
66564  145 
and get_min = get_min and merge = merge 
146 
and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree 

62706  147 
proof(standard, goal_cases) 
148 
case 1 show ?case by simp 

149 
next 

64975  150 
case (2 q) show ?case by (cases q) auto 
62706  151 
next 
64975  152 
case 3 show ?case by(rule mset_insert) 
153 
next 

68021  154 
case 4 show ?case by(rule mset_del_min) 
62706  155 
next 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

156 
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

157 
next 
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

158 
case 6 thus ?case by(simp) 
62706  159 
next 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

160 
case 7 thus ?case by(simp add: heap_insert ltree_insert) 
64969  161 
next 
68021  162 
case 8 thus ?case by(simp add: heap_del_min ltree_del_min) 
66564  163 
next 
164 
case 9 thus ?case by (simp add: mset_merge) 

165 
next 

166 
case 10 thus ?case by (simp add: heap_merge ltree_merge) 

62706  167 
qed 
168 

169 

170 
subsection "Complexity" 

171 

64973  172 
lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t" 
62706  173 
proof(induction t) 
174 
case Leaf show ?case by simp 

175 
next 

176 
case (Node n l a r) 

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

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

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

180 
by(simp add: mult_2) 

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

182 
using Node * by (simp del: power_increasing_iff) 

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

184 
finally show ?case . 

185 
qed 

186 

66492  187 
text\<open>Explicit termination argument: sum of sizes\<close> 
188 

66502  189 
fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where 
64976  190 
"t_merge Leaf t2 = 1"  
191 
"t_merge t2 Leaf = 1"  

66492  192 
"t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) = 
193 
(if a1 \<le> a2 then 1 + t_merge r1 t2 

194 
else 1 + t_merge r2 t1)" 

62706  195 

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

64976  197 
"t_insert x t = t_merge (Node 1 Leaf x Leaf) t" 
62706  198 

68021  199 
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where 
200 
"t_del_min Leaf = 1"  

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

62706  202 

64976  203 
lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1" 
204 
proof(induction l r rule: merge.induct) 

62706  205 
case 3 thus ?case 
64976  206 
by(simp)(fastforce split: tree.splits simp del: t_merge.simps) 
62706  207 
qed simp_all 
208 

64976  209 
corollary t_merge_log: assumes "ltree l" "ltree r" 
210 
shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1" 

62706  211 
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]] 
64976  212 
le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r] 
62706  213 
by linarith 
214 

64973  215 
corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2" 
64976  216 
using t_merge_log[of "Node 1 Leaf x Leaf" t] 
62706  217 
by(simp add: t_insert_def split: tree.split) 
218 

66492  219 
(* FIXME mv ? *) 
62706  220 
lemma ld_ld_1_less: 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

221 
assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)" 
62706  222 
proof  
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

223 
have "2 powr (log 2 x + log 2 y + 1) = 2*x*y" 
64977  224 
using assms by(simp add: powr_add) 
225 
also have "\<dots> < (x+y)^2" using assms 

62706  226 
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos) 
64977  227 
also have "\<dots> = 2 powr (2 * log 2 (x+y))" 
66492  228 
using assms by(simp add: powr_add log_powr[symmetric]) 
64977  229 
finally show ?thesis by simp 
62706  230 
qed 
231 

68021  232 
corollary t_del_min_log: assumes "ltree t" 
233 
shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1" 

62706  234 
proof(cases t) 
235 
case Leaf thus ?thesis using assms by simp 

236 
next 

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

68021  238 
have "t_del_min t = t_merge t1 t2" by simp 
62706  239 
also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1" 
64976  240 
using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps) 
62706  241 
also have "\<dots> \<le> 2 * log 2 (size1 t) + 1" 
242 
using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp) 

243 
finally show ?thesis . 

244 
qed 

245 

246 
end 