Exercises/ex12/ex12.thy
 changeset 69841 d2283b15d2ca parent 69840 0c9bba1e8e97 child 69842 985eb3b647ab
equal inserted replaced
69840:0c9bba1e8e97 69841:d2283b15d2ca
`    21 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where`
`    21 fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where`
`    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 `
`       `
`    27 text \<open>Note that we assume that the size computation in \<open>balance\<close> only takes constant time.`
`       `
`    28 In reality the time is linear. How would you avoid that?\<close>`
`    26 `
`    29 `
`    27 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where`
`    30 fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where`
`    28 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"`
`    31 "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"`
`    29 `
`    32 `
`    30 fun t_deq :: "'a queue \<Rightarrow> nat" where`
`    33 fun t_deq :: "'a queue \<Rightarrow> nat" where`