merged draft
authorlammich <lammich@in.tum.de>
Tue, 04 Jul 2017 16:34:18 +0200
changeset 69824 1732e9f5ccc8
parent 69823 ea44de9dcc72 (current diff)
parent 69821 b2c28b39893d (diff)
child 69825 d3e83bb8db26
child 69827 6280da38ced7
merged
Slides/Leftist_Heap_Slides.thy~
Slides/RBT_Slides.thy~
Slides/Sorting_Slides.thy~
Slides/Tree_Slides.thy~
Slides/Trie_Slides.thy~
--- a/ROOT	Tue Jul 04 16:33:55 2017 +0200
+++ b/ROOT	Tue Jul 04 16:34:18 2017 +0200
@@ -27,9 +27,10 @@
   document_files
     "root.tex"
     "root_handout.tex"
+    "main.tex"
     "prelude.tex"
 
-    
+
 session Slides_Heaps in Slides = "HOL-FDS17" +
   options [document_output = tex, document = pdf, names_short = true
       , document_variants = "partial"]
@@ -40,3 +41,13 @@
   document_files
     "root_partial.tex"
     "prelude.tex"
+
+
+session Amor_Slides in Slides = "HOL-FDS17" +
+  options [document_output = tex, document = pdf, names_short = true
+      , document_variants = "amor"]
+  theories[show_question_marks=false]
+    Amor_Slides
+  document_files
+    "root_amor.tex"
+    "prelude.tex"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Amor_Slides.thy	Tue Jul 04 16:34:18 2017 +0200
@@ -0,0 +1,40 @@
+(*<*)
+theory Amor_Slides
+imports
+  FDSlatex
+begin
+(*>*)
+text_raw{*
+\end{isabellebody}%
+\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
+\section{Amortized Complexity}
+%-------------------------------------------------------------
+\begin{frame}{The problem}
+\begin{center}
+Worst case complexities of \high{individual operations}\\
+may lead to \bad{overestimation} of\\
+worst case complexities of \bad{sequences of operations}
+\end{center}
+\end{frame}
+%-------------------------------------------------------------
+\begin{frame}{Priority queues are multisets}
+\begin{center}
+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}
+%-------------------------------------------------------------
+\begin{frame}{Multisets in Isabelle}
+
+Import \texttt{"Library/Multiset"}
+\end{frame}
+%-------------------------------------------------------------
+\begin{isabellebody}%
+*}
+(*<*)
+end
+(*>*)
--- a/Slides/Leftist_Heap_Slides.thy~	Tue Jul 04 16:33:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,299 +0,0 @@
-(*<*)
-theory Leftist_Heap_Slides
-imports
-  FDSlatex
-  "../../Public/Thys/Leftist_Heap"
-begin
-
-lemma merge2_alt: "merge t\<^sub>1 \<langle>\<rangle> = t\<^sub>1" by (cases t\<^sub>1) auto
-  
-  
-notation size1 ("|_|\<^sub>1")
-(*>*)
-text_raw{*
-\end{isabellebody}%
-\newcommand{\revealbeamer}[1]{\uncover<+->{\invisible<handout>{#1}}}
-\section{Priority Queues}
-%-------------------------------------------------------------
-\begin{frame}{Priority queue informally}
-\begin{center}
-Collection of elements with priorities
-\end{center}
-\pause
-Operations:
-\begin{itemize}
-\pause
-\item empty
-\pause
-\item emptiness test
-\pause
-\item insert
-\pause
-\item get element with minimal priority
-\pause
-\item delete element with minimal priority
-\end{itemize}
-\bigskip\pause
-\begin{center}
-We focus on the priorities:\\
-\high{element = priority}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Priority queues are multisets}
-\begin{center}
-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}
-%-------------------------------------------------------------
-\begin{frame}{Multisets in Isabelle}
-
-Import \texttt{"Library/Multiset"}
-\end{frame}
-%-------------------------------------------------------------
-*}
-text_raw (in Priority_Queue) {*
-%-------------------------------------------------------------
-\begin{frame}{Interface of implementation}
-\begin{center}
-The type of elements (= priorities) \ \high{@{typ 'a}} \ is a linear order
-\end{center}
-\pause
-An implementation of a priority queue of elements of type \ @{typ 'a} \ must provide
-\begin{itemize}
-\pause
-\item An implementation type \ \high{@{typ 'q}}
-\pause
-\item \high{\<open>empty ::\<close> @{typ 'q}}
-\pause
-\item \high{\<open>is_empty ::\<close> @{typ "'q \<Rightarrow> bool"}}
-\pause
-\item \high{\<open>insert ::\<close> @{typ"'a \<Rightarrow> 'q \<Rightarrow> 'q"}}
-\pause
-\item \high{\<open>get_min ::\<close> @{typ"'q \<Rightarrow> 'a"}}
-\pause
-\item \high{\<open>del_min ::\<close> @{typ"'q \<Rightarrow> 'q"}}
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{More operations}
-\begin{itemize}
-\item \high{\<open>merge ::\<close> @{typ"'q \<Rightarrow> 'q \<Rightarrow> 'q"}}\\
-Often provided
-\pause
-\item decrease key/priority\\ Not easy in functional setting
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of implementation}
-A priority queue represents a \high{multiset} of priorities.
-
-Correctness proof requires:
-\begin{center}
-\begin{tabular}{ll}
-Abstraction function: & \high{@{term[source]"mset :: 'q \<Rightarrow> 'a multiset"}}
-\\\pause
-Invariant: & \high{@{term[source]"invar :: 'q \<Rightarrow> bool"}}
-\end{tabular}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of implementation}
-Must prove \ \high{@{prop"invar q"}} \<open>\<Longrightarrow>\<close>\medskip
-
-\pause
-\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}}\\
-\bigskip\pause
-\high{@{thm (concl) invar_empty}}\\
-\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 $\ge$ all elements in the subtrees.
-\end{center}
-\pause
-
-The term ``heap'' is frequently used synonymously with ``priority queue''.
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Priority queue via heap}
-\begin{itemize}
-\pause
-\item \<open>empty = \<langle>\<rangle>\<close>
-\pause
-\item \<open>is_empty h = (h = \<langle>\<rangle>)\<close>
-\pause
-\item \<open>get_min \<langle>_, a, _\<rangle> = a\<close>
-\pause
-\item Assume we have \<open>merge\<close>
-\pause
-\item @{text"insert a t = merge \<langle>\<langle>\<rangle>, a, \<langle>\<rangle>\<rangle> t"}
-\pause
-\item \<open>del_min \<langle>l, a, r\<rangle> = merge l r\<close>
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Priority queue via heap}
-A naive merge:
-\medskip\pause
-
-\<open>merge t\<^sub>1 t\<^sub>2 = (\<^latex>\<open>{\sf case}\<close> (t\<^sub>1,t\<^sub>2) \<^latex>\<open>{\sf of}\<close>\<close>\\
-\quad\<open>(\<langle>\<rangle>, _) \<Rightarrow> t\<^sub>2 |\<close>\\
-\quad@{text"(_, \<langle>\<rangle>) \<Rightarrow> t\<^sub>1 |"}\\\pause
-\quad@{text"(\<langle>l\<^sub>1,a\<^sub>1,r\<^sub>1\<rangle>, \<langle>l\<^sub>2,a\<^sub>2,r\<^sub>2\<rangle>) \<Rightarrow>"}\\
-\qquad@{text"\<^latex>\<open>{\\sf if}\<close> a\<^sub>1 \<le> a\<^sub>2 \<^latex>\<open>{\\sf then}\<close> \<langle>merge l\<^sub>1 r\<^sub>1, a\<^sub>1, t\<^sub>2\<rangle>"}\\
-\qquad@{text"\<^latex>\<open>{\\sf else}\<close> \<langle>t\<^sub>1, a\<^sub>2, merge l\<^sub>2 r\<^sub>2\<rangle>"}
-\bigskip\pause
-
-\bad{Challenge:} how to maintain some kind of balance
-\end{frame}
-%-------------------------------------------------------------
-*}
-text_raw {*
-%-------------------------------------------------------------
-\section{Leftist Heap}
-%-------------------------------------------------------------
-\thyfile{Leftist\char`_Heap}{}
-%-------------------------------------------------------------
-\begin{frame}{Leftist tree informally}
-The \high{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
-
-\pause\bigskip
-Insertions are done on the right. Thus rank bounds number of descends.
-
-\pause\bigskip
-If rank of right child gets to large: swap with left child.
-
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Implementation type}
-\isakeyword{datatype}\\
-\quad \high{@{text "'a lheap = Leaf | Node nat ('a tree) 'a ('a tree)"}}
-\medskip\pause
-
-Abbreviations \high{@{const Leaf}} and \high{@{term "\<langle>h, l, a, r\<rangle>"}} as usual
-\bigskip\pause
-
-Abstraction function:\\
-@{const mset_tree} \<open>::\<close> @{typ "'a lheap \<Rightarrow> 'a multiset"}\\\smallskip\pause
-\high{@{thm mset_tree.simps(1)}}\\
-\high{@{thm[break,margin=50] (dummy_pats) mset_tree.simps(2)}}
-\end{frame}
-%-------------------------------------------------------------
-\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}
-%-------------------------------------------------------------
-\begin{frame}{Leftist tree}
-@{const rank} \<open>::\<close> @{typ "'a lheap \<Rightarrow> nat"}\\\smallskip\pause
-\high{@{thm rank.simps(1)}}\\
-\high{@{thm (dummy_pats) rank.simps(2)}}
-\bigskip\pause
-
-Node @{term "Node n l a r"}: \<open>n = \<close> rank of node
-\bigskip\pause
-
-@{const ltree} \<open>::\<close> @{typ "'a lheap \<Rightarrow> bool"}\\\smallskip\pause
-\high{@{thm ltree.simps(1)}}\\
-\high{@{thm[break,margin=60] (dummy_pats) ltree.simps(2)}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Leftist heap invariant}
-\begin{center}
-\high{@{prop"invar h = (heap h \<and> ltree h)"}}
-\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
-
-\high{@{thm[break] (sub) merge.simps(1) merge2_alt}}\\\pause
-\high{@{thm[break] (sub,dummy_pats) merge.simps(3)}}
-\bigskip\pause
-
-@{const node} \<open>::\<close> @{typ "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap"}\\\smallskip\pause
-\high{@{thm[break,margin=65] (sub) node_def}}\\
-where @{thm (dummy_pats) rk.simps(2)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{@{const merge}}
-@{thm[break] (sub,dummy_pats) merge.simps(3)}
-\bigskip\pause
-
-\high{\onslide<2->{Function @{const merge} terminates because}
-\onslide<-2>{\revealbeamer{?}}
-\onslide<3->{\revealbeamer{@{term"size t\<^sub>1 + size t\<^sub>2"}}}
-\onslide<2->{decreases with every recursive call.}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Functional correctness proofs}{including preservation of \<open>invar\<close>}
-Straightforward
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Logarithmic complexity}
-Correlation of rank and size:\\ 
-  \textbf{Lemma} @{thm pow2_rank_size1}
-\pause\bigskip
-
-Complexity measures @{const t_merge}, @{const t_insert} @{const t_del_min}:\\
- count calls of @{const merge}.
-\pause\bigskip
-
-\textbf{Lemma} @{thm t_merge_rank}
-\pause
-
-\textbf{Lemma} @{thm[break,margin=40] t_merge_log}
-\pause\bigskip
-
-\textbf{Lemma}\\ @{thm t_insert_log}
-\pause\bigskip
-
-\textbf{Lemma}\\ @{thm t_del_min_log}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}
-\begin{center}
-\bad{Can we avoid the rank info in each node?}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-
-\begin{isabellebody}%
-*}
-  
-  
-(*<*)
-end
-(*>*)
--- a/Slides/RBT_Slides.thy~	Tue Jul 04 16:33:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,234 +0,0 @@
-(*<*)
-theory RBT_Slides
-imports
-  FDSlatex
-  "../Material/Thys/RBT_Set"
-begin
-(*
-fun Bpl :: "'a rbt \<Rightarrow> nat set" where
-"Bpl Leaf = {0}" |
-"Bpl (Node c l _ r) =
-  (let Bs = Bpl l \<union> Bpl r
-   in if c = Black then {n+1 |n. n \<in> Bs} else Bs)"
-
-lemma invh_Bpl: "invh t \<Longrightarrow> Bpl t = {bheight t}"
-by(induction t) auto
-*)
-
-(*
-lemma combine_simp2: "combine t \<langle>\<rangle> = t"
-by (cases t) auto
-
-lemmas combine_simps = combine.simps(1) combine_simp2 combine.simps(3-)
-*)
-notation size1 ("|_|\<^sub>1")
-notation height ("h'(_')" 100)
-notation bheight ("bh'(_')" 100)
-(*>*)
-text_raw{*
-\end{isabellebody}%
-\section{Red-Black Trees}
-%-------------------------------------------------------------
-\thyfile{Thys/RBT\char`_Set}{}
-%-------------------------------------------------------------
-\begin{frame}{Relationship to 2-3-4 trees}
-Idea:
-\begin{tabular}[t]{l}
- encode 2-3-4 trees as binary trees;\\\pause
- use color to express grouping
-\end{tabular}
-\pause\bigskip
-
-\begin{tabular}{rcl}
-@{const Leaf} &$\approx$& @{const Leaf}\\\pause
-@{text"\<langle>t\<^sub>1,a,t\<^sub>2\<rangle>"} &$\approx$& @{text"\<langle>t\<^sub>1,a,t\<^sub>2\<rangle>"}\\\pause
-@{text"\<langle>t\<^sub>1,a,t\<^sub>2,b,t\<^sub>3\<rangle>"} &$\approx$&\pause \<open>\<langle>\<close>\bad{\<open>\<langle>t\<^sub>1,a,t\<^sub>2\<rangle>\<close>}\<open>,b,t\<^sub>3\<rangle>\<close>
- \pause\<open>\<langle>t\<^sub>1,a,\<close>\bad{\<open>\<langle>t\<^sub>2,b,t\<^sub>3\<rangle>\<close>}\<open>\<rangle>\<close>\\\pause
-@{text"\<langle>t\<^sub>1,a,t\<^sub>2,b,t\<^sub>3,c,t\<^sub>4\<rangle>"} &$\approx$& \pause\<open>\<langle>\<close>\bad{\<open>\<langle>t\<^sub>1,a,t\<^sub>2\<rangle>\<close>}\<open>,b,\<close>\bad{\<open>\<langle>t\<^sub>3,c,t\<^sub>4\<rangle>\<close>}\<open>\<rangle>\<close>\\
-\end{tabular}
-\bigskip\pause
-
-\begin{center}
-\bad{Red} means ``I am part of a bigger node''
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Invariants}
-\begin{itemize}
-\pause
-\item The root is \pause\invisible<handout>{Black.}
-\pause
-\item Every @{const Leaf} is considered Black.
-\pause
-\item If a node is \bad{Red},
- \pause\invisible<handout>{its children are Black.}
-\pause
-\item All paths from a node to a leaf have the same number of
- \pause\invisible<handout>{Black nodes.}
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Red-black trees}
-@{datatype [display] color}
-\pause
-\isakeyword{datatype}\\
-\quad \high{@{text "'a rbt = Leaf | Node color ('a tree) 'a ('a tree)"}}
-\bigskip\pause
-
-Abbreviations:
-\smallskip
-\begin{center}
-\begin{tabular}{rcl}
-\high{@{const Leaf}} &\<open>\<equiv>\<close>& @{text Leaf}\\\pause
-\high{@{term "\<langle>c, l, a, r\<rangle>"}} &\<open>\<equiv>\<close>& @{term[source] "Node c l a r"}\medskip
-\\\pause
-\high{@{term "R l a r"}} &\<open>\<equiv>\<close>& @{term[source] "Node Red l a r"}\\\pause
-\high{@{term "B l a r"}} &\<open>\<equiv>\<close>& @{term[source] "Node Black l a r"}
-\end{tabular}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Color}
-\pause
-
-@{const color} \<open>::\<close> @{typ "'a rbt \<Rightarrow> color"}\\\smallskip\pause
-\high{@{thm color.simps(1)}}\\
-\high{@{thm (dummy_pats) color.simps(2)}}
-\bigskip\pause
-
-@{const paint} \<open>::\<close> @{typ "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"}\\\smallskip\pause
-\high{@{thm paint.simps(1)}}\\
-\high{@{thm (dummy_pats) paint.simps(2)}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Invariants}
-\pause
-
-@{const rbt} \<open>::\<close> @{typ "'a rbt \<Rightarrow> bool"}\\\smallskip\pause
-\high{@{thm rbt_def}}
-\bigskip\pause
-
-@{const invc} \<open>::\<close> @{typ "'a rbt \<Rightarrow> bool"}\\\smallskip\pause
-\high{@{thm [break,margin=50] (dummy_pats) invc.simps}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Invariants}
-
-@{const invh} \<open>::\<close> @{typ "'a rbt \<Rightarrow> bool"}\\\smallskip\pause
-\high{@{thm [break,margin=55] (dummy_pats) invh.simps}}
-\bigskip\pause
-
-@{const bheight} \<open>::\<close> @{typ "'a rbt \<Rightarrow> nat"}\\\smallskip\pause
-\high{@{thm [break,margin=55] (dummy_pats) bheight.simps}}
-\end{frame}
-%-------------------------------------------------------------
-%\begin{frame}{Exercise}
-%\begin{center}
-%\bad{Is @ {const invh} what we want?}
-%\end{center}
-%\pause
-%
-%Define a function \ \high{@ {const Bpl} \<open>::\<close> @ {typ "'a rbt \<Rightarrow> nat set"}}\\
-%such that @ {term "Bpl t"} (``black path lengths'')
-%is the set of all \<open>n\<close> such that there is a path
-%from the root of \<open>t\<close> to a leaf that contains exactly \<open>n\<close> black nodes.
-%\pause\medskip
-%
-%Prove \ \high{@ {thm invh_Bpl}}
-%\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Logarithmic height}
-\begin{lemma}
-@{thm rbt_height_le}
-\end{lemma}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Insertion}
-
-@{const insert} \<open>::\<close> @{typ "'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"}\\\smallskip\pause
-\high{@{thm insert_def}}
-\bigskip\pause
-
-@{const ins} \<open>::\<close> @{typ "'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"}\\\smallskip\pause
-\high{@{thm ins.simps(1)}}\pause\vspace{-1ex}
-\high{@{thm[display] (dummy_pats) ins.simps(2)}}\pause\vspace{-1ex}
-\high{@{thm[display] (dummy_pats) ins.simps(3)}}
-
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Adjusting colors}
-@{const baliL}, @{const baliR} \<open>::\<close> @{typ "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"}
-\begin{itemize}
-\pause
-\item Combine arguments \<open>l\<close> \<open>a\<close> \<open>r\<close> into tree, ideally \<open>\<langle>l, a, r\<rangle>\<close>
-\pause
-\item Treat invariant violation \bad{Red-Red} in \<open>l\<close>/\<open>r\<close>\\\pause
-\high{@{term (sub) "baliL (R (R t1 a1 t2) a2 t3) a3 t4"}\\
-\quad \<open>=\<close> @{term (sub) "R (B t1 a1 t2) a2 (B t3 a3 t4)"}}
-\pause
-
-\high{@{term (sub) "baliL (R t1 a1 (R t2 a2 t3)) a3 t4"}\\
-\quad \<open>=\<close> @{term (sub) "R (B t1 a1 t2) a2 (B t3 a3 t4)"}}
-\pause
-\item Principle: replace \bad{Red-Red} by \high{Red-Black}
-\pause
-\item Final equation: \\\pause
-\high{@{prop (sub) "baliL l a r = B l a r"}}
-\pause
-\item Symmetric: @{const baliR}
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-%\begin{frame}{Correctness via sorted lists}
-%\pause
-%\begin{lemma}
-%\high{@ {thm inorder_baliL}}\\
-%\high{@ {thm inorder_baliR}}
-%\end{lemma}
-%\pause
-%\begin{lemma}
-%\high{@ {thm[break,margin=60] inorder_ins}}
-%\end{lemma}
-%\pause
-%\begin{corollary}
-%\high{@ {thm[break,margin=60] inorder_insert}}
-%\end{corollary}
-%\bigskip\pause
-%
-%Proofs easy!
-%\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Preservation of invariant}
-\begin{theorem}
-\high{@{thm rbt_insert}}
-\end{theorem}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Deletion}
-
-\high{@{thm delete_def}}
-\bigskip\pause
-
-\high{@{thm [break,margin=55](dummy_pats) del.simps}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Deletion}
-Tricky functions: \high{@{const baldL}, @{const baldR}, @{const combine}}
-\bigskip\pause
-
-Tricky invariant preservation lemmas, eg
-
-\high{@{thm [display,margin=55] del_invc_invh}}
-\pause
-
-\begin{theorem}
-\high{@{thm rbt_delete}}
-\end{theorem}
-\end{frame}
-%-------------------------------------------------------------
-
-\begin{isabellebody}%
-*}
-(*<*)
-end
-(*>*)
--- a/Slides/Sorting_Slides.thy~	Tue Jul 04 16:33:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,205 +0,0 @@
-(*<*)
-theory Sorting_Slides
-imports
-  FDSlatex
-  "../Material/Thys/Sorting"
-begin
-
-definition dummyid :: "'a \<Rightarrow> 'a" where
-"dummyid x = x"
-
-notation (latex output) dummyid ("_")
-
-lemma sorted_Cons: "sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> dummyid y) & sorted xs)"
-by(simp add: dummyid_def)
-
-lemmas sorted_simps = sorted.simps(1) sorted_Cons
-
-lemma merge_simp2: "merge xs [] = xs"
-by (cases xs) auto
-(*>*)
-text_raw{*
-\end{isabellebody}%
-%-------------------------------------------------------------
-\section{Correctness}
-%-------------------------------------------------------------
-\begin{frame}
-\high{@{const sorted} \<open>::\<close> @{typ[source]"('a::linorder) list \<Rightarrow> bool"}}
-\pause
-\high{@{thm[display] sorted_simps}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of sorting}
-Specification of \<open>sort ::\<close> @{typ[source] "('a::linorder) list \<Rightarrow> 'a list"}:
-\begin{center}
-\high{@{prop "sorted (sort xs)"}}
-\end{center}
-\pause
-Is that it? \pause How about
-\begin{center}
-@{prop "set (sort xs) = set xs"}
-\end{center}
-\pause
-Better: every \<open>x\<close> occurs as often in @{term "sort xs"} as in \<open>xs\<close>.
-\pause\medskip
-
-More succinctly:
-\begin{center}
-\high{@{prop "mset (sort xs) = mset xs"}}
-\end{center}
-where \high{@{const_typ mset}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{What are multisets?}
-\pause
-\begin{center}
-\high{Sets with (possibly) repeated elements}
-\end{center}
-\pause
-Some operations:\medskip
-
-\begin{tabular}{rcl}
-\high{@{const Mempty}} &\<open>::\<close>& @{typ "'a multiset"}\\
-\high{@{const add_mset}} &\<open>::\<close>& @{typ "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"}\\
-\high{\<open>+\<close>} &\<open>::\<close>& @{typ "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"}\\\pause
-\high{@{const mset}} &\<open>::\<close>& @{typ "'a list \<Rightarrow> 'a multiset"}\\
-\high{@{const set_mset}} &\<open>::\<close>& @{typ "'a multiset \<Rightarrow> 'a set"}\\
-\end{tabular}
-\end{frame}
-%-------------------------------------------------------------
-\section{Insertion Sort}
-%-------------------------------------------------------------
-\thyfile{Thys/Sorting}{Insertion sort correctness}
-%-------------------------------------------------------------
-\section{Time}
-%-------------------------------------------------------------
-\begin{frame}{Principle: Count function calls}
-\pause
-\begin{tabular}{@ {}ll@ {}}
-For every function & \ \<open>f :: \<tau>\<^sub>1 \<Rightarrow> ... \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>\<close>\\
-define a \concept{timing function} & \high{\<open>t_f :: \<tau>\<^sub>1 \<Rightarrow> ... \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> nat\<close>}:
-\end{tabular}
-\smallskip\pause
-Translation of defining equations:
-\[
-\frac{e \leadsto \high{e'}}{f\,p_1 \dots p_n = e ~\leadsto~ \high{t\_f\,p_1 \dots p_n = e' + 1}}
-\]
-\pause
-
-Translation of expressions:
-\[ \frac{s_1 \leadsto \high{t_1} \quad \dots \quad s_k \leadsto \high{t_k}}
-   {g\,s_1 \dots s_k \leadsto \high{t_1 + \dots + t_k + t\_g\, s_1 \dots s_k}}
-\]
-\pause
-\begin{itemize}
-\item
-Variable $\leadsto$ 0, Constant $\leadsto$ 0
-\pause
-\item
-Constructor calls and primitive operations on @{typ bool} and numbers cost 1
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Example}
-\<open>app [] ys = ys\<close>\\
-\pause$\leadsto$\\
-\high{\<open>t_app [] ys = 0 + 1\<close>}\\
-\pause\bigskip
-
-\<open>app (x#xs) ys = x # app xs ys\<close>\\
-\pause$\leadsto$\\
-\high{\<open>t_app (x#xs) ys = 0 + (0 + 0 + t_app xs ys) + 1 + 1\<close>}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{A compact formulation of $e \leadsto t$}
-\pause
-\begin{center}
-\begin{tabular}{l}
-\high{\<open>t\<close>} \ is the sum of all \high{\<open>t_g s\<^sub>1 ... s\<^sub>k\<close>}\\
-such that \<open>g s\<^sub>1 ... s\<^sub>n\<close> is a subterm of \<open>e\<close>
-\end{tabular}
-\end{center}
-\pause\smallskip
-
-If $g$ is
-\begin{itemize}
-\item a constructor or
-\item a predefined function on @{typ bool} or numbers
-\end{itemize}
-then \<open>t_g ... = 1\<close>.
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{\emph{if} and \emph{case}}
-\pause
-\begin{center}
-So far we model a call-by-value semantics
-\end{center}
-\pause
-Conditionals and case expressions are evaluated \bad{lazily}.
-\smallskip\pause
-
-Translation:
-\[ \frac{b \leadsto \high{t} \quad s_1 \leadsto \high{t_1} \quad s_2 \leadsto \high{t_2}}
-   {\textit{if } b \textit{ then } s_1 \textit{ else } s_2 \leadsto \high{t + (\textit{if } b \textit{ then } t_1 \textit{ else } t_2)}}
-\]
-\pause
-Similarly for \emph{case}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{$O(.)$ is enough}
-\pause
-$\Longrightarrow$ Reduce all additive constants to 1
-\pause
-\begin{example}
-\high{\<open>t_app (x#xs) ys = t_app xs ys + 1\<close>}
-\end{example}
-%\bigskip\pause
-
-%$\Longrightarrow$ May start with 0 instead of 1 in base case
-%\pause
-%\begin{example}
-%\high{\<open>t_app [] ys = 0\<close>}
-%\end{example}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Discussion}
-\begin{itemize}
-\pause
-\item
-The definition of \<open>t_f\<close> from \<open>f\<close> can be automated.
-\pause
-\item
-The correctness of \<open>t_f\<close> could be proved w.r.t.\\ a semantics
-that counts computation steps.
-\pause
-\item
-Precise complexity bounds (as opposed to $O(.)$)
-would require a formal model of (at least) the compiler and the hardware.
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\thyfile{Thys/Sorting}{Insertion sort complexity}
-%-------------------------------------------------------------
-\section{Merge Sort}
-%-------------------------------------------------------------
-\begin{frame}
-@{const_typ merge}\smallskip\\
-\pause
-\high{@{thm merge.simps(1)}}\\
-\high{@{thm merge_simp2}}\\
-\pause
-\high{@{thm[break,margin=60] merge.simps(3)}}
-\bigskip\pause
-
-@{const_typ msort}\smallskip\\
-\pause
-\high{@{thm[break,margin=60] msort.simps}}
-\end{frame}
-%-------------------------------------------------------------
-\thyfile{Thys/Sorting}{Merge sort}
-%-------------------------------------------------------------
-\begin{isabellebody}%
-*}
-(*<*)
-end
-(*>*)
--- a/Slides/Tree_Slides.thy~	Tue Jul 04 16:33:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(*<*)
-theory Tree_Slides
-imports
-  Tree_Notation
-  "../Material/Thys/Tree_Additions"
-begin
-
-lemma size_Node: "size(Node l a r) = size l + size r + 1"
-by simp
-
-lemmas size_simps = tree.size(3) size_Node
-
-(* TODO: SOS *)
-(*>*)
-text_raw{*
-\end{isabellebody}%
-\section{Binary Trees}
-%-------------------------------------------------------------
-\ttfilepage{HOL/Library/Tree.thy\\ Thys/Tree\char`\_Additions.thy}{}
-%-------------------------------------------------------------
-\begin{frame}{Binary trees}
-\begin{center}
-\isakeyword{datatype} \high{@{text "'a tree = Leaf | Node ('a tree) 'a ('a tree)"}}
-\end{center}
-\pause
-
-Abbreviations:
-\begin{tabular}{rcl}
-\high{@{const Leaf}} &\<open>\<equiv>\<close>& @{text Leaf}\\\pause
-\high{@{term "\<langle>l, a, r\<rangle>"}} &\<open>\<equiv>\<close>& @{text "Node l a r"}
-\end{tabular}
-%\pause\medskip
-
-%Terminology:
-%\begin{tabular}{rcl}
-%\high{leaf} & means & @ {text Leaf}\\\pause
-%\high{node} & means & @ {const Node}\\\pause
-%\high{leaf node} & means & @ {term"Node Leaf a Leaf"}
-%\end{tabular}
-\pause\vfill
-\begin{center}
-Most of the time: \high{tree = binary tree}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\section{Basic Functions}
-%-------------------------------------------------------------
-\begin{frame}{Tree traversal}
-@{const_typ inorder}\\\smallskip\pause
-\high{@{thm inorder.simps(1)}}\\
-\high{@{thm inorder.simps(2)}}
-\bigskip\pause
-
-@{const_typ preorder}\\\smallskip\pause
-\high{@{thm preorder.simps(1)}}\\
-\high{@{thm preorder.simps(2)}}
-\bigskip\pause
-
-@{const_typ postorder}\\\smallskip\pause
-\high{@{thm postorder.simps(1)}}\\
-\high{@{thm postorder.simps(2)}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Size}
-
-@{const size} \<open>::\<close> @{typ "'a tree \<Rightarrow> nat"}\\\smallskip\pause
-\high{@{thm size_simps(1)}}\\
-\high{@{thm size_simps(2)[of _ DUMMY]}}
-\bigskip\pause
-
-@{const_typ size1}\\\pause
-\high{@{thm size1_def}}\\
-\bigskip\pause
-
-\<open>\<Longrightarrow>\<close>\\
-@{thm size1_simps(1)}\\
-@{thm size1_simps(2)}
-\bigskip\pause
-
-\textbf{Lemma} The number of leaves in \<open>t\<close> is @{term"size1 t"}.
-\bigskip\pause
-
-\bad{Warning: \<open>|.|\<close> and \<open>|.|\<^sub>1\<close> only on slides}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Height}
-
-@{const height} \<open>::\<close> @{typ "'a tree \<Rightarrow> nat"}\\\smallskip\pause
-\high{@{thm height_tree.simps(1)}}\\
-\high{@{thm height_tree.simps(2)[of l DUMMY r]}}
-\pause
-\begin{center}
-\bad{Warning: \<open>h(.)\<close> only on slides}
-\end{center}
-\pause
-
-\textbf{Lemma} @{thm height_le_size_tree}
-\bigskip\pause
-
-\textbf{Lemma} @{thm size1_height}
-\end{frame}
-%-------------------------------------------------------------
-%\thyfile{Thys/Tree\char`\_Additions}{@{thm size1_height}}
-%-------------------------------------------------------------
-\begin{frame}{Minimal height}
-@{const_typ min_height}\\\smallskip\pause
-\high{@{thm min_height.simps(1)}}\\
-\high{@{thm min_height.simps(2)[of l DUMMY r]}}
-\pause
-\begin{center}
-\bad{Warning: \<open>mh(.)\<close> only on slides}
-\end{center}
-\pause
-
-\textbf{Lemma} @{thm min_height_le_height}
-\bigskip\pause
-
-\textbf{Lemma} @{thm min_height_size1}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Internal path length}
-\pause
-\begin{center}
-The sum of the lengths of the (simpl) paths\\ from the root to any other node
-\end{center}
-\pause
-
-@{const_typ ipl}\\\smallskip\pause
-\high{@{thm ipl.simps(1)}}\\
-\high{@{thm ipl.simps(2)[of l DUMMY r]}}
-\vfill\pause
-\begin{center}
-Why relevant?
-\pause\bigskip
-
-Upper bound?
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\section{Complete and Balanced Trees}
-%-------------------------------------------------------------
-\begin{frame}{Complete tree}
-@{const_typ complete}\\\pause
-\high{@{thm[break,margin=50] (dummy_pats) complete.simps}}
-\bigskip\pause
-
-\textbf{Lemma} @{thm complete_iff_height}
-\bigskip\pause
-
-\textbf{Lemma} @{thm size1_if_complete}
-%Proof by induction; induction-free proof: 2^mh(t) <= size1 t <= 2^h(t)
-\bigskip\pause
-
-\textbf{Lemma} @{thm complete_if_size1_height}
-\pause
-
-\textbf{Lemma} @{thm complete_if_size1_min_height}
-\bigskip\pause
-
-\textbf{Corollary} @{thm size1_height_if_incomplete}
-\pause
-
-\textbf{Corollary} @{thm min_height_size1_if_incomplete}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Complete tree: @{const ipl}}
-\textbf{Lemma} A complete tree of height \<open>h\<close> has internal path length
-\high{@{term "(h - 2)*2^h + 2"}}.
-\bigskip\pause
-
-In a search tree, finding the node labelled \<open>x\<close>
-takes as many steps as the path from the root to \<open>x\<close> is long.
-\pause
-
-Thus the average time to find an element that is in the tree is
-\high{@{term "ipl t"} \<open>/\<close> @{term "size(t::'a tree)"}}.
-\bigskip\pause
-
-\textbf{Lemma} Let \<open>t\<close> be a complete search tree of height \<open>h\<close>.
-\pause
-The average time to find a random element that is in the tree
-is asymptotically \high{\<open>h - 2\<close>} (as \<open>h\<close> approaches \<open>\<infinity>\<close>):\pause
-\begin{center}
-\high{@{term "ipl t"} \<open>/\<close> @{term "size(t::'a tree)"} \<open>\<sim>\<close> @{term"h-2::int"}}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Complete tree: @{const ipl}}
-A problem: \high{@{term "(h - 2)*2^h + 2"}} is only correct if interpreted
-over type \high{@{typ int}}, not \bad{@{typ nat}}.
-\bigskip\pause
-
-Correct version:
-
-\textbf{Lemma} @{thm (prem 1) ipl_if_complete_int} \<open>\<Longrightarrow>\<close>
-\mbox{@{thm (concl) ipl_if_complete_int}}
-\vfill\pause
-
-We do not cover the Isabelle formalization of limits.
-
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Balanced tree}
-@{const_typ balanced}\\\smallskip\pause
-\high{@{thm balanced_def}}
-\bigskip\pause
-
-Balanced trees have optimal height:\\
-\textbf{Lemma} @{thm[mode=IfThen] balanced_optimal}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Warning}
-\begin{itemize}
-\item The terms \bad{\emph{complete}} and \bad{\emph{balanced}}\\
- are not defined uniquely in the literature.
-\bigskip\pause
-
-\item For example,\\
-Knuth calls \bad{\emph{complete}} what we call \bad{\emph{balanced}}.
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{isabellebody}%
-*}
-(*<*)
-end
-(*>*)
--- a/Slides/Trie_Slides.thy~	Tue Jul 04 16:33:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,223 +0,0 @@
-(*<*)
-theory Trie_Slides
-imports
-  FDSlatex
-  "../Material/Thys/Trie2"
-begin
-(*>*)
-text_raw{*
-\end{isabellebody}%
-%-------------------------------------------------------------
-\section{Tries and Patricia Tries}
-%-------------------------------------------------------------
-\ttfilepage{Thys/Trie1\\Thys/Trie2}{}
-%-------------------------------------------------------------
-\begin{frame}{Trie}
-\framesubtitle{[Fredkin, CACM 1960]}
-Name: \emph{reTRIEval}
-\pause
-\begin{itemize}
-\item
-Tries are search trees indexed by lists.
-\pause
-\item
-Each node maps the next element in the list\\ to a subtrie.
-\pause
-\item
-For simplicity we consider only binary tries:
-\high{@{datatype[display] trie}}
-\end{itemize}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Patricia trie}
-\framesubtitle{[Morrison, JACM 1968]}
-Sequences of edges without branching are compressed
-\pause
-\high{@{datatype[display,margin=60] ptrie}}
-\pause
-
-Name: PATRICIA = \emph{Practical Algorithm To Retrieve Information Coded in Alphanumeric}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{From trie to Patricia trie}
-\framesubtitle{and beyond}
-\pause
-\begin{center}
-\Large An exercise in data refinement
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\subsection{Data Refinement Basics}
-%-------------------------------------------------------------
-\begin{frame}{Data refinement}
-How to implement an abstract type \<open>A\<close> by a concrete (``refined'') type \<open>C\<close>
-with \high{invariant \<open>inv\<^sub>C :: C \<Rightarrow> bool\<close>}:
-\begin{itemize}
-\pause
-\item
-Define an \high{abstraction function \<open>abs\<^sub>C :: C \<Rightarrow> A\<close>}
-\pause
-\item Implement each interface function \<open>f\<^sub>A\<close> on \<open>A\<close>\\ by some \<open>f\<^sub>C\<close> on \<open>C\<close>
-\pause
-\item Prove that each \<open>f\<^sub>C\<close> implements \<open>f\<^sub>A\<close>:\\
-\high{\<open>inv\<^sub>C t \<Longrightarrow> abs\<^sub>C (f\<^sub>C t) = f\<^sub>A (abs\<^sub>C t)\<close>}\\\pause
-and preserves the invariant:\\
-\high{\<open>inv\<^sub>C t \<Longrightarrow> inv\<^sub>C (f\<^sub>C t)\<close>}
-\end{itemize}
-\pause
-The \<open>f\<close>\,s may take more parameters\\\pause
- and may return values not of type \<open>A\<close>/\<open>C\<close>.
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Data refinement}
-\begin{center}
-\high{Multiple refinement steps can help\\
-to reduce the complexity of correctness proofs}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\subsection{Trie}
-%-------------------------------------------------------------
-\begin{frame}{Trie}
-\high{@{datatype[display] trie}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Trie @{const isin}}
-@{thm isin.simps(1)}\pause
-@{thm[display,margin=60] isin.simps(2)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Trie @{const insert}}
-@{thm insert.simps(1)}\\\pause
-@{thm insert.simps(2)}\\\pause
-@{thm[display,margin=60] insert.simps(3)}\pause
-@{thm[break,margin=60] insert.simps(4)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of \<open>trie\<close> w.r.t. \<open>set\<close>}
-\begin{center}
-\high{@{thm isin_insert}}
-\end{center}
-\pause
-Note: @{const isin} doubles as abstraction function
-\end{frame}
-%-------------------------------------------------------------
-\subsection{Patricia Trie}
-%-------------------------------------------------------------
-\begin{frame}{Patricia trie}
-\high{@{datatype[display,margin=60] ptrie}}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{@{const isinP}}
-@{thm isinP.simps(1)}\pause
-@{thm[display,margin=60] isinP.simps(2)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Splitting lists}
-\high{@{prop "split xs ys = (zs,xs',ys')"}}\\\pause
-iff \<open>zs\<close> is the longest common prefix of \<open>xs\<close> and \<open>ys\<close>\\\pause
-and \<open>xs'\<close>/\<open>ys'\<close> is the remainder of \<open>xs\<close>/\<open>ys\<close>
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{@{const insertP}}
-\pause
-\small
-@{thm[break,margin=60] insertP.simps(2)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{@{const_typ abs_ptrie}}
-\pause
-\high{@{thm abs_ptrie.simps(1)}}
-\pause
-\high{@{thm[display] abs_ptrie.simps(2)}}
-\pause
-@{const_typ prefix_trie}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of @{typ ptrie} w.r.t. @{typ trie}}
-\begin{center}
-\high{@{thm isinP}}
-\bigskip\pause
-
-\high{@{thm abs_ptrie_insertP}}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\subsection{Patricia Trie for Words}
-%-------------------------------------------------------------
-\begin{frame}{Patricia trie for words}
-\framesubtitle{[Okasaki \& Gill, 1998]}
-\high{@{datatype[display,margin=50] ptrieW}}
-\bigskip\pause
-
-@{const_typ to_bl}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{@{const isinW}}
-@{thm isinW.simps(1)}\pause
-@{thm[display,margin=60] isinW.simps(2)}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Correctness of @{typ ptrie} w.r.t. @{typ trie}}
-\begin{center}
-\high{@{thm[display,margin=60] isinW_correct}}
-\end{center}
-\pause
-Proof uses intermedidate version of Patricia trie for lists
-where nodes contain complete prefixes (@{const isinL}).
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Refinement hierarchy}
-\begin{center}
-\begin{tabular}{cl}
-@{typ trie}\\
-$\uparrow$ & @{const abs_ptrie}\\
-@{typ ptrie}\\
-$\uparrow$ & @{const abs_ptrieL}\\
-@{typ ptrieL}\\
-$\uparrow$ & @{const abs_ptrieW}\\
-@{typ ptrieW}\\[1ex]
-\multicolumn{2}{l}{\pause where @{typ ptrieL} \<open>=\<close> @{typ ptrie}}
-\end{tabular}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{\mbox{@{const_typ inv_ptrieW}}}
-\pause
-\high{@{thm inv_ptrieW.simps(1)}}
-\pause
-\high{@{thm[display,margin=60] inv_ptrieW.simps(2)}}
-\pause
-@{thm[display,margin=50] inv_pref_def}
-\pause
-@{thm[break,margin=60] inv_mask_def}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{\mbox{@{const_typ abs_ptrieW}}}
-\pause
-\high{@{thm abs_ptrieW.simps(1)}}
-\pause
-\high{@{thm[display] abs_ptrieW.simps(2)}}
-\pause
-@{thm[display,margin=60] abs_pmb_def}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{\mbox{@{text insertW}}}
-\begin{center}
-\Large\bad{?}
-\end{center}
-\end{frame}
-%-------------------------------------------------------------
-\begin{frame}{Further space optimization?}
-\pause
-\textbf{datatype} \<open>ptrieW2 =\<close>\\
-\quad \<open>LeafW2\<close> ~$|$\\
-\quad \<open>SingW2 (32 word)\<close> ~$|$\\
-\quad \<open>NodeW2 (32 word) (32 word) (ptrieW2 \<times> ptrieW2)\<close>
-\end{frame}
-%-------------------------------------------------------------
-\begin{isabellebody}%
-*}
-(*<*)
-end
-(*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/main.tex	Tue Jul 04 16:34:18 2017 +0200
@@ -0,0 +1,39 @@
+\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}
+\subtitle{with Isabelle/HOL}
+\author{Tobias Nipkow}
+\institute[]{%
+	Fakult\"at f\"ur Informatik\\
+	Technische Universit\"at M\"unchen}
+\date{\the\year-\the\month-\the\day}
+\frame{\titlepage}
+\subtitle{}
+
+\mypartpage{II}{Functional Data Structures}
+\setcounter{part}{5}
+\part{Sorting}
+\input{Sorting_Slides}
+\part{Binary Trees}
+\input{Tree_Slides}
+\part{Search Trees}
+\input{Search_Trees}
+\input{Tree23_Slides}
+\input{RBT_Slides}
+\input{Trie_Slides}
+\part{Priority Queues}
+\input{Leftist_Heap_Slides}
+\input{Braun_Tree_Slides}
+%\input{Binomial_Tree_Slides}
+
+%Amortized:
+%\input{Skew_Heap_Slides}
+\end{document}
--- a/Slides/document/root.tex	Tue Jul 04 16:33:55 2017 +0200
+++ b/Slides/document/root.tex	Tue Jul 04 16:34:18 2017 +0200
@@ -1,43 +1,3 @@
-\documentclass[14pt
-%,handout%
-]{beamer}
-
-\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}
+\documentclass[14pt]{beamer}
+\input{main}
 
-\title{Functional Data Structures}
-\subtitle{with Isabelle/HOL}
-\author{Tobias Nipkow}
-\institute[]{%
-	Fakult\"at f\"ur Informatik\\
-	Technische Universit\"at M\"unchen}
-\date{\the\year-\the\month-\the\day}
-\frame{\titlepage}
-\subtitle{}
-
-\mypartpage{II}{Functional Data Structures}
-\setcounter{part}{5}
-\part{Sorting}
-\input{Sorting_Slides}
-\part{Binary Trees}
-\input{Tree_Slides}
-\part{Search Trees}
-\input{Search_Trees}
-\input{Tree23_Slides}
-\input{RBT_Slides}
-\input{Trie_Slides}
-\part{Priority Queues}
-\input{Leftist_Heap_Slides}
-\input{Braun_Tree_Slides}
-%\input{Binomial_Tree_Slides}
-
-%Amortized:
-%\input{Skew_Heap_Slides}
-\end{document}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/root_amor.tex	Tue Jul 04 16:34:18 2017 +0200
@@ -0,0 +1,19 @@
+\documentclass[14pt
+%,handout%
+]{beamer}
+
+\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}
+
+\input{session}
+
+%Amortized:
+%\input{Skew_Heap_Slides}
+\end{document}
--- a/Slides/document/root_handout.tex	Tue Jul 04 16:33:55 2017 +0200
+++ b/Slides/document/root_handout.tex	Tue Jul 04 16:34:18 2017 +0200
@@ -1,43 +1,2 @@
-\documentclass[14pt
-,handout%
-]{beamer}
-
-\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}
-\subtitle{with Isabelle/HOL}
-\author{Tobias Nipkow}
-\institute[]{%
-	Fakult\"at f\"ur Informatik\\
-	Technische Universit\"at M\"unchen}
-\date{\the\year-\the\month-\the\day}
-\frame{\titlepage}
-\subtitle{}
-
-\mypartpage{II}{Functional Data Structures}
-\setcounter{part}{5}
-\part{Sorting}
-\input{Sorting_Slides}
-\part{Binary Trees}
-\input{Tree_Slides}
-\part{Search Trees}
-\input{Search_Trees}
-\input{Tree23_Slides}
-\input{RBT_Slides}
-\input{Trie_Slides}
-\part{Priority Queues}
-\input{Leftist_Heap_Slides}
-\input{Braun_Tree_Slides}
-%\input{Binomial_Tree_Slides}
-
-%Amortized:
-%\input{Skew_Heap_Slides}
-\end{document}
+\documentclass[14pt,handout]{beamer}
+\input{main}