src/HOL/Data_Structures/Priority_Queue.thy
 author nipkow Tue Aug 15 09:29:35 2017 +0200 (23 months ago) changeset 66425 8756322dc5de parent 66419 8194ed7cf2cb child 66453 cc19f7ca2ed6 permissions -rw-r--r--
```     1 (* Author: Tobias Nipkow, Peter Lammich *)
```
```     2
```
```     3 section \<open>Priority Queue Interface\<close>
```
```     4
```
```     5 theory Priority_Queue
```
```     6 imports "~~/src/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 begin
```
```    29
```
```    30 (* FIXME why? *)
```
```    31
```
```    32 lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow>
```
```    33   get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
```
```    34   by (simp add: mset_get_min)
```
```    35
```
```    36 lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
```
```    37 lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
```
```    38
```
```    39 end
```
```    40
```
```    41 end
```