src/HOL/Data_Structures/Priority_Queue.thy
author nipkow
Mon Aug 14 22:06:26 2017 +0200 (23 months ago)
changeset 66419 8194ed7cf2cb
child 66425 8756322dc5de
permissions -rw-r--r--
separate file for priority queue interface; extended Leftist_Heap.
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
nipkow@66419
     6
imports "~~/src/HOL/Library/Multiset"
nipkow@66419
     7
begin
nipkow@66419
     8
nipkow@66419
     9
(* FIXME abbreviation? mv *)
nipkow@66419
    10
definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
nipkow@66419
    11
"Min_mset = Min o set_mset"
nipkow@66419
    12
nipkow@66419
    13
(* FIXME intros needed? *)
nipkow@66419
    14
nipkow@66419
    15
lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
nipkow@66419
    16
by (simp add: Min_mset_def)
nipkow@66419
    17
nipkow@66419
    18
lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
nipkow@66419
    19
by (simp add: Min_mset_def)
nipkow@66419
    20
    
nipkow@66419
    21
lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
nipkow@66419
    22
by (simp add: antisym)    
nipkow@66419
    23
nipkow@66419
    24
(* FIXME a bit special *)
nipkow@66419
    25
lemma eq_min_msetI[intro?]: 
nipkow@66419
    26
  "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"    
nipkow@66419
    27
using Min_mset_alt by blast
nipkow@66419
    28
    
nipkow@66419
    29
lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
nipkow@66419
    30
by (simp add: Min_mset_def)
nipkow@66419
    31
    
nipkow@66419
    32
lemma Min_mset_insert[simp]: 
nipkow@66419
    33
  "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
nipkow@66419
    34
by (simp add: Min_mset_def)
nipkow@66419
    35
nipkow@66419
    36
text \<open>Priority queue interface:\<close>
nipkow@66419
    37
    
nipkow@66419
    38
locale Priority_Queue =
nipkow@66419
    39
fixes empty :: "'q"
nipkow@66419
    40
and is_empty :: "'q \<Rightarrow> bool"
nipkow@66419
    41
and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
nipkow@66419
    42
and get_min :: "'q \<Rightarrow> 'a"
nipkow@66419
    43
and del_min :: "'q \<Rightarrow> 'q"
nipkow@66419
    44
and invar :: "'q \<Rightarrow> bool"
nipkow@66419
    45
and mset :: "'q \<Rightarrow> 'a multiset"
nipkow@66419
    46
assumes mset_empty: "mset empty = {#}"
nipkow@66419
    47
and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
nipkow@66419
    48
and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
nipkow@66419
    49
and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
nipkow@66419
    50
    mset (del_min q) = mset q - {# get_min q #}"
nipkow@66419
    51
and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
nipkow@66419
    52
and invar_empty: "invar empty"
nipkow@66419
    53
and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
nipkow@66419
    54
and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
nipkow@66419
    55
begin
nipkow@66419
    56
nipkow@66419
    57
(* FIXME why? *)
nipkow@66419
    58
nipkow@66419
    59
lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
nipkow@66419
    60
  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
nipkow@66419
    61
  by (simp add: mset_get_min)
nipkow@66419
    62
  
nipkow@66419
    63
lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
nipkow@66419
    64
lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
nipkow@66419
    65
nipkow@66419
    66
end
nipkow@66419
    67
nipkow@66419
    68
end