# 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 \<open>Leftist Heap\<close>
 
 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 \<Longrightarrow> is_measure g \<Longrightarrow> is_measure (size_prod f g)"
+by (rule is_measure_trivial)
+
 fun mset_tree :: "('a,'b) tree \<Rightarrow> '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 \<Rightarrow> 'a" where
 "get_min(Node n l a r) = a"
 
-function merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
+fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "merge Leaf t2 = t2" |
 "merge t1 Leaf = t1" |
 "merge (Node n1 l1 a1 r1) (Node n2 l2 a2 r2) =
    (if a1 \<le> 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, _) \<Rightarrow> t2 |
@@ -66,8 +72,12 @@
 
 subsection "Lemmas"
 
+(* FIXME mv DS_Base *)
 declare Let_def [simp]
 
+lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
 lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> 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 \<Rightarrow> bool"
-and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
-and get_min :: "'q \<Rightarrow> 'a"
-and del_min :: "'q \<Rightarrow> 'q"
-and invar :: "'q \<Rightarrow> bool"
-and mset :: "'q \<Rightarrow> 'a multiset"
-assumes mset_empty: "mset empty = {#}"
-and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
-and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
-and mset_del_min: "invar q \<Longrightarrow> mset (del_min q) = mset q - {#get_min q#}"
-and get_min: "invar q \<Longrightarrow> q \<noteq> empty \<Longrightarrow>
-   get_min q \<in> set_mset(mset q) \<and> (\<forall>x \<in># mset q. get_min q \<le> x)"
-and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
-and invar_del_min: "invar q \<Longrightarrow> 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 \<Longrightarrow> h \<noteq> Leaf \<Longrightarrow>
-   get_min h \<in> set_mset(mset_tree h) \<and> (\<forall>x \<in># mset_tree h. get_min h \<le> x)"
-by (induction h) (auto)
+lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> 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 \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 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 \<le> 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 \<Rightarrow> 'a lheap \<Rightarrow> 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 "\<dots> < (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 \<open>Priority Queue Interface\<close>
+
+theory Priority_Queue
+imports "~~/src/HOL/Library/Multiset"
+begin
+
+(* FIXME abbreviation? mv *)
+definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
+"Min_mset = Min o set_mset"
+
+(* FIXME intros needed? *)
+
+lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
+by (simp add: Min_mset_def)
+
+lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
+by (simp add: Min_mset_def)
+    
+lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
+by (simp add: antisym)    
+
+(* FIXME a bit special *)
+lemma eq_min_msetI[intro?]: 
+  "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> 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\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
+by (simp add: Min_mset_def)
+
+text \<open>Priority queue interface:\<close>
+    
+locale Priority_Queue =
+fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
+and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'a"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> 'a multiset"
+assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
+    mset (del_min q) = mset q - {# get_min q #}"
+and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
+and invar_empty: "invar empty"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
+begin
+
+(* FIXME why? *)
+
+lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
+  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> 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