src/HOL/Data_Structures/Priority_Queue.thy
changeset 66565 ff561d9cb661
parent 66453 cc19f7ca2ed6
child 68020 6aade817bee5
     1.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Wed Aug 30 22:51:44 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Thu Aug 31 08:39:42 2017 +0200
     1.3 @@ -25,17 +25,12 @@
     1.4  and invar_empty: "invar empty"
     1.5  and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
     1.6  and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
     1.7 -begin
     1.8  
     1.9 -(* FIXME why? *)
    1.10 +text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
    1.11  
    1.12 -lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    1.13 -  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
    1.14 -  by (simp add: mset_get_min)
    1.15 -  
    1.16 -lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
    1.17 -lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
    1.18 +locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
    1.19 +fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
    1.20 +assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
    1.21 +and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
    1.22  
    1.23  end
    1.24 -
    1.25 -end