72389
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
section \<open>Queue Implementation via 2 Lists\<close>
|
|
4 |
|
|
5 |
theory Queue_2Lists
|
|
6 |
imports Queue_Spec
|
|
7 |
begin
|
|
8 |
|
|
9 |
text \<open>Definitions:\<close>
|
|
10 |
|
|
11 |
type_synonym 'a queue = "'a list \<times> 'a list"
|
|
12 |
|
|
13 |
fun norm :: "'a queue \<Rightarrow> 'a queue" where
|
|
14 |
"norm (os,is) = (if os = [] then (rev is, []) else (os,is))"
|
|
15 |
|
|
16 |
fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
|
|
17 |
"enq a (os,is) = norm(os, a # is)"
|
|
18 |
|
|
19 |
fun deq :: "'a queue \<Rightarrow> 'a queue" where
|
|
20 |
"deq (os,is) = (if os = [] then (os,is) else norm(tl os,is))"
|
|
21 |
|
|
22 |
fun front :: "'a queue \<Rightarrow> 'a" where
|
|
23 |
"front (a # os,is) = a"
|
|
24 |
|
|
25 |
fun is_empty :: "'a queue \<Rightarrow> bool" where
|
|
26 |
"is_empty (os,is) = (os = [])"
|
|
27 |
|
|
28 |
fun list :: "'a queue \<Rightarrow> 'a list" where
|
|
29 |
"list (os,is) = os @ rev is"
|
|
30 |
|
|
31 |
fun invar :: "'a queue \<Rightarrow> bool" where
|
|
32 |
"invar (os,is) = (os = [] \<longrightarrow> is = [])"
|
|
33 |
|
|
34 |
|
|
35 |
text \<open>Implementation correctness:\<close>
|
|
36 |
|
|
37 |
interpretation Queue
|
|
38 |
where empty = "([],[])" and enq = enq and deq = deq and front = front
|
|
39 |
and is_empty = is_empty and list = list and invar = invar
|
|
40 |
proof (standard, goal_cases)
|
|
41 |
case 1 show ?case by (simp)
|
|
42 |
next
|
|
43 |
case (2 q) thus ?case by(cases q) (simp)
|
|
44 |
next
|
|
45 |
case (3 q) thus ?case by(cases q) (simp)
|
|
46 |
next
|
|
47 |
case (4 q) thus ?case by(cases q) (auto simp: neq_Nil_conv)
|
|
48 |
next
|
|
49 |
case (5 q) thus ?case by(cases q) (auto)
|
|
50 |
next
|
|
51 |
case 6 show ?case by(simp)
|
|
52 |
next
|
|
53 |
case (7 q) thus ?case by(cases q) (simp)
|
|
54 |
next
|
|
55 |
case (8 q) thus ?case by(cases q) (simp)
|
|
56 |
qed
|
|
57 |
|
|
58 |
text \<open>Running times:\<close>
|
|
59 |
|
|
60 |
fun t_norm :: "'a queue \<Rightarrow> nat" where
|
|
61 |
"t_norm (os,is) = (if os = [] then length is else 0) + 1"
|
|
62 |
|
|
63 |
fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
|
|
64 |
"t_enq a (os,is) = t_norm(os, a # is)"
|
|
65 |
|
|
66 |
fun t_deq :: "'a queue \<Rightarrow> nat" where
|
|
67 |
"t_deq (os,is) = (if os = [] then 0 else t_norm(tl os,is)) + 1"
|
|
68 |
|
|
69 |
fun t_front :: "'a queue \<Rightarrow> nat" where
|
|
70 |
"t_front (a # os,is) = 1"
|
|
71 |
|
|
72 |
fun t_is_empty :: "'a queue \<Rightarrow> nat" where
|
|
73 |
"t_is_empty (os,is) = 1"
|
|
74 |
|
|
75 |
text \<open>Amortized running times:\<close>
|
|
76 |
|
|
77 |
fun \<Phi> :: "'a queue \<Rightarrow> nat" where
|
|
78 |
"\<Phi>(os,is) = length is"
|
|
79 |
|
|
80 |
lemma a_enq: "t_enq a (os,is) + \<Phi>(enq a (os,is)) - \<Phi>(os,is) \<le> 2"
|
|
81 |
by(auto)
|
|
82 |
|
|
83 |
lemma a_deq: "t_deq (os,is) + \<Phi>(deq (os,is)) - \<Phi>(os,is) \<le> 2"
|
|
84 |
by(auto)
|
|
85 |
|
|
86 |
end
|