69840

1 
theory ex12


2 
imports Complex_Main


3 
begin


4 


5 
subsection "Uebungsaufgabe"


6 


7 
text \<open>Consider locale \<open>Queue\<close> in file \<open>Thys/Amortized_Examples\<close>. A call of \<open>deq (xs,[])\<close>


8 
requires the reversal of \<open>xs\<close>, which may be very long. We can reduce that impact


9 
by shifting \<open>xs\<close> over to \<open>ys\<close> whenever \<open>length xs > length ys\<close>. This does not improve


10 
the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity


11 
of individual calls of \<open>deq\<close>. Modify local \<open>Queue\<close> as follows:\<close>


12 


13 
locale Queue


14 
begin


15 


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


17 


18 
fun balance :: "'a queue \<Rightarrow> 'a queue" where


19 
"balance(xs,ys) = (if size xs \<le> size ys then (xs,ys) else ([], ys @ rev xs))"


20 


21 
fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where


22 
"enq a (xs,ys) = balance (a#xs, ys)"


23 


24 
fun deq :: "'a queue \<Rightarrow> 'a queue" where


25 
"deq (xs,ys) = balance (xs, tl ys)"


26 

69841

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>


29 

69840

30 
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)"


32 


33 
fun t_deq :: "'a queue \<Rightarrow> nat" where


34 
"t_deq (xs,ys) = (if size xs \<le> size ys  1 then 0 else size xs + (size ys  1))"


35 


36 
end


37 


38 
text \<open>You will also have to modify \<open>invar\<close> and \<open>\<Phi>\<close>. In the end you should be able to prove


39 
that the amortized complexity of \<open>enq\<close> is \<open> \<le> 3\<close> and of \<open>deq\<close> is \<open>= 0\<close>.\<close>


40 


41 
(* hide *)


42 
context Queue


43 
begin


44 


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


46 


47 
fun invar where


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


49 


50 
fun \<Phi> :: "'a queue \<Rightarrow> nat" where


51 
"\<Phi> (xs,ys) = 2 * size xs"


52 


53 
lemma "\<Phi> t \<ge> 0"


54 
apply(cases t)


55 
apply(auto)


56 
done


57 


58 
lemma "\<Phi> init = 0"


59 
by(simp add: init_def)


60 


61 
lemma a_enq: "invar q \<Longrightarrow> t_enq a q + \<Phi>(enq a q)  \<Phi> q \<le> 3"


62 
apply(cases q)


63 
apply(auto)


64 
done


65 


66 
lemma a_deq: "invar q \<Longrightarrow> t_deq q + \<Phi>(deq q)  \<Phi> q = 0"


67 
apply(cases q)


68 
apply(auto)


69 
done


70 


71 
end


72 
(* end hide *)


73 


74 
subsection "Homework"


75 


76 
type_synonym tab = "nat \<times> nat"


77 


78 
text \<open>In file \<open>Thys/Amortized_Examples\<close> in the repository there is a formalization


79 
of dynamic tables in locale \<open>Dyn_Tab\<close> with the potential function \<open>\<Phi> (n,l) = 2*n  l\<close>


80 
and a discussion of why this is tricky. The standard definition you find in textbooks


81 
does not rely on cutoff subtraction on \<open>nat\<close> but uses standard real numbers:\<close>


82 


83 
fun \<Phi> :: "tab \<Rightarrow> real" where


84 
"\<Phi> (n,l) = 2*(real n)  real l"


85 


86 
text \<open>Start with the locale \<open>Dyn_Tab\<close> in file \<open>Thys/Amortized_Examples\<close>


87 
but use the above definition of \<open>\<Phi> :: tab \<Rightarrow> real\<close>. A number of proofs will now fail


88 
because the invariant is now too weak.


89 
Find a stronger invariant such that all the proofs work again.\<close>


90 


91 
(* hide *)


92 
locale Dyn_Tab


93 
begin


94 


95 
type_synonym tab = "nat \<times> nat"


96 


97 
fun invar :: "tab \<Rightarrow> bool" where


98 
"invar (n,l) = (n=0 \<and> l = 0 \<or> l < 2*n \<and> n \<le> l)"


99 


100 
definition init :: tab where


101 
"init = (0,0)"


102 


103 
text\<open>Insertion: the element does not matter\<close>


104 
fun ins :: "tab \<Rightarrow> tab" where


105 
"ins (n,l) = (n+1, if n<l then l else if l=0 then 1 else 2*l)"


106 


107 
text\<open>Time: if the table overflows, we count only the time for copying elements\<close>


108 
fun t_ins :: "nat \<times> nat \<Rightarrow> nat" where


109 
"t_ins (n,l) = (if n<l then 1 else n+1)"


110 


111 
lemma "invar init"


112 
by(simp add: init_def)


113 


114 
lemma "invar t \<Longrightarrow> invar(ins t)"


115 
apply(cases t)


116 
apply(auto)


117 
done


118 


119 
fun \<Phi> :: "tab \<Rightarrow> real" where


120 
"\<Phi> (n,l) = 2*(real n)  real l"


121 


122 
lemma "invar t \<Longrightarrow> \<Phi> t \<ge> 0"


123 
apply(cases t)


124 
apply(auto)


125 
done


126 


127 
lemma "\<Phi> init = 0"


128 
by(simp add: init_def)


129 


130 
lemma a_ins: "invar t \<Longrightarrow> t_ins t + \<Phi>(ins t)  \<Phi> t \<le> 3"


131 
apply(cases t)


132 
apply(auto split: if_splits)


133 
done


134 


135 
end


136 
(* end hide *)


137 


138 
end
