added PQ with merge
authornipkow
Thu Aug 31 08:39:42 2017 +0200 (22 months ago)
changeset 66565ff561d9cb661
parent 66562 ad0cefe1e9a9
child 66566 a14bbbaa628d
added PQ with merge
src/HOL/Data_Structures/Binomial_Heap.thy
src/HOL/Data_Structures/Leftist_Heap.thy
src/HOL/Data_Structures/Priority_Queue.thy
     1.1 --- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Aug 30 22:51:44 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Aug 31 08:39:42 2017 +0200
     1.3 @@ -386,35 +386,35 @@
     1.4  
     1.5  subsubsection \<open>Instantiating the Priority Queue Locale\<close>
     1.6  
     1.7 -interpretation binheap: Priority_Queue
     1.8 +text \<open>Last step of functional correctness proof: combine all the above lemmas
     1.9 +to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
    1.10 +
    1.11 +interpretation binheap: Priority_Queue_Merge
    1.12    where empty = "[]" and is_empty = "op = []" and insert = insert
    1.13 -  and get_min = get_min and del_min = del_min
    1.14 +  and get_min = get_min and del_min = del_min and merge = merge
    1.15    and invar = invar and mset = mset_heap
    1.16  proof (unfold_locales, goal_cases)
    1.17 -  case 1
    1.18 -  then show ?case by simp
    1.19 +  case 1 thus ?case by simp
    1.20  next
    1.21 -  case (2 q)
    1.22 -  then show ?case by auto
    1.23 +  case 2 thus ?case by auto
    1.24  next
    1.25 -  case (3 q x)
    1.26 -  then show ?case by auto
    1.27 +  case 3 thus ?case by auto
    1.28  next
    1.29    case (4 q)
    1.30 -  then show ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
    1.31 +  thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 
    1.32      by (auto simp: union_single_eq_diff)
    1.33  next
    1.34 -  case (5 q)
    1.35 -  then show ?case using get_min[of q] by auto
    1.36 +  case (5 q) thus ?case using get_min[of q] by auto
    1.37  next 
    1.38 -  case 6 
    1.39 -  then show ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
    1.40 +  case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
    1.41 +next
    1.42 +  case 7 thus ?case by simp
    1.43  next
    1.44 -  case (7 q x)
    1.45 -  then show ?case by simp
    1.46 +  case 8 thus ?case by simp
    1.47  next
    1.48 -  case (8 q)
    1.49 -  then show ?case by simp
    1.50 +  case 9 thus ?case by simp
    1.51 +next
    1.52 +  case 10 thus ?case by simp
    1.53  qed
    1.54  
    1.55  
     2.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Aug 30 22:51:44 2017 +0100
     2.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Aug 31 08:39:42 2017 +0200
     2.3 @@ -136,12 +136,14 @@
     2.4  lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
     2.5  by(cases t)(auto simp add: heap_merge simp del: merge.simps)
     2.6  
     2.7 +text \<open>Last step of functional correctness proof: combine all the above lemmas
     2.8 +to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
     2.9  
    2.10 -interpretation lheap: Priority_Queue
    2.11 +interpretation lheap: Priority_Queue_Merge
    2.12  where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
    2.13  and insert = insert and del_min = del_min
    2.14 -and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h"
    2.15 -and mset = mset_tree
    2.16 +and get_min = get_min and merge = merge
    2.17 +and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
    2.18  proof(standard, goal_cases)
    2.19    case 1 show ?case by simp
    2.20  next
    2.21 @@ -158,6 +160,10 @@
    2.22    case 7 thus ?case by(simp add: heap_insert ltree_insert)
    2.23  next
    2.24    case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
    2.25 +next
    2.26 +  case 9 thus ?case by (simp add: mset_merge)
    2.27 +next
    2.28 +  case 10 thus ?case by (simp add: heap_merge ltree_merge)
    2.29  qed
    2.30  
    2.31  
     3.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Wed Aug 30 22:51:44 2017 +0100
     3.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Thu Aug 31 08:39:42 2017 +0200
     3.3 @@ -25,17 +25,12 @@
     3.4  and invar_empty: "invar empty"
     3.5  and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
     3.6  and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
     3.7 -begin
     3.8  
     3.9 -(* FIXME why? *)
    3.10 +text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
    3.11  
    3.12 -lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    3.13 -  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
    3.14 -  by (simp add: mset_get_min)
    3.15 -  
    3.16 -lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
    3.17 -lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
    3.18 +locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
    3.19 +fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
    3.20 +assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
    3.21 +and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
    3.22  
    3.23  end
    3.24 -
    3.25 -end