author  nipkow 
Tue, 29 Aug 2017 17:01:11 +0200  
changeset 66550  b8a6f9337229 
parent 66549  253880668a43 
child 66564  ff561d9cb661 
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 
66492  9 
Base_FDS 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

11 
Priority_Queue 
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 

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

18 
The presentation is engineered for simplicity, and most 
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 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

31 
"mset_tree (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_tree t)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

32 

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

33 
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

34 
"mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

35 

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

36 
lemma mset_tree_simp_alt[simp]: 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

39 
declare mset_tree.simps[simp del] 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

40 

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

41 
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}" 
66524  42 
by (cases t) auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

43 

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

44 
lemma mset_heap_Nil[simp]: 
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) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

50 

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) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

53 

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

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

56 

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

57 
lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts" 
66524  58 
by (auto simp: mset_heap_def) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

59 

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

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

61 

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

62 
text \<open>Binomial invariant\<close> 
66524  63 
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where 
64 
"invar_btree (Node r x ts) \<longleftrightarrow> 

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 
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where 
66524  68 
"invar_bheap ts 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

69 
\<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (op <) (map rank ts))" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

70 

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

71 
text \<open>Ordering (heap) invariant\<close> 
66524  72 
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where 
73 
"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

74 

66524  75 
definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where 
76 
"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)" 

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

77 

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

78 
definition invar :: "'a::linorder heap \<Rightarrow> bool" where 
66524  79 
"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

80 

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

81 
text \<open>The children of a node are a valid heap\<close> 
66524  82 
lemma invar_oheap_children: 
83 
"invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)" 

84 
by (auto simp: invar_oheap_def) 

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

85 

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

87 
"invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)" 
66524  88 
by (auto simp: invar_bheap_def rev_map[symmetric]) 
89 

90 

91 
subsection \<open>Operations and Their Functional Correctness\<close> 

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

92 

66524  93 
subsubsection \<open>\<open>link\<close>\<close> 
94 

66549  95 
context 
96 
includes pattern_aliases 

97 
begin 

98 

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

66550  100 
"link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) = 
101 
(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  102 

103 
end 

66492  104 

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

106 
assumes "invar_btree t\<^sub>1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

107 
assumes "invar_btree t\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

109 
shows "invar_btree (link t\<^sub>1 t\<^sub>2)" 
66524  110 
using assms 
66549  111 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 
66524  112 

113 
lemma invar_link_otree: 

114 
assumes "invar_otree t\<^sub>1" 

115 
assumes "invar_otree t\<^sub>2" 

116 
shows "invar_otree (link t\<^sub>1 t\<^sub>2)" 

117 
using assms 

66549  118 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto 
66524  119 

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

66549  121 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

122 

66524  123 
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" 
66549  124 
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

125 

66524  126 
subsubsection \<open>\<open>ins_tree\<close>\<close> 
127 

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

128 
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

129 
"ins_tree t [] = [t]" 
66524  130 
 "ins_tree t\<^sub>1 (t\<^sub>2#ts) = 
131 
(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)" 

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

132 

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

133 
lemma invar_bheap_Cons[simp]: 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

134 
"invar_bheap (t#ts) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

135 
\<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" 
66524  136 
by (auto simp: sorted_wrt_Cons invar_bheap_def) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

137 

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

139 
assumes "invar_btree t" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

142 
shows "invar_bheap (ins_tree t ts)" 
66524  143 
using assms 
144 
by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric]) 

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

145 

66524  146 
lemma invar_oheap_Cons[simp]: 
147 
"invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts" 

148 
by (auto simp: invar_oheap_def) 

149 

150 
lemma invar_oheap_ins_tree: 

151 
assumes "invar_otree t" 

152 
assumes "invar_oheap ts" 

153 
shows "invar_oheap (ins_tree t ts)" 

154 
using assms 

155 
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree) 

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

156 

66524  157 
lemma mset_heap_ins_tree[simp]: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

158 
"mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" 
66524  159 
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

160 

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

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

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

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

164 
assumes "rank t\<^sub>0 < rank t" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

165 
shows "rank t\<^sub>0 < rank t'" 
66524  166 
using assms 
167 
by (induction t ts rule: ins_tree.induct) (auto split: if_splits) 

168 

169 
subsubsection \<open>\<open>insert\<close>\<close> 

170 

171 
hide_const (open) insert 

172 

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

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

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

175 

66524  176 
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)" 
177 
by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def) 

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

178 

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

181 

182 
subsubsection \<open>\<open>merge\<close>\<close> 

66492  183 

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

184 
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

185 
"merge ts\<^sub>1 [] = ts\<^sub>1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

186 
 "merge [] ts\<^sub>2 = ts\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

187 
 "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = ( 
66492  188 
if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) else 
189 
if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2 

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

190 
else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) 
66492  191 
)" 
192 

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

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

195 

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

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

197 
assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

203 
(auto split: if_splits simp: ins_tree_rank_bound) 

204 

205 
lemma invar_bheap_merge: 

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

206 
assumes "invar_bheap ts\<^sub>1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

207 
assumes "invar_bheap ts\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

210 
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

211 
case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

212 

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

213 
from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

215 

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

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

217 
 (GT) "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 
 (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

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

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

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

222 
then show ?thesis using 3 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

223 
by (force elim!: merge_rank_bound) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

226 
then show ?thesis using 3 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

227 
by (force elim!: merge_rank_bound) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

229 
case [simp]: EQ 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

230 

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

231 
from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

233 

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

234 
have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t' 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

236 
apply (rule merge_rank_bound) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

237 
using "3.prems" by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

238 
with EQ show ?thesis 
66524  239 
by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

242 

66524  243 
lemma invar_oheap_merge: 
244 
assumes "invar_oheap ts\<^sub>1" 

245 
assumes "invar_oheap ts\<^sub>2" 

246 
shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)" 

247 
using assms 

248 
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) 

249 
(auto simp: invar_oheap_ins_tree invar_link_otree) 

250 

251 
lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)" 

252 
by (auto simp: invar_def invar_bheap_merge invar_oheap_merge) 

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

253 

66524  254 
lemma mset_heap_merge[simp]: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

255 
"mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2" 
66524  256 
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

257 

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

259 

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

66546  262 
 "get_min (t#ts) = min (root t) (get_min ts)" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

263 

66524  264 
lemma invar_otree_root_min: 
265 
assumes "invar_otree t" 

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

266 
assumes "x \<in># mset_tree t" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

267 
shows "root t \<le> x" 
66524  268 
using assms 
269 
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def) 

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

270 

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

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

274 
assumes "x \<in># mset_heap ts" 
66524  275 
shows "get_min ts \<le> x" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

276 
using assms 
66524  277 
apply (induction ts arbitrary: x rule: get_min.induct) 
278 
apply (auto 

66546  279 
simp: invar_otree_root_min min_def intro: order_trans; 
66524  280 
meson linear order_trans invar_otree_root_min 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

281 
)+ 
66524  282 
done 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

283 

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

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

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

287 
assumes "x \<in># mset_heap ts" 
66524  288 
shows "get_min ts \<le> x" 
289 
using assms by (auto simp: invar_def get_min_mset_aux) 

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

290 

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

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

295 
lemma get_min: 

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

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

297 
assumes "invar ts" 
66524  298 
shows "get_min ts = Min_mset (mset_heap ts)" 
299 
using assms get_min_member get_min_mset 

300 
by (auto simp: eq_Min_iff) 

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

301 

66524  302 
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

303 

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

306 
 "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

307 
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

308 

66524  309 
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

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

313 
using assms 

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

316 
lemma mset_get_min_rest: 

317 
assumes "get_min_rest ts = (t',ts')" 

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

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

319 
shows "mset ts = {#t'#} + mset ts'" 
66524  320 
using assms 
321 
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) 

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

322 

66524  323 
lemma set_get_min_rest: 
324 
assumes "get_min_rest ts = (t', ts')" 

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

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

328 
by auto 

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

329 

66524  330 
lemma invar_bheap_get_min_rest: 
331 
assumes "get_min_rest ts = (t',ts')" 

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

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

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

334 
shows "invar_btree t'" and "invar_bheap ts'" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

336 
have "invar_btree t' \<and> invar_bheap ts'" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

337 
using assms 
66524  338 
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

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

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

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

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

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

345 
thus "invar_btree t'" and "invar_bheap ts'" by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

346 
qed 
66524  347 

348 
lemma invar_oheap_get_min_rest: 

349 
assumes "get_min_rest ts = (t',ts')" 

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

350 
assumes "ts\<noteq>[]" 
66524  351 
assumes "invar_oheap ts" 
352 
shows "invar_otree t'" and "invar_oheap ts'" 

353 
using assms 

354 
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) 

355 

356 
subsubsection \<open>\<open>del_min\<close>\<close> 

357 

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

358 
definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where 
66524  359 
"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

360 
(Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

361 

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

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

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

365 
shows "invar (del_min ts)" 
66524  366 
using assms 
367 
unfolding invar_def del_min_def 

368 
by (auto 

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

369 
split: prod.split tree.split 
66524  370 
intro!: invar_bheap_merge invar_oheap_merge 
371 
dest: invar_bheap_get_min_rest invar_oheap_get_min_rest 

372 
intro!: invar_oheap_children invar_bheap_children 

373 
) 

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

374 

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

376 
assumes "ts \<noteq> []" 
66524  377 
shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}" 
378 
using assms 

379 
unfolding del_min_def 

380 
apply (clarsimp split: tree.split prod.split) 

381 
apply (frule (1) get_min_rest_get_min_same_root) 

382 
apply (frule (1) mset_get_min_rest) 

383 
apply (auto simp: mset_heap_def) 

384 
done 

385 

386 

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

388 

389 
interpretation binheap: Priority_Queue 

390 
where empty = "[]" and is_empty = "op = []" and insert = insert 

391 
and get_min = get_min and del_min = del_min 

392 
and invar = invar and mset = mset_heap 

393 
proof (unfold_locales, goal_cases) 

394 
case 1 

395 
then show ?case by simp 

396 
next 

397 
case (2 q) 

398 
then show ?case by auto 

399 
next 

400 
case (3 q x) 

401 
then show ?case by auto 

402 
next 

403 
case (4 q) 

404 
then show ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 

405 
by (auto simp: union_single_eq_diff) 

406 
next 

407 
case (5 q) 

408 
then show ?case using get_min[of q] by auto 

409 
next 

410 
case 6 

411 
then show ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def) 

412 
next 

413 
case (7 q x) 

414 
then show ?case by simp 

415 
next 

416 
case (8 q) 

417 
then show ?case by simp 

418 
qed 

419 

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

420 

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

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

422 

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

423 
text \<open>The size of a binomial tree is determined by its rank\<close> 
66524  424 
lemma size_mset_btree: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

425 
assumes "invar_btree t" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

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

430 
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

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

432 

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

433 
from Node have COMPL: "map rank ts = rev [0..<r]" by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

434 

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

435 
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

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

437 
also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

438 
by (auto cong: sum_list_cong) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

439 
also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

441 
also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

443 
by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

444 
also have "\<dots> = 2^r  1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

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

449 

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

450 
text \<open>The length of a binomial heap is bounded by the number of its elements\<close> 
66547  451 
lemma size_mset_bheap: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

453 
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

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

455 
from \<open>invar_bheap ts\<close> have 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

456 
ASC: "sorted_wrt (op <) (map rank ts)" and 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

457 
TINV: "\<forall>t\<in>set ts. invar_btree t" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

459 

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

460 
have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

462 
also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

463 
using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "op ^ (2::nat)"] 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

464 
using power_increasing[where a="2::nat"] 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

466 
also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV 
66524  467 
by (auto cong: sum_list_cong simp: size_mset_btree) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

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

472 

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

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

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

476 
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

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

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

479 
definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

481 

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

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

483 
"t_ins_tree t [] = 1" 
66524  484 
 "t_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = ( 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

485 
(if rank t\<^sub>1 < rank t\<^sub>2 then 1 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

486 
else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

487 
)" 
66524  488 

489 
definition t_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where 

490 
"t_insert x ts = t_ins_tree (Node 0 x []) ts" 

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

491 

66524  492 
lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" 
493 
by (induction t ts rule: t_ins_tree.induct) auto 

494 

495 
subsubsection \<open>\<open>t_insert\<close>\<close> 

496 

497 
lemma t_insert_bound: 

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

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

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

501 

66524  502 
have 1: "t_insert x ts \<le> length ts + 1" 
503 
unfolding t_insert_def by (rule t_ins_tree_simple_bound) 

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

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

505 
proof  
66547  506 
from size_mset_bheap[of ts] assms 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

507 
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

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

509 
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

510 
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

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

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

513 
by (simp only: log_mult of_nat_mult) auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

514 
qed 
66524  515 

516 
subsubsection \<open>\<open>t_merge\<close>\<close> 

517 

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

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

519 
"t_merge ts\<^sub>1 [] = 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

520 
 "t_merge [] ts\<^sub>2 = 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

521 
 "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + ( 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

522 
if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

523 
else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

524 
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 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

526 

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

527 
text \<open>A crucial idea is to estimate the time in correlation with the 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

528 
result length, as each carry reduces the length of the result.\<close> 
66524  529 

530 
lemma t_ins_tree_length: 

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

531 
"t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts" 
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 

66524  534 
lemma t_merge_length: 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
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" 
66524  536 
by (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct) 
537 
(auto simp: t_ins_tree_length algebra_simps) 

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

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

541 
fixes ts\<^sub>1 ts\<^sub>2 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

542 
defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)" 
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)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

544 
assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

547 
define n where "n = n\<^sub>1 + n\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

548 

66524  549 
from t_merge_length[of ts\<^sub>1 ts\<^sub>2] 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

552 
by (rule power_increasing) auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

554 
by (auto simp: algebra_simps power_add power_mult) 
66547  555 
also note BINVARS(1)[THEN size_mset_bheap] 
556 
also note BINVARS(2)[THEN size_mset_bheap] 

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

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

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

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

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

561 
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

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

563 
also have "n\<^sub>2 \<le> n" by (auto simp: n_def) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

564 
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)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

566 
also have "n\<^sub>1 \<le> n" by (auto simp: n_def) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

569 
also have "log 2 2 \<le> 2" by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

571 
thus ?thesis unfolding n_def by (auto simp: algebra_simps) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

573 

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

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

575 
fixes ts\<^sub>1 ts\<^sub>2 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

577 
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

578 
assumes "invar ts\<^sub>1" "invar ts\<^sub>2" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

581 

66524  582 
subsubsection \<open>\<open>t_get_min\<close>\<close> 
583 

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

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

585 
"t_get_min [t] = 1" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

587 

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

588 
lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts" 
66524  589 
by (induction ts rule: t_get_min.induct) auto 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

590 

66524  591 
lemma t_get_min_bound: 
592 
assumes "invar ts" 

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

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

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

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

596 
have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

597 
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

598 
proof  
66547  599 
from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1" 
66524  600 
unfolding invar_def by auto 
601 
thus ?thesis using le_log2_of_power by blast 

602 
qed 

603 
finally show ?thesis by auto 

604 
qed 

605 

606 
subsubsection \<open>\<open>t_del_min\<close>\<close> 

607 

608 
fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where 

609 
"t_get_min_rest [t] = 1" 

610 
 "t_get_min_rest (t#ts) = 1 + t_get_min_rest ts" 

611 

612 
lemma t_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min_rest ts = length ts" 

613 
by (induction ts rule: t_get_min_rest.induct) auto 

614 

615 
lemma t_get_min_rest_bound_aux: 

616 
assumes "invar_bheap ts" 

617 
assumes "ts\<noteq>[]" 

618 
shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)" 

619 
proof  

620 
have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto 

621 
also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)" 

622 
proof  

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

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

625 
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

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

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

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

629 

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

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

632 
assumes "ts\<noteq>[]" 
66524  633 
shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)" 
634 
using assms t_get_min_rest_bound_aux unfolding invar_def by blast 

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

635 

66524  636 
text\<open>Note that although the definition of function @{const rev} has quadratic complexity, 
637 
it can and is implemented (via suitable code lemmas) as a linear time function. 

638 
Thus the following definition is justified:\<close> 

639 

640 
definition "t_rev xs = length xs + 1" 

641 

642 
definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where 

643 
"t_del_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2) 

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

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

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

646 

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

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

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

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

650 
assumes BINVAR: "invar_bheap (rev ts)" 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

652 
proof  
66524  653 
have "t_rev ts = length ts + 1" by (auto simp: t_rev_def) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

654 
hence "2^t_rev ts = 2*2^length ts" by auto 
66547  655 
also have "\<dots> \<le> 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

656 
finally have "2 ^ t_rev ts \<le> 2 * n + 2" . 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

660 
by (simp only: of_nat_mult log_mult) auto 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

661 
finally show ?thesis by (auto simp: algebra_simps) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

662 
qed 
66524  663 

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

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

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

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

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

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

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

670 
proof  
66524  671 
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

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

673 

66524  674 
note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR] 
675 
hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children) 

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

676 

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

677 
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

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

679 

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

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

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

682 
note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def] 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

684 
unfolding n\<^sub>1_def n_def 
66524  685 
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

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

687 
finally show ?thesis by (auto simp: algebra_simps) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

689 

66524  690 
have "t_del_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

691 
unfolding t_del_min_def by (simp add: GM) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

692 
also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" 
66524  693 
using t_get_min_rest_bound_aux[OF assms(2)] by (auto simp: n_def) 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

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

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

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

698 
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

699 
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

700 
unfolding n\<^sub>1_def n\<^sub>2_def n_def 
66524  701 
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

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

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

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

705 
thus ?thesis by (simp add: algebra_simps) 
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

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

707 

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

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

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

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

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

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

713 
shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3" 
66524  714 
using assms t_del_min_bound_aux unfolding invar_def by blast 
66436
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset

715 

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

716 
end 