equal
deleted
inserted
replaced
22 "enq a (xs,ys) = balance (a#xs, ys)" |
22 "enq a (xs,ys) = balance (a#xs, ys)" |
23 |
23 |
24 fun deq :: "'a queue \<Rightarrow> 'a queue" where |
24 fun deq :: "'a queue \<Rightarrow> 'a queue" where |
25 "deq (xs,ys) = balance (xs, tl ys)" |
25 "deq (xs,ys) = balance (xs, tl ys)" |
26 |
26 |
27 text \<open>Note that we assume that the size computation in \<open>balance\<close> only takes constant time. |
27 text \<open>Again, we count only the newly allocated list cells.\<close> |
28 In reality the time is linear. How would you avoid that?\<close> |
|
29 |
28 |
30 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where |
29 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where |
31 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)" |
30 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)" |
32 |
31 |
33 fun t_deq :: "'a queue \<Rightarrow> nat" where |
32 fun t_deq :: "'a queue \<Rightarrow> nat" where |