added Leftist_Heap
authornipkow
Thu Mar 24 15:56:47 2016 +0100 (2016-03-24)
changeset 6270649c6a54ceab6
parent 62700 e3ca8dc01c4f
child 62707 3f724ca245d0
added Leftist_Heap
src/HOL/Data_Structures/Leftist_Heap.thy
src/HOL/Data_Structures/document/root.bib
src/HOL/Data_Structures/document/root.tex
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Mar 24 15:56:47 2016 +0100
     1.3 @@ -0,0 +1,214 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section \<open>Leftist Heap\<close>
     1.7 +
     1.8 +theory Leftist_Heap
     1.9 +imports Tree2 "~~/src/HOL/Library/Multiset" Complex_Main
    1.10 +begin
    1.11 +
    1.12 +type_synonym 'a lheap = "('a,nat)tree"
    1.13 +
    1.14 +fun rank :: "'a lheap \<Rightarrow> nat" where
    1.15 +"rank Leaf = 0" |
    1.16 +"rank (Node _ _ _ r) = rank r + 1"
    1.17 +
    1.18 +fun rk :: "'a lheap \<Rightarrow> nat" where
    1.19 +"rk Leaf = 0" |
    1.20 +"rk (Node n _ _ _) = n"
    1.21 +
    1.22 +text{* The invariant: *}
    1.23 +
    1.24 +fun lheap :: "'a lheap \<Rightarrow> bool" where
    1.25 +"lheap Leaf = True" |
    1.26 +"lheap (Node n l a r) =
    1.27 + (n = rank r + 1 \<and> rank l \<ge> rank r \<and> lheap l & lheap r)"
    1.28 +
    1.29 +definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.30 +"node l a r =
    1.31 + (let rl = rk l; rr = rk r
    1.32 +  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
    1.33 +
    1.34 +fun get_min :: "'a lheap \<Rightarrow> 'a" where
    1.35 +"get_min(Node n l a r) = a"
    1.36 +
    1.37 +function meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.38 +"meld Leaf t2 = t2" |
    1.39 +"meld t1 Leaf = t1" |
    1.40 +"meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
    1.41 +   (if a1 \<le> a2 then node l1 a1 (meld r1 (Node n2 l2 a2 r2))
    1.42 +    else node l2 a2 (meld r2 (Node n1 l1 a1 r1)))"
    1.43 +by pat_completeness auto
    1.44 +termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
    1.45 +
    1.46 +lemma meld_code: "meld t1 t2 = (case (t1,t2) of
    1.47 +  (Leaf, _) \<Rightarrow> t2 |
    1.48 +  (_, Leaf) \<Rightarrow> t1 |
    1.49 +  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
    1.50 +    if a1 \<le> a2 then node l1 a1 (meld r1 t2) else node l2 a2 (meld r2 t1))"
    1.51 +by(induction t1 t2 rule: meld.induct) (simp_all split: tree.split)
    1.52 +
    1.53 +definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.54 +"insert x t = meld (Node 1 Leaf x Leaf) t"
    1.55 +
    1.56 +fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
    1.57 +"del_min Leaf = Leaf" |
    1.58 +"del_min (Node n l x r) = meld l r"
    1.59 +
    1.60 +
    1.61 +subsection "Lemmas"
    1.62 +
    1.63 +declare Let_def [simp]
    1.64 +
    1.65 +lemma rk_eq_rank[simp]: "lheap t \<Longrightarrow> rk t = rank t"
    1.66 +by(cases t) auto
    1.67 +
    1.68 +lemma lheap_node: "lheap (node l a r) \<longleftrightarrow> lheap l \<and> lheap r"
    1.69 +by(auto simp add: node_def)
    1.70 +
    1.71 +
    1.72 +subsection "Functional Correctness"
    1.73 +
    1.74 +locale Priority_Queue =
    1.75 +fixes empty :: "'pq"
    1.76 +and insert :: "'a \<Rightarrow> 'pq \<Rightarrow> 'pq"
    1.77 +and get_min :: "'pq \<Rightarrow> 'a"
    1.78 +and del_min :: "'pq \<Rightarrow> 'pq"
    1.79 +and invar :: "'pq \<Rightarrow> bool"
    1.80 +and mset :: "'pq \<Rightarrow> 'a multiset"
    1.81 +assumes mset_empty: "mset empty = {#}"
    1.82 +and mset_insert: "invar pq \<Longrightarrow> mset (insert x pq) = {#x#} + mset pq"
    1.83 +and mset_del_min: "invar pq \<Longrightarrow> mset (del_min pq) = mset pq - {#get_min pq#}"
    1.84 +and invar_insert: "invar pq \<Longrightarrow> invar (insert x pq)"
    1.85 +and invar_del_min: "invar pq \<Longrightarrow> invar (del_min pq)"
    1.86 +
    1.87 +
    1.88 +fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
    1.89 +"mset_tree Leaf = {#}" |
    1.90 +"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
    1.91 +
    1.92 +
    1.93 +lemma mset_meld: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2"
    1.94 +by (induction h1 h2 rule: meld.induct) (auto simp add: node_def ac_simps)
    1.95 +
    1.96 +lemma mset_insert: "mset_tree (insert x t) = {#x#} + mset_tree t"
    1.97 +by (auto simp add: insert_def mset_meld)
    1.98 +
    1.99 +lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
   1.100 +by (cases h) (auto simp: mset_meld ac_simps subset_mset.diff_add_assoc)
   1.101 +
   1.102 +
   1.103 +lemma lheap_meld: "\<lbrakk> lheap l; lheap r \<rbrakk> \<Longrightarrow> lheap (meld l r)"
   1.104 +proof(induction l r rule: meld.induct)
   1.105 +  case (3 n1 l1 a1 r1 n2 l2 a2 r2)
   1.106 +  show ?case (is "lheap(meld ?t1 ?t2)")
   1.107 +  proof cases
   1.108 +    assume "a1 \<le> a2"
   1.109 +    hence "lheap (meld ?t1 ?t2) = lheap (node l1 a1 (meld r1 ?t2))" by simp
   1.110 +    also have "\<dots> = (lheap l1 \<and> lheap(meld r1 ?t2))"
   1.111 +      by(simp add: lheap_node)
   1.112 +    also have "..." using "3.prems" "3.IH"(1)[OF `a1 \<le> a2`] by (simp)
   1.113 +    finally show ?thesis .
   1.114 +  next (* analogous but automatic *)
   1.115 +    assume "\<not> a1 \<le> a2"
   1.116 +    thus ?thesis using 3 by(simp)(auto simp: lheap_node)
   1.117 +  qed
   1.118 +qed simp_all
   1.119 +
   1.120 +lemma lheap_insert: "lheap t \<Longrightarrow> lheap(insert x t)"
   1.121 +by(simp add: insert_def lheap_meld del: meld.simps split: tree.split)
   1.122 +
   1.123 +lemma lheap_del_min: "lheap t \<Longrightarrow> lheap(del_min t)"
   1.124 +by(cases t)(auto simp add: lheap_meld simp del: meld.simps)
   1.125 +
   1.126 +
   1.127 +interpretation lheap: Priority_Queue
   1.128 +where empty = Leaf and insert = insert and del_min = del_min
   1.129 +and get_min = get_min and invar = lheap and mset = mset_tree
   1.130 +proof(standard, goal_cases)
   1.131 +  case 1 show ?case by simp
   1.132 +next
   1.133 +  case 2 show ?case by(rule mset_insert)
   1.134 +next
   1.135 +  case 3 show ?case by(rule mset_del_min)
   1.136 +next
   1.137 +  case 4 thus ?case by(rule lheap_insert)
   1.138 +next
   1.139 +  case 5 thus ?case by(rule lheap_del_min)
   1.140 +qed
   1.141 +
   1.142 +
   1.143 +subsection "Complexity"
   1.144 +
   1.145 +lemma pow2_rank_size1: "lheap t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
   1.146 +proof(induction t)
   1.147 +  case Leaf show ?case by simp
   1.148 +next
   1.149 +  case (Node n l a r)
   1.150 +  hence "rank r \<le> rank l" by simp
   1.151 +  hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
   1.152 +  have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
   1.153 +    by(simp add: mult_2)
   1.154 +  also have "\<dots> \<le> size1 l + size1 r"
   1.155 +    using Node * by (simp del: power_increasing_iff)
   1.156 +  also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp
   1.157 +  finally show ?case .
   1.158 +qed
   1.159 +
   1.160 +function t_meld :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
   1.161 +"t_meld Leaf t2 = 1" |
   1.162 +"t_meld t2 Leaf = 1" |
   1.163 +"t_meld (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
   1.164 +  (if a1 \<le> a2 then 1 + t_meld r1 (Node n2 l2 a2 r2)
   1.165 +   else 1 + t_meld r2 (Node n1 l1 a1 r1))"
   1.166 +by pat_completeness auto
   1.167 +termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto
   1.168 +
   1.169 +definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
   1.170 +"t_insert x t = t_meld (Node 1 Leaf x Leaf) t"
   1.171 +
   1.172 +fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
   1.173 +"t_del_min Leaf = 1" |
   1.174 +"t_del_min (Node n l a r) = t_meld l r"
   1.175 +
   1.176 +lemma t_meld_rank: "t_meld l r \<le> rank l + rank r + 1"
   1.177 +proof(induction l r rule: meld.induct)
   1.178 +  case 3 thus ?case
   1.179 +    by(simp)(fastforce split: tree.splits simp del: t_meld.simps)
   1.180 +qed simp_all
   1.181 +
   1.182 +corollary t_meld_log: assumes "lheap l" "lheap r"
   1.183 +  shows "t_meld l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
   1.184 +using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
   1.185 +  le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_meld_rank[of l r]
   1.186 +by linarith
   1.187 +
   1.188 +corollary t_insert_log: "lheap t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
   1.189 +using t_meld_log[of "Node 1 Leaf x Leaf" t]
   1.190 +by(simp add: t_insert_def split: tree.split)
   1.191 +
   1.192 +lemma ld_ld_1_less:
   1.193 +  assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)"
   1.194 +proof -
   1.195 +  have 1: "2*x*y < (x+y)^2" using assms
   1.196 +    by(simp add: numeral_eq_Suc algebra_simps add_pos_pos)
   1.197 +  show ?thesis
   1.198 +    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
   1.199 +     apply simp
   1.200 +    using assms 1 by(simp add: powr_add log_powr[symmetric] powr_numeral)
   1.201 +qed
   1.202 +
   1.203 +corollary t_del_min_log: assumes "lheap t"
   1.204 +  shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
   1.205 +proof(cases t)
   1.206 +  case Leaf thus ?thesis using assms by simp
   1.207 +next
   1.208 +  case [simp]: (Node _ t1 _ t2)
   1.209 +  have "t_del_min t = t_meld t1 t2" by simp
   1.210 +  also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
   1.211 +    using \<open>lheap t\<close> by (auto simp: t_meld_log simp del: t_meld.simps)
   1.212 +  also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
   1.213 +    using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
   1.214 +  finally show ?thesis .
   1.215 +qed
   1.216 +
   1.217 +end
     2.1 --- a/src/HOL/Data_Structures/document/root.bib	Wed Mar 23 16:37:19 2016 +0100
     2.2 +++ b/src/HOL/Data_Structures/document/root.bib	Thu Mar 24 15:56:47 2016 +0100
     2.3 @@ -3,6 +3,10 @@
     2.4  booktitle={Algorithms and Data Structures (WADS '93)},
     2.5  series={LNCS},volume={709},publisher={Springer}}
     2.6  
     2.7 +@phdthesis{Crane72,author={Clark A. Crane},
     2.8 +title={Linear Lists and Prorty Queues as Balanced Binary Trees},
     2.9 +school={Computer Science Department, Stanford University},year=1972}
    2.10 +
    2.11  @article{Hinze-bro12,author={Ralf Hinze},
    2.12  title={Purely Functional 1-2 Brother Trees},
    2.13  journal={J. Functional Programming},
    2.14 @@ -23,6 +27,23 @@
    2.15  title={Automatic Functional Correctness Proofs for Functional Search Trees},
    2.16  year=2016,month=feb,note={\url{http://www.in.tum.de/~nipkow/pubs/trees.html}}}
    2.17  
    2.18 +@inproceedings{NunezPP95,
    2.19 +  author    = {Manuel N{\'{u}}{\~{n}}ez and
    2.20 +               Pedro Palao and
    2.21 +               Ricardo Pena},
    2.22 +  title     = {A Second Year Course on Data Structures Based on Functional Programming},
    2.23 +  booktitle = {Functional Programming Languages in Education},
    2.24 +  pages     = {65--84},
    2.25 +  year      = {1995},
    2.26 +  editor    = {Pieter H. Hartel and
    2.27 +               Marinus J. Plasmeijer},
    2.28 +  series    = {LNCS},
    2.29 +  volume    = {1022},
    2.30 +  publisher = {Springer},
    2.31 +  year      = {1995},
    2.32 +}
    2.33 +
    2.34 +
    2.35  @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
    2.36  publisher="Cambridge University Press",year=1998}
    2.37  
     3.1 --- a/src/HOL/Data_Structures/document/root.tex	Wed Mar 23 16:37:19 2016 +0100
     3.2 +++ b/src/HOL/Data_Structures/document/root.tex	Thu Mar 24 15:56:47 2016 +0100
     3.3 @@ -63,6 +63,10 @@
     3.4  They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
     3.5  Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
     3.6  
     3.7 +\paragraph{Leftist heaps}
     3.8 +They were invented by Crane \cite{Crane72}. A first functional implementation
     3.9 +is due to N\'u\~{n}ez \emph{et al.}~\cite{NunezPP95}.
    3.10 +
    3.11  \bibliographystyle{abbrv}
    3.12  \bibliography{root}
    3.13  
     4.1 --- a/src/HOL/ROOT	Wed Mar 23 16:37:19 2016 +0100
     4.2 +++ b/src/HOL/ROOT	Thu Mar 24 15:56:47 2016 +0100
     4.3 @@ -173,6 +173,7 @@
     4.4    options [document_variants = document]
     4.5    theories [document = false]
     4.6      "Less_False"
     4.7 +    "~~/src/HOL/Library/Multiset"
     4.8    theories
     4.9      Tree_Map
    4.10      AVL_Map
    4.11 @@ -182,6 +183,7 @@
    4.12      Brother12_Map
    4.13      AA_Map
    4.14      Splay_Map
    4.15 +    Leftist_Heap
    4.16    document_files "root.tex" "root.bib"
    4.17  
    4.18  session "HOL-Import" in Import = HOL +