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