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 


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


29 


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


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


32 


33 
end


34 


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


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


37 


38 
(* hide *)


39 
context Queue


40 
begin


41 


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


43 


44 
fun invar where


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


46 


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


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


49 


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


51 
apply(cases t)


52 
apply(auto)


53 
done


54 


55 
lemma "\<Phi> init = 0"


56 
by(simp add: init_def)


57 


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


59 
apply(cases q)


60 
apply(auto)


61 
done


62 


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


64 
apply(cases q)


65 
apply(auto)


66 
done


67 


68 
end


69 
(* end hide *)


70 


71 
subsection "Homework"


72 


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


74 


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


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


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


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


79 


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


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


82 


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


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


85 
because the invariant is now too weak.


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


87 


88 
(* hide *)


89 
locale Dyn_Tab


90 
begin


91 


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


93 


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


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


96 


97 
definition init :: tab where


98 
"init = (0,0)"


99 


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


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


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


103 


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


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


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


107 


108 
lemma "invar init"


109 
by(simp add: init_def)


110 


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


112 
apply(cases t)


113 
apply(auto)


114 
done


115 


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


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


118 


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


120 
apply(cases t)


121 
apply(auto)


122 
done


123 


124 
lemma "\<Phi> init = 0"


125 
by(simp add: init_def)


126 


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


128 
apply(cases t)


129 
apply(auto split: if_splits)


130 
done


131 


132 
end


133 
(* end hide *)


134 


135 
end
