.

--- a/ROOT	Thu Aug 03 09:43:22 2017 +0200
+++ b/ROOT	Tue Aug 08 17:22:04 2017 +0200
@@ -104,3 +104,4 @@
     "clrsrbtd4.pdf"
     "clrsrbtd5.pdf"
     "clrsrbtd6.pdf"
+    "Code_AA.tex"
\ No newline at end of file

--- a/Slides/Binomial_Tree_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/Binomial_Tree_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -5,8 +5,10 @@
   "../../Public/Thys/BinHeap"
 begin
   
-thm btree_invar.simps[unfolded compl_descending_def]
-  
+lemma invar_btree_simps: "invar_btree (Node r x ts) \<longleftrightarrow> 
+      (\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
+by(simp add: compl_descending_def dummyid_def)
+
 lemmas merge_simps = merge.simps(1) merge_simp2 merge.simps(3)
   
 thm get_min.simps  
@@ -16,14 +18,22 @@
 
 abbreviation (latex) sz_tree ("|_|") where "sz_tree t \<equiv> size (mset_tree t)"
 abbreviation (latex) sz_heap ("|_|") where "sz_heap t \<equiv> size (mset_heap t)"
-    
+(*
+lemma l_ins_tree_estimate': 
+  "t_ins_tree t ts + length (ins_tree t ts) - length ts = 2"
+using l_ins_tree_estimate[of t ts] by linarith
+
+lemma l_merge_estimate': 
+  "t_merge ts\<^sub>1 ts\<^sub>2 + length (merge ts\<^sub>1 ts\<^sub>2) - 2 * (length ts\<^sub>1 + length ts\<^sub>2) \<le> 1"
+using l_merge_estimate[of ts\<^sub>1 ts\<^sub>2] by linarith
+*)
 (*>*)
 text_raw{*
 \end{isabellebody}%
 %-------------------------------------------------------------
-\section{Binomial Heaps}
+\section{Binomial Heap}
 %-------------------------------------------------------------
-\ifMOD\else\thyfile{Thys/BinHeap}{Binomial Heaps --- Correctness and Complexity}\fi
+\ifMOD\else\thyfile{Thys/BinHeap}{Binomial Heap --- Correctness and Complexity}\fi
 %-------------------------------------------------------------
 \begin{frame}{Numerical method}
 Idea: only use trees \<open>t\<^sub>i\<close> of size \<open>2\<^sup>i\<close>\\
@@ -44,42 +54,47 @@
 \end{tabular}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Binomial trees}
-\high{@{theory_text \<open>datatype 'a tree = Node (rank: nat) (root: 'a) ("'a tree list")\<close>}}\\
-  \smallskip\pause
+\begin{frame}{Binomial tree}
+\high{\textbf{datatype} \<open>'a tree =\<close>\\
+\quad \<open>Node (rank: nat) (root: 'a) ('a tree list)\<close>}
+\bigskip\pause
   
-  Node with rank \<open>i\<close> has successors \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close>
-  with ranks \<open>[i-1,\<dots>,0]\<close>
-  \high{@{thm [display] btree_invar.simps[unfolded compl_descending_def]}}
-  \smallskip\pause
+Invariant: Node of rank \<open>i\<close> has children \<open>[t\<^sub>i\<^sub>-\<^sub>1,\<dots>t\<^sub>0]\<close> of ranks \<open>[i-1,\<dots>,0]\<close>:
+\pause
+\high{@{thm [display] invar_btree_simps}}
+\pause
 
-  Tree has exactly @{term \<open>(2::nat)^rank t\<close>} nodes
-  \high{@{thm [display] size_btree}}
+\begin{lemma}
+\high{@{thm size_btree}}
+\end{lemma}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Linking two Trees}
-  Given two trees of rank \<open>i\<close>, join them to tree of rank \<open>i+1\<close>.\\
-  \smallskip\pause
+\begin{frame}{Combining two trees}
+How to combine
+\begin{tabular}[t]{l}
+two trees of rank \<open>i\<close>\\
+into one tree of rank \<open>i+1\<close>
+\end{tabular}
+\pause
 
-  Idea: Insert one tree under root of other tree
-  \smallskip\pause
-
-  \high{@{thm[display] link_def}}
+\high{@{thm[display] link_def}}
 \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>
-  \bigskip\pause
+\begin{frame}{Binomial heap}
+Use 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>
+\pause
 
-  \high{@{theory_text \<open>(*<*)type_synonym (*>*)'a heap = "'a tree list"\<close>}}
-  \smallskip\pause
+\high{@{theory_text[display] \<open>type_synonym 'a heap = "'a tree list"\<close>}}
+\pause
+Remember: \<open>tree\<close> contains rank
+\bigskip\pause
 
-  \high{@{thm bheap_invar_def}}\\
-  Ranks in \high{ascending} order\\
+Invariant:
+\high{@{thm[display,margin=60] invar_bheap_def}}
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Inserting a Tree}
+\begin{frame}{Inserting a tree}
   \high{@{thm [display, margin=60] ins_tree.simps}}
   \smallskip\pause
 
@@ -90,7 +105,7 @@
   Rank of inserted tree \<open>\<le>\<close> ranks of trees in heap \\
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Merge}
+\begin{frame}{@{const merge}}
   \high{@{thm [display] merge_simps}}
   \smallskip\pause
 
@@ -100,30 +115,30 @@
   Note: Handling of carry after recursive call
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Find/Delete Minimum Element}
-  All trees are min-heaps
+\begin{frame}{Find/delete minimum element}
+  All trees are min-heaps.
   \smallskip\pause
 
-  Smallest element may be any root node
+  Smallest element may be any root node:
   \high{@{thm [display] find_min_alt}}
   \smallskip\pause
 
-  Similar: \high{@{term_type get_min}} \\
-  Returns tree with minimal root, and other trees
+  Similar: \high{@{const_typ get_min}} \\
+  Returns tree with minimal root, and remaining trees
+\bigskip\pause
 
-  \smallskip\pause
-  Delete via merge
-  \high{@{thm [display, margin=60] delete_min_def}}
-  Note the \<open>rev\<close>!
-
+\high{@{thm [display, margin=60] delete_min_def}}
+\ifMOD\else
+Why \<open>rev\<close>? \pause Rank decreasing in \<open>ts\<^sub>1\<close> but increasing in \<open>ts\<^sub>2\<close>
+\fi
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Complexity}
-  Recall: @{term \<open>size (mset_tree t) = 2^rank t\<close>}
+  Recall: @{thm (concl) size_btree}
   \smallskip\pause
 
-  Similarly for heap: @{term \<open>size (mset_heap h) \<ge> 2^length h\<close>}
-  \smallskip\pause
+Similarly for heap: @{thm (concl) size_bheap}
+\smallskip\pause
 
   Complexity of operations: linear in length of heap\\ \pause
   i.e., logarithmic in number of elements
@@ -132,32 +147,36 @@
   Proofs: \pause straightforward\pause ?
 \end{frame}
 %-------------------------------------------------------------
-\begin{frame}{Complexity of Merge}
+\begin{frame}[t]{Complexity of @{const merge}}
+  \high{@{thm [display] merge_simps(3)}}
+\smallskip\pause
+
+Complexity of @{const ins_tree}: \<open>t_ins_tree t ts \<le> length ts + 1\<close>
+\smallskip\pause
+
+A call @{term (sub) \<open>merge t1 t2\<close>} (where \<open>length t\<^sub>1 = length t\<^sub>2 = n\<close>)
+can lead to calls of \<open>ins_tree\<close> on lists of length 1, \ldots, \<open>n\<close>.
+\smallskip\pause
+
+\bad{\<open>\<Sum> \<in> O(n\<^sup>2)\<close>}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}[t]{Complexity of  @{const merge}}
   \high{@{thm [display] merge_simps(3)}}
   \smallskip\pause
 
-  Complexity of @{const ins_tree} call depends on length of result of recursive call.
-  \smallskip\pause
-
-  Naive: @{term \<open>length (merge ts\<^sub>1 ts\<^sub>2) \<le> length ts\<^sub>1 + length ts\<^sub>2\<close>}
-  \smallskip\pause
+  Relate time and length of input/output:
+\smallskip
 
-  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
+  \high{@{thm l_ins_tree_estimate}}
+\smallskip
 
-  Idea: Estimate cost and length of result:
-  \high{@{thm [display, margin=60] l_ins_tree_estimate l_merge_estimate}}
+  \high{@{thm [break, margin=60] l_merge_estimate}}
 
   \smallskip\pause
   Yields desired linear bound!
 \end{frame}
 
-
-
 \begin{isabellebody}%
 *}
 (*<*)

--- a/Slides/Braun_Tree_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/Braun_Tree_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -37,20 +37,10 @@
 text_raw{*
 \end{isabellebody}%
 %-------------------------------------------------------------
-\section{Priority Queues Based on Braun Trees}
+\section{Priority Queue via Braun Tree}
 %-------------------------------------------------------------
 \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
@@ -170,6 +160,14 @@
 Above running times logarithmic in size
 \end{frame}
 %-------------------------------------------------------------
+\begin{frame}{Source of code}
+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}
+%-------------------------------------------------------------
 \ifMOD\else
 \begin{frame}[t]{Sorting with priority queue}
 \pause

--- a/Slides/FDSlatex.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/FDSlatex.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -31,7 +31,9 @@
 
 notation (latex output) dummyid ("_")
 
+translations "x" <= "CONST Int.int x"
 translations "x" <= "CONST Real.real x"
+translations "x" <= "CONST Real.real_of_int x"
 
 (* log *)
 notation (latex output)

--- a/Slides/Leftist_Heap_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/Leftist_Heap_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -320,8 +320,7 @@
 
 \begin{isabellebody}%
 *}
-  
-  
+
 (*<*)
 end
 (*>*)

--- a/Slides/RBT_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/RBT_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -252,6 +252,71 @@
 \includegraphics[scale=0.2]{clrsrbtd6}
 \end{frame}
 %-------------------------------------------------------------
+\begin{frame}{Source of code}
+Insertion:\smallskip\\
+Okasaki's \emph{Purely Functional Data Structures}
+\bigskip\pause
+
+Deletion:\smallskip\\
+Stefan Kahrs. \emph{Red Black Trees with Types}.\\ J. Functional Programming. 1996.
+\end{frame}
+%-------------------------------------------------------------
+\section{More Search Trees}
+%---------------------------------------------------------------------------
+\subsection{AA Trees}
+%---------------------------------------------------------------------------
+\begin{frame}{AA trees}
+\framesubtitle{[Arne Andersson 93, Ragde 14]}
+\begin{itemize}
+\pause
+\item \high{Simulation of 2-3 trees by binary trees}\\
+  \high{\<open>\<langle>t\<^sub>1,a,t\<^sub>2,b,t\<^sub>3\<rangle>\<close> \ $\leadsto$ \ \<open>\<langle>t\<^sub>1,a,\<langle>t\<^sub>2,b,t\<^sub>3\<rangle>\<rangle>\<close>}
+\pause
+\item Height field (or single bit) to distinguish\\ single from double node
+\pause
+\item Code short but opaque
+\pause
+\item \bad{4 bugs} in \<open>delete\<close> in [Ragde 14]:\\\pause
+ \bad{non-linear pattern; \pause going down wrong subtree;\\\pause
+ missing function call; \pause off by 1}
+\end{itemize}
+\end{frame}
+%---------------------------------------------------------------------------
+\begin{frame}{AA trees}
+\framesubtitle{[Arne Andersson 93, Ragde 14]}
+\pause
+After corrections, the proofs:
+\begin{itemize}
+\pause
+\item Code relies on tricky pre- and post-conditions
+\pause
+\item Functional correctness proofs again automatic \pause\\
+--- once the pre-conditions have been found
+\pause
+\item Structural invariant preservation requires most of the work
+\end{itemize}
+\end{frame}
+%---------------------------------------------------------------------------
+\subsection{Scapegoat Trees}
+%---------------------------------------------------------------------------
+\begin{frame}{Scapegoat trees}
+\framesubtitle{[Anderson 89, Igal \& Rivest 93]}
+\begin{center}
+\pause
+Central idea:
+\medskip
+
+\bad{Don't rebalance every time},\\
+\high{Rebuild when the tree gets ``too unbalanced''}
+\end{center}
+\begin{itemize}
+\pause
+\item Functional correctness proofs again automatic
+\pause
+\item Tricky: amortized logarithmic complexity analysis
+\end{itemize}
+\end{frame}
+%---------------------------------------------------------------------------
 
 \begin{isabellebody}%
 *}

--- a/Slides/Skew_Heap_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/Skew_Heap_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -2,14 +2,29 @@
 theory Skew_Heap_Slides
 imports
   Tree_Notation
-  "../../Public/Thys/Skew_Heap_Analysis"
+  "../../Public/Thys/Skew_Heap_Analysis2"
 begin
 (*>*)
 text_raw{*
 \end{isabellebody}%
 %-------------------------------------------------------------
+\ifMOD
+\afpentry{Amortized_Analysis}
+\fi
+%-------------------------------------------------------------
 \section{Skew Heap}
 %-------------------------------------------------------------
+\ifMOD
+\begin{frame}
+\begin{center}
+A \concept{skew heap} is a self-adjusting heap (priority queue)
+\pause\bigskip
+
+Almost like leftist heap, but \high{no size info needed}
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
+\else
 \thyfile{Thys/Skew\char`\_Heap\char`\_Analysis}{}
 %-------------------------------------------------------------
 \begin{frame}
@@ -30,6 +45,7 @@
 
 Invariant: @{const heap}
 \end{frame}
+\fi
 %-------------------------------------------------------------
 \begin{frame}{@{const merge}}
 \high{@{thm (sub) merge.simps(1)}}\\
@@ -39,11 +55,12 @@
 
 \high{@{prop[break,margin=60] (sub) "merge (K2 h1 (Node l1 a r1)) (K2 h2 (Node l2 b r2)) =
 (if a \<le> b then Node (merge h2 r1) a l1 else Node (merge h1 r2) b l2)"}}
-\pause\medskip
 
-Function @{const merge} terminates because \dots
+%Function @ {const merge} terminates because \dots
+
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}{@{const merge}}
 Very similar to leftist heap but
 \begin{itemize}
@@ -55,8 +72,9 @@
 \high{no size information needed}
 \end{itemize}
 \end{frame}
+\fi
 %-------------------------------------------------------------
-\begin{frame}{Functional correctness proofs}{including preservation of @{const heap}}
+\begin{frame}{Functional correctness proofs}
 Straightforward
 \end{frame}
 %-------------------------------------------------------------
@@ -68,11 +86,13 @@
 %-------------------------------------------------------------
 \begin{frame}{Towards the proof}
 \pause
-@{thm rheavy.simps[of _ DUMMY]}
-\pause
-@{thm[display] lpath.simps}
-\pause
-@{thm G.simps}
+Right heavy:\\
+\high{@{thm rh_def}}
+\pause\bigskip
+
+Number of right heavy nodes on left spine:\smallskip\\
+\high{@{thm lrh.simps(1)}}\\
+\high{@{thm (dummy_pats) lrh.simps(2)}}
 \bigskip\pause
 
 \begin{lemma}
@@ -85,9 +105,13 @@
 \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}
+Right heavy:\\
+\high{@{thm rh_def}}
+\bigskip
+
+Number of not right heavy nodes on right spine:\smallskip\\
+\high{@{thm rlh.simps(1)}}\\
+\high{@{thm (dummy_pats) rlh.simps(2)}}
 \bigskip
 
 \begin{lemma}
@@ -99,18 +123,21 @@
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Potential}
-\high{The potential is the number of \bad{@{const rheavy}} nodes:}
+\high{The potential is the number of right heavy nodes:}
 \smallskip\pause
 
 @{thm (dummy_pats) \<Phi>.simps}
 \smallskip\pause
 
-@{const merge} descends on the right \<open>\<Longrightarrow>\<close> \bad{@{const rheavy}} nodes are \bad{bad}
+\invisible<handout>{@{const merge} descends on the right\\ \<open>\<Longrightarrow>\<close> \bad{right heavy nodes are bad}}
 \bigskip\pause
 
 \begin{lemma}
 @{thm[break,margin=60] (sub) amor_le}
 \end{lemma}
+\pause\smallskip
+
+\texttt{by(induction t1 t2 rule:~merge.induct)(auto)}
 \end{frame}
 %-------------------------------------------------------------
 \begin{frame}{Main proof}
@@ -132,6 +159,7 @@
 @{text"="} @{term (sub) "3 * log 2 (size1 t1 + size1 t2) + 1"}
 \end{frame}
 %-------------------------------------------------------------
+\ifMOD\else
 \begin{frame}{@{const Skew_Heap.insert} and @{const del_min}}
 \pause
 Easy consequences:
@@ -142,20 +170,21 @@
 \high{@{thm[break,margin=50] (sub) a_del_min}}
 \end{lemma}
 \end{frame}
+\fi
 %-------------------------------------------------------------
 \begin{frame}{Sources}
 The inventors of skew heaps:
 \smallskip
 
-\high{Daniel Sleator and Robert Tarjan.\\
-Self-adjusting Heaps.}\\ \emph{SIAM J. Computing}, 1986.
+Daniel Sleator and Robert Tarjan.\\
+Self-adjusting Heaps.\\ \emph{SIAM J. Computing}, 1986.
 \bigskip\pause
 
 The formalization is based on
 \smallskip
 
-\high{Anne Kaldewaij and Berry Schoenmakers.\\
-The Derivation of a Tighter Bound for Top-down Skew Heaps.}
+Anne Kaldewaij and Berry Schoenmakers.\\
+The Derivation of a Tighter Bound for Top-down Skew Heaps.
 \emph{Information Processing Letters}, 1991.
 \end{frame}
 %-------------------------------------------------------------

--- a/Slides/Tree23_Slides.thy	Thu Aug 03 09:43:22 2017 +0200
+++ b/Slides/Tree23_Slides.thy	Tue Aug 08 17:22:04 2017 +0200
@@ -131,7 +131,7 @@
 \onslide<2->
 \textbf{Proof} by induction on \<open>t\<close>.
 \onslide<6->
-Step automatic.
+Base and step automatic.
 \bigskip\onslide<7->
 \begin{corollary}
 \high{@{thm bal_insert}}
@@ -145,7 +145,7 @@
 \pause
 @{const Node3} & $\leadsto$ & @{const Node2} \\
 \pause
-@{const Node2} & $\leadsto$ & \bad{underflow}, height -1
+@{const Node2} & $\leadsto$ & \bad{underflow}, height decreases by 1
 \end{tabular}
 \end{center}
 \pause