1(* Author: Tobias Nipkow, Peter Lammich *) 2 3section \<open>Priority Queue Specifications\<close> 4 5theory Priority_Queue_Specs 6imports "HOL-Library.Multiset" 7begin 8 9text \<open>Priority queue interface + specification:\<close> 10 11locale Priority_Queue = 12fixes empty :: "'q" 13and is_empty :: "'q \<Rightarrow> bool" 14and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q" 15and get_min :: "'q \<Rightarrow> 'a" 16and del_min :: "'q \<Rightarrow> 'q" 17and invar :: "'q \<Rightarrow> bool" 18and mset :: "'q \<Rightarrow> 'a multiset" 19assumes mset_empty: "mset empty = {#}" 20and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})" 21and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}" 22and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 23 mset (del_min q) = mset q - {# get_min q #}" 24and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)" 25and invar_empty: "invar empty" 26and invar_insert: "invar q \<Longrightarrow> invar (insert x q)" 27and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)" 28 29text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close> 30 31locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q + 32fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q" 33assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2" 34and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)" 35 36end 37