ex13 draft
authornipkow
Sun, 09 Jul 2017 12:35:48 +0200
changeset 69843 028198aa6afc
parent 69842 985eb3b647ab
child 69844 bec9aeaeb6c2
ex13
Exercises/ex13/ex13.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex13/ex13.thy	Sun Jul 09 12:35:48 2017 +0200
@@ -0,0 +1,207 @@
+theory ex13
+imports "$AFP/Skew_Heap/Skew_Heap"
+begin
+
+subsection "Uebungsaufgabe"
+
+(* FIXME: Should there be a hint about function "abs" for the use in \<Phi>? *)
+
+text \<open>Design a double-ended queue where all operations have constant-time amortized
+complexity. Prove this.
+
+Explanation: A double-ended queue is like a queue with two further operations:
+Function \<open>enq_front\<close> adds an element at the front (whereas \<open>enq\<close> adds an element at the back).
+Function \<open>deq_back\<close> removes an element at the back (whereas \<open>deq\<close> removes an element at the front).
+Here is a formal specification where the double ended queue is just a list:
+\<close>
+
+fun enq_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_list x xs = xs @ [x]"
+
+fun enq_front_list :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"enq_front_list x xs = x # xs"
+
+fun deq_list :: "'a list \<Rightarrow> 'a list" where
+"deq_list xs = tl xs"
+
+fun deq_back_list :: "'a list \<Rightarrow> 'a list" where
+"deq_back_list xs = butlast xs"
+
+text\<open>
+Hint: You may want to start with the \<open>Queue\<close> implementation in \<open>Thys/Amortized_Examples\<close>.
+
+In a second step you should also prove correctness of your functions \<open>enq\<close>, \<open>enq_front\<close>, \<open>deq\<close>
+and \<open>deq_back\<close> w.r.t.\ the abstract specification above. You need to define an abstraction
+function \<open>list_of :: my_deque_type \<Rightarrow> 'a list\<close> and prove the standard homomorphism properties:\<close>
+
+lemma "list_of(enq x q) = enq_list x (list_of q)"
+sorry
+
+lemma "list_of(enq_front x q) = enq_front_list x (list_of q)"
+sorry
+
+lemma "list_of(deq q) = deq_list (list_of q)"
+sorry
+
+lemma "list_of(deq_back q) = deq_back_list (list_of q)"
+sorry
+
+(* hide *)
+type_synonym 'a queue = "'a list * 'a list"
+
+definition init :: "'a queue" where
+"init = ([],[])"
+
+fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+"enq x (xs,ys) = (x#xs, ys)"
+
+fun enq_front :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+"enq_front x (xs,ys) = (xs, x#ys)"
+
+fun deq :: "'a queue \<Rightarrow> 'a queue" where
+"deq (xs,ys) =
+  (if ys = []
+   then let n = length xs div 2
+        in (take n xs, tl(rev (drop n xs)))
+   else (xs, tl ys))"
+
+fun deq_back :: "'a queue \<Rightarrow> 'a queue" where
+"deq_back (xs,ys) =
+  (if xs = []
+   then let n = length ys div 2
+        in (tl(rev (drop n ys)), take n ys)
+   else (tl xs, ys))"
+
+text \<open>Time: we count only the number of newly allocated list cells.\<close>
+
+fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> int" where
+"t_enq x (xs,ys) = 1"
+
+fun t_enq_front :: "'a \<Rightarrow> 'a queue \<Rightarrow> int" where
+"t_enq_front x (xs,ys) = 1"
+
+text \<open>We assume that function \<open>rev\<close> has linear complexity.\<close>
+
+fun t_deq :: "'a queue \<Rightarrow> int" where
+"t_deq (xs,ys) =
+  (if ys = []
+   then let n = length xs div 2
+        in int(n + (length xs - n))
+   else 0)"
+
+fun t_deq_back :: "'a queue \<Rightarrow> int" where
+"t_deq_back (xs,ys) =
+  (if xs = []
+   then let n = length ys; m = n div 2
+        in int((length ys - n) + n)
+   else 0)"
+
+fun \<Phi> :: "'a queue \<Rightarrow> int" where
+"\<Phi> (xs,ys) = abs(int(length xs) - int(length ys))"
+
+lemma "\<Phi> q \<ge> 0"
+by(cases q) simp
+
+lemma "\<Phi> init = 0"
+by(simp add: init_def)
+
+lemma "t_enq x q + \<Phi>(enq x q) - \<Phi> q \<le> 2"
+by(cases q) auto
+
+lemma "t_enq_front x q + \<Phi>(enq_front x q) - \<Phi> q \<le> 2"
+by(cases q) auto
+
+lemma "t_deq q + \<Phi>(deq q) - \<Phi> q \<le> 2"
+by(cases q) (auto simp: Let_def)
+
+lemma "t_deq_back q + \<Phi>(deq_back q) - \<Phi> q \<le> 2"
+by(cases q) (auto simp: Let_def)
+
+fun list_of :: "'a queue \<Rightarrow> 'a list" where
+"list_of(xs,ys) = ys @ rev xs"
+
+lemma "list_of(enq x q) = enq_list x (list_of q)"
+by(cases q) auto
+
+lemma "list_of(enq_front x q) = enq_front_list x (list_of q)"
+by(cases q) auto
+
+lemma "list_of(deq q) = deq_list (list_of q)"
+proof (cases q)
+  case [simp]: (Pair xs ys)
+  show ?thesis
+  proof cases
+    let ?n = "length xs" let ?m = "?n - ?n div 2"
+    assume "ys = []"
+    then have "list_of (deq q) = tl (take ?m (rev xs)) @ drop ?m (rev xs)"
+      by(auto simp: Let_def rev_drop rev_take)
+    also have "\<dots> = tl (take ?m (rev xs) @ drop ?m (rev xs))"
+    proof (cases "take ?m (rev xs) = []")
+      case True thus ?thesis by(auto)
+    next
+      case False thus ?thesis by (metis tl_append2)
+    qed
+    also have "\<dots> = tl (rev xs)"
+      by simp
+    finally show ?thesis using \<open>ys = []\<close> by simp
+  next
+    assume "ys \<noteq> []"
+    thus ?thesis by(auto)
+  qed
+qed
+
+lemma rev_tl_butlast_rev: "rev (tl xs) = butlast(rev xs)"
+by (metis One_nat_def butlast_conv_take drop_0 drop_Suc drop_rev rev_swap)
+
+lemma "list_of(deq_back q) = deq_back_list (list_of q)"
+proof (cases q)
+  case [simp]: (Pair xs ys)
+  show ?thesis
+  proof cases
+    let ?n = "length ys div 2"
+    assume "xs = []"
+    then have "list_of (deq_back q) = take ?n ys @ drop ?n (butlast ys)"
+      by(simp add: Let_def rev_tl_butlast_rev butlast_drop)
+    also have "\<dots> = butlast (take ?n ys @ drop ?n ys)"
+    proof (cases "drop ?n ys = []")
+      case True thus ?thesis by(auto)
+    next
+      case False thus ?thesis by (metis butlast_append drop_butlast)
+    qed
+    also have "\<dots> = butlast ys"
+      by simp
+    finally show ?thesis using \<open>xs = []\<close> by simp
+  next
+    assume "xs \<noteq> []"
+    thus ?thesis by(auto simp: rev_tl_butlast_rev butlast_append)
+  qed
+qed
+(* end hide *)
+
+subsection "Homework"
+
+text \<open>Skew Heaps:
+Prove that inserting a list of elements \<open>xs\<close> one by one into the empty heap (\<open>Leaf\<close>)
+creates a skew heap of height at most \<open>length xs\<close>:\<close>
+
+lemma "height (fold Skew_Heap.insert xs Leaf) \<le> length xs"
+sorry
+
+text \<open>Function \<open>fold\<close> is predefined in the list library.
+
+Hint: prove something else first.\<close>
+
+(* hide *)
+lemma size_insert:  "size(Skew_Heap.insert x t) = size t + 1"
+by(simp add: Skew_Heap.insert_def)
+
+lemma size_fold_insert: "size(fold Skew_Heap.insert xs t) = size t + length xs"
+apply(induction xs arbitrary: t)
+apply(auto simp: size_insert)
+done
+
+lemma "height(fold Skew_Heap.insert xs Leaf) \<le> length xs"
+by (metis add.left_neutral height_le_size_tree size_fold_insert tree.size(3))
+(* end hide *)
+
+end