merged draft
authorlammich <lammich@in.tum.de>
Mon, 10 Jul 2017 13:49:39 +0200
changeset 69846 4bd3ade120e9
parent 69845 f7e66bb05be9 (current diff)
parent 69844 bec9aeaeb6c2 (diff)
child 69847 2510274a20a5
merged
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex12/ex12.thy	Mon Jul 10 13:49:39 2017 +0200
@@ -0,0 +1,137 @@
+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>Again, we count only the newly allocated list cells.\<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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex13/ex13.thy	Mon Jul 10 13:49:39 2017 +0200
@@ -0,0 +1,207 @@
+theory ex13
+imports "../../../Public/Thys/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
--- a/ROOT	Mon Jul 10 13:49:05 2017 +0200
+++ b/ROOT	Mon Jul 10 13:49:39 2017 +0200
@@ -9,6 +9,7 @@
     "../Public/Thys/Trie2"
     "../Public/Thys/Leftist_Heap"
     "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
+    "../Public/Thys/Skew_Heap_Analysis"
     "Slides/Tree_Notation"
     "../Public/Thys/BinHeap"
 
@@ -49,6 +50,7 @@
       , document_variants = "amor"]
   theories[show_question_marks=false]
     Amor_Slides
+    Skew_Heap_Slides
   document_files
     "root_amor.tex"
     "prelude.tex"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Skew_Heap_Slides.thy	Mon Jul 10 13:49:39 2017 +0200
@@ -0,0 +1,138 @@
+(*<*)
+theory Skew_Heap_Slides
+imports
+  Tree_Notation
+  "../../Public/Thys/Skew_Heap_Analysis"
+begin
+(*>*)
+text_raw{*
+\end{isabellebody}%
+%-------------------------------------------------------------
+\section{Skew Heap}
+%-------------------------------------------------------------
+\afpentry{Skew_Heap}
+%-------------------------------------------------------------
+\begin{frame}
+Note: \<open>merge\<close> is called @{const meld}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Implementation type}
+Ordinary binary trees
+\bigskip\pause
+
+Invariant: @{const heap}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{@{const meld}}
+Principle: swap subtrees when descending
+\pause
+\high{@{thm[display,margin=60] (sub) meld_code}}
+\pause
+Function @{const meld} terminates because \dots
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{@{const meld}}
+Very similar to leftist heaps but
+\begin{itemize}
+\pause
+\item
+subtrees are always swapped
+\pause
+\item
+\high{no size information needed}
+\end{itemize}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Functional correctness proofs}{including preservation of @{const heap}}
+Straightforward
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{\mbox{Logarithmic amortized complexity}}
+\begin{theorem}
+\high{@{thm[break,margin=60] (sub) a_meld}}
+\end{theorem}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Towards the proof}
+\pause
+@{thm rheavy.simps[of _ DUMMY]}
+\pause
+@{thm[display] lpath.simps}
+\pause
+@{thm G.simps}
+\bigskip\pause
+
+\begin{lemma}
+@{thm Gexp}
+\end{lemma}
+\pause
+\begin{corollary}
+@{thm Glog}
+\end{corollary}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Towards the proof}
+@{thm rheavy.simps[of _ DUMMY]}
+@{thm[display] rpath.simps}
+@{prop[source]"D h = length(filter (\<lambda>p. \<not> rheavy p) (rpath h))"}%@ {thm D.simps}
+\bigskip
+
+\begin{lemma}
+@{thm Dexp}
+\end{lemma}
+\begin{corollary}
+@{thm Dlog}
+\end{corollary}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Potential}
+\high{The potential is the number of \bad{@{const rheavy}} nodes:}
+\smallskip\pause
+
+@{thm (dummy_pats) \<Phi>.simps}
+\smallskip\pause
+
+@{const meld} descends on the right \<open>\<Longrightarrow>\<close> \bad{@{const rheavy}} nodes are \bad{bad}
+\bigskip\pause
+
+\begin{lemma}
+@{thm[break,margin=60] (sub) amor_le}
+\end{lemma}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Main proof}
+@{thm (lhs,sub) a_meld}\\\pause
+@{text"\<le>"} @{thm (rhs,sub) amor_le[of t1 t2]} % by Lemma
+\\\pause
+@{text"\<le>"} @{term (sub) "log 2 (size1(meld t1 t2))"} @{text"+"}
+  @{term (sub) "log 2 (size1 t1)"} @{text"+"} @{term (sub) "log 2 (size1 t2) + 1"}
+% by Corollaries
+\\\pause
+@{text"="} @{term (sub) "log 2 (size1 t1 + size1 t2 - 1)"} @{text"+"}
+  @{term (sub) "log 2 (size1 t1)"} @{text"+"} @{term (sub) "log 2 (size1 t2) + 1"}\\\pause
+% because @ {thm (sub) size_meld}
+@{text"\<le>"} @{term (sub) "log 2 (size1 t1 + size1 t2)"} @{text"+"}
+  @{term (sub) "log 2 (size1 t1)"} @{text"+"} @{term (sub) "log 2 (size1 t2) + 1"}\\\pause
+@{text"\<le>"} @{term (sub) "log 2 (size1 t1 + size1 t2)"} @{text"+"}
+  @{term (sub) "2 * log 2 (size1 t1 + size1 t2) + 1"}\\
+\mbox{}\hfill because @{thm (concl) plus_log_le_2log_plus[where b=2]} if \<open>x,y > 0\<close>\\\pause
+@{text"="} @{term (sub) "3 * log 2 (size1 t1 + size1 t2) + 1"}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{@{const Skew_Heap.insert} and @{const del_min}}
+\pause
+Easy consequences:
+\begin{lemma}
+\high{@{thm[break,margin=50] (sub) a_insert}}
+\end{lemma}
+\begin{lemma}
+\high{@{thm[break,margin=50] (sub) a_del_min}}
+\end{lemma}
+\end{frame}
+%-------------------------------------------------------------
+
+\begin{isabellebody}%
+*}
+(*<*)
+end
+(*>*)
--- a/Slides/document/main.tex	Mon Jul 10 13:49:05 2017 +0200
+++ b/Slides/document/main.tex	Mon Jul 10 13:49:39 2017 +0200
@@ -1,13 +1,5 @@
 \input{prelude}
 
-\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
-
-\renewcommand{\isadigit}[1]{\ensuremath{#1}}
-
-\newcommand{\afpentry}[1]
-{\filepage{Archive of Formal Proofs}
-{\url{https://www.isa-afp.org/entries/#1.shtml}}}
-
 \begin{document}
 
 \title{Functional Data Structures}
--- a/Slides/document/prelude.tex	Mon Jul 10 13:49:05 2017 +0200
+++ b/Slides/document/prelude.tex	Mon Jul 10 13:49:39 2017 +0200
@@ -28,6 +28,8 @@
 \let\isakeywordold=\isakeyword
 \renewcommand{\isakeyword}[1]{\isakeywordold{\def\_{{\texttt{\char`_}}}#1}}
 
+\renewcommand{\isadigit}[1]{\ensuremath{#1}}
+
 \renewcommand{\isacharbackquoteopen}{\isacharbackquote}
 \renewcommand{\isacharbackquoteclose}{\isacharbackquote}
 \renewcommand{\isasymnabla}{\raisebox{2pt}{\isamath{\normalbigtriangledown}}}
@@ -45,6 +47,8 @@
 \newcommand{\concept}[1]{\high{\emph{#1}}}
 \newcommand{\important}{{\Large \textbf{!}}}
 
+\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
+
 \newcommand{\filepage}[2]
 {\title{\textcolor{darkblue}{#1}}
 \author{#2}\institute{}\date{}
@@ -59,6 +63,10 @@
 \newcommand{\demofile}[2]
 {\thyfile{#1\char`\_Demo}{#2}}
 
+\newcommand{\afpentry}[1]
+{\filepage{Archive of Formal Proofs}
+{\url{https://www.isa-afp.org/entries/#1.shtml}}}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \setbeamersize{text margin left=0.5cm,text margin right=0.5cm}
 \renewcommand\partname{Chapter}
--- a/Slides/document/root_amor.tex	Mon Jul 10 13:49:05 2017 +0200
+++ b/Slides/document/root_amor.tex	Mon Jul 10 13:49:39 2017 +0200
@@ -4,12 +4,6 @@
 
 \input{prelude}
 
-\renewcommand{\isadigit}[1]{\ensuremath{#1}}
-
-\newcommand{\afpentry}[1]
-{\filepage{Archive of Formal Proofs}
-{\url{https://www.isa-afp.org/entries/#1.shtml}}}
-
 \begin{document}
 
 \part{Amortized Complexity}
--- a/Slides/document/root_partial.tex	Mon Jul 10 13:49:05 2017 +0200
+++ b/Slides/document/root_partial.tex	Mon Jul 10 13:49:39 2017 +0200
@@ -4,12 +4,6 @@
 
 \input{prelude}
 
-\renewcommand{\isadigit}[1]{\ensuremath{#1}}
-
-\newcommand{\afpentry}[1]
-{\filepage{Archive of Formal Proofs}
-{\url{https://www.isa-afp.org/entries/#1.shtml}}}
-
 \begin{document}
 
 \title{Functional Data Structures}