src/HOL/Data_Structures/Priority_Queue.thy
author wenzelm
Fri Aug 18 20:47:47 2017 +0200 (23 months ago)
changeset 66453 cc19f7ca2ed6
parent 66425 8756322dc5de
child 66565 ff561d9cb661
permissions -rw-r--r--
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
     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 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