author | nipkow |
Sat, 21 Apr 2018 08:41:42 +0200 | |
changeset 68020 | 6aade817bee5 |
parent 66565 | ff561d9cb661 |
child 68021 | b91a043c0dcb |
permissions | -rw-r--r-- |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Peter Lammich *) |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
2 |
|
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
3 |
section \<open>Priority Queue Interface\<close> |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
4 |
|
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
5 |
theory Priority_Queue |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66425
diff
changeset
|
6 |
imports "HOL-Library.Multiset" |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
7 |
begin |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
8 |
|
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
9 |
text \<open>Priority queue interface:\<close> |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
10 |
|
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
11 |
locale Priority_Queue = |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
12 |
fixes empty :: "'q" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
13 |
and is_empty :: "'q \<Rightarrow> bool" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
14 |
and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
15 |
and get_min :: "'q \<Rightarrow> 'a" |
68020 | 16 |
and split_min :: "'q \<Rightarrow> 'q" |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
17 |
and invar :: "'q \<Rightarrow> bool" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
18 |
and mset :: "'q \<Rightarrow> 'a multiset" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
19 |
assumes mset_empty: "mset empty = {#}" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
20 |
and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
21 |
and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}" |
68020 | 22 |
and mset_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> |
23 |
mset (split_min q) = mset q - {# get_min q #}" |
|
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
24 |
and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
25 |
and invar_empty: "invar empty" |
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
26 |
and invar_insert: "invar q \<Longrightarrow> invar (insert x q)" |
68020 | 27 |
and invar_split_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (split_min q)" |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
28 |
|
66565 | 29 |
text \<open>Extend locale with \<open>merge\<close>. Need to enforce that \<open>'q\<close> is the same in both locales.\<close> |
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
30 |
|
66565 | 31 |
locale Priority_Queue_Merge = Priority_Queue where empty = empty for empty :: 'q + |
32 |
fixes merge :: "'q \<Rightarrow> 'q \<Rightarrow> 'q" |
|
33 |
assumes mset_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> mset (merge q1 q2) = mset q1 + mset q2" |
|
34 |
and invar_merge: "\<lbrakk> invar q1; invar q2 \<rbrakk> \<Longrightarrow> invar (merge q1 q2)" |
|
66419
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
35 |
|
8194ed7cf2cb
separate file for priority queue interface; extended Leftist_Heap.
nipkow
parents:
diff
changeset
|
36 |
end |