author  Peter Lammich 
Fri, 04 Dec 2020 17:54:57 +0000  
changeset 72812  caf2fd14e28b 
parent 72808  ba65dc3e35af 
child 72910  c145be662fbd 
permissions  rwrr 
66522  1 
(* Author: Peter Lammich 
2 
Tobias Nipkow (tuning) 

3 
*) 

66434
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 
70450  9 
"HOLLibrary.Pattern_Aliases" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

10 
Complex_Main 
72812  11 
Priority_Queue_Specs 
66434
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 

67486  18 
The presentation is engineered for simplicity, and most 
66434
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 
70607  31 
"mset_tree (Node _ a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)" 
67486  32 

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

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

36 
lemma mset_tree_simp_alt[simp]: 

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

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

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

66522  42 
by (cases t) auto 
67486  43 

44 
lemma mset_heap_Nil[simp]: 

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

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

66434
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" 
66522  49 
by (auto simp: mset_heap_def) 
67486  50 

66434
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=[]" 
66522  52 
by (auto simp: mset_heap_def) 
67486  53 

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

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

66522  58 
by (auto simp: mset_heap_def) 
67486  59 

60 
subsubsection \<open>Invariants\<close> 

61 

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

62 
text \<open>Binomial tree\<close> 
66522  63 
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where 
67486  64 
"invar_btree (Node r x ts) \<longleftrightarrow> 
66522  65 
(\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]" 
66434
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> 
66522  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)" 

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

70 

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

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

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

73 
text \<open>Binomial Heap invariant\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

75 

67486  76 

66434
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> 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

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

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

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

82 

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

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

66548  87 
context 
88 
includes pattern_aliases 

89 
begin 

90 

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

67486  92 
"link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) = 
66549  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))" 
66548  94 

95 
end 

66491  96 

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

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

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

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

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

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

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

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

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

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

66434
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]" 
66522  115 
 "ins_tree t\<^sub>1 (t\<^sub>2#ts) = 
67486  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 

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

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

119 
unfolding invar_tree_def by auto 
67486  120 

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

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

122 
"invar (t#ts) 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

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

125 

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

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

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

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

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

132 
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric]) 
67486  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 

66434
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: 
67486  139 
assumes "t' \<in> set (ins_tree t ts)" 
66434
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'" 
67486  141 
assumes "rank t\<^sub>0 < rank t" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

142 
shows "rank t\<^sub>0 < rank t'" 
67486  143 
using assms 
66522  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" 

67486  152 

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

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

66522  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> 

66491  160 

70607  161 
context 
162 
includes pattern_aliases 

163 
begin 

164 

66434
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" 
67486  167 
 "merge [] ts\<^sub>2 = ts\<^sub>2" 
70607  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 

66434
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) 
66491  172 
)" 
173 

70607  174 
end 
175 

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

67486  178 

66434
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)" 
70607  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" 

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

183 
shows "rank t < rank t'" 
66522  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 

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

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

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

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

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

192 
using assms 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
diff
changeset

195 

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

196 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
diff
changeset

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

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

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

202 
shows "invar (merge ts\<^sub>1 ts\<^sub>2)" 
66434
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) 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

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

208 
"invar_tree t\<^sub>1" "invar_tree t\<^sub>2" 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
diff
changeset

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

212 
by auto 
67486  213 

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

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

66434
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 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

220 
case LT 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
diff
changeset

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

224 
\<comment> \<open>Invariant follows from induction hypothesis\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

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

227 

ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
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:
72714
diff
changeset

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

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

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

234 
next 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

236 
case GT 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

238 
then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound) 
66434
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 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
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:
72714
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:
72714
diff
changeset

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

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

72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

249 
ranks in the merged remaining heaps\<close> 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
diff
changeset

251 
proof  
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
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:
72714
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:
72714
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:
72714
diff
changeset

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

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

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

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

259 
qed auto 
67486  260 

261 

262 
lemma mset_heap_merge[simp]: 

66434
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" 
67486  264 
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto 
265 

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

267 

66522  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)" 
67486  271 

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

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

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

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

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

279 
lemma get_min_mset: 

280 
assumes "ts\<noteq>[]" 

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

281 
assumes "invar ts" 
67486  282 
assumes "x \<in># mset_heap ts" 
66522  283 
shows "get_min ts \<le> x" 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

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

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

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

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

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

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

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

291 

67486  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) 
66522  295 

67486  296 
lemma get_min: 
66434
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" 
66522  299 
shows "get_min ts = Min_mset (mset_heap ts)" 
67486  300 
using assms get_min_member get_min_mset 
66522  301 
by (auto simp: eq_Min_iff) 
67486  302 

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

304 

66522  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 

66434
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 

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

311 
assumes "ts\<noteq>[]" 
67486  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) 
66522  316 

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

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

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

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

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

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

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

330 

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

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

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

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

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

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

337 
have "invar_tree t' \<and> invar ts'" 
67486  338 
using assms 
66522  339 
proof (induction ts arbitrary: t' ts' rule: get_min.induct) 
66434
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) 
72551  343 
apply (drule set_get_min_rest; fastforce) 
67486  344 
done 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

347 
qed 
66522  348 

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

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

66434
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)" 
67486  354 

68021  355 
lemma invar_del_min[simp]: 
66434
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)" 
67486  359 
using assms 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

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

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

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

364 
dest: invar_get_min_rest 
66522  365 
) 
67486  366 

68021  367 
lemma mset_heap_del_min: 
66434
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 #}" 
66522  370 
using assms 
68021  371 
unfolding del_min_def 
66522  372 
apply (clarsimp split: tree.split prod.split) 
67486  373 
apply (frule (1) get_min_rest_get_min_same_root) 
374 
apply (frule (1) mset_get_min_rest) 

66522  375 
apply (auto simp: mset_heap_def) 
67486  376 
done 
66522  377 

378 

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

380 

66565  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 
66522  387 
and invar = invar and mset = mset_heap 
388 
proof (unfold_locales, goal_cases) 

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

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

66565  399 
case (5 q) thus ?case using get_min[of q] by auto 
67486  400 
next 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

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

66522  404 
next 
66565  405 
case 8 thus ?case by simp 
66522  406 
next 
66565  407 
case 9 thus ?case by simp 
408 
next 

409 
case 10 thus ?case by simp 

66522  410 
qed 
411 

66434
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> 
67486  414 

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

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

417 
assumes "invar_btree t" 
67486  418 
shows "size (mset_tree t) = 2^rank t" 
66434
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 
67486  424 

66434
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 
67486  426 

66434
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 
67486  430 
by (auto cong: map_cong) 
431 
also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" 

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

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

66434
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) 
67486  436 
also have "\<dots> = 2^r  1" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

437 
by (induction r) auto 
67486  438 
finally show ?case 
66434
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 
67486  441 

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

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

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

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

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

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

447 

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

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

450 
assumes "invar ts" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

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

456 
unfolding invar_def by auto 
67486  457 

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

66434
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)"] 
67486  462 
using power_increasing[where a="2::nat"] 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

465 
by (auto cong: map_cong simp: size_mset_tree) 
66434
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 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

468 
finally show ?thesis . 
67486  469 
qed 
470 

66522  471 
subsubsection \<open>Timing Functions\<close> 
472 

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

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

474 
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

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

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

477 
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:
70607
diff
changeset

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

479 

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

480 
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:
70607
diff
changeset

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

482 
 "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = ( 
67486  483 
(if rank t\<^sub>1 < rank t\<^sub>2 then 1 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

484 
else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest) 
67486  485 
)" 
66522  486 

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

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

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

489 

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

490 
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:
70607
diff
changeset

491 
by (induction t ts rule: T_ins_tree.induct) auto 
66522  492 

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

493 
subsubsection \<open>\<open>T_insert\<close>\<close> 
66522  494 

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

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

496 
assumes "invar ts" 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

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

499 

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

500 
have 1: "T_insert x ts \<le> length ts + 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

501 
unfolding T_insert_def by (rule T_ins_tree_simple_bound) 
67486  502 
also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

503 
proof  
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

504 
from size_mset_heap[of ts] assms 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

506 
unfolding invar_def by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

507 
hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

508 
thus ?thesis using le_log2_of_power by blast 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

509 
qed 
67486  510 
finally show ?thesis 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

511 
by (simp only: log_mult of_nat_mult) auto 
67486  512 
qed 
66522  513 

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

514 
subsubsection \<open>\<open>T_merge\<close>\<close> 
66522  515 

70607  516 
context 
517 
includes pattern_aliases 

518 
begin 

519 

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

520 
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:
70607
diff
changeset

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

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

523 
 "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:
70607
diff
changeset

524 
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:
70607
diff
changeset

525 
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:
70607
diff
changeset

526 
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 
67486  527 
)" 
528 

70607  529 
end 
530 

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

66522  533 

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

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

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

536 
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

537 

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

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

539 
"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:
70607
diff
changeset

540 
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:
70607
diff
changeset

541 
(auto simp: T_ins_tree_length algebra_simps) 
66522  542 

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

543 
text \<open>Finally, we get the desired logarithmic bound\<close> 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

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

547 
defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)" 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

548 
assumes BINVARS: "invar ts\<^sub>1" "invar ts\<^sub>2" 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

550 
proof  
67486  551 
define n where "n = n\<^sub>1 + n\<^sub>2" 
552 

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

553 
from T_merge_length[of ts\<^sub>1 ts\<^sub>2] 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

555 
hence "(2::nat)^T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

556 
by (rule power_increasing) auto 
67486  557 
also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

558 
by (auto simp: algebra_simps power_add power_mult) 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

559 
also note BINVARS(1)[THEN size_mset_heap] 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

560 
also note BINVARS(2)[THEN size_mset_heap] 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

561 
finally have "2 ^ T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

562 
by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def) 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

563 
from le_log2_of_power[OF this] have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

565 
also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

567 
also have "n\<^sub>2 \<le> n" by (auto simp: n_def) 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

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

570 
also have "n\<^sub>1 \<le> n" by (auto simp: n_def) 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

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

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

573 
also have "log 2 2 \<le> 2" by auto 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

574 
finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

575 
thus ?thesis unfolding n_def by (auto simp: algebra_simps) 
67486  576 
qed 
577 

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

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

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

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

582 
assumes "invar ts\<^sub>1" "invar ts\<^sub>2" 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

583 
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

584 
using assms T_merge_bound_aux unfolding invar_def by blast 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

585 

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

586 
subsubsection \<open>\<open>T_get_min\<close>\<close> 
66522  587 

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

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

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

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

591 

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

592 
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:
70607
diff
changeset

593 
by (induction ts rule: T_get_min.induct) auto 
67486  594 

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

595 
lemma T_get_min_bound: 
66522  596 
assumes "invar ts" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

599 
proof  
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

600 
have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

602 
proof  
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

603 
from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1" 
66522  604 
unfolding invar_def by auto 
605 
thus ?thesis using le_log2_of_power by blast 

606 
qed 

67486  607 
finally show ?thesis by auto 
608 
qed 

66522  609 

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

610 
subsubsection \<open>\<open>T_del_min\<close>\<close> 
66522  611 

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

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

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

614 
 "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts" 
66522  615 

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

616 
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:
70607
diff
changeset

617 
by (induction ts rule: T_get_min_rest.induct) auto 
67486  618 

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

619 
lemma T_get_min_rest_bound_aux: 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

620 
assumes "invar ts" 
66522  621 
assumes "ts\<noteq>[]" 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

622 
shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)" 
66522  623 
proof  
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

624 
have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto 
66522  625 
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)" 
626 
proof  

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

627 
from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

629 
thus ?thesis using le_log2_of_power by blast 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

630 
qed 
67486  631 
finally show ?thesis by auto 
632 
qed 

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

633 

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

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

635 
assumes "invar ts" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

638 
using assms T_get_min_rest_bound_aux unfolding invar_def by blast 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

639 

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

643 

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

644 
definition "T_rev xs = length xs + 1" 
66522  645 

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

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

647 
"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:
70607
diff
changeset

648 
\<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

649 
)" 
67486  650 

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

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

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

653 
defines "n \<equiv> size (mset_heap ts)" 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

654 
assumes BINVAR: "invar (rev ts)" 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

655 
shows "T_rev ts \<le> 1 + log 2 (n+1)" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

656 
proof  
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

657 
have "T_rev ts = length ts + 1" by (auto simp: T_rev_def) 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

658 
hence "2^T_rev ts = 2*2^length ts" by auto 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

659 
also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def) 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

660 
finally have "2 ^ T_rev ts \<le> 2 * n + 2" . 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

661 
from le_log2_of_power[OF this] have "T_rev ts \<le> log 2 (2 * (n + 1))" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

663 
also have "\<dots> = 1 + log 2 (n+1)" 
67486  664 
by (simp only: of_nat_mult log_mult) auto 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

665 
finally show ?thesis by (auto simp: algebra_simps) 
67486  666 
qed 
66522  667 

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

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

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

670 
defines "n \<equiv> size (mset_heap ts)" 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

671 
assumes BINVAR: "invar ts" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

673 
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

677 

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

678 
note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR] 
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

679 
hence BINVAR1: "invar (rev ts\<^sub>1)" by (blast intro: invar_children) 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

680 

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

681 
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

682 
define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)" 
67486  683 

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

684 
have T_rev_ts1_bound: "T_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

685 
proof  
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

686 
note T_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def] 
67486  687 
also have "n\<^sub>1 \<le> n" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

688 
unfolding n\<^sub>1_def n_def 
66522  689 
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>] 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

691 
finally show ?thesis by (auto simp: algebra_simps) 
67486  692 
qed 
693 

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

694 
have "T_del_min ts = T_get_min_rest ts + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

695 
unfolding T_del_min_def by (simp add: GM) 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

696 
also have "\<dots> \<le> log 2 (n+1) + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

697 
using T_get_min_rest_bound_aux[OF assms(2)] by (auto simp: n_def) 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

698 
also have "\<dots> \<le> 2*log 2 (n+1) + T_merge (rev ts\<^sub>1) ts\<^sub>2 + 1" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

699 
using T_rev_ts1_bound by auto 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

700 
also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3" 
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset

701 
using T_merge_bound_aux[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>] 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

702 
by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

703 
also have "n\<^sub>1 + n\<^sub>2 \<le> n" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

704 
unfolding n\<^sub>1_def n\<^sub>2_def n_def 
66522  705 
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>] 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

706 
by (auto simp: mset_heap_def) 
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

707 
finally have "T_del_min ts \<le> 6 * log 2 (n+1) + 3" 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

709 
thus ?thesis by (simp add: algebra_simps) 
67486  710 
qed 
711 

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

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

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

714 
defines "n \<equiv> size (mset_heap ts)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

715 
assumes "invar ts" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

717 
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3" 
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset

718 
using assms T_del_min_bound_aux unfolding invar_def by blast 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

719 

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

720 
end 