--- a/ROOT Wed Aug 02 17:11:04 2017 +0200
+++ b/ROOT Wed Aug 02 17:11:23 2017 +0200
@@ -37,6 +37,16 @@
"root_handout.tex"
"main.tex"
"prelude.tex"
+ "clrsrbti1.pdf"
+ "clrsrbti2.pdf"
+ "clrsrbti3.pdf"
+ "clrsrbti4.pdf"
+ "clrsrbtd1.pdf"
+ "clrsrbtd2.pdf"
+ "clrsrbtd3.pdf"
+ "clrsrbtd4.pdf"
+ "clrsrbtd5.pdf"
+ "clrsrbtd6.pdf"
session Slides_Heaps in Slides = "HOL-FDS17" +
@@ -84,3 +94,13 @@
document_files
"root_mod.tex"
"prelude.tex"
+ "clrsrbti1.pdf"
+ "clrsrbti2.pdf"
+ "clrsrbti3.pdf"
+ "clrsrbti4.pdf"
+ "clrsrbtd1.pdf"
+ "clrsrbtd2.pdf"
+ "clrsrbtd3.pdf"
+ "clrsrbtd4.pdf"
+ "clrsrbtd5.pdf"
+ "clrsrbtd6.pdf"
--- a/Slides/RBT_Slides.thy Wed Aug 02 17:11:04 2017 +0200
+++ b/Slides/RBT_Slides.thy Wed Aug 02 17:11:23 2017 +0200
@@ -29,7 +29,7 @@
\end{isabellebody}%
\section{Red-Black Trees}
%-------------------------------------------------------------
-\thyfile{Thys/RBT\char`_Set}{}
+\ifMOD\else\thyfile{Thys/RBT\char`_Set}{}\fi
%-------------------------------------------------------------
\begin{frame}{Relationship to 2-3-4 trees}
Idea:
@@ -53,6 +53,7 @@
\end{center}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{Invariants}
\begin{itemize}
\pause
@@ -67,6 +68,7 @@
\pause\invisible<handout>{Black nodes.}
\end{itemize}
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}{Red-black trees}
@{datatype [display] color}
@@ -199,11 +201,22 @@
%\end{frame}
%-------------------------------------------------------------
\begin{frame}{Preservation of invariant}
+After 14 simple lemmas:
+
\begin{theorem}
\high{@{thm rbt_insert}}
\end{theorem}
\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}
+
+\includegraphics[scale=0.2,angle=90]{clrsrbti1} \hspace{-1em}
+\includegraphics[scale=0.2,angle=90]{clrsrbti2}
+\end{frame}
+%-------------------------------------------------------------
\begin{frame}{Deletion}
\high{@{thm delete_def}}
@@ -214,9 +227,9 @@
%-------------------------------------------------------------
\begin{frame}{Deletion}
Tricky functions: \high{@{const baldL}, @{const baldR}, @{const combine}}
-\bigskip\pause
+\medskip\pause
-Tricky invariant preservation lemmas, eg
+12 short but tricky to find invariant lemmas with short proofs. The worst:
\high{@{thm [display,margin=55] del_invc_invh}}
\pause
@@ -226,6 +239,18 @@
\end{theorem}
\end{frame}
%-------------------------------------------------------------
+\begin{frame}{Code and proof in CLRS}
+\vspace{-2em}
+\hspace{-1em} \includegraphics[scale=0.2]{clrsrbtd1} \hspace{-1em}
+\hspace{-1em} \includegraphics[scale=0.2]{clrsrbtd2} \hspace{-1em}
+\includegraphics[scale=0.2]{clrsrbtd3}
+\vspace{-3em}
+
+\hspace{-1em} \includegraphics[scale=0.2]{clrsrbtd4} \hspace{-1em}
+\hspace{-1em} \includegraphics[scale=0.2]{clrsrbtd5} \hspace{-1em}
+\includegraphics[scale=0.2]{clrsrbtd6}
+\end{frame}
+%-------------------------------------------------------------
\begin{isabellebody}%
*}
--- a/Slides/Sorting_Slides.thy Wed Aug 02 17:11:04 2017 +0200
+++ b/Slides/Sorting_Slides.thy Wed Aug 02 17:11:23 2017 +0200
@@ -60,6 +60,9 @@
\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}
+\bigskip\pause
+
+Import \texttt{"~~/src/HOL/Library/Multiset"}
\end{frame}
%-------------------------------------------------------------
\section{Insertion Sort}
--- a/Slides/Tree23_Slides.thy Wed Aug 02 17:11:04 2017 +0200
+++ b/Slides/Tree23_Slides.thy Wed Aug 02 17:11:23 2017 +0200
@@ -5,8 +5,14 @@
"~~/src/HOL/Data_Structures/Tree23_Set"
begin
+lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
+by (induction t) auto
+
notation height ("h'(_')" 100)
+abbreviation (latex output) tree23_size :: "'a tree23 \<Rightarrow> nat" ("|_|") where
+"tree23_size \<equiv> size"
+
lemma del_simp4: "l \<noteq> Leaf \<Longrightarrow> r \<noteq> Leaf \<Longrightarrow> del x (Node2 l a r) =
(case cmp x a of
LT \<Rightarrow> node21 (del x l) a r |
@@ -19,7 +25,7 @@
%-------------------------------------------------------------
\section{2-3 Trees}
%-------------------------------------------------------------
-\thyfile{HOL/Data\char`_Structures/Tree23\char`_Set}{}
+\ifMOD\else\thyfile{HOL/Data\char`_Structures/Tree23\char`_Set}{}\fi
%-------------------------------------------------------------
\begin{frame}{2-3 Trees}
\high{@{datatype[display,margin=55] tree23}}
@@ -35,21 +41,27 @@
\end{center}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{@{const isin}}
\high{@{thm[display,margin=25]isin.simps(3)}}
\pause
Assumes the usual ordering invariant
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}{Invariant @{const bal}}
All leaves are at the same level:
-\pause
+\ifMOD\else\pause\fi
\high{@{thm[display,margin=55]bal.simps(1)}}
+\ifMOD\else\pause\fi
+\high{@{thm bal.simps(2)[of _ DUMMY]}}
+\ifMOD\else\pause\fi
+\high{@{thm[display,margin=55]bal.simps(3)[of _ DUMMY _ DUMMY]}}
\pause
-\high{@{thm bal.simps(2)[of _ DUMMY]}}
-\pause
-\high{@{thm[display,margin=55]bal.simps(3)[of _ DUMMY _ DUMMY]}}
+\begin{lemma}
+@{thm ht_sz_if_bal}
+\end{lemma}
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Insertion}
@@ -91,6 +103,7 @@
@{const_typ ins}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{Insertion}
\high{@{thm ins.simps(1)}}
\smallskip\pause
@@ -98,6 +111,7 @@
\high{@{thm (lhs,sub) ins.simps(2)} \<open>=\<close>}\\\pause
\high{@{thm [break,margin=60] (rhs,sub) ins.simps(2)}}
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}{Insertion}
\high{@{thm (lhs,sub) ins.simps(3)} \<open>=\<close>}\\\pause
@@ -106,7 +120,7 @@
%-------------------------------------------------------------
\begin{frame}{Insertion preserves @{const bal}}
\begin{lemma}
-\high{\alt<1-4>{@{prop"bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t))"}}{@{thm bal_ins}}}
+\high{\alt<5->{@{thm bal_ins}}{@{prop"bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t))"}}}
\smallskip
\onslide<3->
@@ -115,8 +129,10 @@
@{thm [break]height_up\<^sub>i.simps}
\end{lemma}
\onslide<2->
-\textbf{Proof} by induction on \<open>t\<close>
-\bigskip\onslide<6->
+\textbf{Proof} by induction on \<open>t\<close>.
+\onslide<6->
+Step automatic.
+\bigskip\onslide<7->
\begin{corollary}
\high{@{thm bal_insert}}
\end{corollary}
@@ -158,6 +174,7 @@
@{const_typ del}
\end{frame}
%-------------------------------------------------------------
+\ifMOD\else
\begin{frame}{Deletion}
@{thm del.simps(1)}
\smallskip\pause
@@ -167,16 +184,20 @@
@{thm (lhs) del.simps(3)} \<open>= ...\<close>
\end{frame}
+\fi
%-------------------------------------------------------------
\begin{frame}
\high{@{thm[display,margin=60] (concl) del_simp4}}
\pause
@{thm[display,margin=60] (sub) node21.simps}
-\pause
-@{thm[display,margin=60] (sub) node22.simps}
+%\pause
+%@ {thm[display,margin=60] (sub) node22.simps}
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Deletion preserves @{const bal}}
+\pause
+After 13 simple lemmas:
+
\begin{lemma}
\high{@{thm bal_tree\<^sub>d_del}}
\end{lemma}
@@ -198,7 +219,7 @@
\pause
The general case:
\begin{center}
- B-trees and (a,b) trees
+ B-trees and $(a,b)$-trees
\end{center}
\end{frame}
%-------------------------------------------------------------
--- a/Slides/document/main.tex Wed Aug 02 17:11:04 2017 +0200
+++ b/Slides/document/main.tex Wed Aug 02 17:11:23 2017 +0200
@@ -1,3 +1,4 @@
+\newif\ifMOD%\MODtrue %true for short version for summer schools
\input{prelude}
\begin{document}