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;
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@66419
    16
and del_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@66419
    22
and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
nipkow@66419
    23
    mset (del_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@66419
    27
and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
nipkow@66419
    28
begin
nipkow@66419
    29
nipkow@66419
    30
(* FIXME why? *)
nipkow@66419
    31
nipkow@66419
    32
lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
nipkow@66419
    33
  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
nipkow@66419
    34
  by (simp add: mset_get_min)
nipkow@66419
    35
  
nipkow@66419
    36
lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
nipkow@66419
    37
lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
nipkow@66419
    38
nipkow@66419
    39
end
nipkow@66419
    40
nipkow@66419
    41
end