author  nipkow 
Mon, 03 May 2021 19:06:33 +0200  
changeset 73875  0c8d6bec6491 
parent 72773  8eabaf951e6b 
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 
70636  7 
"HOLLibrary.Pattern_Aliases" 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

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

10 
Complex_Main 
62706  11 
begin 
12 

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

13 
fun mset_tree :: "('a*'b) tree \<Rightarrow> 'a multiset" where 
64969  14 
"mset_tree Leaf = {#}"  
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

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

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

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

72773  19 
fun mht :: "'a lheap \<Rightarrow> nat" where 
20 
"mht Leaf = 0"  

21 
"mht (Node _ (_, n) _) = n" 

62706  22 

67406  23 
text\<open>The invariants:\<close> 
64969  24 

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

25 
fun (in linorder) heap :: "('a*'b) tree \<Rightarrow> bool" where 
64969  26 
"heap Leaf = True"  
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

27 
"heap (Node l (m, _) r) = 
72773  28 
((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)" 
62706  29 

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

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

32 
"ltree (Node l (a, n) r) = 
72773  33 
(min_height l \<ge> min_height r \<and> n = min_height r + 1 \<and> ltree l & ltree r)" 
62706  34 

70771  35 
definition empty :: "'a lheap" where 
36 
"empty = Leaf" 

37 

62706  38 
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where 
39 
"node l a r = 

73875  40 
(let mhl = mht l; mhr = mht r 
41 
in if mhl \<ge> mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)" 

62706  42 

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

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

44 
"get_min(Node l (a, n) r) = a" 
62706  45 

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

66492  48 

66502  49 
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where 
70771  50 
"merge Leaf t = t"  
51 
"merge t Leaf = t"  

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

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

70771  56 
text \<open>Termination of @{const merge}: by sum or lexicographic product of the sizes 
57 
of the two arguments. Isabelle uses a lexicographic product.\<close> 

58 

64976  59 
lemma merge_code: "merge t1 t2 = (case (t1,t2) of 
62706  60 
(Leaf, _) \<Rightarrow> t2  
61 
(_, Leaf) \<Rightarrow> t1  

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

62 
(Node l1 (a1, n1) r1, Node l2 (a2, n2) r2) \<Rightarrow> 
68600  63 
if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))" 
64976  64 
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split) 
62706  65 

66524  66 
hide_const (open) insert 
67 

62706  68 
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where 
70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

69 
"insert x t = merge (Node Leaf (x,1) Leaf) t" 
62706  70 

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

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

73 
"del_min (Node l _ r) = merge l r" 
62706  74 

75 

76 
subsection "Lemmas" 

77 

66422
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 

72773  81 
lemma mht_eq_min_height: "ltree t \<Longrightarrow> mht t = min_height t" 
62706  82 
by(cases t) auto 
83 

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

64969  87 
lemma heap_node: "heap (node l a r) \<longleftrightarrow> 
70771  88 
heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)" 
64969  89 
by(auto simp add: node_def) 
90 

70771  91 
lemma set_tree_mset: "set_tree t = set_mset(mset_tree t)" 
92 
by(induction t) auto 

62706  93 

94 
subsection "Functional Correctness" 

95 

72513  96 
lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2" 
97 
by (induction t1 t2 rule: merge.induct) (auto simp add: node_def ac_simps) 

62706  98 

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

72513  102 
lemma get_min: "\<lbrakk> heap t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min t = Min(set_tree t)" 
103 
by (cases t) (auto simp add: eq_Min_iff) 

64969  104 

72513  105 
lemma mset_del_min: "mset_tree (del_min t) = mset_tree t  {# get_min t #}" 
106 
by (cases t) (auto simp: mset_merge) 

62706  107 

64976  108 
lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)" 
72513  109 
by(induction l r rule: merge.induct)(auto simp: ltree_node) 
62706  110 

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

70771  113 
case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un set_tree_mset) 
64969  114 
qed simp_all 
115 

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

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

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

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

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

62706  130 

66564  131 
interpretation lheap: Priority_Queue_Merge 
72513  132 
where empty = empty and is_empty = "\<lambda>t. t = Leaf" 
68021  133 
and insert = insert and del_min = del_min 
66564  134 
and get_min = get_min and merge = merge 
72513  135 
and invar = "\<lambda>t. heap t \<and> ltree t" and mset = mset_tree 
62706  136 
proof(standard, goal_cases) 
70771  137 
case 1 show ?case by (simp add: empty_def) 
62706  138 
next 
64975  139 
case (2 q) show ?case by (cases q) auto 
62706  140 
next 
64975  141 
case 3 show ?case by(rule mset_insert) 
142 
next 

68021  143 
case 4 show ?case by(rule mset_del_min) 
62706  144 
next 
70771  145 
case 5 thus ?case by(simp add: get_min mset_tree_empty set_tree_mset) 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

146 
next 
70771  147 
case 6 thus ?case by(simp add: empty_def) 
62706  148 
next 
66422
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
64977
diff
changeset

149 
case 7 thus ?case by(simp add: heap_insert ltree_insert) 
64969  150 
next 
68021  151 
case 8 thus ?case by(simp add: heap_del_min ltree_del_min) 
66564  152 
next 
153 
case 9 thus ?case by (simp add: mset_merge) 

154 
next 

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

62706  156 
qed 
157 

158 

159 
subsection "Complexity" 

160 

66492  161 
text\<open>Explicit termination argument: sum of sizes\<close> 
162 

72773  163 
fun T_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where 
164 
"T_merge Leaf t = 1"  

165 
"T_merge t Leaf = 1"  

166 
"T_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) = 

167 
(if a1 \<le> a2 then T_merge r1 t2 

168 
else T_merge t1 r2) + 1" 

62706  169 

72773  170 
definition T_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where 
171 
"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t + 1" 

62706  172 

72773  173 
fun T_del_min :: "'a::ord lheap \<Rightarrow> nat" where 
174 
"T_del_min Leaf = 1"  

175 
"T_del_min (Node l _ r) = T_merge l r + 1" 

62706  176 

72773  177 
lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1" 
64976  178 
proof(induction l r rule: merge.induct) 
72773  179 
case 3 thus ?case by(auto) 
62706  180 
qed simp_all 
181 

72773  182 
corollary T_merge_log: assumes "ltree l" "ltree r" 
183 
shows "T_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1" 

184 
using le_log2_of_power[OF min_height_size1[of l]] 

185 
le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms 

62706  186 
by linarith 
187 

72773  188 
corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 3" 
189 
using T_merge_log[of "Node Leaf (x, 1) Leaf" t] 

190 
by(simp add: T_insert_def split: tree.split) 

62706  191 

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

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

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

62706  199 
by(simp add: numeral_eq_Suc algebra_simps add_pos_pos) 
64977  200 
also have "\<dots> = 2 powr (2 * log 2 (x+y))" 
66492  201 
using assms by(simp add: powr_add log_powr[symmetric]) 
64977  202 
finally show ?thesis by simp 
62706  203 
qed 
204 

72773  205 
corollary T_del_min_log: assumes "ltree t" 
206 
shows "T_del_min t \<le> 2 * log 2 (size1 t) + 1" 

70944
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70771
diff
changeset

207 
proof(cases t rule: tree2_cases) 
62706  208 
case Leaf thus ?thesis using assms by simp 
209 
next 

72773  210 
case [simp]: (Node l _ _ r) 
211 
have "T_del_min t = T_merge l r + 1" by simp 

212 
also have "\<dots> \<le> log 2 (size1 l) + log 2 (size1 r) + 2" 

213 
using \<open>ltree t\<close> T_merge_log[of l r] by (auto simp del: T_merge.simps) 

62706  214 
also have "\<dots> \<le> 2 * log 2 (size1 t) + 1" 
72773  215 
using ld_ld_1_less[of "size1 l" "size1 r"] by (simp) 
62706  216 
finally show ?thesis . 
217 
qed 

218 

219 
end 