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