[7860bc]: thys / Collections / PrioUniqueSpec.thy  Maximize  Restore  History

Download this file

144 lines (123 with data), 5.0 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
header {*\isaheader{Specification of Unique Priority Queues}*}
theory PrioUniqueSpec
imports Main
begin
text {*
We define unique priority queues, where each element may occur at most once.
We provide operations to get and remove the element with the minimum priority,
as well as to access and change an elements priority (decrease-key operation).
Unique priority queues are abstracted to maps from elements to priorities.
*}
locale uprio =
fixes \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes invar :: "'s \<Rightarrow> bool"
locale uprio_finite = uprio +
assumes finite_correct:
"invar s \<Longrightarrow> finite (dom (\<alpha> s))"
subsection "Basic Upriority Queue Functions"
subsubsection "Empty Queue"
locale uprio_empty = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes empty :: "'s"
assumes empty_correct:
"invar empty"
"\<alpha> empty = Map.empty"
subsubsection "Emptiness Predicate"
locale uprio_isEmpty = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes isEmpty :: "'s \<Rightarrow> bool"
assumes isEmpty_correct:
"invar s \<Longrightarrow> (isEmpty s) = (\<alpha> s = Map.empty)"
subsubsection "Find and Remove Minimal Element"
locale uprio_pop = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes pop :: "'s \<Rightarrow> ('e \<times> 'a \<times> 's)"
assumes pop_correct:
"\<lbrakk>invar s; \<alpha> s \<noteq> Map.empty; pop s = (e,a,s')\<rbrakk> \<Longrightarrow>
invar s' \<and>
\<alpha> s' = (\<alpha> s)(e := None) \<and>
(\<alpha> s) e = Some a \<and>
(\<forall>y \<in> ran (\<alpha> s). a \<le> y)"
begin
lemma popE:
assumes
"invar s"
"\<alpha> s \<noteq> Map.empty"
obtains e a s' where
"pop s = (e, a, s')"
"invar s'"
"\<alpha> s' = (\<alpha> s)(e := None)"
"(\<alpha> s) e = Some a"
"(\<forall>y \<in> ran (\<alpha> s). a \<le> y)"
using assms
apply (cases "pop s")
apply (drule (2) pop_correct)
apply blast
done
end
subsubsection "Insert"
text {*
If an existing element is inserted, its priority will be overwritten.
This can be used to implement a decrease-key operation.
*}
(* TODO: Implement decrease-key generic algorithm, and specify decrease-key operation here! *)
locale uprio_insert = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes insert :: "'s \<Rightarrow> 'e \<Rightarrow> 'a \<Rightarrow> 's"
assumes insert_correct:
"invar s \<Longrightarrow> invar (insert s e a)"
"invar s \<Longrightarrow> \<alpha> (insert s e a) = (\<alpha> s)(e \<mapsto> a)"
subsubsection "Distinct Insert"
text {*
This operation only allows insertion of elements
that are not yet in the queue.
*}
locale uprio_distinct_insert = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes insert :: "'s \<Rightarrow> 'e \<Rightarrow> 'a \<Rightarrow> 's"
assumes distinct_insert_correct:
"\<lbrakk>invar s; e \<notin> dom (\<alpha> s)\<rbrakk> \<Longrightarrow> invar (insert s e a)"
"\<lbrakk>invar s; e \<notin> dom (\<alpha> s)\<rbrakk> \<Longrightarrow> \<alpha> (insert s e a) = (\<alpha> s)(e \<mapsto> a)"
subsubsection "Looking up Priorities"
locale uprio_prio = uprio +
constrains \<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a::linorder)"
fixes prio :: "'s \<Rightarrow> 'e \<Rightarrow> 'a option"
assumes prio_correct:
"invar s \<Longrightarrow> prio s e = (\<alpha> s) e"
subsection "Record Based Interface"
record ('e, 'a, 's) uprio_ops =
upr_\<alpha> :: "'s \<Rightarrow> ('e \<rightharpoonup> 'a)"
upr_invar :: "'s \<Rightarrow> bool"
upr_empty :: "'s"
upr_isEmpty :: "'s \<Rightarrow> bool"
upr_insert :: "'s \<Rightarrow> 'e \<Rightarrow> 'a \<Rightarrow> 's"
upr_pop :: "'s \<Rightarrow> ('e \<times> 'a \<times> 's)"
upr_prio :: "'s \<Rightarrow> 'e \<Rightarrow> 'a option"
locale StdUprioDefs =
fixes ops :: "('e,'a::linorder,'s, 'more) uprio_ops_scheme"
begin
abbreviation \<alpha> where "\<alpha> == upr_\<alpha> ops"
abbreviation invar where "invar == upr_invar ops"
abbreviation empty where "empty == upr_empty ops"
abbreviation isEmpty where "isEmpty == upr_isEmpty ops"
abbreviation insert where "insert == upr_insert ops"
abbreviation pop where "pop == upr_pop ops"
abbreviation prio where "prio == upr_prio ops"
end
locale StdUprio = StdUprioDefs ops +
uprio_finite \<alpha> invar +
uprio_empty \<alpha> invar empty +
uprio_isEmpty \<alpha> invar isEmpty +
uprio_insert \<alpha> invar insert +
uprio_pop \<alpha> invar pop +
uprio_prio \<alpha> invar prio
for ops
begin
lemmas correct =
finite_correct
empty_correct
isEmpty_correct
insert_correct
prio_correct
end
end