Homework solutions draft
authorlammich <lammich@in.tum.de>
Sat, 29 Jul 2017 19:33:57 +0200
changeset 69873 9a1629ac93f4
parent 69870 1f5cd3af3d78
child 69874 f30fdac78cce
Homework solutions
Exercises/hwsol/document/build
Exercises/hwsol/document/exercise.sty
Exercises/hwsol/document/root.tex
Exercises/hwsol/hwsol01.thy
Exercises/hwsol/hwsol02.thy
Exercises/hwsol/hwsol03.thy
Exercises/hwsol/hwsol04.thy
Exercises/hwsol/hwsol05.thy
Exercises/hwsol/hwsol06.thy
Exercises/hwsol/hwsol07.thy
Exercises/hwsol/hwsol08.thy
Exercises/hwsol/hwsol09.thy
Exercises/hwsol/hwsol10.thy
Exercises/hwsol/hwsol11.thy
Exercises/hwsol/hwsol12.thy
Exercises/hwsol/hwsol13.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/document/build	Sat Jul 29 19:33:57 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/hwsol/document/exercise.sty	Sat Jul 29 19:33:57 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/hwsol/document/root.tex	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,71 @@
+\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}{\_}
+
+\newcommand{\Homework}[2]{\section*{#1}}
+\newcommand{\NumHomework}[2]{\section*{#1}}
+
+\newcommand{\hwsol}[1]{\clearpage{\huge\center{Solution for Homework #1}}\\[3em]}
+
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol01.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,77 @@
+text_raw \<open>\hwsol{1}\<close>
+theory hwsol01
+imports Main
+begin
+fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"  where
+"snoc [] x = [x]" |
+"snoc (y # ys) x = y # (snoc ys x)" 
+
+fun reverse :: "'a list \<Rightarrow> 'a list"  where
+"reverse [] = []" |
+"reverse (x # xs) = snoc (reverse xs) x" 
+
+
+text {* \NumHomework{Maximum Value in List}{May 5} *}
+
+text \<open>
+  Submit your solution via \url{https://vmnipkow3.in.tum.de}.
+  Submit a theory file that runs in Isabelle-2016-1 {\bfseries without errors}.
+  
+  General hints:
+  \begin{itemize}
+    \item If you cannot prove a lemma, that you need for a subsequent
+    proof, assume this lemma by using sorry.
+    \item Define the functions as simple as possible.
+      In particular, do not try to make them tail recursive by 
+      introducing extra accumulator parameters --- this will 
+      complicate the proofs!
+    \item All proofs should be straightforward, and take only a few 
+      lines.
+  \end{itemize}  
+
+  Define a function that returns the maximal element of a list of natural numbers.
+  The result for the empty list shall be $0$.
+\<close>
+fun lmax :: "nat list \<Rightarrow> nat" 
+
+  where
+  "lmax [] = 0"
+| "lmax (a#xs) = max a (lmax xs)"
+
+
+text \<open>Define a function that checks whether an element is contained in a list\<close>  
+fun lcont :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" 
+
+where
+    "lcont x [] \<longleftrightarrow> False"
+  | "lcont x (y#ys) \<longleftrightarrow> (if x=y then True else lcont x ys)"  
+  
+  
+text \<open>Show that the maximum is greater or equal to every element of the list.\<close>
+lemma max_greater: "lcont x xs \<Longrightarrow> x\<le>lmax xs"
+
+  by (induction xs) (auto split: if_splits)
+  
+text \<open>Hint: If you see an \<open>if then else\<close> term in your premises, 
+  try to pass the option \<open>split: if_splits\<close> to @{method auto} or @{method simp},
+  e.g. \<open>apply (auto split: if_splits)\<close>
+\<close>
+  
+text \<open>Prove that reversing the list does not affect its maximum.
+  Note that we use the @{const reverse} function from exercise 4 here.
+\<close>
+
+lemma [simp]: "lmax (snoc xs a) = max a (lmax xs)"
+  by (induction xs) auto
+
+lemma "lmax (reverse xs) = lmax xs"
+
+  by (induction xs) (auto)
+
+text \<open>Hint: Induction. You may need an auxiliary lemma about 
+  @{const lmax} and @{const snoc}.\<close>
+
+
+end
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol02.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,151 @@
+text_raw \<open>\hwsol{2}\<close>
+
+theory hwsol02
+imports Complex_Main
+begin
+
+
+
+
+    
+text \<open>\NumHomework{Distinct lists}{May 12}
+  Submit your solution via \url{https://vmnipkow3.in.tum.de}.
+  Submit a theory file that runs in Isabelle-2016-1 {\bfseries without errors}.
+
+  Define a function \<open>contains\<close>, that checks whether an element is contained 
+  in a list. Define the function directly, not using \<open>set\<close>.
+\<close>    
+fun contains :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+  
+  where
+  "contains x [] = False"
+| "contains x (y#ys) \<longleftrightarrow> x=y \<or> contains x ys"  
+  
+   
+text \<open>Define a predicate \<open>ldistinct\<close> to characterize \emph{distinct} lists, i.e., 
+  lists whose elements are pairwise disjoint. Hint: Use the function contains.\<close>
+fun ldistinct :: "'a list \<Rightarrow> bool" 
+  
+  where
+  "ldistinct [] = True"
+| "ldistinct (x#xs) \<longleftrightarrow> \<not>contains x xs \<and> ldistinct xs"  
+  
+  
+text \<open>Show that a reversed list is distinct if and only if the 
+  original list is distinct. Hint: You may require multiple 
+  auxiliary lemmas.\<close>
+  
+lemma [simp]: "contains x (ys@[y]) \<longleftrightarrow> x=y \<or> contains x ys"  
+  by (induction ys) auto
+  
+lemma [simp]: "ldistinct (xs@[x]) \<longleftrightarrow> ldistinct xs \<and> \<not>contains x xs"  
+  by (induction xs) auto
+  
+lemma [simp]: "contains x (rev ys) \<longleftrightarrow> contains x ys"
+  by (induction ys) auto
+    
+lemma "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
+  by (induction xs) (auto) 
+    
+text {* \NumHomework{More on fold}{May 12} *}
+
+text \<open>Isabelle's fold function implements a left-fold. Additionally, 
+  Isabelle also provides a right-fold \<open>foldr\<close>.
+
+  Use both functions to specify the length of a list.
+\<close>  
+  
+thm fold.simps
+thm foldr.simps  
+  
+definition length_fold :: "'a list \<Rightarrow> nat"  
+   where
+  "length_fold l \<equiv> fold (\<lambda>_. Suc) l 0"
+  
+
+definition length_foldr :: "'a list \<Rightarrow> nat"  
+   where
+  "length_foldr l \<equiv> foldr (\<lambda>_. Suc) l 0"
+  
+
+  
+lemma aux2: "fold (\<lambda>_. Suc) l a = length l + a"  
+  by (induction l arbitrary: a) auto  
+  
+    
+lemma "length_fold l = length l"  
+  
+  unfolding length_fold_def by (simp add: aux2)
+    
+
+lemma "length_foldr l = length l"  
+  
+  unfolding length_foldr_def by (induction l) auto
+    
+
+
+text {* \NumHomework{List Slices}{May 12} 
+  Specify a function \<open>slice xs s l\<close>, that, for a list
+  \<open>xs=[x\<^sub>0,...,x\<^sub>n]\<close> returns the slice starting at s with length l, i.e.,
+  \<open>[x\<^sub>s,...,x\<^bsub>s+len-1\<^esub>]\<close>.
+
+  If \<open>s\<close> or \<open>len\<close> is out of range, return a shorter (or the empty) list.
+*}
+
+  
+fun slice :: "'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" 
+  where
+  
+  "slice (x#xs) (Suc n) l = slice xs n l"
+| "slice (x#xs) 0 (Suc l) = x # slice xs 0 l"  
+| "slice _ _ _ = []"  
+    
+text \<open>Hint: Use pattern matching instead of \<open>if\<close>-expressions. For example, instead
+  of writing \<open>f x = (if x>0 then \<dots> else \<dots>)\<close> you should define two equations
+  \<open>f 0 = \<dots>\<close> and \<open>f (Suc n) = \<dots>\<close>.
+\<close>  
+  
+text \<open>Some test cases, which should all hold, i.e., yield \<open>True\<close>\<close>
+value "slice [0,1,2,3,4,5,6::int] 2 3 = [2,3,4]" -- \<open>In range\<close>
+value "slice [0,1,2,3,4,5,6::int] 2 10 = [2,3,4,5,6]" -- \<open>Length out of range\<close>
+value "slice [0,1,2,3,4,5,6::int] 10 10 = []" -- \<open>Start index out of range\<close>
+  
+  
+text \<open>Show that the length of a list slice is always less than or equal to 
+  the specified length:\<close>  
+lemma "length (slice xs s l) \<le> l"
+  
+  by (induction xs s l rule: slice.induct) auto  
+    
+  
+text \<open>Show that, if the start position and length are in range, the length 
+  of the slice is equal to the specified length\<close>
+lemma "length xs \<ge> s + l \<Longrightarrow> length (slice xs s l) = l"
+  
+  by (induction xs s l rule: slice.induct) auto  
+
+
+    
+text \<open>Show that concatenation of two adjacent slices can be expressed as 
+  a single slice:\<close>
+lemma "slice xs s l1 @ slice xs (s+l1) l2 = slice xs s (l1+l2)"
+  
+  by (induction xs s l1 rule: slice.induct) auto  
+
+
+text \<open>Show that a slice of a distinct list is distinct.\<close>    
+    
+lemma aux1: "contains x (slice xs s l) \<Longrightarrow> contains x xs"    
+  by (induction xs s l rule: slice.induct) auto  
+    
+      
+lemma "ldistinct xs \<Longrightarrow> ldistinct (slice xs s l)"
+    
+  by (induction xs s l rule: slice.induct) (auto simp: aux1)
+    
+    
+    
+
+end
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol03.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,154 @@
+text_raw \<open>\hwsol{3}\<close>
+
+theory hwsol03
+  imports "../../../Public/Demos/BST_Demo"
+begin
+      
+text \<open>
+  \Homework{BSTs with Duplicates}{May 19}
+
+  \<^item> Have a look at @{const bst_eq} in \<open>~~/src/HOL/Library/Tree\<close>, which defines BSTs with duplicate elements.
+  \<^item> Warmup: Show that @{const isin} and @{const ins} are also correct for @{const bst_eq}.
+\<close>
+lemma "bst_eq t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
+
+apply(induction t)
+apply auto
+done
+
+  
+lemma bst_eq_ins: "bst_eq t \<Longrightarrow> bst_eq (ins x t)"
+
+apply(induction t)
+apply (auto simp: set_tree_ins)
+done
+
+
+text \<open>  
+  \<^item> Define a function \<open>ins_eq\<close> to insert into a BST with duplicates.
+\<close>
+fun ins_eq :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+
+  where
+"ins_eq x Leaf = Node Leaf x Leaf" |
+"ins_eq x (Node l a r) =
+  (if x < a then Node (ins_eq x l) a r 
+   else Node l a (ins_eq x r))"
+
+  
+  
+text \<open>  
+  \<^item> Show that \<open>ins_eq\<close> preserves the invariant @{const \<open>bst_eq\<close>}
+\<close>
+  
+
+lemma set_tree_ins_eq: "set_tree (ins_eq x t) = insert x (set_tree t)"
+apply(induction t)
+apply auto
+done
+
+    
+lemma bst_eq_ins_eq: "bst_eq t \<Longrightarrow> bst_eq (ins_eq x t)"
+
+apply(induction t)
+apply (auto simp: set_tree_ins_eq)
+done
+
+  
+  
+  
+text \<open>  
+  \<^item> Define a function \<open>count_tree\<close> to count how often a given element occurs in a tree
+\<close>
+fun count_tree :: "'a \<Rightarrow> 'a tree \<Rightarrow> nat" 
+
+  where
+  "count_tree x Leaf = 0"
+| "count_tree x (Node l y r) = count_tree x l + (if x=y then 1 else 0) + count_tree x r"  
+
+  
+text \<open>  
+  \<^item> Show that the \<open>ins_eq\<close> function inserts the desired element, and does not
+    affect other elements.
+\<close>
+lemma "count_tree x (ins_eq x t) = Suc (count_tree x t)"  
+
+  by (induction t) auto
+
+
+lemma "x\<noteq>y \<Longrightarrow> count_tree y (ins_eq x t) = count_tree y t"  
+
+  by (induction t) auto
+
+  
+  
+text \<open>  
+  The next exercise is a bonus exercise, yielding bonus points.
+  Bonus points count as achieved points, but not for the maximum 
+  achievable points, when computing the percentage of the achieved homework 
+  points.
+
+  \<^item> Bonus (5p): Use BSTs with duplicates to sort a list (cf.\ Exercise 3). 
+    Prove that the resulted list is sorted, and contains exactly the 
+    same number of each element as the original list.
+    Hint: Use a \<open>count\<close> function for lists, and relate it with the 
+    \<open>count_tree\<close>-function for trees.
+\<close>      
+
+
+fun count where
+  "count x [] = 0"
+| "count x (y#ys) = (if x=y then Suc (count x ys) else count x ys)"  
+  
+lemma count_append[simp]: "count x (xs@ys) = count x xs + count x ys"  
+  by (induction xs) auto
+  
+lemma [simp]: "x\<noteq>y \<Longrightarrow> count x (inorder (ins_eq y t)) = count x (inorder t)"  
+  apply (induction t)
+  apply auto  
+  done  
+  
+lemma [simp]: "count x (inorder (ins_eq x t)) = Suc (count x (inorder t))"    
+  apply (induction t)
+  apply auto  
+  done  
+
+lemma "count x (inorder t) = count_tree x t"
+  apply (induction t)
+  apply auto  
+  done  
+  
+definition "mk_tree_eq l = fold ins_eq l Leaf"  
+  
+lemma bst_mk_tree_eq_aux: "bst_eq t \<Longrightarrow> bst_eq (fold ins_eq l t)"
+  apply (induction l arbitrary: t) apply (auto simp: bst_eq_ins_eq) done
+  
+lemma bst_eq_mk_tree_eq: "bst_eq (mk_tree_eq l)"
+  by (simp add: mk_tree_eq_def bst_mk_tree_eq_aux)
+
+lemma count_mktree_eq_aux: "count x (inorder (fold ins_eq l t)) = count x l + count x (inorder t)"
+  apply (induction l arbitrary: t)
+  apply auto  
+  done  
+
+    
+definition bst_eq_sort :: "'a::linorder list \<Rightarrow> 'a list" 
+
+  where "bst_eq_sort l = inorder (mk_tree_eq l)"
+
+    
+theorem count_bst_eq_sort: "count x (bst_eq_sort l) = count x l"
+
+  by (auto simp: bst_eq_sort_def mk_tree_eq_def count_mktree_eq_aux)  
+
+  
+theorem sorted_bst_eq_sort: "sorted (bst_eq_sort l)"
+
+  by (auto simp: bst_eq_sort_def bst_eq_mk_tree_eq bst_eq_imp_sorted)  
+
+      
+    
+
+end
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol04.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,85 @@
+text_raw \<open>\hwsol{4}\<close>
+
+theory hwsol04
+  imports "../../../Public/Demos/BST_Demo"
+begin
+
+
+    
+text \<open>
+  \Homework{Delete Minimum}{May 26}
+
+  Define a function to return and delete the minimum element from a 
+    non-empty BST. You may omit the equation for the empty tree.
+\<close>    
+fun del_min :: "'a tree \<Rightarrow> 'a * 'a tree" where
+  
+"del_min (Node l a r) =
+   (if l = Leaf then (a,r) else let (a',l') = del_min l in (a', Node l' a r))"
+
+
+text \<open>
+  Show that your function preserves the search tree property.
+  Hint: An auxiliary lemma of the form \<open>t\<noteq>Leaf \<Longrightarrow> del_min t = (x,t') \<Longrightarrow> \<dots>\<close>
+  relating \<open>set_tree t\<close> and \<open>set_tree t'\<close> may be helpful.
+\<close>
+
+lemma del_min_set: "t\<noteq>Leaf \<Longrightarrow> del_min t = (x,t') \<Longrightarrow> set_tree t = insert x (set_tree t')"
+  apply (induction t arbitrary: t') 
+  apply (auto split: if_splits prod.splits)
+  done
+    
+    
+lemma "\<lbrakk>t\<noteq>Leaf; bst t\<rbrakk> \<Longrightarrow> bst (snd (del_min t))" 
+  
+  apply (induction t)
+  apply (auto split: prod.split simp: del_min_set) 
+  done  
+
+
+text \<open>Show that your function returns the first element of the inorder traversal,
+  and a tree whose inorder traversal corresponds to the tail of the original inorder traversal.
+  Hint: You may need auxiliary lemmas. Some subgoals may require more \<open>force\<close>ful methods than \<open>auto\<close>.
+\<close>
+  
+lemma [simp]: "inorder t = [] \<longleftrightarrow> t=Leaf" 
+  by (induction t) auto
+    
+
+lemma "t\<noteq>Leaf \<Longrightarrow> del_min t = (x,t') 
+  \<Longrightarrow> case inorder t of (y#ys) \<Rightarrow> x=y \<and> inorder t' = ys"    
+  
+  apply (induction t arbitrary: t')
+  apply (simp split: prod.splits list.splits if_splits)
+  apply (force split: prod.splits list.splits if_splits)
+  done
+    
+    
+text \<open>Define a function \<open>del_min2\<close> that uses so called continuations: 
+  The second argument is a function which is applied to the result.
+  (i.e. the minimum element and the tree of remaining elements) 
+
+  Do not use \<open>del_min\<close> for the definition, but define \<open>del_min2\<close> recursively, passing 
+  down (modified) continuations.
+\<close>    
+
+fun del_min2 :: "'a tree \<Rightarrow> ('a  \<Rightarrow> 'a tree \<Rightarrow> 'a tree) \<Rightarrow> 'a tree"
+  
+   where
+"del_min2 (Node l a r) nd =
+   (if l = Leaf then nd a r else del_min2 l (\<lambda>a' l'. nd a' (Node l' a r)))"
+
+
+text \<open>Show that your function definition corresponds to \<open>del_min\<close>\<close>
+lemma del_min2_del_min:
+   "t \<noteq> Leaf \<Longrightarrow> del_min2 t f = (let (a,t') = del_min t in f a t')"
+  
+apply(induction t arbitrary: f)
+apply (auto split: prod.splits)
+done
+
+    
+
+end
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol05.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,58 @@
+text_raw \<open>\hwsol{5}\<close>
+
+theory hwsol05
+  imports 
+    Complex_Main 
+    "~~/src/HOL/Library/Tree"
+begin
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" 
+  where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (x#xs) v \<longleftrightarrow> G u x \<and> path G x xs v"  
+
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"  
+  by (induction p1 arbitrary: u) auto  
+  
+    
+text \<open>
+  \NumHomework{Simple Paths}{June 2}
+  This homework is worth 5 bonus points.
+
+  A simple path is a path without loops, or, in other words, a path 
+  where no node occurs twice. (Note that the first node of the path is 
+  not included, such that there may be a simple path from \<open>u\<close> to \<open>u\<close>.)
+
+  Show that for every path, there is a corresponding simple path:
+\<close>    
+lemma exists_simple_path:
+  assumes "path G u p v"    
+  shows "\<exists>p'. path G u p' v \<and> distinct p'"  
+  using assms  
+proof (induction p rule: length_induct)
+  case (1 p)
+  assume IH: "\<forall>pp. length pp < length p \<longrightarrow> path G u pp v 
+                  \<longrightarrow> (\<exists>p'. path G u p' v \<and> distinct p')"  
+  assume PREM: "path G u p v"
+  show "\<exists>p'. path G u p' v \<and> distinct p'" 
+  text \<open>Fill in your proof here.\<close>  
+    
+  proof cases
+    assume "distinct p"
+    with PREM show ?thesis by auto
+  next
+    assume A: "\<not>distinct p"
+    from not_distinct_decomp[OF A]
+    obtain xs ys zs y where [simp]: "p = xs @ [y] @ ys @ [y] @ zs" by blast
+    then have PP: "path G u (xs@y#zs) v" using PREM by auto
+    have "length (xs@y#zs) < length p" by auto
+    with IH PP obtain p' where P': "path G u p' v" "distinct p'"
+      by blast
+    thus ?thesis by blast
+  qed
+    
+qed
+
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol06.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,146 @@
+text_raw \<open>\hwsol{6}\<close>
+
+theory hwsol06
+  imports 
+    Complex_Main 
+    "~~/src/HOL/Library/Multiset" 
+begin
+
+(* From Sorting.thy *)  
+hide_const List.sorted List.insort List.insort_key
+
+fun sorted :: "'a::linorder list \<Rightarrow> bool" where
+"sorted [] = True" |
+"sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> y) & sorted xs)"
+
+lemma sorted_append:
+  "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
+by (induct xs) (auto)
+  
+  
+
+  
+      
+text \<open>\Homework{Quicksort}{2.~6.~2017}
+  We extend the notion of a sorting algorithm, by 
+  providing a key function that maps the actual list elements to a linearly 
+  ordered type. The elements shall be sorted according to their keys.
+\<close>
+
+fun sorted_key :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "sorted_key k [] = True"
+| "sorted_key k (x # xs) = ((\<forall>y\<in>set xs. k x \<le> k y) & sorted_key k xs)"
+
+text \<open>Quicksort can be defined as follows: 
+  (Note that we use \<open>nat\<close> for the keys, as this causes less trouble when 
+  writing Isar proofs than a generic \<open>'b::linorder\<close>)\<close>
+fun qsort :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "qsort k [] = []"
+| "qsort k (p#xs) = qsort k [x\<leftarrow>xs. k x<k p]@p#qsort k [x\<leftarrow>xs. \<not>k x<k p]"
+text \<open>The syntax @{term \<open>[x\<leftarrow>xs. P x]\<close>} is a shortcut 
+  notation for @{term \<open>filter (\<lambda>x. P x) xs\<close>}.\<close>
+  
+text \<open>Show that quicksort is a sorting algorithm:\<close>  
+lemma qsort_preserves_mset: "mset (qsort k xs) = mset xs"
+  
+  apply (induction k xs rule: qsort.induct)
+  by (auto)
+
+
+  
+lemma qsort_preserves_set: "set (qsort k xs) = set xs"
+  by (metis qsort_preserves_mset set_mset_mset)
+    
+lemma sorted_key_append:
+  "sorted_key k (xs@ys) = (sorted_key k xs & sorted_key k ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. k x\<le>k y))"
+    by (induct xs) (auto)
+
+       
+lemma qsort_sorts: "sorted_key k (qsort k xs)"
+  
+  apply (induction k xs rule: qsort.induct)
+  apply (auto simp: sorted_key_append qsort_preserves_set)
+  done
+
+
+
+text \<open>The following is a cost function for the comparsions of quicksort: \<close>    
+fun c_qsort :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
+  "c_qsort k [] = 0"
+| "c_qsort k (p#xs) 
+    = c_qsort k [x\<leftarrow>xs. k x<k p] + c_qsort k [x\<leftarrow>xs. k x\<ge>k p] + 2*length xs"
+
+
+text \<open>Show that the number of required comparisons is at most \<open>(length xs)\<^sup>2\<close>.
+
+  Hints: 
+    \<^item> Do an induction on the length of the list,
+      and, afterwards, a case distinction on the list constructors.
+    \<^item> It might be useful to prove \<open>a\<^sup>2+b\<^sup>2 \<le> (a+b)\<^sup>2\<close> for \<open>a b :: nat\<close>
+    \<^item> Have a look at the lemma @{thm [source] sum_length_filter_compl}
+\<close>  
+  
+lemmas length_induct_rule = measure_induct_rule[where f=length, case_names shorter]
+  
+lemma "c_qsort k xs \<le> (length xs)\<^sup>2"
+proof (induction xs rule: length_induct_rule)
+  case (shorter xs) thm shorter.IH
+  show ?case proof (cases xs)
+    case Nil
+    then show ?thesis by auto
+  next
+    case (Cons x xs')
+    text \<open>Insert your proof here\<close>  
+  
+    note Cons[simp]    
+    let ?left = "[xa\<leftarrow>xs' . k xa < k x]"
+    let ?right = "[xa\<leftarrow>xs' . k xa \<ge> k x]"
+    have R_ALT: "?right = [xa\<leftarrow>xs' . \<not> k xa < k x]"
+      by (induction xs') auto
+
+    from shorter.IH have IH: "c_qsort k ys \<le> (length ys)\<^sup>2" if "length ys \<le> length xs'" for ys
+      using that by auto
+
+    have X1: "c_qsort k ?left \<le> (length ?left)\<^sup>2"
+      by (rule IH) auto
+
+    have X2: "c_qsort k ?right \<le> (length ?right)\<^sup>2"
+      by (rule IH) auto
+
+    have "c_qsort k xs = c_qsort k ?left + c_qsort k ?right + 2 * length xs'" by simp
+    also have "\<dots> \<le> (length ?left)\<^sup>2 + (length ?right)\<^sup>2 + 2 * length xs'" using X1 X2 by simp
+    also have "\<dots> \<le> (length ?left + length ?right)\<^sup>2 + 2 * length xs'"
+      by (auto simp: eval_nat_numeral field_simps)
+    also have "\<dots> \<le> (length xs')\<^sup>2 + 2 * length xs'"
+      by (auto simp: R_ALT sum_length_filter_compl)
+    also have "\<dots> \<le> (length xs)\<^sup>2"
+      by (auto simp: eval_nat_numeral)
+    finally show ?thesis .
+
+  qed
+qed
+    
+text \<open>For 3 bonus points, show that quicksort is stable. 
+  You will probably run into subgoals containing terms like  
+  @{term \<open>[x\<leftarrow>xs . k x < k p \<and> k x = a]\<close>}.
+  Try to find a simpler form for them. (Cases on \<open>a<k p\<close>)!
+\<close>     
+lemma qsort_stable: "[x\<leftarrow>qsort k xs . k x = a] = [x\<leftarrow>xs . k x = a]"  
+  
+proof -
+  have [simp]: "[x\<leftarrow>xs . k x < k p \<and> k x = a] = (if a<k p then [x\<leftarrow>xs. k x = a] else [])" for k :: "'a \<Rightarrow> nat" and xs p   
+    by (induction xs) auto
+  have [simp]: "[x\<leftarrow>xs . \<not>k x < k p \<and> k x = a] = (if k p \<le> a then [x\<leftarrow>xs. k x = a] else [])" for k :: "'a \<Rightarrow> nat" and xs p   
+    by (induction xs) auto
+      
+  show ?thesis
+    apply (induction k xs rule: qsort.induct)
+    apply (auto)
+    done  
+      
+qed      
+
+    
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol07.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,80 @@
+text_raw \<open>\hwsol{7}\<close>
+
+theory hwsol07
+  imports 
+    Complex_Main 
+    "~~/src/HOL/Library/Tree"
+begin
+  
+    
+  
+text \<open>
+  \Homework{Cost for \<open>remdups\<close>}{16.~6.~2017}
+
+  The following function removes all duplicates from a list.
+  It uses the auxiliary function \<open>member\<close> to determine 
+  whether an element is contained in a list.
+\<close>  
+
+fun member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "member x [] \<longleftrightarrow> False"
+| "member x (y#ys) \<longleftrightarrow> (if x=y then True else member x ys)"
+  
+fun rem_dups :: "'a list \<Rightarrow> 'a list" where
+  "rem_dups [] = []" |
+  "rem_dups (x # xs) = (if member x xs then rem_dups xs else x # rem_dups xs)"
+  
+text \<open>
+  Show that this function is equal to the HOL standard function @{const \<open>remdups\<close>}
+\<close>  
+  
+lemma member_correct: "member x xs \<longleftrightarrow> x\<in>set xs" by (induction xs) auto
+    
+lemma rem_dups_correct: "rem_dups xs = remdups xs"
+  
+  by (induction xs) (auto simp: member_correct)
+    
+
+text \<open>Define the timing functions for @{const \<open>member\<close>} and @{const rem_dups}, 
+  as described on the slides:\<close>
+fun t_member :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" 
+  
+  where
+  "t_member x [] = 1"
+| "t_member x (y#ys) = 1 + (if x=y then 1 else t_member x ys)"
+  
+  
+fun t_rem_dups :: "'a list \<Rightarrow> nat" 
+  
+  where
+  "t_rem_dups [] = 1" |
+  "t_rem_dups (x # xs) = 1 + t_member x xs + (if member x xs then t_rem_dups xs else 1 + t_rem_dups xs)"
+  
+    
+text \<open>Estimate \<open>t_rem_dups xs\<close> to be quadratic in the length of \<open>xs\<close>.
+  Hint: The estimate @{term \<open>(length xs + 1)\<^sup>2\<close>} should work.
+\<close>
+
+lemma t_member_est: "t_member x xs \<le> length xs + 1"
+  by (induction xs) auto
+  
+lemma "t_rem_dups xs \<le> (length xs+1)\<^sup>2"
+proof (induction xs)
+  case Nil
+  then show ?case by simp
+next
+  case (Cons x xs)
+  have "t_rem_dups (x # xs) \<le> 2 + t_member x xs + t_rem_dups xs"  
+    by auto
+  also have "\<dots> \<le> 3 + length xs + t_rem_dups xs" using t_member_est by auto
+  also have "\<dots> \<le> 3 + length xs + (length xs + 1)\<^sup>2" using Cons.IH by auto
+  also have "\<dots> = 4 + 3*length xs + (length xs)\<^sup>2" by (auto simp: eval_nat_numeral)
+  also have "\<dots> \<le> 4 + 4*length xs + (length xs)\<^sup>2" by auto
+  also have "\<dots> = (length (x # xs) + 1)\<^sup>2" by (auto simp: eval_nat_numeral)
+  finally show ?case .
+qed
+  
+  
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol08.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,242 @@
+text_raw \<open>\hwsol{8}\<close>
+
+theory hwsol08
+  imports 
+    Complex_Main 
+    "../../../Public/Demos/BST_Demo"
+    "~~/src/HOL/Library/Multiset" 
+    (*"~~/src/HOL/Library/List_lexord"*)
+    "~~/src/HOL/Data_Structures/Tree23_Set"
+begin
+  
+  
+locale set_interface =
+  fixes invar :: "'s \<Rightarrow> bool" and \<alpha> :: "'s \<Rightarrow> 'a set"
+  fixes empty :: 's
+  assumes empty_invar: "invar empty" and empty_\<alpha>: "\<alpha> empty = {}"
+  
+  fixes is_in :: "'s \<Rightarrow> 'a \<Rightarrow> bool"  
+  assumes is_in_\<alpha>: "invar s \<Longrightarrow> is_in s x \<longleftrightarrow> x \<in> \<alpha> s"
+    
+  fixes ins :: "'a \<Rightarrow> 's \<Rightarrow> 's"  
+  assumes ins_invar: "invar s \<Longrightarrow> invar (ins x s)" and ins_\<alpha>: "invar s \<Longrightarrow> \<alpha> (ins x s) = Set.insert x (\<alpha> s)"
+   
+  fixes to_list :: "'s \<Rightarrow> 'a list" 
+  assumes to_list_\<alpha>: "invar s \<Longrightarrow> set (to_list s) = \<alpha> s"
+begin  
+
+    
+end  
+
+  
+  
+text \<open>
+  \NumHomework{Estimating the Size of 2-3-Trees}{23.~6.~2017}
+
+    Show that for 2-3-trees, we have:
+    @{text [display] \<open> log\<^sub>3 ( s(t) + 1 ) \<le> h(t) \<le> log\<^sub>2 (s(t) + 1)\<close>}
+
+    Hint: It helps to first raise the two sides of the 
+      inequation to the 2nd/3rd power. 
+      Use sledgehammer and find-theorems to search for the appropriate lemmas.
+\<close>  
+
+  
+lemma height_est_upper_aux: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
+  by (induction t) auto
+
+    
+lemma height_est_upper: "bal t \<Longrightarrow> height t \<le> log 2 (size t + 1)"
+  
+  using height_est_upper_aux le_log2_of_power by blast
+    
+
+  
+lemma height_est_lower_aux:
+  assumes "bal t"  
+  shows "size t + 1 \<le> 3^(height t)"
+  using assms  
+  by (induction t) auto
+    
+
+lemma height_est_lower: "bal t \<Longrightarrow> log 3 (size t + 1) \<le> height t"
+  
+proof -
+  assume A: "bal t"
+  from log_le_cancel_iff[of 3 "size t + 1" "3^height t"]
+    and height_est_lower_aux[OF A]
+  have "log 3 (size t + 1) \<le> log 3 (3 ^ height t)"
+    apply simp
+    by (metis of_nat_Suc real_of_nat_le_numeral_power_cancel_iff)
+  also have "\<dots> = height t" by (simp add: log_nat_power)
+  finally show ?thesis .
+qed      
+    
+
+text \<open>Define a function to count the number of leaves of a 2-3-tree\<close>  
+fun num_leaves :: "_ tree23 \<Rightarrow> nat" 
+  
+  where
+  "num_leaves \<langle>\<rangle> = 1"
+| "num_leaves \<langle>l,_,r\<rangle> = num_leaves l + num_leaves r"  
+| "num_leaves \<langle>l,_,m,_,r\<rangle> = num_leaves l + num_leaves m + num_leaves r"  
+  
+  
+text \<open>Define a function to determine whether a tree only consists of 2-nodes 
+  and leaves:\<close>  
+fun is_2_tree :: "_ tree23 \<Rightarrow> bool" 
+  
+  where
+  "is_2_tree \<langle>\<rangle> \<longleftrightarrow> True"
+| "is_2_tree \<langle>l,_,r\<rangle> \<longleftrightarrow> is_2_tree l \<and> is_2_tree r"  
+| "is_2_tree _ \<longleftrightarrow> False"  
+  
+
+lemma 
+  assumes "bal t" 
+  assumes "is_2_tree t"  
+  shows "size t + 1 = 2^height t"
+  using assms by (induction t) auto  
+    
+  
+  
+lemma is_2_tree_imp_num_leaves:
+  assumes "bal t" 
+  assumes "is_2_tree t"  
+  shows "num_leaves t = 2^height t"
+  using assms by (induction t) auto  
+  
+lemma num_leaves_lower:
+  assumes "bal t"
+  shows "num_leaves t \<ge> 2^height t"
+  using assms 
+  by (induction t) auto
+    
+lemma num_leaves_imp_is_two_tree:
+  assumes "bal t"
+  assumes "num_leaves t = 2^height t"
+  shows "is_2_tree t"  
+  using assms 
+  apply (induction t)
+  apply auto
+  apply (metis (no_types, lifting) Nat.le_diff_conv2 add_diff_cancel_right' le_add2 le_antisym mult_2 nat_add_left_cancel_le num_leaves_lower)  
+  apply (metis (no_types, lifting) Nat.le_diff_conv2 add_diff_cancel_left' le_add1 le_antisym mult_2 num_leaves_lower)
+  by (smt Nat.add_diff_assoc2 add.commute add_diff_cancel_right' diff_is_0_eq diff_zero le_add1 mult_2 nat.simps(3) num_leaves_lower numeral_2_eq_2 power_eq_0_iff)
+    
+
+text \<open>Show that a 2-3-tree has only 2 nodes, if and only if its number of leafs is 2 to the power of its height!
+
+  Hint: The \<open>\<longrightarrow>\<close> direction is quite easy, the \<open>\<longleftarrow>\<close> direction requires a bit more work!
+\<close>    
+lemma "bal t \<Longrightarrow> is_2_tree t \<longleftrightarrow> num_leaves t = 2^height t"
+  
+  using is_2_tree_imp_num_leaves num_leaves_imp_is_two_tree by blast
+    
+    
+  
+text \<open>
+  \NumHomework{Deforestation}{23.~6.~2017}
+
+    A disadvantage of using the generic algorithms from the set interface for 
+    binary trees (and other data structures) is that they construct an 
+    intermediate list containing the elements of one tree.
+
+    Define a function that folds over the in-order traversal of a binary tree 
+    directly, without constructing an intermediate list, and show that it is 
+    correct.
+
+    Note: Optimizations like this are called deforestation, as they get rid 
+      of intermediate tree-structured data (in our case: lists which are degenerated trees).
+\<close>  
+  
+fun fold_tree :: "('a \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> 'a tree \<Rightarrow> 's \<Rightarrow> 's" 
+  
+  where
+  "fold_tree f \<langle>\<rangle> s = s"
+| "fold_tree f \<langle>l,x,r\<rangle> s = fold_tree f r (f x (fold_tree f l s))"  
+  
+  
+lemma "fold_tree f t s = fold f (Tree.inorder t) s"  
+  
+  by (induction t arbitrary: s) auto  
+    
+  
+  
+text \<open>
+  \NumHomework{Bit-Vectors}{23.~6.~2017}
+  {\bf Bonus Homework (3p)}
+
+  A bit-vector is a list of Booleans that encodes a finite set of 
+  natural numbers as follows: A number \<open>i\<close> is in the set, 
+  if \<open>i\<close> is less than the length of the list and the \<open>i\<close>th element of the list 
+  is true.
+
+  For 3 bonus points, define the operations empty, member, insert, and to-list
+  on bit-vectors, and instantiate the set-interface from Exercise~1!
+\<close>  
+  
+type_synonym bv = "bool list"
+  
+definition bv_\<alpha> :: "bv \<Rightarrow> nat set" 
+  where "bv_\<alpha> l = { i. i<length l \<and> l!i }"
+    
+definition bv_empty :: bv 
+  
+  where "bv_empty = []"  
+
+    
+definition bv_member :: "bv \<Rightarrow> nat \<Rightarrow> bool" 
+  
+  where "bv_member l x \<longleftrightarrow> x<length l \<and> l!x"
+
+    
+definition bv_ins :: "nat \<Rightarrow> bv \<Rightarrow> bv" 
+  
+  where "bv_ins x l = (
+    let l = (if x<length l then l else l@replicate (x - length l + 1) False)
+    in l[x := True]
+  )"  
+
+    
+definition bv_to_list :: "bv \<Rightarrow> nat list" 
+  
+  where "bv_to_list l \<equiv> filter (\<lambda>i. l!i) [0..<length l]"
+
+    
+  
+lemma bv_ins_\<alpha>: "bv_\<alpha> (bv_ins x l) = Set.insert x (bv_\<alpha> l)"  
+  apply (rule)
+  subgoal  
+    unfolding bv_\<alpha>_def bv_ins_def
+    apply (auto simp: nth_list_update nth_append nth_Cons')
+    using Suc_less_eq less_Suc_eq_le by fastforce
+  subgoal
+    unfolding bv_\<alpha>_def bv_ins_def
+    by (auto simp: nth_list_update nth_append nth_Cons')
+  done
+  
+    
+lemma bv_to_list_\<alpha>: "set (bv_to_list l) = bv_\<alpha> l"  
+  apply (induction l)
+  unfolding bv_\<alpha>_def bv_to_list_def
+  apply (auto simp: nth_Cons')
+  using less_antisym apply blast  
+  using less_antisym apply blast  
+  done  
+  
+    
+interpretation bv_set: set_interface "\<lambda>_. True" bv_\<alpha> bv_empty bv_member bv_ins bv_to_list
+  
+  apply unfold_locales
+  subgoal by simp  
+  subgoal unfolding bv_\<alpha>_def bv_empty_def by auto
+  subgoal unfolding bv_\<alpha>_def bv_member_def by auto
+  subgoal by simp
+  subgoal by (simp add: bv_ins_\<alpha>)    
+  subgoal by (simp add: bv_to_list_\<alpha>)    
+  done
+  
+  
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol09.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,122 @@
+text_raw \<open>\hwsol{9}\<close>
+
+theory hwsol09
+  imports "../../../Public/Thys/Trie1"
+begin
+  
+    
+text \<open>
+  \NumHomework{Shrunk Trees}{30.~6.~2017}
+
+  Have a look at the @{const delete2} function for tries. It maintains a 
+  ``shrunk'' - property on tries. Identify this property, define a predicate 
+  for it, and show that it is indeed maintained by empty, insert, and delete2!
+\<close>    
+
+fun shrunk :: "trie \<Rightarrow> bool" 
+  
+  where
+  "shrunk Leaf \<longleftrightarrow> True"
+| "shrunk (Node v (l,r)) \<longleftrightarrow> shrunk l \<and> shrunk r \<and> (\<not>v \<longrightarrow> (l,r)\<noteq>(Leaf,Leaf))"
+  
+
+lemma "shrunk Leaf"
+ 
+  by simp 
+
+  
+  
+lemma [simp]: "insert ks t \<noteq> Leaf"
+  by (induction ks t rule: insert.induct) auto  
+  
+    
+lemma "shrunk t \<Longrightarrow> shrunk (insert ks t)"
+  
+  by (induction ks t rule: insert.induct) auto  
+  
+  
+lemma "shrunk t \<Longrightarrow> shrunk (delete2 ks t)"    
+  
+  by (induction t arbitrary: ks) (auto split: list.split)
+  
+    
+  
+text \<open>
+  \NumHomework{Refining Delete}{30.~6.~2017}
+
+  Refine the delete function to intermediate tries and further down 
+  to Patricia tries.
+\<close>    
+    
+datatype itrie = LeafI | UnaryI bool itrie | BinaryI bool "itrie * itrie"
+
+fun abs_itrie :: "itrie \<Rightarrow> trie" -- \<open>Abstraction to tries\<close>  
+  where
+  "abs_itrie LeafI = Leaf"
+| "abs_itrie (UnaryI True t) = Node False (Leaf, abs_itrie t)"
+| "abs_itrie (UnaryI False t) = Node False (abs_itrie t, Leaf)"
+| "abs_itrie (BinaryI v (l,r)) = Node v (abs_itrie l, abs_itrie r)"  
+  
+  
+fun deleteI :: "bool list \<Rightarrow> itrie \<Rightarrow> itrie" where
+  
+  "deleteI ks LeafI = LeafI"
+| "deleteI [] (UnaryI x t) = UnaryI x t"
+| "deleteI (k#ks) (UnaryI x t) = (if k=x then UnaryI x (deleteI ks t) else UnaryI x t)"
+| "deleteI [] (BinaryI _ lr) = BinaryI False lr"  
+| "deleteI (k#ks) (BinaryI v (l,r)) = BinaryI v (if k then (l,deleteI ks r) else (deleteI ks l,r))"  
+  
+
+  
+  lemma [simp]: "abs_itrie (UnaryI k t) = Node False (if k then (Leaf, abs_itrie t) else (abs_itrie t, Leaf))"
+    by auto
+  
+  
+lemma "abs_itrie (deleteI ks t) = delete ks (abs_itrie t)"
+  
+  by (induction ks t rule: deleteI.induct) auto  
+  
+fun unaryP :: "bool \<Rightarrow> ptrie \<Rightarrow> ptrie" where
+  "unaryP x (NodeP xs v lr) = NodeP (x#xs) v lr"
+  
+fun size1P :: "ptrie \<Rightarrow> nat" where
+  "size1P LeafP = 0"
+| "size1P (NodeP ps v (l,r)) = 1 + size ps + size1P l + size1P r"
+  
+lemma [measure_function]: "is_measure size1P" by (rule is_measure_trivial) 
+  
+fun absI_ptrie :: "ptrie \<Rightarrow> itrie" where
+  "absI_ptrie LeafP = LeafI"  
+| "absI_ptrie (NodeP [] v (l,r)) = BinaryI v (absI_ptrie l, absI_ptrie r)"
+| "absI_ptrie (NodeP (x#xs) v (l,r)) = UnaryI x (absI_ptrie (NodeP xs v (l,r)))"
+
+lemma unaryP_refines[simp]: "t\<noteq>LeafP \<Longrightarrow> absI_ptrie (unaryP k t) = UnaryI k (absI_ptrie t)"    
+  by (cases t) auto
+    
+    
+fun pdelete :: "bool list \<Rightarrow> ptrie \<Rightarrow> ptrie"
+  
+  where  
+  "pdelete ks LeafP = LeafP"
+| "pdelete [] (NodeP (x#xs) v lr) = NodeP (x#xs) v lr"
+| "pdelete (k#ks) (NodeP (x#xs) v lr) = (
+      if k=x then unaryP x (pdelete ks (NodeP xs v lr))
+      else NodeP (x#xs) v lr)"
+| "pdelete [] (NodeP [] _ lr) = NodeP [] False lr"  
+| "pdelete (k#ks) (NodeP [] v (l,r)) = NodeP [] v (if k then (l,pdelete ks r) else (pdelete ks l,r))"  
+  
+lemma [simp]: "t\<noteq>LeafP \<Longrightarrow> unaryP k t \<noteq> LeafP" by (cases t) auto
+  
+
+lemma [simp]: "pdelete ks t = LeafP \<longleftrightarrow> t=LeafP"  
+  by (induction ks t rule: pdelete.induct) auto  
+  
+  
+lemma "absI_ptrie (pdelete ks t) = deleteI ks (absI_ptrie t)"  
+
+  by (induction ks t rule: pdelete.induct) auto
+  
+    
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol10.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,101 @@
+text_raw \<open>\hwsol{10}\<close>
+
+theory hwsol10
+imports 
+    "../../../Public/Thys/Leftist_Heap"    
+begin
+  
+  
+text\<open>
+\Homework{Constructing a Heap from a List of Elements}{7.~7.~2017}
+
+The naive solution of starting with the empty heap and inserting the elements one by one
+can be improved by repeatedly merging heaps of roughly equal size.
+Start by turning the list of elements into a list of singleton heaps.
+Now make repeated passes over the list,
+merging adjacent pairs of heaps in each pass (thus halving the list length)
+until only a single heap is left.
+It can be shown that this takes linear time.
+
+Define a function \<open>heap_of_list ::\<close> @{typ "'a list \<Rightarrow> 'a lheap"} and prove its functional
+correctness.
+\<close>
+
+  
+fun mset_forest :: "'a lheap list \<Rightarrow> 'a multiset" 
+  where
+"mset_forest [] = {#}" |
+"mset_forest (x # xs) = mset_tree x + mset_forest xs"
+
+fun merge_adjacent :: "'a::ord lheap list \<Rightarrow> 'a lheap list" where
+"merge_adjacent [] = []" |
+"merge_adjacent [t] = [t]" |
+"merge_adjacent (t\<^sub>1 # t\<^sub>2 # ts) = merge t\<^sub>1 t\<^sub>2 # merge_adjacent ts"
+
+text \<open>For the termination proof of \<open>merge_forest\<close> below.\<close>
+lemma length_merge_adjacent[simp]: "length (merge_adjacent ts) = (length ts + 1) div 2"
+  by (induction ts rule: merge_adjacent.induct) auto
+
+lemma mset_merge_adjacent: "mset_forest (merge_adjacent ts) = mset_forest ts"
+by (induction ts rule: merge_adjacent.induct) (auto simp: mset_merge)
+
+fun merge_forest :: "'a::ord lheap list \<Rightarrow> 'a lheap" where
+"merge_forest [] = Leaf" |
+"merge_forest [x] = x" |
+"merge_forest xs = merge_forest (merge_adjacent xs)"
+
+lemma mset_merge_forest: "mset_tree (merge_forest ts) = mset_forest ts"
+by (induction ts rule: merge_forest.induct) (auto simp: mset_merge mset_merge_adjacent)
+
+  
+  
+definition heap_of_list :: "'a::ord list \<Rightarrow> 'a lheap" 
+  
+  where "heap_of_list xs = merge_forest [Node 1 Leaf x Leaf . x \<leftarrow> xs]"
+  
+
+lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs"
+  
+  by (induction xs) (auto simp: heap_of_list_def mset_merge_forest)
+  
+  
+  
+lemma heap_merge_adjacent: 
+  "\<forall>h\<in>set hs. heap h \<Longrightarrow> h\<in>set (merge_adjacent hs) \<Longrightarrow> heap h"  
+  by (induction hs rule: merge_adjacent.induct) (auto simp: heap_merge)
+  
+lemma heap_merge_forest: "\<forall>h\<in>set hs. heap h \<Longrightarrow> heap (merge_forest hs)"  
+  apply (induction hs rule: merge_forest.induct)
+  apply (auto simp: heap_merge heap_merge_adjacent)
+  done
+  
+  
+lemma heap_heap_of_list: "heap (heap_of_list xs)"  
+  
+  apply (induction xs) 
+  apply (auto simp: heap_of_list_def heap_merge_forest)
+  done  
+  
+  
+  
+lemma ltree_merge_adjacent: 
+  "\<forall>h\<in>set hs. ltree h \<Longrightarrow> h\<in>set (merge_adjacent hs) \<Longrightarrow> ltree h"  
+  by (induction hs rule: merge_adjacent.induct) (auto simp: ltree_merge)
+  
+lemma ltree_merge_forest: "\<forall>h\<in>set hs. ltree h \<Longrightarrow> ltree (merge_forest hs)"  
+  apply (induction hs rule: merge_forest.induct)
+  apply (auto simp: ltree_merge ltree_merge_adjacent)
+  done
+  
+  
+    
+lemma ltree_ltree_of_list: "ltree (heap_of_list xs)"  
+  
+  apply (induction xs) 
+  apply (auto simp: heap_of_list_def ltree_merge_forest)
+  done  
+  
+    
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol11.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,80 @@
+text_raw \<open>\hwsol{11}\<close>
+
+theory hwsol11
+imports 
+    "../../../Public/Thys/Heap_Prelim"    
+begin
+
+type_synonym rank = nat
+type_synonym snat = "rank list"
+
+abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> strictly_ascending s"  
+definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"
+  
+  
+lemma \<alpha>_Nil[simp]: "\<alpha> [] = 0"
+  unfolding \<alpha>_def by auto
+  
+lemma \<alpha>_Cons[simp]: "\<alpha> (r#rs) = 2^r + \<alpha> rs"
+  unfolding \<alpha>_def by auto
+
+lemma \<alpha>_append[simp]: "\<alpha> (rs\<^sub>1@rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
+  unfolding \<alpha>_def by auto
+  
+  
+text \<open>
+  \NumHomework{Largest Representable Number}{14.~7.~2017}
+
+  Assume we use numbers \<open>{0..<K}\<close> to represent the ranks in a sparse binary number.
+  Define \<open>max_snat K\<close> to be the largest representable sparse binary number (its value should be \<open>2\<^sup>K-1\<close>), and
+  prove that your definition is correct.
+\<close>  
+
+definition max_snat :: "nat \<Rightarrow> snat" 
+  
+  where "max_snat K = [0..<K]"
+  
+  
+lemma "invar (max_snat K)"
+  
+  unfolding max_snat_def by (induction K) auto
+  
+  
+lemma \<alpha>_max_snat: "\<alpha> (max_snat K) = 2^K - 1"
+  
+  unfolding \<alpha>_def max_snat_def
+  by (simp add: interv_sum_list_conv_sum_set_nat power2sum)
+  
+
+lemma max_snat_bounded: "set (max_snat K) \<subseteq> {0..<K}"
+  
+  unfolding max_snat_def by auto
+  
+    
+lemma max_snat_max:
+  assumes "invar rs"
+  assumes "set rs \<subseteq> {0..<K}"  
+  shows "\<alpha> rs \<le> \<alpha> (max_snat K)"
+  
+  unfolding \<alpha>_max_snat 
+  using assms
+proof (induction rs arbitrary: K rule: rev_induct)
+  case Nil
+  then show ?case by simp
+next
+  case (snoc r rs)
+  from snoc.prems have "invar rs" (*"\<forall>r'\<in>set rs. r'<r"*) "set rs \<subseteq> {0..<r}" by auto
+  from snoc.IH[OF this] have IH: "\<alpha> rs \<le> 2 ^ r - 1" .    
+    
+  from snoc.prems have "r<K" by auto
+  hence "r+1 \<le> K" by auto
+      
+  have "\<alpha> (rs @ [r]) = \<alpha> rs + 2^r" unfolding \<alpha>_def by auto
+  also have "\<dots> \<le> 2^r - 1 + 2^r" using IH by auto
+  also have "\<dots> = 2^(r+1) - 1" by auto
+  also note \<open>r+1 \<le> K\<close>
+  finally show ?case by (auto simp: diff_le_mono)
+qed    
+
+end
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol12.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,75 @@
+text_raw \<open>\hwsol{12}\<close>
+
+theory hwsol12
+imports Complex_Main
+begin
+  
+
+text \<open>
+  \Homework{Dynamic Tables with real-valued Potential}{21.~7.~2017}
+
+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"
+
+text \<open>Start with the locale \<open>Dyn_Tab\<close> in file \<open>Thys/Amortized_Examples\<close>
+but use the above definition of \<open>\<Phi> :: tab \<Rightarrow> real\<close>. A number of proofs will now fail
+because the invariant is now too weak.
+Find a stronger invariant such that all the proofs work again.\<close>
+
+
+locale Dyn_Tab
+begin
+
+type_synonym tab = "nat \<times> nat"
+
+fun invar :: "tab \<Rightarrow> bool" where
+"invar (n,l) = (n=0 \<and> l = 0 \<or> l < 2*n \<and> n \<le> l)"
+
+definition init :: tab where
+"init = (0,0)"
+
+text\<open>Insertion: the element does not matter\<close>
+fun ins :: "tab \<Rightarrow> tab" where
+"ins (n,l) = (n+1, if n<l then l else if l=0 then 1 else 2*l)"
+
+text\<open>Time: if the table overflows, we count only the time for copying elements\<close>
+fun t_ins :: "nat \<times> nat \<Rightarrow> nat" where
+"t_ins (n,l) = (if n<l then 1 else n+1)"
+
+lemma "invar init"
+by(simp add: init_def)
+
+lemma "invar t \<Longrightarrow> invar(ins t)"
+apply(cases t)
+apply(auto)
+done
+
+fun \<Phi> :: "tab \<Rightarrow> real" where
+"\<Phi> (n,l) = 2*(real n) - real l"
+
+lemma "invar t \<Longrightarrow> \<Phi> t \<ge> 0"
+apply(cases t)
+apply(auto)
+done
+
+lemma "\<Phi> init = 0"
+by(simp add: init_def)
+
+lemma a_ins: "invar t \<Longrightarrow> t_ins t + \<Phi>(ins t) - \<Phi> t \<le> 3"
+apply(cases t)
+apply(auto split: if_splits)
+done
+
+end
+
+
+  
+end
+  
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Exercises/hwsol/hwsol13.thy	Sat Jul 29 19:33:57 2017 +0200
@@ -0,0 +1,93 @@
+text_raw \<open>\hwsol{13}\<close>
+
+theory hwsol13
+imports "../../../Public/Thys/Skew_Heap"
+begin
+  
+text \<open>
+  \Homework{Pairing Heap}{28.~07.~2017}
+
+The datatype of pairing heaps defined in the theory \verb!Thys/Pairing_Heap!
+comes with the unstated invariant that \<open>Empty\<close> occurs only at the root.
+We can avoid this invariant by a slightly different representation:
+\<close>
+
+datatype 'a hp = Hp 'a "'a hp list"
+type_synonym 'a heap = "'a hp option"
+
+text \<open>Carry out the development with this new representation.
+Restrict yourself to the \<open>get_min\<close> and \<open>delete_min\<close> operations.
+That is, define the following functions (and any auxiliary function required)
+\<close>
+
+fun get_min  :: "('a :: linorder) heap \<Rightarrow> 'a" where
+
+"get_min (Some(Hp x _)) = x"
+
+fun merge :: "('a :: linorder) hp \<Rightarrow> 'a hp \<Rightarrow> 'a hp" where
+"merge (Hp x lx) (Hp y ly) = 
+    (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"
+
+
+
+
+
+fun merge_pairs :: "('a :: linorder) hp list \<Rightarrow> 'a heap" where
+  "merge_pairs [] = None"
+| "merge_pairs [h] = Some h" 
+| "merge_pairs (h1 # h2 # hs) =
+ Some(let h = merge h1 h2 in case merge_pairs hs of None \<Rightarrow> h | Some h' \<Rightarrow> merge h h')"
+
+
+fun del_min :: "'a :: linorder heap \<Rightarrow> 'a heap" where
+
+  "del_min None = None"
+| "del_min (Some(Hp x hs)) = merge_pairs hs"
+
+
+fun php :: "('a :: linorder) hp \<Rightarrow> bool" where
+
+"php (Hp x hs) = (\<forall>h \<in> set hs. (\<forall>y \<in> set_hp h. x \<le> y) \<and> php h)"
+
+
+fun mset_hp :: "'a hp \<Rightarrow>'a multiset" where
+
+"mset_hp (Hp x hs) = {#x#} + Union_mset(mset(map mset_hp hs))"
+
+
+fun mset_heap :: "'a heap \<Rightarrow>'a multiset" where
+
+"mset_heap None = {#}" |
+"mset_heap (Some h) = mset_hp h"
+
+text \<open>and prove the following functional correctness theorems and any lemmas required,
+but excluding preservation of the invariant:\<close>
+
+theorem get_min_in: "get_min (Some h) \<in> set_hp(h)"
+
+by(cases h)(auto)
+
+
+lemma get_min_min: "\<lbrakk> php h; x \<in> set_hp(h) \<rbrakk> \<Longrightarrow> get_min (Some h) \<le> x"
+
+by(cases h)(auto)
+
+lemma mset_merge: "mset_hp (merge h1 h2) = mset_hp h1 + mset_hp h2"
+by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)
+
+lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = Union_mset(image_mset mset_hp(mset hs))"
+by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge Let_def split: option.split)
+
+
+lemma mset_del_min: "mset_heap (del_min (Some h)) = mset_hp h - {#get_min(Some h)#}"
+
+by(cases h) (auto simp: mset_merge_pairs)
+
+
+text \<open>It is recommended to start with the original theory and modify it as much as needed.
+
+Note that function @{const set_hp} is defined automatically by the definition of type \<open>hp\<close>.\<close>
+
+  
+end
+