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