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

### 110 lines (94 with data), 4.1 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``` ```header {*\isaheader{Specification of Priority Queues}*} theory PrioSpec imports Main Multiset begin text {* We specify priority queues, that are abstracted to multisets of pairs of elements and priorities. *} locale prio = fixes \ :: "'p \ ('e \ 'a::linorder) multiset" -- "Abstraction to multiset" fixes invar :: "'p \ bool" -- "Invariant" subsection "Basic Priority Queue Functions" subsubsection "Empty Queue" locale prio_empty = prio + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes empty :: "'p" assumes empty_correct: "invar empty" "\ empty = {#}" subsubsection "Emptiness Predicate" locale prio_isEmpty = prio + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes isEmpty :: "'p \ bool" assumes isEmpty_correct: "invar p \ (isEmpty p) = (\ p = {#})" subsubsection "Find Minimal Element" locale prio_find = prio + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes find :: "'p \ ('e \ 'a::linorder)" assumes find_correct: "\invar p; \ p \ {#}\ \ (find p) \# (\ p) \ (\y \ set_of (\ p). snd (find p) \ snd y)" subsubsection "Insert" locale prio_insert = prio + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes insert :: "'e \ 'a \ 'p \ 'p" assumes insert_correct: "invar p \ invar (insert e a p)" "invar p \ \ (insert e a p) = (\ p) + {#(e,a)#}" subsubsection "Meld Two Queues" locale prio_meld = prio + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes meld :: "'p \ 'p \ 'p" assumes meld_correct: "\invar p; invar p'\ \ invar (meld p p')" "\invar p; invar p'\ \ \ (meld p p') = (\ p) + (\ p')" subsubsection "Delete Minimal Element" text {* Delete the same element that find will return *} locale prio_delete = prio_find + constrains \ :: "'p \ ('e \ 'a::linorder) multiset" fixes delete :: "'p \ 'p" assumes delete_correct: "\invar p; \ p \ {#}\ \ invar (delete p)" "\invar p; \ p \ {#}\ \ \ (delete p) = (\ p) - {# (find p) #}" subsection "Record based interface" record ('e, 'a, 'p) prio_ops = prio_op_\ :: "'p \ ('e \ 'a) multiset" prio_op_invar :: "'p \ bool" prio_op_empty :: "'p" prio_op_isEmpty :: "'p \ bool" prio_op_insert :: "'e \ 'a \ 'p \ 'p" prio_op_find :: "'p \ 'e \ 'a" prio_op_delete :: "'p \ 'p" prio_op_meld :: "'p \ 'p \ 'p" locale StdPrioDefs = fixes ops :: "('e,'a::linorder,'p) prio_ops" begin abbreviation \ where "\ == prio_op_\ ops" abbreviation invar where "invar == prio_op_invar ops" abbreviation empty where "empty == prio_op_empty ops" abbreviation isEmpty where "isEmpty == prio_op_isEmpty ops" abbreviation insert where "insert == prio_op_insert ops" abbreviation find where "find == prio_op_find ops" abbreviation delete where "delete == prio_op_delete ops" abbreviation meld where "meld == prio_op_meld ops" end locale StdPrio = StdPrioDefs ops + prio \ invar + prio_empty \ invar empty + prio_isEmpty \ invar isEmpty + prio_find \ invar find + prio_insert \ invar insert + prio_meld \ invar meld + prio_delete \ invar find delete for ops begin lemmas correct = empty_correct isEmpty_correct find_correct insert_correct meld_correct delete_correct end end ```