# HG changeset patch
# User nipkow
# Date 1504161582 -7200
# Node ID ff561d9cb661010bf16b39d97a9774f91287db13
# Parent  ad0cefe1e9a9cdfec1dab066a351c74a69cc6018
added PQ with merge

diff -r ad0cefe1e9a9 -r ff561d9cb661 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Aug 30 22:51:44 2017 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Aug 31 08:39:42 2017 +0200
@@ -386,35 +386,35 @@
 
 subsubsection \<open>Instantiating the Priority Queue Locale\<close>
 
-interpretation binheap: Priority_Queue
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
+
+interpretation binheap: Priority_Queue_Merge
   where empty = "[]" and is_empty = "op = []" and insert = insert
-  and get_min = get_min and del_min = del_min
+  and get_min = get_min and del_min = del_min and merge = merge
   and invar = invar and mset = mset_heap
 proof (unfold_locales, goal_cases)
-  case 1
-  then show ?case by simp
+  case 1 thus ?case by simp
 next
-  case (2 q)
-  then show ?case by auto
+  case 2 thus ?case by auto
 next
-  case (3 q x)
-  then show ?case by auto
+  case 3 thus ?case by auto
 next
   case (4 q)
-  then show ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
+  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
     by (auto simp: union_single_eq_diff)
 next
-  case (5 q)
-  then show ?case using get_min[of q] by auto
+  case (5 q) thus ?case using get_min[of q] by auto
 next 
-  case 6 
-  then show ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
+  case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
+next
+  case 7 thus ?case by simp
 next
-  case (7 q x)
-  then show ?case by simp
+  case 8 thus ?case by simp
 next
-  case (8 q)
-  then show ?case by simp
+  case 9 thus ?case by simp
+next
+  case 10 thus ?case by simp
 qed
 
 
diff -r ad0cefe1e9a9 -r ff561d9cb661 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Aug 30 22:51:44 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Aug 31 08:39:42 2017 +0200
@@ -136,12 +136,14 @@
 lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
 by(cases t)(auto simp add: heap_merge simp del: merge.simps)
 
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
 
-interpretation lheap: Priority_Queue
+interpretation lheap: Priority_Queue_Merge
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
 and insert = insert and del_min = del_min
-and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h"
-and mset = mset_tree
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
@@ -158,6 +160,10 @@
   case 7 thus ?case by(simp add: heap_insert ltree_insert)
 next
   case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
 qed
 
 
diff -r ad0cefe1e9a9 -r ff561d9cb661 src/HOL/Data_Structures/Priority_Queue.thy
--- a/src/HOL/Data_Structures/Priority_Queue.thy	Wed Aug 30 22:51:44 2017 +0100
+++ b/src/HOL/Data_Structures/Priority_Queue.thy	Thu Aug 31 08:39:42 2017 +0200
@@ -25,17 +25,12 @@
 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? *)
+text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
 
-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
+locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
+fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
+assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
+and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
 
 end
-
-end