(*<*) theory tut12 imports Complex_Main begin (*>*) text {* \ExerciseSheet{12}{14.~7.~2017} *} text \ \Exercise{Balanced Queues} Consider locale \Queue\ in file \Thys/Amortized_Examples\. A call of \deq (xs,[])\ requires the reversal of \xs\, which may be very long. We can reduce that impact by shifting \xs\ over to \ys\ whenever \length xs > length ys\. This does not improve the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity of individual calls of \deq\. Modify locale \Queue\ as follows:\ locale Queue begin type_synonym 'a queue = "'a list * 'a list" definition "init = ([],[])" fun balance :: "'a queue \ 'a queue" where "balance(xs,ys) = (if size xs \ size ys then (xs,ys) else ([], ys @ rev xs))" fun enq :: "'a \ 'a queue \ 'a queue" where "enq a (xs,ys) = balance (a#xs, ys)" fun deq :: "'a queue \ 'a queue" where "deq (xs,ys) = balance (xs, tl ys)" text \Again, we count only the newly allocated list cells.\ fun t_balance :: "'a queue \ nat" where "t_balance (xs,ys) = (if size xs \ size ys then 0 else size xs + size ys)" fun t_enq :: "'a \ 'a queue \ nat" where "t_enq a (xs,ys) = 1 + t_balance (a#xs, ys)" fun t_deq :: "'a queue \ nat" where "t_deq (xs,ys) = t_balance (xs, tl ys)" text \ \<^item> Start over with showing functional correctness. Hint: You will require an invariant. \ fun invar :: "'a queue \ bool" (*<*) where "invar (xs,ys) \ size xs \ size ys" (*>*) fun abs :: "'a queue \ 'a list" (*<*) where "abs (xs,ys) = xs@rev ys" (*>*) lemma [simp]: "invar init" by (simp add: init_def) lemma [simp]: "invar q \ invar (enq x q)" by (cases q) auto lemma [simp]: "invar q \ invar (deq q)" by (cases q) auto lemma [simp]: "abs init = []" by (auto simp: init_def) lemma [simp]: "invar q \ abs (enq x q) = x#abs q" by (cases q) auto lemma [simp]: "length a \ length b \ a @ rev (tl b) = butlast (a @ rev b)" apply (induction b) apply (auto simp: butlast_append) done lemma [simp]: "invar q \ abs (deq q) = butlast (abs q)" apply (cases q) apply auto done text \ \<^item> Next, define a suitable potential function \\\, and prove that the amortized complexity of \enq\ is \ \ 3\ and of \deq\ is \ \ 0\. \ fun \ :: "'a queue \ int" (*<*) where "\ (xs,ys) = 2*length xs" (*>*) lemma \_non_neg: "\ t \ 0" by (cases t) auto lemma \_init: "\ init = 0" unfolding init_def by auto lemma a_enq: " t_enq a q + \(enq a q) - \ q \ 3" by (cases q) auto lemma a_deq: " t_deq q + \(deq q) - \ q \ 0" by (cases q) auto text \Finally, show that a sequence of enqueue and dequeue operations requires linear cost in its length: \ (*<*) (* Establish abstraction boundary *) lemmas [simp del] = \.simps enq.simps deq.simps t_enq.simps t_deq.simps (*>*) datatype 'a opr = ENQ 'a | DEQ fun execute :: "'a queue \ 'a opr list \ 'a queue" where "execute q [] = q" | "execute q (ENQ x#ops) = execute (enq x q) ops" | "execute q (DEQ#ops) = execute (deq q) ops" text \Count only list cell allocations! \ fun t_execute :: "'a queue \ 'a opr list \ nat" where "t_execute q [] = 0" | "t_execute q (ENQ x#ops) = t_execute (enq x q) ops + t_enq x q" | "t_execute q (DEQ#ops) = t_execute (deq q) ops + t_deq q" lemma t_execute_aux: "t_execute q ops \ 3*length ops + \ q - \ (execute q ops)" proof (induction q ops rule: execute.induct) case (1 q) then show ?case by simp next case (2 q x ops) then show ?case using a_enq[of x q] by auto next case (3 q ops) then show ?case using a_deq[of q] by auto qed term init lemma t_execute: "t_execute init ops \ 3*length ops" using t_execute_aux[of init ops] \_non_neg[of "execute init ops"] by (auto simp: \_init) lemma "t_execute (init::'b queue) ops \ 3*length ops" using t_execute_aux[of init ops] \_non_neg[of "execute init ops"] \_init[where ?'a='b] by (auto) end (*<*) end (*>*)