Exercises/ex12/ex12.thy

.

theory ex12
imports Complex_Main
begin

subsection "Uebungsaufgabe"

text \<open>Consider locale \<open>Queue\<close> in file \<open>Thys/Amortized_Examples\<close>. A call of \<open>deq (xs,[])\<close>
requires the reversal of \<open>xs\<close>, which may be very long. We can reduce that impact
by shifting \<open>xs\<close> over to \<open>ys\<close> whenever \<open>length xs > length ys\<close>. This does not improve
the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity
of individual calls of \<open>deq\<close>. Modify local \<open>Queue\<close> as follows:\<close>

locale Queue
begin

type_synonym 'a queue = "'a list * 'a list"

fun balance :: "'a queue \<Rightarrow> 'a queue" where
"balance(xs,ys) = (if size xs \<le> size ys then (xs,ys) else ([], ys @ rev xs))"

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
"t_deq (xs,ys) = (if size xs \<le> size ys - 1 then 0 else size xs + (size ys - 1))"

end

text \<open>You will also have to modify \<open>invar\<close> and \<open>\<Phi>\<close>. In the end you should be able to prove
that the amortized complexity of \<open>enq\<close> is \<open> \<le> 3\<close> and of \<open>deq\<close> is \<open>= 0\<close>.\<close>

(* hide *)
context Queue
begin

definition "init = ([],[])"

fun invar where
"invar (xs,ys) = (size xs \<le> size ys)"

fun \<Phi> :: "'a queue \<Rightarrow> nat" where
"\<Phi> (xs,ys) = 2 * size xs"

lemma "\<Phi> t \<ge> 0"
apply(cases t)
apply(auto)
done

lemma "\<Phi> init = 0"
by(simp add: init_def)

lemma a_enq: "invar q \<Longrightarrow> t_enq a q + \<Phi>(enq a q) - \<Phi> q \<le> 3"
apply(cases q)
apply(auto)
done

lemma a_deq: "invar q \<Longrightarrow> t_deq q + \<Phi>(deq q) - \<Phi> q = 0"
apply(cases q)
apply(auto)
done

end
(* end hide *)

subsection "Homework"

type_synonym tab = "nat \<times> nat"

text \<open>In file \<open>Thys/Amortized_Examples\<close> in the repository there is a formalization
of dynamic tables in locale \<open>Dyn_Tab\<close> with the potential function \<open>\<Phi> (n,l) = 2*n - l\<close>
and a discussion of why this is tricky. The standard definition you find in textbooks
does not rely on cut-off subtraction on \<open>nat\<close> but uses standard real numbers:\<close>

fun \<Phi> :: "tab \<Rightarrow> real" where
"\<Phi> (n,l) = 2*(real n) - real l"

text \<open>Start with the locale \<open>Dyn_Tab\<close> in file \<open>Thys/Amortized_Examples\<close>
but use the above definition of \<open>\<Phi> :: tab \<Rightarrow> real\<close>. A number of proofs will now fail
because the invariant is now too weak.
Find a stronger invariant such that all the proofs work again.\<close>

(* hide *)
locale Dyn_Tab
begin

type_synonym tab = "nat \<times> nat"

fun invar :: "tab \<Rightarrow> bool" where
"invar (n,l) = (n=0 \<and> l = 0 \<or> l < 2*n \<and> n \<le> l)"

definition init :: tab where
"init = (0,0)"

text\<open>Insertion: the element does not matter\<close>
fun ins :: "tab \<Rightarrow> tab" where
"ins (n,l) = (n+1, if n<l then l else if l=0 then 1 else 2*l)"

text\<open>Time: if the table overflows, we count only the time for copying elements\<close>
fun t_ins :: "nat \<times> nat \<Rightarrow> nat" where
"t_ins (n,l) = (if n<l then 1 else n+1)"

lemma "invar init"
by(simp add: init_def)

lemma "invar t \<Longrightarrow> invar(ins t)"
apply(cases t)
apply(auto)
done

fun \<Phi> :: "tab \<Rightarrow> real" where
"\<Phi> (n,l) = 2*(real n) - real l"

lemma "invar t \<Longrightarrow> \<Phi> t \<ge> 0"
apply(cases t)
apply(auto)
done

lemma "\<Phi> init = 0"
by(simp add: init_def)

lemma a_ins: "invar t \<Longrightarrow> t_ins t + \<Phi>(ins t) - \<Phi> t \<le> 3"
apply(cases t)
apply(auto split: if_splits)
done

end
(* end hide *)

end