--- a/Exercises/ROOT Thu Jul 13 15:33:16 2017 +0200
+++ b/Exercises/ROOT Thu Jul 13 15:33:38 2017 +0200
@@ -68,6 +68,11 @@
session "ex11" in "ex11" = HOL +
options [document = pdf, document_output = "generated", document_variants = "ex11"]
theories [document=false]
- "../../Thys/Heap_Prelim"
+ "../../../Public/Thys/Heap_Prelim"
theories ex11
document_files "root.tex" "exercise.sty" "build"
+
+session "ex12" in "ex12" = HOL +
+ options [document = pdf, document_output = "generated", document_variants = "ex12"]
+ theories ex12
+ document_files "root.tex" "exercise.sty" "build"
Binary file Exercises/ex11.pdf has changed
--- a/Exercises/ex11/ex11.thy Thu Jul 13 15:33:16 2017 +0200
+++ b/Exercises/ex11/ex11.thy Thu Jul 13 15:33:38 2017 +0200
@@ -1,7 +1,7 @@
(*<*)
theory ex11
imports
- "../../Thys/Heap_Prelim"
+ "../../../Public/Thys/Heap_Prelim"
begin
(*>*)
text {* \ExerciseSheet{11}{7.~7.~2017} *}
Binary file Exercises/ex12.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex12/document/build Thu Jul 13 15:33:38 2017 +0200
@@ -0,0 +1,8 @@
+#!/bin/sh
+
+${ISABELLE_TOOL} latex -o sty root.tex && \
+${ISABELLE_TOOL} latex -o pdf root.tex && \
+${ISABELLE_TOOL} latex -o pdf root.tex && \
+${ISABELLE_TOOL} latex -o pdf root.tex && \
+cp root.pdf ../../../$2.pdf
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex12/document/exercise.sty Thu Jul 13 15:33:38 2017 +0200
@@ -0,0 +1,51 @@
+
+\newcommand{\Lecture}{Functional Data Structures}
+\newcommand{\Semester}{SS 2017}
+\newcommand{\Prof}{Prof.~Tobias~Nipkow,~Ph.D.}
+\newcommand{\Tutor}{Dr. Peter Lammich}
+
+\newcounter{sheet}
+\newcounter{homework}
+
+\newlength{\abslength}\setlength{\abslength}{2mm plus 1mm minus 1mm}
+\newcommand{\abs}{\par\vspace{\abslength}}
+
+\newlength{\TUMBr}\settowidth{\TUMBr}{{\bf Technische Universit{\"a}t M{\"u}nchen}}
+\newcommand{\Header}[5]{{\bf
+ \makebox[\TUMBr]{Technische Universit{\"a}t M{\"u}nchen} \hfill #3\\
+ \makebox[\TUMBr]{Institut f{\"u}r Informatik} \hfill #4\\
+ \makebox[\TUMBr]{#1} \hfill #5\\
+ \makebox[\TUMBr]{#2}}\abs}
+
+\newcommand{\Title}[1]{%
+ \begin{center}{\LARGE\bf\Lecture}\\[1ex]{\bf Exercise Sheet #1}\end{center}}
+
+\newcommand{\ExerciseSheet}[2]{%
+ \pagestyle{empty}%
+ \setcounter{sheet}{#1}%
+ \vspace*{-2cm}\Header{\Prof}{\Tutor}{\Semester}{#2}{}\vspace*{1cm}%
+ \Title{#1}\abs}
+
+\newcounter{exercise}
+\newcommand{\Exercise}[1]{%
+ \refstepcounter{exercise}%
+ \pagebreak[3]%
+ \relax%
+ \vspace{0.8em}%
+ \subsection*{{Exercise \arabic{sheet}.\arabic{exercise}\ \ \normalfont\sffamily #1}}}
+
+\newcommand{\Homework}[2]{%
+ \pagebreak[3]%
+ \relax%
+ \vspace{0.8em}%
+ \subsection*{{Homework \arabic{sheet}\ \ \normalfont\sffamily #1}}%
+ \emph{Submission until Friday, #2, 11:59am.}}
+
+\newcommand{\NumHomework}[2]{%
+ \refstepcounter{homework}%
+ \pagebreak[3]%
+ \relax%
+ \vspace{0.8em}%
+ \subsection*{{Homework \arabic{sheet}.\arabic{homework}\ \ \normalfont\sffamily #1}}%
+ \emph{Submission until Friday, #2, 11:59am.}}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/ex12/document/root.tex Thu Jul 13 15:33:38 2017 +0200
@@ -0,0 +1,66 @@
+\documentclass[11pt,a4paper]{scrartcl}
+\usepackage{isabelle,isabellesym}
+\usepackage{exercise}
+\usepackage{amsmath}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+\usepackage{amssymb}
+ %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+ %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+ %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage[greek,english]{babel}
+ %option greek for \<euro>
+ %option english (default language) for \<guillemotleft>, \<guillemotright>
+
+\usepackage[latin1]{inputenc}
+ %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
+ %\<threesuperior>, \<threequarters>, \<degree>
+
+\usepackage[only,bigsqcap]{stmaryrd}
+ %for \<Sqinter>
+
+%\usepackage{eufrak}
+ %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+ %for \<cent>, \<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+\begin{document}
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+
+\renewcommand{\isachardoublequote}{`\"}
+\renewcommand{\isachardoublequoteopen}{``}
+\renewcommand{\isachardoublequoteclose}{''}
+\renewcommand{\isacharunderscore}{\_}
+\renewcommand{\isacharunderscorekeyword}{\_}
+
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- a/Exercises/ex12/ex12.thy Thu Jul 13 15:33:16 2017 +0200
+++ b/Exercises/ex12/ex12.thy Thu Jul 13 15:33:38 2017 +0200
@@ -1,84 +1,190 @@
+(*<*)
theory ex12
imports Complex_Main
begin
-
-subsection "Uebungsaufgabe"
+(*>*)
-text \<open>Consider locale \<open>Queue\<close> in file \<open>Thys/Amortized_Examples\<close>. A call of \<open>deq (xs,[])\<close>
-requires the reversal of \<open>xs\<close>, which may be very long. We can reduce that impact
-by shifting \<open>xs\<close> over to \<open>ys\<close> whenever \<open>length xs > length ys\<close>. This does not improve
-the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity
-of individual calls of \<open>deq\<close>. Modify local \<open>Queue\<close> as follows:\<close>
+text {* \ExerciseSheet{12}{14.~7.~2017} *}
+
+text \<open>
+ \Exercise{Balanced Queues}
+
+ Consider locale \<open>Queue\<close> in file \<open>Thys/Amortized_Examples\<close>. A call of \<open>deq (xs,[])\<close>
+ requires the reversal of \<open>xs\<close>, which may be very long. We can reduce that impact
+ by shifting \<open>xs\<close> over to \<open>ys\<close> whenever \<open>length xs > length ys\<close>. This does not improve
+ the amortized complexity (in fact it increases it by 1) but reduces the worst case complexity
+ of individual calls of \<open>deq\<close>. Modify locale \<open>Queue\<close> as follows:\<close>
-locale Queue
-begin
+locale Queue begin
type_synonym 'a queue = "'a list * 'a list"
+definition "init = ([],[])"
fun balance :: "'a queue \<Rightarrow> 'a queue" where
"balance(xs,ys) = (if size xs \<le> size ys then (xs,ys) else ([], ys @ rev xs))"
-
fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
"enq a (xs,ys) = balance (a#xs, ys)"
-
fun deq :: "'a queue \<Rightarrow> 'a queue" where
"deq (xs,ys) = balance (xs, tl ys)"
text \<open>Again, we count only the newly allocated list cells.\<close>
-
+fun t_balance :: "'a queue \<Rightarrow> nat" where
+ "t_balance (xs,ys) = (if size xs \<le> size ys then 0 else size xs + size ys)"
fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
-"t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"
-
+"t_enq a (xs,ys) = 1 + t_balance (a#xs, ys)"
fun t_deq :: "'a queue \<Rightarrow> nat" where
-"t_deq (xs,ys) = (if size xs \<le> size ys - 1 then 0 else size xs + (size ys - 1))"
+"t_deq (xs,ys) = t_balance (xs, tl ys)"
-end
-
-text \<open>You will also have to modify \<open>invar\<close> and \<open>\<Phi>\<close>. In the end you should be able to prove
-that the amortized complexity of \<open>enq\<close> is \<open> \<le> 3\<close> and of \<open>deq\<close> is \<open>= 0\<close>.\<close>
+text \<open>
+ \<^item> Start over with showing functional correctness. Hint: You will require an invariant.
+\<close>
-(* hide *)
-context Queue
-begin
-
-definition "init = ([],[])"
+fun invar :: "'a queue \<Rightarrow> bool"
+(*<*)
+ where
+ "invar (xs,ys) \<longleftrightarrow> size xs \<le> size ys"
+(*>*)
+
+fun abs :: "'a queue \<Rightarrow> 'a list"
+(*<*)
+ where
+ "abs (xs,ys) = xs @ rev ys"
+(*>*)
+
+lemma [simp]: "invar init"
+(*<*)
+ by (auto simp: init_def)
+(*>*)
+
+lemma [simp]: "invar q \<Longrightarrow> invar (enq x q)"
+(*<*)
+ by (cases q) auto
+(*>*)
+
+lemma [simp]: "invar q \<Longrightarrow> invar (deq q)"
+(*<*)
+ by (cases q) auto
+(*>*)
+
+lemma [simp]: "abs init = []"
+(*<*)
+ by (auto simp: init_def)
+(*>*)
+
+lemma [simp]: "invar q \<Longrightarrow> abs (enq x q) = x#abs q"
+(*<*)
+ by (cases q) (auto)
+(*>*)
+
+(*<*)
+lemma butlast_rev: "butlast (rev xs) = rev (tl xs)"
+ by (induction xs) auto
+(*>*)
+
+lemma [simp]: "invar q \<Longrightarrow> abs (deq q) = butlast (abs q)"
+(*<*)
+ by (cases q) (auto simp: butlast_append butlast_rev)
+(*>*)
+
-fun invar where
-"invar (xs,ys) = (size xs \<le> size ys)"
+
+
+text \<open>
+ \<^item> Next, define a suitable potential function \<open>\<Phi>\<close>, and prove
+ that the amortized complexity of \<open>enq\<close> is \<open> \<le> 3\<close> and of \<open>deq\<close> is \<open> \<le> 0\<close>.
+\<close>
-fun \<Phi> :: "'a queue \<Rightarrow> nat" where
-"\<Phi> (xs,ys) = 2 * size xs"
+fun \<Phi> :: "'a queue \<Rightarrow> int"
+(*<*)
+ where "\<Phi> (xs,ys) = 2 * size xs"
+(*>*)
-lemma "\<Phi> t \<ge> 0"
+lemma \<Phi>_non_neg: "\<Phi> t \<ge> 0"
+(*<*)
apply(cases t)
apply(auto)
done
+(*>*)
-lemma "\<Phi> init = 0"
+lemma \<Phi>_init: "\<Phi> init = 0"
+(*<*)
by(simp add: init_def)
+(*>*)
-lemma a_enq: "invar q \<Longrightarrow> t_enq a q + \<Phi>(enq a q) - \<Phi> q \<le> 3"
+lemma a_enq: " t_enq a q + \<Phi>(enq a q) - \<Phi> q \<le> 3"
+(*<*)
+apply(cases q)
+apply(auto)
+done
+(*>*)
+
+lemma a_deq: " t_deq q + \<Phi>(deq q) - \<Phi> q \<le> 0"
+(*<*)
apply(cases q)
apply(auto)
done
+(*>*)
-lemma a_deq: "invar q \<Longrightarrow> t_deq q + \<Phi>(deq q) - \<Phi> q = 0"
-apply(cases q)
-apply(auto)
-done
+text \<open>Finally, show that a sequence of enqueue and dequeue operations requires
+ linear cost in its length:
+\<close>
+
+(*<*)
+(* Establish abstraction boundary *)
+lemmas [simp del] = \<Phi>.simps enq.simps deq.simps t_enq.simps t_deq.simps
+(*>*)
+datatype 'a opr = ENQ 'a | DEQ
+
+fun execute :: "'a queue \<Rightarrow> 'a opr list \<Rightarrow> 'a queue"
+ where
+ "execute q [] = q"
+| "execute q (ENQ x#ops) = execute (enq x q) ops"
+| "execute q (DEQ#ops) = execute (deq q) ops"
+
+text \<open>Count only list cell allocations! \<close>
+fun t_execute :: "'a queue \<Rightarrow> 'a opr list \<Rightarrow> nat"
+(*<*)
+ where
+ "t_execute q [] = 0"
+| "t_execute q (ENQ x#ops) = t_enq x q + t_execute (enq x q) ops"
+| "t_execute q (DEQ#ops) = t_deq q + t_execute (deq q) ops"
+(*>*)
+
+
+(*<*)
+lemma t_execute_aux: "t_execute q ops \<le> 3*length ops + \<Phi> q - \<Phi> (execute q ops)"
+proof (induction q ops rule: execute.induct)
+ case (1 q)
+ then show ?case by simp
+next
+ case (2 q x ops)
+ then show ?case using a_enq[of x q] by (auto)
+next
+ case (3 q ops)
+ then show ?case using a_deq[of q] by auto
+qed
+(*>*)
+
+lemma t_execute: "t_execute init ops \<le> 3*length ops"
+ (*<*)
+ using t_execute_aux[of init ops] \<Phi>_non_neg[of "execute init ops"]
+ by (auto simp: \<Phi>_init)
+ (*>*)
+(*<*)
end
-(* end hide *)
-
-subsection "Homework"
+(*>*)
-type_synonym tab = "nat \<times> nat"
+text \<open>
+ \Homework{Dynamic Tables with real-valued Potential}{21.~7.~2017}
-text \<open>In file \<open>Thys/Amortized_Examples\<close> in the repository there is a formalization
+In file \<open>Thys/Amortized_Examples\<close> in the repository there is a formalization
of dynamic tables in locale \<open>Dyn_Tab\<close> with the potential function \<open>\<Phi> (n,l) = 2*n - l\<close>
and a discussion of why this is tricky. The standard definition you find in textbooks
does not rely on cut-off subtraction on \<open>nat\<close> but uses standard real numbers:\<close>
+type_synonym tab = "nat \<times> nat"
+
fun \<Phi> :: "tab \<Rightarrow> real" where
"\<Phi> (n,l) = 2*(real n) - real l"
@@ -87,7 +193,7 @@
because the invariant is now too weak.
Find a stronger invariant such that all the proofs work again.\<close>
-(* hide *)
+(*<*)
locale Dyn_Tab
begin
@@ -132,6 +238,8 @@
done
end
-(* end hide *)
+(*>*)
+(*<*)
end
+(*>*)