1(* Author: Tobias Nipkow *)
2
3section \<open>Leftist Heap\<close>
4
5theory Leftist_Heap
6imports
7  Base_FDS
8  Tree2
9  Priority_Queue_Specs
10  Complex_Main
11begin
12
13fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
14"mset_tree Leaf = {#}" |
15"mset_tree (Node l a _ r) = {#a#} + mset_tree l + mset_tree r"
16
17type_synonym 'a lheap = "('a,nat)tree"
18
19fun rank :: "'a lheap \<Rightarrow> nat" where
20"rank Leaf = 0" |
21"rank (Node _ _ _ r) = rank r + 1"
22
23fun rk :: "'a lheap \<Rightarrow> nat" where
24"rk Leaf = 0" |
25"rk (Node _ _ n _) = n"
26
27text\<open>The invariants:\<close>
28
29fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
30"heap Leaf = True" |
31"heap (Node l m _ r) =
32  (heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))"
33
34fun ltree :: "'a lheap \<Rightarrow> bool" where
35"ltree Leaf = True" |
36"ltree (Node l a n r) =
37 (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
38
39definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
40"node l a r =
41 (let rl = rk l; rr = rk r
42  in if rl \<ge> rr then Node l a (rr+1) r else Node r a (rl+1) l)"
43
44fun get_min :: "'a lheap \<Rightarrow> 'a" where
45"get_min(Node l a n r) = a"
46
47text \<open>For function \<open>merge\<close>:\<close>
48unbundle pattern_aliases
49declare size_prod_measure[measure_function]
50
51fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
52"merge Leaf t2 = t2" |
53"merge t1 Leaf = t1" |
54"merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
55   (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
56    else node l2 a2 (merge t1 r2))"
57
58lemma merge_code: "merge t1 t2 = (case (t1,t2) of
59  (Leaf, _) \<Rightarrow> t2 |
60  (_, Leaf) \<Rightarrow> t1 |
61  (Node l1 a1 n1 r1, Node l2 a2 n2 r2) \<Rightarrow>
62    if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))"
63by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
64
65hide_const (open) insert
66
67definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
68"insert x t = merge (Node Leaf x 1 Leaf) t"
69
70fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
71"del_min Leaf = Leaf" |
72"del_min (Node l x n r) = merge l r"
73
74
75subsection "Lemmas"
76
77lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
78by(cases t) auto
79
80lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
81by(cases t) auto
82
83lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
84by(auto simp add: node_def)
85
86lemma heap_node: "heap (node l a r) \<longleftrightarrow>
87  heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)"
88by(auto simp add: node_def)
89
90
91subsection "Functional Correctness"
92
93lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
94by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps)
95
96lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
97by (auto simp add: insert_def mset_merge)
98
99lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
100by (induction h) (auto simp add: eq_Min_iff)
101
102lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
103by (cases h) (auto simp: mset_merge)
104
105lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
106proof(induction l r rule: merge.induct)
107  case (3 l1 a1 n1 r1 l2 a2 n2 r2)
108  show ?case (is "ltree(merge ?t1 ?t2)")
109  proof cases
110    assume "a1 \<le> a2"
111    hence "ltree (merge ?t1 ?t2) = ltree (node l1 a1 (merge r1 ?t2))" by simp
112    also have "\<dots> = (ltree l1 \<and> ltree(merge r1 ?t2))"
113      by(simp add: ltree_node)
114    also have "..." using "3.prems" "3.IH"(1)[OF \<open>a1 \<le> a2\<close>] by (simp)
115    finally show ?thesis .
116  next (* analogous but automatic *)
117    assume "\<not> a1 \<le> a2"
118    thus ?thesis using 3 by(simp)(auto simp: ltree_node)
119  qed
120qed simp_all
121
122lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
123proof(induction l r rule: merge.induct)
124  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
125qed simp_all
126
127lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
128by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)
129
130lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
131by(simp add: insert_def heap_merge del: merge.simps split: tree.split)
132
133lemma ltree_del_min: "ltree t \<Longrightarrow> ltree(del_min t)"
134by(cases t)(auto simp add: ltree_merge simp del: merge.simps)
135
136lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
137by(cases t)(auto simp add: heap_merge simp del: merge.simps)
138
139text \<open>Last step of functional correctness proof: combine all the above lemmas
140to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
141
142interpretation lheap: Priority_Queue_Merge
143where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
144and insert = insert and del_min = del_min
145and get_min = get_min and merge = merge
146and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
147proof(standard, goal_cases)
148  case 1 show ?case by simp
149next
150  case (2 q) show ?case by (cases q) auto
151next
152  case 3 show ?case by(rule mset_insert)
153next
154  case 4 show ?case by(rule mset_del_min)
155next
156  case 5 thus ?case by(simp add: get_min mset_tree_empty)
157next
158  case 6 thus ?case by(simp)
159next
160  case 7 thus ?case by(simp add: heap_insert ltree_insert)
161next
162  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
163next
164  case 9 thus ?case by (simp add: mset_merge)
165next
166  case 10 thus ?case by (simp add: heap_merge ltree_merge)
167qed
168
169
170subsection "Complexity"
171
172lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
173proof(induction t)
174  case Leaf show ?case by simp
175next
176  case (Node l a n r)
177  hence "rank r \<le> rank l" by simp
178  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
179  have "(2::nat) ^ rank \<langle>l, a, n, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
180    by(simp add: mult_2)
181  also have "\<dots> \<le> size1 l + size1 r"
182    using Node * by (simp del: power_increasing_iff)
183  also have "\<dots> = size1 \<langle>l, a, n, r\<rangle>" by simp
184  finally show ?case .
185qed
186
187text\<open>Explicit termination argument: sum of sizes\<close>
188
189fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
190"t_merge Leaf t2 = 1" |
191"t_merge t2 Leaf = 1" |
192"t_merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
193  (if a1 \<le> a2 then 1 + t_merge r1 t2
194   else 1 + t_merge t1 r2)"
195
196definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
197"t_insert x t = t_merge (Node Leaf x 1 Leaf) t"
198
199fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
200"t_del_min Leaf = 1" |
201"t_del_min (Node l a n r) = t_merge l r"
202
203lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
204proof(induction l r rule: merge.induct)
205  case 3 thus ?case by(simp)
206qed simp_all
207
208corollary t_merge_log: assumes "ltree l" "ltree r"
209  shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
210using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
211  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r]
212by linarith
213
214corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
215using t_merge_log[of "Node Leaf x 1 Leaf" t]
216by(simp add: t_insert_def split: tree.split)
217
218(* FIXME mv ? *)
219lemma ld_ld_1_less:
220  assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)"
221proof -
222  have "2 powr (log 2 x + log 2 y + 1) = 2*x*y"
223    using assms by(simp add: powr_add)
224  also have "\<dots> < (x+y)^2" using assms
225    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
226  also have "\<dots> = 2 powr (2 * log 2 (x+y))"
227    using assms by(simp add: powr_add log_powr[symmetric])
228  finally show ?thesis by simp
229qed
230
231corollary t_del_min_log: assumes "ltree t"
232  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
233proof(cases t)
234  case Leaf thus ?thesis using assms by simp
235next
236  case [simp]: (Node t1 _ _ t2)
237  have "t_del_min t = t_merge t1 t2" by simp
238  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
239    using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
240  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
241    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
242  finally show ?thesis .
243qed
244
245end
246