--- a/Slides/Amor_Slides.thy Thu Jul 06 15:01:10 2017 +0200
+++ b/Slides/Amor_Slides.thy Thu Jul 06 16:57:33 2017 +0200
@@ -16,11 +16,8 @@
definition \<Phi> :: "bool list \<Rightarrow> real" where
"\<Phi> bs = length(filter id bs)"
-definition a_incr :: "bool list \<Rightarrow> real" where
-"a_incr bs = 2"
-
-lemma incr_thm: "t_incr bs + \<Phi> (incr bs) - \<Phi> bs = a_incr bs"
-by(induction bs) (auto simp: \<Phi>_def a_incr_def)
+lemma incr_thm: "t_incr bs + \<Phi> (incr bs) - \<Phi> bs = 2"
+by(induction bs) (auto simp: \<Phi>_def)
(*>*)
text_raw{*
\end{isabellebody}%
@@ -136,7 +133,7 @@
\pause
\item Operation(s) \<open>f :: \<tau> \<Rightarrow> \<tau>\<close>\\\pause (may have additional parameters)
\pause
-\item Initial ``state'': \<open>s\<^sub>0 :: \<tau>\<close>\\ (function ``empty'')
+\item Initial value: \<open>init :: \<tau>\<close>\\ (function ``empty'')
\end{itemize}
\pause
Needed for complexity analysis:
@@ -150,14 +147,15 @@
\high{Potential \<open>\<Phi> :: \<tau> \<Rightarrow> num\<close>} \pause\quad (creative spark!)
\end{itemize}
\pause
-Need to prove: \high{\<open>\<Phi> s \<ge> 0\<close>} and \high{\<open>\<Phi> s\<^sub>0 = 0\<close>}
+Need to prove: \high{\<open>\<Phi> s \<ge> 0\<close>} and \high{\<open>\<Phi> init = 0\<close>}
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Amortized and real cost}
Sequence of operations: \<open>f\<^sub>1\<close>, \dots, \<open>f\<^sub>n\<close>
\pause
-Sequence of states: \<open>s\<^sub>0\<close>, \pause \<open>s\<^sub>1\<close> \<open>:= f\<^sub>1 s\<^sub>0\<close>, \pause \dots, \<open>s\<^sub>n\<close> \<open>:= f\<^sub>n s\<^bsub>n-1\<^esub>\<close>
+Sequence of states:\\
+\qquad \<open>s\<^sub>0 := init\<close>, \pause \<open>s\<^sub>1\<close> \<open>:= f\<^sub>1 s\<^sub>0\<close>, \pause \dots, \<open>s\<^sub>n\<close> \<open>:= f\<^sub>n s\<^bsub>n-1\<^esub>\<close>
\pause
\begin{center}
@@ -174,7 +172,7 @@
\begin{tabular}{rcl}
$\sum_{i=1}^n$ \<open>a\<^sub>i\<close> & \<open>=\<close> & $\sum_{i=1}^n$ (\<open>t_f\<^sub>i s\<^bsub>i-1\<^esub> + \<Phi> s\<^sub>i - \<Phi> s\<^bsub>i-1\<^esub>\<close>)\\\pause
- &\<open>=\<close>& ($\sum_{i=1}^n$ \<open>t_f\<^sub>i s\<^bsub>i-1\<^esub>\<close>) \<open>+ \<Phi> s\<^sub>n - \<Phi> s\<^sub>0\<close>\\\pause
+ &\<open>=\<close>& ($\sum_{i=1}^n$ \<open>t_f\<^sub>i s\<^bsub>i-1\<^esub>\<close>) \<open>+ \<Phi> s\<^sub>n - \<Phi> init\<close>\\\pause
&\<open>\<ge>\<close>& $\sum_{i=1}^n$ \<open>t_f\<^sub>i s\<^bsub>i-1\<^esub>\<close>
\end{tabular}
\end{center}
@@ -197,24 +195,23 @@
@{thm incr.simps}
\medskip\pause
-@{prop \<open>s\<^sub>0 = []\<close>}
+@{prop \<open>init = []\<close>}
\medskip\pause
@{thm \<Phi>_def}
\medskip\pause
-@{thm a_incr_def}
-\medskip\pause
-
\begin{lemma}
\high{@{thm incr_thm}}
\end{lemma}
+\pause
+\textbf{Proof} by induction
\end{frame}
%-------------------------------------------------------------
\begin{frame}{Proof obligation summary}
\begin{itemize}
\item \high{\<open>\<Phi> s \<ge> 0\<close>}
-\item \high{\<open>\<Phi> s\<^sub>0 = 0\<close>}
+\item \high{\<open>\<Phi> init = 0\<close>}
\item For every operation \<open>f :: \<tau> \<Rightarrow> ... \<Rightarrow> \<tau>\<close>:\\
\high{\<open>t_f s\<close>\ $\overline{x}$\ \<open> + \<Phi>(f s\<close>\ $\overline{x}$\<open>) - \<Phi> s \<le> a_f s\<close>\ $\overline{x}$}
\end{itemize}
@@ -229,6 +226,7 @@
\begin{frame}{Warning: real time}
Amortized analysis unsuitable for real time applications:
+\pause
\begin{center}
\bad{Real running time for individual calls\\ may be much worse than amortized time}
\end{center}
@@ -245,9 +243,9 @@
Otherwise:
\begin{center}
\begin{tabular}{rl}
-{\sf\emph{ let}} & \<open>counter = 0;\<close>\\
- & \<open>bad =\<close> increment \<open>counter\<close> $2^n-1$ times;\\
- & \<open>_ = incr bad;\<close>\\
+{\sf\emph{ let}} & \<open>counter = 0;\<close>\\\pause
+ & \<open>bad =\<close> increment \<open>counter\<close> $2^n-1$ times;\\\pause
+ & \<open>_ = incr bad;\<close>\\\pause
& \bad{\<open>_ = incr bad;\<close>}\\
& \bad{\<open>_ = incr bad;\<close>}\\
& \bad{$\vdots$}
@@ -255,6 +253,10 @@
\end{center}
\end{frame}
%-------------------------------------------------------------
+\subsection{Simple Classical Examples}
+%-------------------------------------------------------------
+\thyfile{Thys/Amortized\char`_Examples}{}
+%-------------------------------------------------------------
\begin{isabellebody}%
*}
(*<*)