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
     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 split_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_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    23     mset (split_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_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_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