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

 ``` 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 \ :: "'s \ ('e \ 'a::linorder)" fixes invar :: "'s \ bool" locale uprio_finite = uprio + assumes finite_correct: "invar s \ finite (dom (\ s))" subsection "Basic Upriority Queue Functions" subsubsection "Empty Queue" locale uprio_empty = uprio + constrains \ :: "'s \ ('e \ 'a::linorder)" fixes empty :: "'s" assumes empty_correct: "invar empty" "\ empty = Map.empty" subsubsection "Emptiness Predicate" locale uprio_isEmpty = uprio + constrains \ :: "'s \ ('e \ 'a::linorder)" fixes isEmpty :: "'s \ bool" assumes isEmpty_correct: "invar s \ (isEmpty s) = (\ s = Map.empty)" subsubsection "Find and Remove Minimal Element" locale uprio_pop = uprio + constrains \ :: "'s \ ('e \ 'a::linorder)" fixes pop :: "'s \ ('e \ 'a \ 's)" assumes pop_correct: "\invar s; \ s \ Map.empty; pop s = (e,a,s')\ \ invar s' \ \ s' = (\ s)(e := None) \ (\ s) e = Some a \ (\y \ ran (\ s). a \ y)" begin lemma popE: assumes "invar s" "\ s \ Map.empty" obtains e a s' where "pop s = (e, a, s')" "invar s'" "\ s' = (\ s)(e := None)" "(\ s) e = Some a" "(\y \ ran (\ s). a \ 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 \ :: "'s \ ('e \ 'a::linorder)" fixes insert :: "'s \ 'e \ 'a \ 's" assumes insert_correct: "invar s \ invar (insert s e a)" "invar s \ \ (insert s e a) = (\ s)(e \ 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 \ :: "'s \ ('e \ 'a::linorder)" fixes insert :: "'s \ 'e \ 'a \ 's" assumes distinct_insert_correct: "\invar s; e \ dom (\ s)\ \ invar (insert s e a)" "\invar s; e \ dom (\ s)\ \ \ (insert s e a) = (\ s)(e \ a)" subsubsection "Looking up Priorities" locale uprio_prio = uprio + constrains \ :: "'s \ ('e \ 'a::linorder)" fixes prio :: "'s \ 'e \ 'a option" assumes prio_correct: "invar s \ prio s e = (\ s) e" subsection "Record Based Interface" record ('e, 'a, 's) uprio_ops = upr_\ :: "'s \ ('e \ 'a)" upr_invar :: "'s \ bool" upr_empty :: "'s" upr_isEmpty :: "'s \ bool" upr_insert :: "'s \ 'e \ 'a \ 's" upr_pop :: "'s \ ('e \ 'a \ 's)" upr_prio :: "'s \ 'e \ 'a option" locale StdUprioDefs = fixes ops :: "('e,'a::linorder,'s, 'more) uprio_ops_scheme" begin abbreviation \ where "\ == upr_\ 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 \ invar + uprio_empty \ invar empty + uprio_isEmpty \ invar isEmpty + uprio_insert \ invar insert + uprio_pop \ invar pop + uprio_prio \ invar prio for ops begin lemmas correct = finite_correct empty_correct isEmpty_correct insert_correct prio_correct end end ```