author  nipkow 
Tue, 05 Jan 2021 11:24:35 +0100  
changeset 73295  2138a4a9031a 
parent 73182  8b92a2ab5370 
permissions  rwrr 
66524  1 
(* Author: Peter Lammich 
2 
Tobias Nipkow (tuning) 

3 
*) 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

4 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

5 
section \<open>Binomial Heap\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

6 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

7 
theory Binomial_Heap 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

8 
imports 
70636  9 
"HOLLibrary.Pattern_Aliases" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

10 
Complex_Main 
73048  11 
Priority_Queue_Specs 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

12 
begin 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

13 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

14 
text \<open> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

15 
We formalize the binomial heap presentation from Okasaki's book. 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

16 
We show the functional correctness and complexity of all operations. 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

17 

67485  18 
The presentation is engineered for simplicity, and most 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

19 
proofs are straightforward and automatic. 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

20 
\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

21 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

22 
subsection \<open>Binomial Tree and Heap Datatype\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

23 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

24 
datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list") 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

25 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

26 
type_synonym 'a heap = "'a tree list" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

27 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

28 
subsubsection \<open>Multiset of elements\<close> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

29 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

30 
fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where 
70793  31 
"mset_tree (Node _ a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)" 
67485  32 

33 
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where 

70793  34 
"mset_heap ts = (\<Sum>t\<in>#mset ts. mset_tree t)" 
67485  35 

36 
lemma mset_tree_simp_alt[simp]: 

70793  37 
"mset_tree (Node r a ts) = {#a#} + mset_heap ts" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

38 
unfolding mset_heap_def by auto 
67485  39 
declare mset_tree.simps[simp del] 
40 

41 
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}" 

66524  42 
by (cases t) auto 
67485  43 

44 
lemma mset_heap_Nil[simp]: 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

45 
"mset_heap [] = {#}" 
66524  46 
by (auto simp: mset_heap_def) 
47 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

48 
lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts" 
66524  49 
by (auto simp: mset_heap_def) 
67485  50 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

51 
lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]" 
66524  52 
by (auto simp: mset_heap_def) 
67485  53 

66524  54 
lemma root_in_mset[simp]: "root t \<in># mset_tree t" 
67485  55 
by (cases t) auto 
56 

57 
lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts" 

66524  58 
by (auto simp: mset_heap_def) 
67485  59 

60 
subsubsection \<open>Invariants\<close> 

61 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

62 
text \<open>Binomial tree\<close> 
66524  63 
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where 
67485  64 
"invar_btree (Node r x ts) \<longleftrightarrow> 
66524  65 
(\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

66 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

67 
text \<open>Ordering (heap) invariant\<close> 
66524  68 
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where 
69 
"invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

70 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

71 
definition "invar_tree t \<longleftrightarrow> invar_btree t \<and> invar_otree t" 
67485  72 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

73 
text \<open>Binomial Heap invariant\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

74 
definition "invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_tree t) \<and> (sorted_wrt (<) (map rank ts))" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

75 

67485  76 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

77 
text \<open>The children of a node are a valid heap\<close> 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

78 
lemma invar_children: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

79 
"invar_tree (Node r v ts) \<Longrightarrow> invar (rev ts)" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

80 
by (auto simp: invar_tree_def invar_def rev_map[symmetric]) 
66524  81 

82 

67485  83 
subsection \<open>Operations and Their Functional Correctness\<close> 
84 

66524  85 
subsubsection \<open>\<open>link\<close>\<close> 
86 

66549  87 
context 
88 
includes pattern_aliases 

89 
begin 

90 

91 
fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where 

67485  92 
"link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) = 
66550  93 
(if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))" 
66549  94 

95 
end 

66492  96 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

97 
lemma invar_link: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

98 
assumes "invar_tree t\<^sub>1" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

99 
assumes "invar_tree t\<^sub>2" 
67485  100 
assumes "rank t\<^sub>1 = rank t\<^sub>2" 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

101 
shows "invar_tree (link t\<^sub>1 t\<^sub>2)" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

102 
using assms unfolding invar_tree_def 
66549  103 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto 
66524  104 

105 
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" 

66549  106 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 
67485  107 

66524  108 
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" 
66549  109 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 
67485  110 

66524  111 
subsubsection \<open>\<open>ins_tree\<close>\<close> 
112 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

113 
fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

114 
"ins_tree t [] = [t]" 
66524  115 
 "ins_tree t\<^sub>1 (t\<^sub>2#ts) = 
67485  116 
(if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)" 
117 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

118 
lemma invar_tree0[simp]: "invar_tree (Node 0 x [])" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

119 
unfolding invar_tree_def by auto 
67485  120 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

121 
lemma invar_Cons[simp]: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

122 
"invar (t#ts) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

123 
\<longleftrightarrow> invar_tree t \<and> invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

124 
by (auto simp: invar_def) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

125 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

126 
lemma invar_ins_tree: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

127 
assumes "invar_tree t" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

128 
assumes "invar ts" 
67485  129 
assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'" 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

130 
shows "invar (ins_tree t ts)" 
66524  131 
using assms 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

132 
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric]) 
67485  133 

134 
lemma mset_heap_ins_tree[simp]: 

135 
"mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" 

136 
by (induction t ts rule: ins_tree.induct) auto 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

137 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

138 
lemma ins_tree_rank_bound: 
67485  139 
assumes "t' \<in> set (ins_tree t ts)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

140 
assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'" 
67485  141 
assumes "rank t\<^sub>0 < rank t" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

142 
shows "rank t\<^sub>0 < rank t'" 
67485  143 
using assms 
66524  144 
by (induction t ts rule: ins_tree.induct) (auto split: if_splits) 
145 

146 
subsubsection \<open>\<open>insert\<close>\<close> 

147 

148 
hide_const (open) insert 

149 

150 
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where 

151 
"insert x ts = ins_tree (Node 0 x []) ts" 

67485  152 

66524  153 
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)" 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

154 
by (auto intro!: invar_ins_tree simp: insert_def) 
67485  155 

66524  156 
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t" 
157 
by(auto simp: insert_def) 

158 

159 
subsubsection \<open>\<open>merge\<close>\<close> 

66492  160 

70793  161 
context 
162 
includes pattern_aliases 

163 
begin 

164 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

165 
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

166 
"merge ts\<^sub>1 [] = ts\<^sub>1" 
67485  167 
 "merge [] ts\<^sub>2 = ts\<^sub>2" 
70793  168 
 "merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = ( 
169 
if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 h\<^sub>2 else 

170 
if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge h\<^sub>1 ts\<^sub>2 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

171 
else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) 
66492  172 
)" 
173 

70793  174 
end 
175 

66524  176 
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" 
177 
by (cases ts\<^sub>2) auto 

67485  178 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

179 
lemma merge_rank_bound: 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

180 
assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" 
70793  181 
assumes "\<forall>t\<^sub>1\<in>set ts\<^sub>1. rank t < rank t\<^sub>1" 
182 
assumes "\<forall>t\<^sub>2\<in>set ts\<^sub>2. rank t < rank t\<^sub>2" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

183 
shows "rank t < rank t'" 
66524  184 
using assms 
185 
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct) 

186 
(auto split: if_splits simp: ins_tree_rank_bound) 

187 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

188 
lemma invar_merge[simp]: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

189 
assumes "invar ts\<^sub>1" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

190 
assumes "invar ts\<^sub>2" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

191 
shows "invar (merge ts\<^sub>1 ts\<^sub>2)" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

192 
using assms 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

193 
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

194 
(auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

195 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

196 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

197 
text \<open>Longer, more explicit proof of @{thm [source] invar_merge}, 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

198 
to illustrate the application of the @{thm [source] merge_rank_bound} lemma.\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

199 
lemma 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

200 
assumes "invar ts\<^sub>1" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

201 
assumes "invar ts\<^sub>2" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

202 
shows "invar (merge ts\<^sub>1 ts\<^sub>2)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

203 
using assms 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

204 
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

205 
case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2) 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

206 
\<comment> \<open>Invariants of the parts can be shown automatically\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

207 
from "3.prems" have [simp]: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

208 
"invar_tree t\<^sub>1" "invar_tree t\<^sub>2" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

209 
(*"invar (merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2)" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

210 
"invar (merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2))" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

211 
"invar (merge ts\<^sub>1 ts\<^sub>2)"*) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

212 
by auto 
67485  213 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

214 
\<comment> \<open>These are the three cases of the @{const merge} function\<close> 
67485  215 
consider (LT) "rank t\<^sub>1 < rank t\<^sub>2" 
216 
 (GT) "rank t\<^sub>1 > rank t\<^sub>2" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

217 
 (EQ) "rank t\<^sub>1 = rank t\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

218 
using antisym_conv3 by blast 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

219 
then show ?case proof cases 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

220 
case LT 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

221 
\<comment> \<open>@{const merge} takes the first tree from the left heap\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

222 
then have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)" by simp 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

223 
also have "invar \<dots>" proof (simp, intro conjI) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

224 
\<comment> \<open>Invariant follows from induction hypothesis\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

225 
show "invar (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2))" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

226 
using LT "3.IH" "3.prems" by simp 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

227 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

228 
\<comment> \<open>It remains to show that \<open>t\<^sub>1\<close> has smallest rank.\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

229 
show "\<forall>t'\<in>set (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)). rank t\<^sub>1 < rank t'" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

230 
\<comment> \<open>Which is done by auxiliary lemma @{thm [source] merge_rank_bound}\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

231 
using LT "3.prems" by (force elim!: merge_rank_bound) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

232 
qed 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

233 
finally show ?thesis . 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

234 
next 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

235 
\<comment> \<open>@{const merge} takes the first tree from the right heap\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

236 
case GT 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

237 
\<comment> \<open>The proof is anaologous to the \<open>LT\<close> case\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

238 
then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

239 
next 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

240 
case [simp]: EQ 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

241 
\<comment> \<open>@{const merge} links both first trees, and inserts them into the merged remaining heaps\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

242 
have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)" by simp 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

243 
also have "invar \<dots>" proof (intro invar_ins_tree invar_link) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

244 
\<comment> \<open>Invariant of merged remaining heaps follows by IH\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

245 
show "invar (merge ts\<^sub>1 ts\<^sub>2)" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

246 
using EQ "3.prems" "3.IH" by auto 
67485  247 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

248 
\<comment> \<open>For insertion, we have to show that the rank of the linked tree is \<open>\<le>\<close> the 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

249 
ranks in the merged remaining heaps\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

250 
show "\<forall>t'\<in>set (merge ts\<^sub>1 ts\<^sub>2). rank (link t\<^sub>1 t\<^sub>2) \<le> rank t'" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

251 
proof  
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

252 
\<comment> \<open>Which is, again, done with the help of @{thm [source] merge_rank_bound}\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

253 
have "rank (link t\<^sub>1 t\<^sub>2) = Suc (rank t\<^sub>2)" by simp 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

254 
thus ?thesis using "3.prems" by (auto simp: Suc_le_eq elim!: merge_rank_bound) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

255 
qed 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

256 
qed simp_all 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

257 
finally show ?thesis . 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

258 
qed 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

259 
qed auto 
67485  260 

261 

262 
lemma mset_heap_merge[simp]: 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

263 
"mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2" 
67485  264 
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto 
265 

66524  266 
subsubsection \<open>\<open>get_min\<close>\<close> 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

267 

66524  268 
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where 
269 
"get_min [t] = root t" 

66546  270 
 "get_min (t#ts) = min (root t) (get_min ts)" 
67485  271 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

272 
lemma invar_tree_root_min: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

273 
assumes "invar_tree t" 
67485  274 
assumes "x \<in># mset_tree t" 
275 
shows "root t \<le> x" 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

276 
using assms unfolding invar_tree_def 
66524  277 
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def) 
67485  278 

279 
lemma get_min_mset: 

280 
assumes "ts\<noteq>[]" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

281 
assumes "invar ts" 
67485  282 
assumes "x \<in># mset_heap ts" 
66524  283 
shows "get_min ts \<le> x" 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

284 
using assms 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

285 
apply (induction ts arbitrary: x rule: get_min.induct) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

286 
apply (auto 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

287 
simp: invar_tree_root_min min_def intro: order_trans; 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

288 
meson linear order_trans invar_tree_root_min 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

289 
)+ 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

290 
done 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

291 

67485  292 
lemma get_min_member: 
293 
"ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts" 

66546  294 
by (induction ts rule: get_min.induct) (auto simp: min_def) 
66524  295 

67485  296 
lemma get_min: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

297 
assumes "mset_heap ts \<noteq> {#}" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

298 
assumes "invar ts" 
66524  299 
shows "get_min ts = Min_mset (mset_heap ts)" 
67485  300 
using assms get_min_member get_min_mset 
66524  301 
by (auto simp: eq_Min_iff) 
67485  302 

66524  303 
subsubsection \<open>\<open>get_min_rest\<close>\<close> 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

304 

66524  305 
fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where 
306 
"get_min_rest [t] = (t,[])" 

307 
 "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

308 
in if root t \<le> root t' then (t,ts) else (t',t#ts'))" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

309 

67485  310 
lemma get_min_rest_get_min_same_root: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

311 
assumes "ts\<noteq>[]" 
67485  312 
assumes "get_min_rest ts = (t',ts')" 
313 
shows "root t' = get_min ts" 

314 
using assms 

66546  315 
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits) 
66524  316 

67485  317 
lemma mset_get_min_rest: 
318 
assumes "get_min_rest ts = (t',ts')" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

319 
assumes "ts\<noteq>[]" 
67485  320 
shows "mset ts = {#t'#} + mset ts'" 
321 
using assms 

66524  322 
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) 
67485  323 

72784  324 
lemma set_get_min_rest: 
67485  325 
assumes "get_min_rest ts = (t', ts')" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

326 
assumes "ts\<noteq>[]" 
66524  327 
shows "set ts = Set.insert t' (set ts')" 
328 
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]] 

67485  329 
by auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

330 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

331 
lemma invar_get_min_rest: 
67485  332 
assumes "get_min_rest ts = (t',ts')" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

333 
assumes "ts\<noteq>[]" 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

334 
assumes "invar ts" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

335 
shows "invar_tree t'" and "invar ts'" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

336 
proof  
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

337 
have "invar_tree t' \<and> invar ts'" 
67485  338 
using assms 
66524  339 
proof (induction ts arbitrary: t' ts' rule: get_min.induct) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

340 
case (2 t v va) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

341 
then show ?case 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

342 
apply (clarsimp split: prod.splits if_splits) 
72784  343 
apply (drule set_get_min_rest; fastforce) 
67485  344 
done 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

345 
qed auto 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

346 
thus "invar_tree t'" and "invar ts'" by auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

347 
qed 
66524  348 

68021  349 
subsubsection \<open>\<open>del_min\<close>\<close> 
66524  350 

68021  351 
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where 
352 
"del_min ts = (case get_min_rest ts of 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

353 
(Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)" 
67485  354 

68021  355 
lemma invar_del_min[simp]: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

356 
assumes "ts \<noteq> []" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

357 
assumes "invar ts" 
68021  358 
shows "invar (del_min ts)" 
67485  359 
using assms 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

360 
unfolding del_min_def 
67485  361 
by (auto 
362 
split: prod.split tree.split 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

363 
intro!: invar_merge invar_children 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

364 
dest: invar_get_min_rest 
66524  365 
) 
67485  366 

68021  367 
lemma mset_heap_del_min: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

368 
assumes "ts \<noteq> []" 
68021  369 
shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}" 
66524  370 
using assms 
68021  371 
unfolding del_min_def 
66524  372 
apply (clarsimp split: tree.split prod.split) 
67485  373 
apply (frule (1) get_min_rest_get_min_same_root) 
374 
apply (frule (1) mset_get_min_rest) 

66524  375 
apply (auto simp: mset_heap_def) 
67485  376 
done 
66524  377 

378 

379 
subsubsection \<open>Instantiating the Priority Queue Locale\<close> 

380 

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

383 

384 
interpretation binheap: Priority_Queue_Merge 

67399  385 
where empty = "[]" and is_empty = "(=) []" and insert = insert 
68021  386 
and get_min = get_min and del_min = del_min and merge = merge 
66524  387 
and invar = invar and mset = mset_heap 
388 
proof (unfold_locales, goal_cases) 

66564  389 
case 1 thus ?case by simp 
66524  390 
next 
66564  391 
case 2 thus ?case by auto 
66524  392 
next 
66564  393 
case 3 thus ?case by auto 
66524  394 
next 
395 
case (4 q) 

68021  396 
thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
66524  397 
by (auto simp: union_single_eq_diff) 
398 
next 

66564  399 
case (5 q) thus ?case using get_min[of q] by auto 
67485  400 
next 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

401 
case 6 thus ?case by (auto simp add: invar_def) 
66564  402 
next 
403 
case 7 thus ?case by simp 

66524  404 
next 
66564  405 
case 8 thus ?case by simp 
66524  406 
next 
66564  407 
case 9 thus ?case by simp 
408 
next 

409 
case 10 thus ?case by simp 

66524  410 
qed 
411 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

412 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

413 
subsection \<open>Complexity\<close> 
67485  414 

415 
text \<open>The size of a binomial tree is determined by its rank\<close> 

66524  416 
lemma size_mset_btree: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

417 
assumes "invar_btree t" 
67485  418 
shows "size (mset_tree t) = 2^rank t" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

419 
using assms 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

420 
proof (induction t) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

421 
case (Node r v ts) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

422 
hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

423 
using that by auto 
67485  424 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

425 
from Node have COMPL: "map rank ts = rev [0..<r]" by auto 
67485  426 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

427 
have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

428 
by (induction ts) auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

429 
also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH 
67485  430 
by (auto cong: map_cong) 
431 
also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

432 
by (induction ts) auto 
67485  433 
also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" 
434 
unfolding COMPL 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

435 
by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat) 
67485  436 
also have "\<dots> = 2^r  1" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

437 
by (induction r) auto 
67485  438 
finally show ?case 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

439 
by (simp) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

440 
qed 
67485  441 

73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

442 
lemma size_mset_tree: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

443 
assumes "invar_tree t" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

444 
shows "size (mset_tree t) = 2^rank t" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

445 
using assms unfolding invar_tree_def 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

446 
by (simp add: size_mset_btree) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

447 

67485  448 
text \<open>The length of a binomial heap is bounded by the number of its elements\<close> 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

449 
lemma size_mset_heap: 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

450 
assumes "invar ts" 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

451 
shows "length ts \<le> log 2 (size (mset_heap ts) + 1)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

452 
proof  
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

453 
from \<open>invar ts\<close> have 
67399  454 
ASC: "sorted_wrt (<) (map rank ts)" and 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

455 
TINV: "\<forall>t\<in>set ts. invar_tree t" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

456 
unfolding invar_def by auto 
67485  457 

458 
have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

459 
by (simp add: sum_power2) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

460 
also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1" 
67399  461 
using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "(^) (2::nat)"] 
67485  462 
using power_increasing[where a="2::nat"] 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

463 
by (auto simp: o_def) 
67485  464 
also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

465 
by (auto cong: map_cong simp: size_mset_tree) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

466 
also have "\<dots> = size (mset_heap ts) + 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

467 
unfolding mset_heap_def by (induction ts) auto 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

468 
finally have "2^length ts \<le> size (mset_heap ts) + 1" . 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

469 
then show ?thesis using le_log2_of_power by blast 
67485  470 
qed 
471 

66524  472 
subsubsection \<open>Timing Functions\<close> 
473 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

474 
text \<open> 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

475 
We define timing functions for each operation, and provide 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

476 
estimations of their complexity. 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

477 
\<close> 
72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

478 
definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

479 
[simp]: "T_link _ _ = 1" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

480 

73182  481 
text \<open>This function is noncanonical: we omitted a \<open>+1\<close> in the \<open>else\<close>part, 
482 
to keep the following analysis simpler and more to the point. 

483 
\<close> 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

484 
fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

485 
"T_ins_tree t [] = 1" 
73295  486 
 "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = ( 
67485  487 
(if rank t\<^sub>1 < rank t\<^sub>2 then 1 
73295  488 
else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts) 
67485  489 
)" 
66524  490 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

491 
definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where 
73175
aa86651805e0
added missing +1 to T_insert (for function call)
Peter Lammich
parents:
73150
diff
changeset

492 
"T_insert x ts = T_ins_tree (Node 0 x []) ts + 1" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

493 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

494 
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

495 
by (induction t ts rule: T_ins_tree.induct) auto 
66524  496 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

497 
subsubsection \<open>\<open>T_insert\<close>\<close> 
66524  498 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

499 
lemma T_insert_bound: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

500 
assumes "invar ts" 
73175
aa86651805e0
added missing +1 to T_insert (for function call)
Peter Lammich
parents:
73150
diff
changeset

501 
shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 2" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

502 
proof  
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

503 
have "real (T_insert x ts) \<le> real (length ts) + 2" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

504 
unfolding T_insert_def using T_ins_tree_simple_bound 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

505 
using of_nat_mono by fastforce 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

506 
also note size_mset_heap[OF \<open>invar ts\<close>] 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

507 
finally show ?thesis by simp 
67485  508 
qed 
66524  509 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

510 
subsubsection \<open>\<open>T_merge\<close>\<close> 
66524  511 

70793  512 
context 
513 
includes pattern_aliases 

514 
begin 

515 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

516 
fun T_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

517 
"T_merge ts\<^sub>1 [] = 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

518 
 "T_merge [] ts\<^sub>2 = 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

519 
 "T_merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = 1 + ( 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

520 
if rank t\<^sub>1 < rank t\<^sub>2 then T_merge ts\<^sub>1 h\<^sub>2 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

521 
else if rank t\<^sub>2 < rank t\<^sub>1 then T_merge h\<^sub>1 ts\<^sub>2 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

522 
else T_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2 
67485  523 
)" 
524 

70793  525 
end 
526 

67485  527 
text \<open>A crucial idea is to estimate the time in correlation with the 
528 
result length, as each carry reduces the length of the result.\<close> 

66524  529 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

530 
lemma T_ins_tree_length: 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

531 
"T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

532 
by (induction t ts rule: ins_tree.induct) auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

533 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

534 
lemma T_merge_length: 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

535 
"length (merge ts\<^sub>1 ts\<^sub>2) + T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

536 
by (induction ts\<^sub>1 ts\<^sub>2 rule: T_merge.induct) 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

537 
(auto simp: T_ins_tree_length algebra_simps) 
66524  538 

66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

539 
text \<open>Finally, we get the desired logarithmic bound\<close> 
73150  540 
lemma T_merge_bound: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

541 
fixes ts\<^sub>1 ts\<^sub>2 
67485  542 
defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

543 
defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)" 
73150  544 
assumes "invar ts\<^sub>1" "invar ts\<^sub>2" 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

545 
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

546 
proof  
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

547 
note n_defs = assms(1,2) 
73150  548 

73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

549 
have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * real (length ts\<^sub>1) + 2 * real (length ts\<^sub>2) + 1" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

550 
using T_merge_length[of ts\<^sub>1 ts\<^sub>2] by simp 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

551 
also note size_mset_heap[OF \<open>invar ts\<^sub>1\<close>] 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

552 
also note size_mset_heap[OF \<open>invar ts\<^sub>2\<close>] 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

553 
finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * log 2 (n\<^sub>1 + 1) + 2 * log 2 (n\<^sub>2 + 1) + 1" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

554 
unfolding n_defs by (simp add: algebra_simps) 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

555 
also have "log 2 (n\<^sub>1 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

556 
unfolding n_defs by (simp add: algebra_simps) 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

557 
also have "log 2 (n\<^sub>2 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

558 
unfolding n_defs by (simp add: algebra_simps) 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

559 
finally show ?thesis by (simp add: algebra_simps) 
67485  560 
qed 
561 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

562 
subsubsection \<open>\<open>T_get_min\<close>\<close> 
66524  563 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

564 
fun T_get_min :: "'a::linorder heap \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

565 
"T_get_min [t] = 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

566 
 "T_get_min (t#ts) = 1 + T_get_min ts" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

567 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

568 
lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

569 
by (induction ts rule: T_get_min.induct) auto 
67485  570 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

571 
lemma T_get_min_bound: 
66524  572 
assumes "invar ts" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

573 
assumes "ts\<noteq>[]" 
72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

574 
shows "T_get_min ts \<le> log 2 (size (mset_heap ts) + 1)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

575 
proof  
72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

576 
have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

577 
also note size_mset_heap[OF \<open>invar ts\<close>] 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

578 
finally show ?thesis . 
67485  579 
qed 
66524  580 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

581 
subsubsection \<open>\<open>T_del_min\<close>\<close> 
66524  582 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

583 
fun T_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

584 
"T_get_min_rest [t] = 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

585 
 "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts" 
66524  586 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

587 
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

588 
by (induction ts rule: T_get_min_rest.induct) auto 
67485  589 

73150  590 
lemma T_get_min_rest_bound: 
73045
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72952
diff
changeset

591 
assumes "invar ts" 
66524  592 
assumes "ts\<noteq>[]" 
72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

593 
shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)" 
66524  594 
proof  
72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

595 
have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

596 
also note size_mset_heap[OF \<open>invar ts\<close>] 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

597 
finally show ?thesis . 
67485  598 
qed 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

599 

69609  600 
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity, 
66524  601 
it can and is implemented (via suitable code lemmas) as a linear time function. 
602 
Thus the following definition is justified:\<close> 

603 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

604 
definition "T_rev xs = length xs + 1" 
66524  605 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

606 
definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

607 
"T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

608 
\<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2 
73182  609 
) + 1" 
67485  610 

73150  611 
lemma T_del_min_bound: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

612 
fixes ts 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

613 
defines "n \<equiv> size (mset_heap ts)" 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

614 
assumes "invar ts" and "ts\<noteq>[]" 
73182  615 
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

616 
proof  
66524  617 
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

618 
by (metis surj_pair tree.exhaust_sel) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

619 

73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

620 
have I1: "invar (rev ts\<^sub>1)" and I2: "invar ts\<^sub>2" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

621 
using invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>] invar_children 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

622 
by auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

623 

5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

624 
define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

625 
define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)" 
67485  626 

73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

627 
have "n\<^sub>1 \<le> n" "n\<^sub>1 + n\<^sub>2 \<le> n" unfolding n_def n\<^sub>1_def n\<^sub>2_def 
66524  628 
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>] 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

629 
by (auto simp: mset_heap_def) 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

630 

73182  631 
have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1" 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

632 
unfolding T_del_min_def GM 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

633 
by simp 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

634 
also have "T_get_min_rest ts \<le> log 2 (n+1)" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

635 
using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

636 
also have "T_rev ts\<^sub>1 \<le> 1 + log 2 (n\<^sub>1 + 1)" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

637 
unfolding T_rev_def n\<^sub>1_def using size_mset_heap[OF I1] by simp 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

638 
also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1" 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

639 
unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps) 
73182  640 
finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3" 
73176
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

641 
by (simp add: algebra_simps) 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

642 
also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close> 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

643 
also note \<open>n\<^sub>1 \<le> n\<close> 
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
73175
diff
changeset

644 
finally show ?thesis by (simp add: algebra_simps) 
67485  645 
qed 
646 

72783
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70793
diff
changeset

647 
end 