Exercises/ex12/ex12.thy
changeset 69842 985eb3b647ab
parent 69841 d2283b15d2ca
child 69848 5a47947a89db
equal deleted inserted replaced
69841:d2283b15d2ca 69842:985eb3b647ab
    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