src/HOL/Data_Structures/Priority_Queue.thy
changeset 68020 6aade817bee5
parent 66565 ff561d9cb661
child 68021 b91a043c0dcb
     1.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Fri Apr 20 22:22:46 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Sat Apr 21 08:41:42 2018 +0200
     1.3 @@ -13,18 +13,18 @@
     1.4  and is_empty :: "'q \<Rightarrow> bool"
     1.5  and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
     1.6  and get_min :: "'q \<Rightarrow> 'a"
     1.7 -and del_min :: "'q \<Rightarrow> 'q"
     1.8 +and split_min :: "'q \<Rightarrow> 'q"
     1.9  and invar :: "'q \<Rightarrow> bool"
    1.10  and mset :: "'q \<Rightarrow> 'a multiset"
    1.11  assumes mset_empty: "mset empty = {#}"
    1.12  and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
    1.13  and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
    1.14 -and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    1.15 -    mset (del_min q) = mset q - {# get_min q #}"
    1.16 +and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    1.17 +    mset (split_min q) = mset q - {# get_min q #}"
    1.18  and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
    1.19  and invar_empty: "invar empty"
    1.20  and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
    1.21 -and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
    1.22 +and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)"
    1.23  
    1.24  text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close>
    1.25