Exercises/ex12/ex12.thy

 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
 "enq a (xs,ys) = balance (a#xs, ys)"
 
 fun deq :: "'a queue \<Rightarrow> 'a queue" where
 "deq (xs,ys) = balance (xs, tl ys)"
+
+text \<open>Note that we assume that the size computation in \<open>balance\<close> only takes constant time.
+In reality the time is linear. How would you avoid that?\<close>
 
 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"
 
 fun t_deq :: "'a queue \<Rightarrow> nat" where