1(* Author: Tobias Nipkow *) 2 3section \<open>Creating Balanced Trees\<close> 4 5theory Balance 6imports 7 "HOL-Library.Tree_Real" 8begin 9 10fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where 11"bal n xs = (if n=0 then (Leaf,xs) else 12 (let m = n div 2; 13 (l, ys) = bal m xs; 14 (r, zs) = bal (n-1-m) (tl ys) 15 in (Node l (hd ys) r, zs)))" 16 17declare bal.simps[simp del] 18 19definition bal_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree" where 20"bal_list n xs = fst (bal n xs)" 21 22definition balance_list :: "'a list \<Rightarrow> 'a tree" where 23"balance_list xs = bal_list (length xs) xs" 24 25definition bal_tree :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where 26"bal_tree n t = bal_list n (inorder t)" 27 28definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where 29"balance_tree t = bal_tree (size t) t" 30 31lemma bal_simps: 32 "bal 0 xs = (Leaf, xs)" 33 "n > 0 \<Longrightarrow> 34 bal n xs = 35 (let m = n div 2; 36 (l, ys) = bal m xs; 37 (r, zs) = bal (n-1-m) (tl ys) 38 in (Node l (hd ys) r, zs))" 39by(simp_all add: bal.simps) 40 41text\<open>Some of the following lemmas take advantage of the fact 42that \<open>bal xs n\<close> yields a result even if \<open>n > length xs\<close>.\<close> 43 44lemma size_bal: "bal n xs = (t,ys) \<Longrightarrow> size t = n" 45proof(induction n xs arbitrary: t ys rule: bal.induct) 46 case (1 n xs) 47 thus ?case 48 by(cases "n=0") 49 (auto simp add: bal_simps Let_def split: prod.splits) 50qed 51 52lemma bal_inorder: 53 "\<lbrakk> bal n xs = (t,ys); n \<le> length xs \<rbrakk> 54 \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs" 55proof(induction n xs arbitrary: t ys rule: bal.induct) 56 case (1 n xs) show ?case 57 proof cases 58 assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps) 59 next 60 assume [arith]: "n \<noteq> 0" 61 let ?n1 = "n div 2" let ?n2 = "n - 1 - ?n1" 62 from "1.prems" obtain l r xs' where 63 b1: "bal ?n1 xs = (l,xs')" and 64 b2: "bal ?n2 (tl xs') = (r,ys)" and 65 t: "t = \<langle>l, hd xs', r\<rangle>" 66 by(auto simp: Let_def bal_simps split: prod.splits) 67 have IH1: "inorder l = take ?n1 xs \<and> xs' = drop ?n1 xs" 68 using b1 "1.prems" by(intro "1.IH"(1)) auto 69 have IH2: "inorder r = take ?n2 (tl xs') \<and> ys = drop ?n2 (tl xs')" 70 using b1 b2 IH1 "1.prems" by(intro "1.IH"(2)) auto 71 have "drop (n div 2) xs \<noteq> []" using "1.prems"(2) by simp 72 hence "hd (drop ?n1 xs) # take ?n2 (tl (drop ?n1 xs)) = take (?n2 + 1) (drop ?n1 xs)" 73 by (metis Suc_eq_plus1 take_Suc) 74 hence *: "inorder t = take n xs" using t IH1 IH2 75 using take_add[of ?n1 "?n2+1" xs] by(simp) 76 have "n - n div 2 + n div 2 = n" by simp 77 hence "ys = drop n xs" using IH1 IH2 by (simp add: drop_Suc[symmetric]) 78 thus ?thesis using * by blast 79 qed 80qed 81 82corollary inorder_bal_list[simp]: 83 "n \<le> length xs \<Longrightarrow> inorder(bal_list n xs) = take n xs" 84unfolding bal_list_def by (metis bal_inorder eq_fst_iff) 85 86corollary inorder_balance_list[simp]: "inorder(balance_list xs) = xs" 87by(simp add: balance_list_def) 88 89corollary inorder_bal_tree: 90 "n \<le> size t \<Longrightarrow> inorder(bal_tree n t) = take n (inorder t)" 91by(simp add: bal_tree_def) 92 93corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t" 94by(simp add: balance_tree_def inorder_bal_tree) 95 96corollary size_bal_list[simp]: "size(bal_list n xs) = n" 97unfolding bal_list_def by (metis prod.collapse size_bal) 98 99corollary size_balance_list[simp]: "size(balance_list xs) = length xs" 100by (simp add: balance_list_def) 101 102corollary size_bal_tree[simp]: "size(bal_tree n t) = n" 103by(simp add: bal_tree_def) 104 105corollary size_balance_tree[simp]: "size(balance_tree t) = size t" 106by(simp add: balance_tree_def) 107 108lemma min_height_bal: 109 "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)" 110proof(induction n xs arbitrary: t ys rule: bal.induct) 111 case (1 n xs) show ?case 112 proof cases 113 assume "n = 0" thus ?thesis 114 using "1.prems" by (simp add: bal_simps) 115 next 116 assume [arith]: "n \<noteq> 0" 117 from "1.prems" obtain l r xs' where 118 b1: "bal (n div 2) xs = (l,xs')" and 119 b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and 120 t: "t = \<langle>l, hd xs', r\<rangle>" 121 by(auto simp: bal_simps Let_def split: prod.splits) 122 let ?log1 = "nat (floor(log 2 (n div 2 + 1)))" 123 let ?log2 = "nat (floor(log 2 (n - 1 - n div 2 + 1)))" 124 have IH1: "min_height l = ?log1" using "1.IH"(1) b1 by simp 125 have IH2: "min_height r = ?log2" using "1.IH"(2) b1 b2 by simp 126 have "(n+1) div 2 \<ge> 1" by arith 127 hence 0: "log 2 ((n+1) div 2) \<ge> 0" by simp 128 have "n - 1 - n div 2 + 1 \<le> n div 2 + 1" by arith 129 hence le: "?log2 \<le> ?log1" 130 by(simp add: nat_mono floor_mono) 131 have "min_height t = min ?log1 ?log2 + 1" by (simp add: t IH1 IH2) 132 also have "\<dots> = ?log2 + 1" using le by (simp add: min_absorb2) 133 also have "n - 1 - n div 2 + 1 = (n+1) div 2" by linarith 134 also have "nat (floor(log 2 ((n+1) div 2))) + 1 135 = nat (floor(log 2 ((n+1) div 2) + 1))" 136 using 0 by linarith 137 also have "\<dots> = nat (floor(log 2 (n + 1)))" 138 using floor_log2_div2[of "n+1"] by (simp add: log_mult) 139 finally show ?thesis . 140 qed 141qed 142 143lemma height_bal: 144 "bal n xs = (t,ys) \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>" 145proof(induction n xs arbitrary: t ys rule: bal.induct) 146 case (1 n xs) show ?case 147 proof cases 148 assume "n = 0" thus ?thesis 149 using "1.prems" by (simp add: bal_simps) 150 next 151 assume [arith]: "n \<noteq> 0" 152 from "1.prems" obtain l r xs' where 153 b1: "bal (n div 2) xs = (l,xs')" and 154 b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and 155 t: "t = \<langle>l, hd xs', r\<rangle>" 156 by(auto simp: bal_simps Let_def split: prod.splits) 157 let ?log1 = "nat \<lceil>log 2 (n div 2 + 1)\<rceil>" 158 let ?log2 = "nat \<lceil>log 2 (n - 1 - n div 2 + 1)\<rceil>" 159 have IH1: "height l = ?log1" using "1.IH"(1) b1 by simp 160 have IH2: "height r = ?log2" using "1.IH"(2) b1 b2 by simp 161 have 0: "log 2 (n div 2 + 1) \<ge> 0" by auto 162 have "n - 1 - n div 2 + 1 \<le> n div 2 + 1" by arith 163 hence le: "?log2 \<le> ?log1" 164 by(simp add: nat_mono ceiling_mono del: nat_ceiling_le_eq) 165 have "height t = max ?log1 ?log2 + 1" by (simp add: t IH1 IH2) 166 also have "\<dots> = ?log1 + 1" using le by (simp add: max_absorb1) 167 also have "\<dots> = nat \<lceil>log 2 (n div 2 + 1) + 1\<rceil>" using 0 by linarith 168 also have "\<dots> = nat \<lceil>log 2 (n + 1)\<rceil>" 169 using ceiling_log2_div2[of "n+1"] by (simp) 170 finally show ?thesis . 171 qed 172qed 173 174lemma balanced_bal: 175 assumes "bal n xs = (t,ys)" shows "balanced t" 176unfolding balanced_def 177using height_bal[OF assms] min_height_bal[OF assms] 178by linarith 179 180lemma height_bal_list: 181 "n \<le> length xs \<Longrightarrow> height (bal_list n xs) = nat \<lceil>log 2 (n + 1)\<rceil>" 182unfolding bal_list_def by (metis height_bal prod.collapse) 183 184lemma height_balance_list: 185 "height (balance_list xs) = nat \<lceil>log 2 (length xs + 1)\<rceil>" 186by (simp add: balance_list_def height_bal_list) 187 188corollary height_bal_tree: 189 "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat\<lceil>log 2 (n + 1)\<rceil>" 190unfolding bal_list_def bal_tree_def 191using height_bal prod.exhaust_sel by blast 192 193corollary height_balance_tree: 194 "height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>" 195by (simp add: bal_tree_def balance_tree_def height_bal_list) 196 197corollary balanced_bal_list[simp]: "balanced (bal_list n xs)" 198unfolding bal_list_def by (metis balanced_bal prod.collapse) 199 200corollary balanced_balance_list[simp]: "balanced (balance_list xs)" 201by (simp add: balance_list_def) 202 203corollary balanced_bal_tree[simp]: "balanced (bal_tree n t)" 204by (simp add: bal_tree_def) 205 206corollary balanced_balance_tree[simp]: "balanced (balance_tree t)" 207by (simp add: balance_tree_def) 208 209lemma wbalanced_bal: "bal n xs = (t,ys) \<Longrightarrow> wbalanced t" 210proof(induction n xs arbitrary: t ys rule: bal.induct) 211 case (1 n xs) 212 show ?case 213 proof cases 214 assume "n = 0" 215 thus ?thesis 216 using "1.prems" by(simp add: bal_simps) 217 next 218 assume "n \<noteq> 0" 219 with "1.prems" obtain l ys r zs where 220 rec1: "bal (n div 2) xs = (l, ys)" and 221 rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and 222 t: "t = \<langle>l, hd ys, r\<rangle>" 223 by(auto simp add: bal_simps Let_def split: prod.splits) 224 have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl rec1] . 225 have "wbalanced r" using "1.IH"(2)[OF \<open>n\<noteq>0\<close> refl rec1[symmetric] refl rec2] . 226 with l t size_bal[OF rec1] size_bal[OF rec2] 227 show ?thesis by auto 228 qed 229qed 230 231text\<open>An alternative proof via @{thm balanced_if_wbalanced}:\<close> 232lemma "bal n xs = (t,ys) \<Longrightarrow> balanced t" 233by(rule balanced_if_wbalanced[OF wbalanced_bal]) 234 235lemma wbalanced_bal_list[simp]: "wbalanced (bal_list n xs)" 236by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal) 237 238lemma wbalanced_balance_list[simp]: "wbalanced (balance_list xs)" 239by(simp add: balance_list_def) 240 241lemma wbalanced_bal_tree[simp]: "wbalanced (bal_tree n t)" 242by(simp add: bal_tree_def) 243 244lemma wbalanced_balance_tree: "wbalanced (balance_tree t)" 245by (simp add: balance_tree_def) 246 247hide_const (open) bal 248 249end 250