# HG changeset patch # User paulson # Date 1502743375 -3600 # Node ID df186e69b651fd267edd86840ecb25e88e2e13cb # Parent 8194ed7cf2cb9d267d7fca7d56f63de6b72ffa62# Parent 2891f33ed4c8331d3c7d72dd22731c674ba654cd merged diff -r 2891f33ed4c8 -r df186e69b651 src/HOL/Data_Structures/Leftist_Heap.thy --- a/src/HOL/Data_Structures/Leftist_Heap.thy Mon Aug 14 19:17:07 2017 +0100 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy Mon Aug 14 21:42:55 2017 +0100 @@ -3,9 +3,17 @@ section \Leftist Heap\ theory Leftist_Heap -imports Tree2 "~~/src/HOL/Library/Multiset" Complex_Main +imports + Tree2 + Priority_Queue + Complex_Main begin +(* FIXME mv Base *) +lemma size_prod_measure[measure_function]: + "is_measure f \ is_measure g \ is_measure (size_prod f g)" +by (rule is_measure_trivial) + fun mset_tree :: "('a,'b) tree \ 'a multiset" where "mset_tree Leaf = {#}" | "mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r" @@ -40,14 +48,12 @@ fun get_min :: "'a lheap \ 'a" where "get_min(Node n l a r) = a" -function merge :: "'a::ord lheap \ 'a lheap \ 'a lheap" where +fun merge :: "'a::ord lheap \ 'a lheap \ 'a lheap" where "merge Leaf t2 = t2" | "merge t1 Leaf = t1" | "merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) = (if a1 \ a2 then node l1 a1 (merge r1 (Node n2 l2 a2 r2)) else node l2 a2 (merge r2 (Node n1 l1 a1 r1)))" -by pat_completeness auto -termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto lemma merge_code: "merge t1 t2 = (case (t1,t2) of (Leaf, _) \ t2 | @@ -66,8 +72,12 @@ subsection "Lemmas" +(* FIXME mv DS_Base *) declare Let_def [simp] +lemma mset_tree_empty: "mset_tree t = {#} \ t = Leaf" +by(cases t) auto + lemma rk_eq_rank[simp]: "ltree t \ rk t = rank t" by(cases t) auto @@ -81,34 +91,14 @@ subsection "Functional Correctness" -locale Priority_Queue = -fixes empty :: "'q" -and is_empty :: "'q \ bool" -and insert :: "'a::linorder \ 'q \ 'q" -and get_min :: "'q \ 'a" -and del_min :: "'q \ 'q" -and invar :: "'q \ bool" -and mset :: "'q \ 'a multiset" -assumes mset_empty: "mset empty = {#}" -and is_empty: "invar q \ is_empty q = (mset q = {#})" -and mset_insert: "invar q \ mset (insert x q) = mset q + {#x#}" -and mset_del_min: "invar q \ mset (del_min q) = mset q - {#get_min q#}" -and get_min: "invar q \ q \ empty \ - get_min q \ set_mset(mset q) \ (\x \# mset q. get_min q \ x)" -and invar_insert: "invar q \ invar (insert x q)" -and invar_del_min: "invar q \ invar (del_min q)" - - lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2" by (induction h1 h2 rule: merge.induct) (auto simp add: node_def ac_simps) lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}" by (auto simp add: insert_def mset_merge) -lemma get_min: - "heap h \ h \ Leaf \ - get_min h \ set_mset(mset_tree h) \ (\x \# mset_tree h. get_min h \ x)" -by (induction h) (auto) +lemma get_min: "\ heap h; h \ Leaf \ \ get_min h = Min_mset (mset_tree h)" +by (induction h) (auto simp add:Min_mset_alt) lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}" by (cases h) (auto simp: mset_merge) @@ -162,11 +152,13 @@ next case 4 show ?case by(rule mset_del_min) next - case 5 thus ?case by(simp add: get_min) + case 5 thus ?case by(simp add: get_min mset_tree_empty) +next + case 6 thus ?case by(simp) next - case 6 thus ?case by(simp add: heap_insert ltree_insert) + case 7 thus ?case by(simp add: heap_insert ltree_insert) next - case 7 thus ?case by(simp add: heap_del_min ltree_del_min) + case 8 thus ?case by(simp add: heap_del_min ltree_del_min) qed @@ -187,14 +179,12 @@ finally show ?case . qed -function t_merge :: "'a::ord lheap \ 'a lheap \ nat" where +fun t_merge :: "'a::ord lheap \ 'a lheap \ nat" where "t_merge Leaf t2 = 1" | "t_merge t2 Leaf = 1" | "t_merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) = (if a1 \ a2 then 1 + t_merge r1 (Node n2 l2 a2 r2) else 1 + t_merge r2 (Node n1 l1 a1 r1))" -by pat_completeness auto -termination by (relation "measure (%(t1,t2). rank t1 + rank t2)") auto definition t_insert :: "'a::ord \ 'a lheap \ nat" where "t_insert x t = t_merge (Node 1 Leaf x Leaf) t" @@ -219,10 +209,11 @@ using t_merge_log[of "Node 1 Leaf x Leaf" t] by(simp add: t_insert_def split: tree.split) +(* FIXME mv Lemmas_log *) lemma ld_ld_1_less: - assumes "x > 0" "y > 0" shows "1 + log 2 x + log 2 y < 2 * log 2 (x+y)" + assumes "x > 0" "y > 0" shows "log 2 x + log 2 y + 1 < 2 * log 2 (x+y)" proof - - have "2 powr (1 + log 2 x + log 2 y) = 2*x*y" + have "2 powr (log 2 x + log 2 y + 1) = 2*x*y" using assms by(simp add: powr_add) also have "\ < (x+y)^2" using assms by(simp add: numeral_eq_Suc algebra_simps add_pos_pos) diff -r 2891f33ed4c8 -r df186e69b651 src/HOL/Data_Structures/Priority_Queue.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Data_Structures/Priority_Queue.thy Mon Aug 14 21:42:55 2017 +0100 @@ -0,0 +1,68 @@ +(* Author: Tobias Nipkow, Peter Lammich *) + +section \Priority Queue Interface\ + +theory Priority_Queue +imports "~~/src/HOL/Library/Multiset" +begin + +(* FIXME abbreviation? mv *) +definition Min_mset :: "'a::linorder multiset \ 'a" where +"Min_mset = Min o set_mset" + +(* FIXME intros needed? *) + +lemma Min_mset_contained[simp, intro]: "m\{#} \ Min_mset m \# m" +by (simp add: Min_mset_def) + +lemma Min_mset_min[simp, intro]: "x\# m \ Min_mset m \ x" +by (simp add: Min_mset_def) + +lemma Min_mset_alt: "m\{#} \ (x=Min_mset m) \ (x\#m \ (\y\#m. x\y))" +by (simp add: antisym) + +(* FIXME a bit special *) +lemma eq_min_msetI[intro?]: + "m\{#} \ (x\#m \ (\y\#m. x\y)) \ x=Min_mset m" +using Min_mset_alt by blast + +lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x" +by (simp add: Min_mset_def) + +lemma Min_mset_insert[simp]: + "m\{#} \ Min_mset (add_mset x m) = min x (Min_mset m)" +by (simp add: Min_mset_def) + +text \Priority queue interface:\ + +locale Priority_Queue = +fixes empty :: "'q" +and is_empty :: "'q \ bool" +and insert :: "'a::linorder \ 'q \ 'q" +and get_min :: "'q \ 'a" +and del_min :: "'q \ 'q" +and invar :: "'q \ bool" +and mset :: "'q \ 'a multiset" +assumes mset_empty: "mset empty = {#}" +and is_empty: "invar q \ is_empty q = (mset q = {#})" +and mset_insert: "invar q \ mset (insert x q) = mset q + {#x#}" +and mset_del_min: "invar q \ mset q \ {#} \ + mset (del_min q) = mset q - {# get_min q #}" +and mset_get_min: "invar q \ mset q \ {#} \ get_min q = Min_mset (mset q)" +and invar_empty: "invar empty" +and invar_insert: "invar q \ invar (insert x q)" +and invar_del_min: "invar q \ mset q \ {#} \ invar (del_min q)" +begin + +(* FIXME why? *) + +lemma get_min_alt: "invar q \ mset q \ {#} \ + get_min q \# mset q \ (\x\#mset q. get_min q \ x)" + by (simp add: mset_get_min) + +lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min +lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min + +end + +end