src/HOL/Data_Structures/Priority_Queue.thy
author nipkow
Sat Apr 21 08:41:42 2018 +0200 (14 months ago)
changeset 68020 6aade817bee5
parent 66565 ff561d9cb661
child 68021 b91a043c0dcb
permissions -rw-r--r--
del_min -> split_min
nipkow@66419
     1
(* Author: Tobias Nipkow, Peter Lammich *)
nipkow@66419
     2
nipkow@66419
     3
section \<open>Priority Queue Interface\<close>
nipkow@66419
     4
nipkow@66419
     5
theory Priority_Queue
wenzelm@66453
     6
imports "HOL-Library.Multiset"
nipkow@66419
     7
begin
nipkow@66419
     8
nipkow@66419
     9
text \<open>Priority queue interface:\<close>
nipkow@66419
    10
    
nipkow@66419
    11
locale Priority_Queue =
nipkow@66419
    12
fixes empty :: "'q"
nipkow@66419
    13
and is_empty :: "'q \<Rightarrow> bool"
nipkow@66419
    14
and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
nipkow@66419
    15
and get_min :: "'q \<Rightarrow> 'a"
nipkow@68020
    16
and split_min :: "'q \<Rightarrow> 'q"
nipkow@66419
    17
and invar :: "'q \<Rightarrow> bool"
nipkow@66419
    18
and mset :: "'q \<Rightarrow> 'a multiset"
nipkow@66419
    19
assumes mset_empty: "mset empty = {#}"
nipkow@66419
    20
and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
nipkow@66419
    21
and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
nipkow@68020
    22
and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
nipkow@68020
    23
    mset (split_min q) = mset q - {# get_min q #}"
nipkow@66419
    24
and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
nipkow@66419
    25
and invar_empty: "invar empty"
nipkow@66419
    26
and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
nipkow@68020
    27
and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
nipkow@66419
    28
nipkow@66565
    29
text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
nipkow@66419
    30
nipkow@66565
    31
locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q +
nipkow@66565
    32
fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q"
nipkow@66565
    33
assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2"
nipkow@66565
    34
and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)"
nipkow@66419
    35
nipkow@66419
    36
end