src/HOL/Data_Structures/Priority_Queue.thy
 author nipkow Sat Apr 21 11:13:35 2018 +0200 (15 months ago) changeset 68021 b91a043c0dcb parent 68020 6aade817bee5 permissions -rw-r--r--
dont rename PQ.del_min
```     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
```