src/HOL/Data_Structures/Leftist_Heap.thy
author nipkow
Thu Mar 24 15:56:47 2016 +0100 (2016-03-24)
changeset 62706 49c6a54ceab6
child 64968 a7ea55c1be52
permissions -rw-r--r--
added Leftist_Heap
nipkow@62706
     1
(* Author: Tobias Nipkow *)
nipkow@62706
     2
nipkow@62706
     3
section \<open>Leftist Heap\<close>
nipkow@62706
     4
nipkow@62706
     5
theory Leftist_Heap
nipkow@62706
     6
imports Tree2 "~~/src/HOL/Library/Multiset" Complex_Main
nipkow@62706
     7
begin
nipkow@62706
     8
nipkow@62706
     9
type_synonym 'a lheap = "('a,nat)tree"
nipkow@62706
    10
nipkow@62706
    11
fun rank :: "'a lheap \<Rightarrow> nat" where
nipkow@62706
    12
"rank Leaf = 0" |
nipkow@62706
    13
"rank (Node _ _ _ r) = rank r + 1"
nipkow@62706
    14
nipkow@62706
    15
fun rk :: "'a lheap \<Rightarrow> nat" where
nipkow@62706
    16
"rk Leaf = 0" |
nipkow@62706
    17
"rk (Node n _ _ _) = n"
nipkow@62706
    18
nipkow@62706
    19
text{* The invariant: *}
nipkow@62706
    20
nipkow@62706
    21
fun lheap :: "'a lheap \<Rightarrow> bool" where
nipkow@62706
    22
"lheap Leaf = True" |
nipkow@62706
    23
"lheap (Node n l a r) =
nipkow@62706
    24
 (n = rank r + 1 \<and> rank l \<ge> rank r \<and> lheap l & lheap r)"
nipkow@62706
    25
nipkow@62706
    26
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
nipkow@62706
    27
"node l a r =
nipkow@62706
    28
 (let rl = rk l; rr = rk r
nipkow@62706
    29
  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
nipkow@62706
    30
nipkow@62706
    31
fun get_min :: "'a lheap \<Rightarrow> 'a" where
nipkow@62706
    32
"get_min(Node n l a r) = a"
nipkow@62706
    33
nipkow@62706
    34
function meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
nipkow@62706
    35
"meld Leaf t2 = t2" |
nipkow@62706
    36
"meld t1 Leaf = t1" |
nipkow@62706
    37
"meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
nipkow@62706
    38
   (if a1 \<le> a2 then node l1 a1 (meld r1 (Node n2 l2 a2 r2))
nipkow@62706
    39
    else node l2 a2 (meld r2 (Node n1 l1 a1 r1)))"
nipkow@62706
    40
by pat_completeness auto
nipkow@62706
    41
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
nipkow@62706
    42
nipkow@62706
    43
lemma meld_code: "meld t1 t2 = (case (t1,t2) of
nipkow@62706
    44
  (Leaf, _) \<Rightarrow> t2 |
nipkow@62706
    45
  (_, Leaf) \<Rightarrow> t1 |
nipkow@62706
    46
  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
nipkow@62706
    47
    if a1 \<le> a2 then node l1 a1 (meld r1 t2) else node l2 a2 (meld r2 t1))"
nipkow@62706
    48
by(induction t1 t2 rule: meld.induct) (simp_all split: tree.split)
nipkow@62706
    49
nipkow@62706
    50
definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
nipkow@62706
    51
"insert x t = meld (Node 1 Leaf x Leaf) t"
nipkow@62706
    52
nipkow@62706
    53
fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
nipkow@62706
    54
"del_min Leaf = Leaf" |
nipkow@62706
    55
"del_min (Node n l x r) = meld l r"
nipkow@62706
    56
nipkow@62706
    57
nipkow@62706
    58
subsection "Lemmas"
nipkow@62706
    59
nipkow@62706
    60
declare Let_def [simp]
nipkow@62706
    61
nipkow@62706
    62
lemma rk_eq_rank[simp]: "lheap t \<Longrightarrow> rk t = rank t"
nipkow@62706
    63
by(cases t) auto
nipkow@62706
    64
nipkow@62706
    65
lemma lheap_node: "lheap (node l a r) \<longleftrightarrow> lheap l \<and> lheap r"
nipkow@62706
    66
by(auto simp add: node_def)
nipkow@62706
    67
nipkow@62706
    68
nipkow@62706
    69
subsection "Functional Correctness"
nipkow@62706
    70
nipkow@62706
    71
locale Priority_Queue =
nipkow@62706
    72
fixes empty :: "'pq"
nipkow@62706
    73
and insert :: "'a \<Rightarrow> 'pq \<Rightarrow> 'pq"
nipkow@62706
    74
and get_min :: "'pq \<Rightarrow> 'a"
nipkow@62706
    75
and del_min :: "'pq \<Rightarrow> 'pq"
nipkow@62706
    76
and invar :: "'pq \<Rightarrow> bool"
nipkow@62706
    77
and mset :: "'pq \<Rightarrow> 'a multiset"
nipkow@62706
    78
assumes mset_empty: "mset empty = {#}"
nipkow@62706
    79
and mset_insert: "invar pq \<Longrightarrow> mset (insert x pq) = {#x#} + mset pq"
nipkow@62706
    80
and mset_del_min: "invar pq \<Longrightarrow> mset (del_min pq) = mset pq - {#get_min pq#}"
nipkow@62706
    81
and invar_insert: "invar pq \<Longrightarrow> invar (insert x pq)"
nipkow@62706
    82
and invar_del_min: "invar pq \<Longrightarrow> invar (del_min pq)"
nipkow@62706
    83
nipkow@62706
    84
nipkow@62706
    85
fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
nipkow@62706
    86
"mset_tree Leaf = {#}" |
nipkow@62706
    87
"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
nipkow@62706
    88
nipkow@62706
    89
nipkow@62706
    90
lemma mset_meld: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2"
nipkow@62706
    91
by (induction h1 h2 rule: meld.induct) (auto simp add: node_def ac_simps)
nipkow@62706
    92
nipkow@62706
    93
lemma mset_insert: "mset_tree (insert x t) = {#x#} + mset_tree t"
nipkow@62706
    94
by (auto simp add: insert_def mset_meld)
nipkow@62706
    95
nipkow@62706
    96
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
nipkow@62706
    97
by (cases h) (auto simp: mset_meld ac_simps subset_mset.diff_add_assoc)
nipkow@62706
    98
nipkow@62706
    99
nipkow@62706
   100
lemma lheap_meld: "\<lbrakk> lheap l; lheap r \<rbrakk> \<Longrightarrow> lheap (meld l r)"
nipkow@62706
   101
proof(induction l r rule: meld.induct)
nipkow@62706
   102
  case (3 n1 l1 a1 r1 n2 l2 a2 r2)
nipkow@62706
   103
  show ?case (is "lheap(meld ?t1 ?t2)")
nipkow@62706
   104
  proof cases
nipkow@62706
   105
    assume "a1 \<le> a2"
nipkow@62706
   106
    hence "lheap (meld ?t1 ?t2) = lheap (node l1 a1 (meld r1 ?t2))" by simp
nipkow@62706
   107
    also have "\<dots> = (lheap l1 \<and> lheap(meld r1 ?t2))"
nipkow@62706
   108
      by(simp add: lheap_node)
nipkow@62706
   109
    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
nipkow@62706
   110
    finally show ?thesis .
nipkow@62706
   111
  next (* analogous but automatic *)
nipkow@62706
   112
    assume "\<not> a1 \<le> a2"
nipkow@62706
   113
    thus ?thesis using 3 by(simp)(auto simp: lheap_node)
nipkow@62706
   114
  qed
nipkow@62706
   115
qed simp_all
nipkow@62706
   116
nipkow@62706
   117
lemma lheap_insert: "lheap t \<Longrightarrow> lheap(insert x t)"
nipkow@62706
   118
by(simp add: insert_def lheap_meld del: meld.simps split: tree.split)
nipkow@62706
   119
nipkow@62706
   120
lemma lheap_del_min: "lheap t \<Longrightarrow> lheap(del_min t)"
nipkow@62706
   121
by(cases t)(auto simp add: lheap_meld simp del: meld.simps)
nipkow@62706
   122
nipkow@62706
   123
nipkow@62706
   124
interpretation lheap: Priority_Queue
nipkow@62706
   125
where empty = Leaf and insert = insert and del_min = del_min
nipkow@62706
   126
and get_min = get_min and invar = lheap and mset = mset_tree
nipkow@62706
   127
proof(standard, goal_cases)
nipkow@62706
   128
  case 1 show ?case by simp
nipkow@62706
   129
next
nipkow@62706
   130
  case 2 show ?case by(rule mset_insert)
nipkow@62706
   131
next
nipkow@62706
   132
  case 3 show ?case by(rule mset_del_min)
nipkow@62706
   133
next
nipkow@62706
   134
  case 4 thus ?case by(rule lheap_insert)
nipkow@62706
   135
next
nipkow@62706
   136
  case 5 thus ?case by(rule lheap_del_min)
nipkow@62706
   137
qed
nipkow@62706
   138
nipkow@62706
   139
nipkow@62706
   140
subsection "Complexity"
nipkow@62706
   141
nipkow@62706
   142
lemma pow2_rank_size1: "lheap t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
nipkow@62706
   143
proof(induction t)
nipkow@62706
   144
  case Leaf show ?case by simp
nipkow@62706
   145
next
nipkow@62706
   146
  case (Node n l a r)
nipkow@62706
   147
  hence "rank r \<le> rank l" by simp
nipkow@62706
   148
  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
nipkow@62706
   149
  have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
nipkow@62706
   150
    by(simp add: mult_2)
nipkow@62706
   151
  also have "\<dots> \<le> size1 l + size1 r"
nipkow@62706
   152
    using Node * by (simp del: power_increasing_iff)
nipkow@62706
   153
  also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp
nipkow@62706
   154
  finally show ?case .
nipkow@62706
   155
qed
nipkow@62706
   156
nipkow@62706
   157
function t_meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
nipkow@62706
   158
"t_meld Leaf t2 = 1" |
nipkow@62706
   159
"t_meld t2 Leaf = 1" |
nipkow@62706
   160
"t_meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
nipkow@62706
   161
  (if a1 \<le> a2 then 1 + t_meld r1 (Node n2 l2 a2 r2)
nipkow@62706
   162
   else 1 + t_meld r2 (Node n1 l1 a1 r1))"
nipkow@62706
   163
by pat_completeness auto
nipkow@62706
   164
termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
nipkow@62706
   165
nipkow@62706
   166
definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
nipkow@62706
   167
"t_insert x t = t_meld (Node 1 Leaf x Leaf) t"
nipkow@62706
   168
nipkow@62706
   169
fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
nipkow@62706
   170
"t_del_min Leaf = 1" |
nipkow@62706
   171
"t_del_min (Node n l a r) = t_meld l r"
nipkow@62706
   172
nipkow@62706
   173
lemma t_meld_rank: "t_meld l r \<le> rank l + rank r + 1"
nipkow@62706
   174
proof(induction l r rule: meld.induct)
nipkow@62706
   175
  case 3 thus ?case
nipkow@62706
   176
    by(simp)(fastforce split: tree.splits simp del: t_meld.simps)
nipkow@62706
   177
qed simp_all
nipkow@62706
   178
nipkow@62706
   179
corollary t_meld_log: assumes "lheap l" "lheap r"
nipkow@62706
   180
  shows "t_meld l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
nipkow@62706
   181
using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
nipkow@62706
   182
  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_meld_rank[of l r]
nipkow@62706
   183
by linarith
nipkow@62706
   184
nipkow@62706
   185
corollary t_insert_log: "lheap t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
nipkow@62706
   186
using t_meld_log[of "Node 1 Leaf x Leaf" t]
nipkow@62706
   187
by(simp add: t_insert_def split: tree.split)
nipkow@62706
   188
nipkow@62706
   189
lemma ld_ld_1_less:
nipkow@62706
   190
  assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)"
nipkow@62706
   191
proof -
nipkow@62706
   192
  have 1: "2*x*y < (x+y)^2" using assms
nipkow@62706
   193
    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
nipkow@62706
   194
  show ?thesis
nipkow@62706
   195
    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
nipkow@62706
   196
     apply simp
nipkow@62706
   197
    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
nipkow@62706
   198
qed
nipkow@62706
   199
nipkow@62706
   200
corollary t_del_min_log: assumes "lheap t"
nipkow@62706
   201
  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
nipkow@62706
   202
proof(cases t)
nipkow@62706
   203
  case Leaf thus ?thesis using assms by simp
nipkow@62706
   204
next
nipkow@62706
   205
  case [simp]: (Node _ t1 _ t2)
nipkow@62706
   206
  have "t_del_min t = t_meld t1 t2" by simp
nipkow@62706
   207
  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
nipkow@62706
   208
    using \<open>lheap t\<close> by (auto simp: t_meld_log simp del: t_meld.simps)
nipkow@62706
   209
  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
nipkow@62706
   210
    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
nipkow@62706
   211
  finally show ?thesis .
nipkow@62706
   212
qed
nipkow@62706
   213
nipkow@62706
   214
end