|
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 |