Exercises/ex12/ex12.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex12/ex12.thy	Fri Jul 07 21:00:57 2017 +0200
@@ -0,0 +1,135 @@
+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)"
+
+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