author nipkow Thu, 03 Aug 2017 09:42:58 +0200 changeset 69885 dbd3e3d7657d parent 69884 8f40f652e71e child 69889 cbd6b89c79e1
.
 Slides/Binomial_Tree_Slides.thy file | annotate | diff | comparison | revisions Slides/Braun_Tree_Slides.thy file | annotate | diff | comparison | revisions Slides/Leftist_Heap_Slides.thy file | annotate | diff | comparison | revisions Slides/RBT_Slides.thy file | annotate | diff | comparison | revisions Slides/Sorting_Slides.thy file | annotate | diff | comparison | revisions Slides/document/prelude.tex file | annotate | diff | comparison | revisions
--- a/Slides/Binomial_Tree_Slides.thy	Tue Aug 01 14:12:13 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy	Thu Aug 03 09:42:58 2017 +0200
@@ -23,23 +23,29 @@
%-------------------------------------------------------------
\section{Binomial Heaps}
%-------------------------------------------------------------
-\thyfile{Thys/BinHeap}{Binomial Heaps --- Correctness and Complexity}
+\ifMOD\else\thyfile{Thys/BinHeap}{Binomial Heaps --- Correctness and Complexity}\fi
%-------------------------------------------------------------
+\begin{frame}{Numerical method}
+Idea: only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
+\pause

-\begin{frame}{Numerical Method}{See \emph{Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1999}}
-  Only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
-  \smallskip\pause
+\begin{example}
+To store (in binary) \<open>11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
+\end{example}
+\pause

-  E.g., to store \<open>0b11001\<close> elements: \<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close>\\
-  \smallskip\pause
+Merge $\approx$ addition with carry
+\pause

-  Meld: Addition with carry. \\
-  \smallskip\pause
-  Linking two trees of size \<open>2\<^sup>i\<close>: Yields size \<open>2\<^sup>i\<^sup>+\<^sup>1\<close> \\
+Needs function to combine
+\begin{tabular}[t]{l}
+two trees of size \<open>2\<^sup>i\<close>\\
+into one tree of size \<open>2\<^sup>i\<^sup>+\<^sup>1\<close>
+\end{tabular}
\end{frame}
-
-\begin{frame}{Organization of Trees}
-  \high{@{theory_text \<open>(*<*)datatype (*>*)'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")\<close>}}\\
+%-------------------------------------------------------------
+\begin{frame}{Binomial trees}
+\high{@{theory_text \<open>datatype 'a tree = Node (rank: nat) (root: 'a) ("'a tree list")\<close>}}\\
\smallskip\pause

Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
@@ -50,7 +56,7 @@
Tree has exactly @{term \<open>(2::nat)^rank t\<close>} nodes
\high{@{thm [display] size_btree}}
\end{frame}
-
+%-------------------------------------------------------------
Given two trees of rank \<open>i\<close>, join them to tree of rank \<open>i+1\<close>.\\
\smallskip\pause
@@ -60,7 +66,7 @@

\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Heap Datatype}
Using sparse representation for binary numbers: \\
\<open>[t\<^sub>0,0,0,t\<^sub>3,t\<^sub>4]\<close> represented as \<open>[ (0,t\<^sub>0), (3,t\<^sub>3),(4,t\<^sub>4) ]\<close>
@@ -72,7 +78,7 @@
\high{@{thm bheap_invar_def}}\\
Ranks in \high{ascending} order\\
\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Inserting a Tree}
\high{@{thm [display, margin=60] ins_tree.simps}}
\smallskip\pause
@@ -83,7 +89,7 @@
Precondition:\\
Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Merge}
\high{@{thm [display] merge_simps}}
\smallskip\pause
@@ -93,7 +99,7 @@

Note: Handling of carry after recursive call
\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Find/Delete Minimum Element}
All trees are min-heaps
\smallskip\pause
@@ -111,7 +117,7 @@
Note the \<open>rev\<close>!

\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Complexity}
Recall: @{term \<open>size (mset_tree t) = 2^rank t\<close>}
\smallskip\pause
@@ -125,7 +131,7 @@

Proofs: \pause straightforward\pause ?
\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Complexity of Merge}
\high{@{thm [display] merge_simps(3)}}
\smallskip\pause
@@ -138,7 +144,7 @@

Yields (roughly) \<open>m n = m (n-2) + n\<close> \pause quadratic!
\end{frame}
-
+%-------------------------------------------------------------
\begin{frame}{Complexity of Merge}
\high{@{thm [display] merge_simps(3)}}
\smallskip\pause
--- a/Slides/Braun_Tree_Slides.thy	Tue Aug 01 14:12:13 2017 +0200
+++ b/Slides/Braun_Tree_Slides.thy	Thu Aug 03 09:42:58 2017 +0200
@@ -4,8 +4,31 @@
Tree_Notation
"$AFP/Priority_Queue_Braun/Priority_Queue_Braun" begin + +fun sm :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> bool" where +"sm Leaf Leaf = True" | +"sm (Node l _ r) (Node l' _ r') = (sm l l' \<and> sm r r')" | +"sm _ _ = False" + +lemma "braun t \<Longrightarrow> braun t' \<Longrightarrow> size t = size t' \<Longrightarrow> sm t t'" +apply(induction t arbitrary: t') + apply (simp add: size_0_iff_Leaf) +apply(case_tac t') + apply simp +apply auto +done + notation (output) insert_pq ("insert") +(* FIXME +1 in AFP source *) +lemma braun_simp2: "braun (Node l x r) = (size r \<le> size l \<and> size l \<le> size r + 1 \<and> braun l \<and> braun r)" +by simp +lemmas braun_simps = braun.simps(1) braun_simp2 + +lemma del_left_simp2: + "l \<noteq> Leaf \<Longrightarrow> del_left (Node l x r) = (let (y,l') = del_left l in (y,Node r x l'))" +by (auto simp: neq_Leaf_iff) + lemma del_min_simp3: "l \<noteq> Leaf \<Longrightarrow> del_min (Node l x r) = (let (y,l') = del_left l in sift_down r y l')" by(auto simp: neq_Leaf_iff) @@ -18,29 +41,58 @@ %------------------------------------------------------------- \afpentry{Priority_Queue_Braun} %------------------------------------------------------------- +\ifMOD +\begin{frame} +Based on code from\smallskip\\ +L.C. Paulson. \emph{ML for the Working Programmer}. 1996 +\smallskip\pause + +based on code from Chris Okasaki. +\end{frame} +\fi +%------------------------------------------------------------- +\tikzset{hide on/.code={\only<#1>{\color{white}}}} \begin{frame}{What is a Braun tree?} @{const_typ braun}\\\smallskip\pause -\high{@{thm[break,margin=60] braun.simps}}\\ -\bigskip\pause +\high{@{thm[break,margin=60] braun_simps}}\\ +\pause +\begin{center} +\begin{tikzpicture} + [thick,level 1/.style={sibling distance=20mm},level 2/.style={sibling distance=10mm}] + \node {1} + child[hide on=-3] {node {2} + child[hide on=-5] {node {4}} + child[hide on=-7] {node {6}} + } + child[hide on=-4] {node {3} + child[hide on=-6] {node {5}} + child[hide on=-8] {node {7}} + }; +\end{tikzpicture} +\end{center} +\onslide<10> \textbf{Lemma} \high{@{thm height_size_braun}} \end{frame} %------------------------------------------------------------- -\begin{frame}{Idea of Invariant Maintenance} -\high{@{thm[break,margin=60] braun.simps}} +\begin{frame}{Idea of invariant maintenance} +\high{@{thm[break,margin=60] braun_simps}} \bigskip\pause -Add element: \pause to right subtree, then swap subtrees\\ \pause - {\bf Goal}: @{term "size l \<le> size r + 1 \<and> size r + 1 \<le> size l + 1"} \pause\qed - +Add element: \pause to right subtree, then swap subtrees\\ +\ifMOD\else\pause +\textbf{Goal}: @{prop "size (l::'a tree) \<le> size (r::'a tree) + 1 \<and> size r + 1 \<le> size l + 1"} \pause\qed +\fi \bigskip\pause -Remove element: \pause from left subtree, then swap subtrees\\ \pause - {\bf Goal}: @{term "size l - 1 \<le> size r \<and> size r \<le> size l"} \pause\qed +Remove element: \pause from left subtree, then swap subtrees\\ +\ifMOD\else\pause +\textbf{Goal}: @{prop "size (l::'a tree) - 1 \<le> size (r::'a tree) \<and> size r \<le> size l"} \pause\qed +\fi \end{frame} %------------------------------------------------------------- \begin{frame}{Priority queue implementation} -Implementation type: ordinary binary trees +Implementation type: @{typ "'a tree"} \bigskip\pause Invariants: @{const heap} and @{const braun} @@ -63,30 +115,44 @@ @{const_typ del_min}\\\smallskip\pause \high{@{thm [break,margin=60] (concl) del_min_simps}} \bigskip\pause - -Idea: Delete leftmost element$y$, put it at top, and sift it down - to adequate position. +\begin{enumerate} +\item Delete leftmost element$y$+\item Sift$y$from the root down +\end{enumerate} \end{frame} %------------------------------------------------------------- \begin{frame}{@{const del_left}} \high<1>{@{const_typ del_left}}\\\smallskip\pause -\high<2>{@{thm [break,margin=60] (sub) del_left.simps(1)}}\\\smallskip\pause -\high<3>{@{thm [break,margin=60] (sub) del_left.simps(2)}} +\high<2>{@{thm [break,margin=60] del_left.simps(1)}}\\\smallskip\pause +\high<3>{@{thm [break,margin=60] (concl) del_left_simp2}} \end{frame} %------------------------------------------------------------- \begin{frame}{@{const sift_down}} \high<1>{@{const_typ sift_down}}\\\smallskip\pause +\ifMOD +\high<2-3>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\ +\high<2-3>{\<open>=\<close>}\\\pause +\high<3>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2 + then Node t1 a t2 + else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2 + else Node t1 x2 (sift_down l2 a r2))"}} +\else \high<2>{@{thm [break,margin=60] (sub) sift_down.simps(1)}}\\\smallskip\pause \high<3>{@{thm [break,margin=60] (sub) sift_down.simps(2)}}\\\smallskip\pause -\high<4>{@{thm [break,margin=60] (sub) sift_down.simps(3)}} +%\high<4>{@ {thm [break,margin=60] (sub) sift_down.simps(3)}} +\high<4-5>{@{text "sift_down (t\<^sub>1 = (Node l\<^sub>1 x\<^sub>1 r\<^sub>1)) a (t\<^sub>2 = (Node l\<^sub>2 x\<^sub>2 r\<^sub>2))"}}\\ +\high<4-5>{\<open>=\<close>}\\\pause +\high<5>{@{term[break,margin=60] (sub) "(if a \<le> x1 \<and> a \<le> x2 + then Node t1 a t2 + else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2 + else Node t1 x2 (sift_down l2 a r2))"}} \bigskip\pause -Maintenance of @{const braun}: Preserves structure of tree. +Maintains @{const braun} +\fi \end{frame} - - %------------------------------------------------------------- -\begin{frame}{Functional correctness proofs for deletion} +\begin{frame}{Functional correctness proofs for @{const del_min}} Many lemmas, mostly straightforward \end{frame} %------------------------------------------------------------- @@ -104,6 +170,7 @@ Above running times logarithmic in size \end{frame} %------------------------------------------------------------- +\ifMOD\else \begin{frame}[t]{Sorting with priority queue} \pause @@ -123,7 +190,7 @@ %Braun trees$\leadsto$functional version of heap sort \end{frame} - +\fi %%------------------------------------------------------------- %\begin{frame}[t]{Sorting with priority queue} % --- a/Slides/Leftist_Heap_Slides.thy Tue Aug 01 14:12:13 2017 +0200 +++ b/Slides/Leftist_Heap_Slides.thy Thu Aug 03 09:42:58 2017 +0200 @@ -14,6 +14,25 @@ \end{isabellebody}% \section{Priority Queues} %------------------------------------------------------------- +\ifMOD +\begin{frame}{Priority queue informally} +\begin{center} +Collection of elements with priorities +\bigskip\pause + +We focus on the priorities:\\ +\high{element = priority} +\bigskip\pause + +The same element can be contained \high{multiple times}\\ in a priority queue +\pause + +$\Longrightarrow$+ +The abstract view of a priority queue is a \high{multiset} +\end{center} +\end{frame} +\else \begin{frame}{Priority queue informally} \begin{center} Collection of elements with priorities @@ -49,11 +68,7 @@ The abstract view of a priority queue is a \high{multiset} \end{center} \end{frame} -%------------------------------------------------------------- -\begin{frame}{Multisets in Isabelle} - -Import \texttt{"Library/Multiset"} -\end{frame} +\fi %------------------------------------------------------------- *} text_raw (in Priority_Queue) {* @@ -68,15 +83,15 @@ \pause \item An implementation type \ \high{@{typ 'q}} \pause -\item \high{\<open>empty ::\<close> @{typ 'q}} +\item<-8> \high{\<open>empty ::\<close> @{typ 'q}} \pause -\item \high{\<open>is_empty ::\<close> @{typ "'q \<Rightarrow> bool"}} +\item<-8> \high{\<open>is_empty ::\<close> @{typ "'q \<Rightarrow> bool"}} \pause -\item \high{\<open>insert ::\<close> @{typ"'a \<Rightarrow> 'q \<Rightarrow> 'q"}} +\item<-9> \high{\<open>insert ::\<close> @{typ"'a \<Rightarrow> 'q \<Rightarrow> 'q"}} \pause -\item \high{\<open>get_min ::\<close> @{typ"'q \<Rightarrow> 'a"}} +\item<-8> \high{\<open>get_min ::\<close> @{typ"'q \<Rightarrow> 'a"}} \pause -\item \high{\<open>del_min ::\<close> @{typ"'q \<Rightarrow> 'q"}} +\item<-9> \high{\high{\<open>del_min ::\<close> @{typ"'q \<Rightarrow> 'q"}}} \end{itemize} \end{frame} %------------------------------------------------------------- @@ -103,25 +118,29 @@ \end{frame} %------------------------------------------------------------- \begin{frame}{Correctness of implementation} -Must prove \ \high{@{prop"invar q"}} \<open>\<Longrightarrow>\<close>\medskip +Must prove \ \high{@{prop"invar q"} \<open>\<Longrightarrow>\<close>}\medskip \pause +\ifMOD\else \high{@{thm mset_empty}}\smallskip\\\pause \high{@{thm (concl) is_empty}}\smallskip\\\pause -\high{@{thm (concl) mset_insert}}\medskip\\\pause -\high{@{thm (prem 2) get_min} \<open>\<Longrightarrow>\<close>}\\ -\high{@{thm (concl) mset_del_min}}\smallskip\\\pause -\high{@{thm (concl) mset_get_min}}\\ +\fi +\high{@{thm (concl) mset_insert}}\smallskip\\\pause +\ifMOD\else +\high{@{thm (prem 2) mset_get_min} \<open>\<Longrightarrow>\<close> @{thm (concl) mset_get_min}}\smallskip\\\pause +\fi +\high{@{thm (prem 2) mset_del_min} \<open>\<Longrightarrow>\<close>}\\ +\high{@{thm (concl) mset_del_min}}\\ \bigskip\pause -\high{@{thm (concl) invar_empty}}\\ +\ifMOD\else\high{@{thm (concl) invar_empty}}\\\fi \high{@{thm (concl) invar_insert}}\\ \high{@{thm (concl) invar_del_min}} \end{frame} %------------------------------------------------------------- \begin{frame}{Terminology} \begin{center} -A tree is a \high{heap} if for every subtree\\ -the root is$\le$all elements in the subtrees. +A tree is a \concept{heap} if for every subtree\\ +the root is$\le$all elements in that subtree. \end{center} \pause @@ -130,10 +149,12 @@ %------------------------------------------------------------- \begin{frame}{Priority queue via heap} \begin{itemize} +\ifMOD\else \pause \item \<open>empty = \<langle>\<rangle>\<close> \pause \item \<open>is_empty h = (h = \<langle>\<rangle>)\<close> +\fi \pause \item \<open>get_min \<langle>_, a, _\<rangle> = a\<close> \pause @@ -145,6 +166,7 @@ \end{itemize} \end{frame} %------------------------------------------------------------- +\ifMOD\else \begin{frame}{Priority queue via heap} A naive merge: \medskip\pause @@ -159,26 +181,27 @@ \bad{Challenge:} how to maintain some kind of balance \end{frame} +\fi %------------------------------------------------------------- *} text_raw {* %------------------------------------------------------------- \section{Leftist Heap} %------------------------------------------------------------- -\thyfile{Leftist\char_Heap}{} +\ifMOD\else\thyfile{Thys/Leftist\char_Heap}{}\fi %------------------------------------------------------------- \begin{frame}{Leftist tree informally} -The \high{rank} of a tree is the depth of the rightmost leaf. +The \concept{rank} of a tree is the depth of the rightmost leaf. \pause\bigskip -In a \high{leftist tree}, the rank of every left child is$\ge$-the rank of its right sibling +In a \concept{leftist tree}, the rank of every left child is$\ge\$
+the rank of its right sibling.

\pause\bigskip
-Insertions are done on the right. Thus rank bounds number of descends.
+Merge descends along the right spine.\\ Thus rank bounds number of steps.

\pause\bigskip
-If rank of right child gets to large: swap with left child.
+If rank of right child gets too large: swap with left child.

\end{frame}
%-------------------------------------------------------------
@@ -196,13 +219,14 @@
\high{@{thm[break,margin=50] (dummy_pats) mset_tree.simps(2)}}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{Heap}
@{const heap} \<open>::\<close> @{typ "'a lheap \<Rightarrow> bool"}\\\smallskip\pause
\high{@{thm heap.simps(1)}}\\
\high{@{text"heap \<langle>_, l, a, r\<rangle> = (heap l \<and> heap r \<and>"}}\\
\quad\high{@{text"(\<forall>x \<in># mset_tree l + mset_tree r. a \<le> x))"}}
-
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}{Leftist tree}
@{const rank} \<open>::\<close> @{typ "'a lheap \<Rightarrow> nat"}\\\smallskip\pause
@@ -224,16 +248,6 @@
\end{center}
\end{frame}
%-------------------------------------------------------------
-\begin{frame}{Why leftist tree?}
-\pause
-
-\textbf{Lemma} \high{@{thm pow2_rank_size1}}
-\bigskip\pause
-
-\textbf{Lemma} Execution time of @{term "merge t\<^sub>1 t\<^sub>2"} is bounded by
-\mbox{@{term"rank t\<^sub>1 + rank t\<^sub>2"}}
-\end{frame}
-%-------------------------------------------------------------
\begin{frame}{@{const merge}}
Principle: descend on the right
\smallskip\pause
@@ -247,6 +261,7 @@
where @{thm (dummy_pats) rk.simps(2)}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{@{const merge}}
@{thm[break] (sub,dummy_pats) merge.simps(3)}
\bigskip\pause
@@ -256,11 +271,24 @@
\onslide<3->{\revealbeamer{@{term"size t\<^sub>1 + size t\<^sub>2"}}}
\onslide<2->{decreases with every recursive call.}}
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}{Functional correctness proofs}{including preservation of \<open>invar\<close>}
Straightforward
\end{frame}
%-------------------------------------------------------------
+\ifMOD
+\begin{frame}{Logarithmic complexity}
+\begin{lemma}
+\high{@{thm pow2_rank_size1}}
+\end{lemma}
+\bigskip\pause
+
+\begin{corollary}
+@{thm[break,margin=40] t_merge_log}
+\end{corollary}
+\end{frame}
+\else
\begin{frame}{Logarithmic complexity}
Correlation of rank and size:\\
\textbf{Lemma} @{thm pow2_rank_size1}
@@ -273,14 +301,15 @@
\textbf{Lemma} @{thm t_merge_rank}
\pause

-\textbf{Lemma} @{thm[break,margin=40] t_merge_log}
+\textbf{Corollary} @{thm[break,margin=40] t_merge_log}
\pause\bigskip

-\textbf{Lemma}\\ @{thm t_insert_log}
+\textbf{Corollary}\\ @{thm t_insert_log}
\pause\bigskip

-\textbf{Lemma}\\ @{thm t_del_min_log}
+\textbf{Corollary}\\ @{thm t_del_min_log}
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}
\begin{center}
--- a/Slides/RBT_Slides.thy	Tue Aug 01 14:12:13 2017 +0200
+++ b/Slides/RBT_Slides.thy	Thu Aug 03 09:42:58 2017 +0200
@@ -209,12 +209,13 @@
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Proof in CLRS}
-\includegraphics[scale=0.2,angle=90]{clrsrbti3} \hspace{-1em}
-\includegraphics[scale=0.2,angle=90]{clrsrbti4}
-\vspace{-1em}
+\vspace{-2em}
+\hspace{2em} \includegraphics[scale=0.2]{clrsrbti1}
+\includegraphics[scale=0.19]{clrsrbti2}
+\vspace{-4em}

-\includegraphics[scale=0.2,angle=90]{clrsrbti1} \hspace{-1em}
-\includegraphics[scale=0.2,angle=90]{clrsrbti2}
+\hspace{2em} \includegraphics[scale=0.2]{clrsrbti3}
+\includegraphics[scale=0.19]{clrsrbti4}
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Deletion}
--- a/Slides/Sorting_Slides.thy	Tue Aug 01 14:12:13 2017 +0200
+++ b/Slides/Sorting_Slides.thy	Thu Aug 03 09:42:58 2017 +0200
@@ -62,7 +62,7 @@
\end{tabular}
\bigskip\pause

-Import \texttt{"~~/src/HOL/Library/Multiset"}
+Import \texttt{"\char\~\char\~/src/HOL/Library/Multiset"}
\end{frame}
%-------------------------------------------------------------
\section{Insertion Sort}
--- a/Slides/document/prelude.tex	Tue Aug 01 14:12:13 2017 +0200
+++ b/Slides/document/prelude.tex	Thu Aug 03 09:42:58 2017 +0200
@@ -64,7 +64,7 @@
{\thyfile{#1\char\_Demo}{#2}}

\newcommand{\afpentry}[1]
-{\filepage{Archive of Formal Proofs}
+{\filepage{\href{https://www.isa-afp.org}{Archive of Formal Proofs}}
{\url{https://www.isa-afp.org/entries/#1.shtml}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`