author nipkow Thu Mar 24 15:56:47 2016 +0100 (2016-03-24) changeset 62706 49c6a54ceab6 parent 62700 e3ca8dc01c4f child 62707 3f724ca245d0
 src/HOL/Data_Structures/Leftist_Heap.thy file | annotate | diff | revisions src/HOL/Data_Structures/document/root.bib file | annotate | diff | revisions src/HOL/Data_Structures/document/root.tex file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions
     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.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.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.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.197 +  show ?thesis
1.198 +    apply(rule powr_less_cancel_iff[of 2, THEN iffD1])
1.199 +     apply simp
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 +