ex3 draft
authorlammich <lammich@in.tum.de>
Fri, 27 Apr 2018 10:24:36 +0200
changeset 69921 17c8fbbda477
parent 69920 994af7618cd7
child 69922 971be3014817
ex3
SS18/Exercises/ROOT
SS18/Exercises/ex03.pdf
SS18/Exercises/ex03/Scratch.thy
SS18/Exercises/ex03/document/build
SS18/Exercises/ex03/document/exercise.sty
SS18/Exercises/ex03/document/root.tex
SS18/Exercises/ex03/ex03.thy
SS18/Exercises/ex03/tmpl03.thy
--- a/SS18/Exercises/ROOT	Mon Apr 23 11:46:13 2018 +0200
+++ b/SS18/Exercises/ROOT	Fri Apr 27 10:24:36 2018 +0200
@@ -8,6 +8,12 @@
   theories ex02
   document_files "root.tex" "exercise.sty" "build"
 
+session "ex03" in "ex03" = HOL +
+  options [document = pdf, document_output = "generated", document_variants = "ex03"]
+  theories [document = false] "../BST_Demo"
+  theories ex03
+  document_files "root.tex" "exercise.sty" "build"
+  
 (*
 session hwsol_basis = HOL +
   theories
Binary file SS18/Exercises/ex03.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex03/Scratch.thy	Fri Apr 27 10:24:36 2018 +0200
@@ -0,0 +1,143 @@
+theory Scratch
+imports 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"  
+(*>*)  
+
+lemma [simp]: "contains a (xs @ [x]) \<longleftrightarrow> contains a xs \<or> a=x" 
+  apply (induction xs) apply auto done
+  
+lemma [simp]: "ldistinct (xs@[x]) \<longleftrightarrow> ldistinct xs \<and> \<not>contains x xs"
+  apply (induction xs)
+  apply auto  
+  done  
+  
+lemma contains_rev[simp]: "contains x (rev xs) \<longleftrightarrow> contains x xs"
+  apply (induction xs)
+  apply auto
+  done  
+    
+lemma "ldistinct (rev xs) \<longleftrightarrow> ldistinct xs"
+  apply (induction xs)
+  apply auto
+  done  
+  
+  
+fun slice :: "'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" 
+  where
+  "slice _ _ 0 = []" 
+| "slice [] _ _ = []"
+| name: "slice (x#xs) (Suc n) l = slice xs n l"
+| "slice (x#xs) 0 (Suc l) = x # slice xs 0 l"  
+thm slice.simps
+thm name    
+  
+  
+lemma [simp]: "slice (x#xs) (Suc n) l = slice xs n l" by (cases l) auto
+  
+(*    
+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  
+(*>*)
+(*>*)
+
+thm slice.simps    
+lemma [simp]: "slice [] x y = []" 
+  apply (cases y) by 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)"
+(*<*)  
+  apply (induction xs s l1 rule: slice.induct)
+    thm slice.simps
+  apply 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)
+(*>*)    
+    
+    
+    
+  
+  
+  
+  
+  
+  
+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) (*>*)
+
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex03/document/build	Fri Apr 27 10:24:36 2018 +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/SS18/Exercises/ex03/document/exercise.sty	Fri Apr 27 10:24:36 2018 +0200
@@ -0,0 +1,51 @@
+
+\newcommand{\Lecture}{Functional Data Structures}
+\newcommand{\Semester}{SS 2018}
+\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/SS18/Exercises/ex03/document/root.tex	Fri Apr 27 10:24:36 2018 +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:
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex03/ex03.thy	Fri Apr 27 10:24:36 2018 +0200
@@ -0,0 +1,354 @@
+(*<*)
+theory ex03
+imports "../BST_Demo"
+begin
+(*>*)
+
+
+
+text {* \ExerciseSheet{3}{27.~4.~2018} *}
+
+text \<open>
+  \Exercise{Membership Test with Less Comparisons}
+
+  In worst case, the @{const isin} function performs two comparisons per node.
+  In this exercise, we want to reduce this to one comparison per node, with the 
+  following idea:
+  
+  One never tests for \<open>>\<close>, but always goes right if not \<open><\<close>. 
+  However, one remembers the value where one should have tested for \<open>=\<close>,
+  and performs the comparison when a leaf is reached.
+\<close>
+      
+fun isin2 :: "('a::linorder) tree \<Rightarrow> 'a option \<Rightarrow> 'a \<Rightarrow> bool" 
+ \<comment> \<open>The second parameter stores the value for the deferred comparison\<close>
+(*<*)
+where
+"isin2 Leaf z x = (case z of None \<Rightarrow> False | Some y \<Rightarrow> x = y) " |
+"isin2 (Node l a r) z x =
+  (if x < a then isin2 l z x else isin2 r (Some a) x)"
+(*>*)  
+
+(*<*)
+lemma isin2_Some:
+  "\<lbrakk> bst t;  \<forall>x \<in> set_tree t. y < x \<rbrakk>
+  \<Longrightarrow> isin2 t (Some y) x = (isin t x \<or> x=y)"
+apply(induction t arbitrary: y)
+apply auto
+done
+(*>*)
+
+text \<open>Show that your function is correct. 
+
+  Hint: Auxiliary lemma for \<open>isin2 t (Some y) x\<close> !
+\<close>
+lemma isin2_None:
+  "bst t \<Longrightarrow> isin2 t None x = isin t x"
+(*<*)
+apply(induction t)
+apply auto
+apply (auto simp: isin2_Some)
+done
+(*>*)
+
+      
+text \<open>
+  \Exercise{Height-Preserving In-Order Join}
+  Write a function that joins two binary trees such that
+  \<^item> The in-order traversal of the new tree is the concatenation of the in-order traversals of the original tree
+  \<^item> The new tree is at most one higher than the highest original tree
+
+  Hint: Once you got the function right, proofs are easy!
+\<close>  
+fun join :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)  
+  where
+"join t Leaf = t" |
+"join Leaf t = t" |
+"join (Node l1 a1 r1) (Node l2 a2 r2) =
+   (case join r1 l2 of
+     Leaf \<Rightarrow> Node l1 a1 (Node Leaf a2 r2) |
+     Node l b r \<Rightarrow> Node (Node l1 a1 l) b (Node r a2 r2))"
+(*>*)
+
+lemma join_inorder[simp]: "inorder(join t1 t2) = inorder t1 @ inorder t2"
+(*<*)  
+apply(induction t1 t2 rule: join.induct)
+apply (auto split: tree.split)
+done
+(*>*)
+
+lemma "height(join t1 t2) \<le> max (height t1) (height t2) + 1"
+(*<*)  
+apply(induction t1 t2 rule: join.induct)
+apply (auto split: tree.split)
+done
+(*>*)
+
+text \<open>
+  \Exercise{Implement Delete}
+  Implement delete using the \<open>join\<close> function from last exercise.
+\<close>  
+
+text \<open>Note: At this point, we are not interested in the implementation details 
+  of join any more, but just in its specification, i.e., what it does to trees.
+  Thus, as first step, we declare its equations to not being automatically unfolded.
+\<close>
+
+declare join.simps[simp del]
+
+text \<open>Both, \<open>set_tree\<close> and \<open>bst\<close> can be expressed by the inorder traversal over trees:\<close>
+
+thm set_inorder[symmetric] bst_iff_sorted_wrt_less
+
+text \<open>Note: As @{thm [source] set_inorder} is declared as simp. 
+  Be careful not to have both directions of the lemma in the simpset at the 
+  same time, otherwise the simplifier is likely to loop.
+  
+  You can use \<open>simp del: set_inorder add: set_inorder[symmetric]\<close>, or
+  \<open>auto simp del: set_inorder simp: set_inorder[symmetric]\<close> to 
+  temporarily remove the lemma from the simpset.
+  
+  Alternatively, you can write \<open>declare set_inorder[simp_del]\<close> to
+  remove it once and forall.
+\<close>
+
+
+text "For the \<open>sorted_wrt\<close> predicate, you might want to use these lemmas as simp:"
+thm sorted_wrt_append sorted_wrt_Cons
+
+text \<open>Show that join preserves the set of entries\<close>
+lemma [simp]: "set_tree (join t1 t2) = set_tree t1 \<union> set_tree t2"
+(*<*)
+  by (simp del: set_inorder add: set_inorder[symmetric])
+(*>*)  
+
+text \<open>Show that joining the left and right child of a BST is again a BST:\<close>
+
+lemma [simp]: "bst (Node l (x::_::linorder) r) \<Longrightarrow> bst (join l r)"
+(*<*)
+  by (simp del: bst_wrt.simps add: bst_iff_sorted_wrt_less sorted_wrt_append sorted_wrt_Cons)
+(*>*)  
+
+text \<open>Implement a delete function using the idea contained in the lemmas above.\<close>  
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)where
+  "delete x Leaf = Leaf"
+| "delete x (Node l v r) = (
+    if x=v then join l r 
+    else if x<v then Node (delete x l) v r
+    else Node l v (delete x r)
+  )"  
+(*>*)  
+
+text \<open>Prove it correct! Note: You'll need the first lemma to prove the second one! \<close>  
+lemma [simp]: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
+(*<*)
+  apply (induction t)
+  apply auto
+  done
+(*>*)
+
+
+lemma "bst t \<Longrightarrow> bst (delete x t)"
+(*<*)
+  apply (induction t)
+  apply auto
+  done
+(*>*)
+  
+
+text {* \NumHomework{Tree Addressing}{May 4} *}
+text \<open>
+  A position in a tree can be given as a list of 
+  navigation instructions from the root, i.e., whether to go 
+  to the left or right subtree. We call such a list a path.
+\<close>
+  datatype direction = L | R
+  type_synonym path = "direction list"
+
+text \<open>Specify when a path is valid:\<close>  
+  
+  fun valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool" where
+(*<*)
+    "valid t [] \<longleftrightarrow> True"
+  | "valid (Node l v r) (L#ps) \<longleftrightarrow> valid l ps"
+  | "valid (Node l v r) (R#ps) \<longleftrightarrow> valid r ps"
+  | "valid _ _ \<longleftrightarrow> False"  
+(*>*)
+  
+text \<open>Specify a function to return the subtree addressed by a given path:\<close>  
+  fun get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree" 
+(*<*)where
+    "get t [] = t"
+  | "get (Node l v r) (L#ps) = get l ps"
+  | "get (Node l v r) (R#ps) = get r ps"
+(*>*)
+
+  | "get _ _ = undefined" -- \<open>Catch-all clause to get rid of missing patterns warning\<close>
+  
+  
+text \<open>Specify a function \<open>put t p s\<close>, that returns \<open>t\<close>, with the subtree 
+  at \<open>p\<close> replaced by \<open>t\<close>.
+\<close>
+  fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)where
+    "put _ [] s = s"
+  | "put (Node l v r) (L#ps) s = Node (put l ps s) v r"  
+  | "put (Node l v r) (R#ps) s = Node l v (put r ps s)"  
+  | "put t _ _ = t"
+(*>*)
+
+text \<open>Specify your function such that it does nothing if an invalid path 
+  is given, and prove:  
+  \<close>
+
+  lemma put_invalid: "\<not>valid t p \<Longrightarrow> put t p s = t"
+(*<*)
+    apply (induction t p s rule: put.induct) by auto
+(*>*)
+
+text \<open>Note: this convention will simplify some of 
+  the lemmas, reducing the required validity preconditions.
+  
+  Prove the following algebraic laws on \<open>put\<close> and \<open>get\<close>. 
+  Add preconditions of the form \<open>valid t p\<close> where needed!
+  \<close>
+
+  lemma get_put[simp]: "put t p (get t p) = t"  
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma put_put[simp]: "put (put t p s) p s' = put t p s'"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+  lemma put_get[simp]:(*<*)
+    assumes "valid t p" shows
+    (*>*) "get (put t p s) p = s"  
+    (*<*)
+    using assms apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+  lemma valid_put[simp]:(*<*)
+    assumes "valid t p"  shows 
+    (*>*) "valid (put t p s) p"
+    (*<*)
+    using assms apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  text \<open>
+    Show the following lemmas about appending two paths:
+  \<close>  
+  lemma valid_append[simp]: "valid t (p@q) \<longleftrightarrow> valid t p \<and> valid (get t p) q"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma get_append[simp]: "valid t p \<Longrightarrow> get t (p@q) = get (get t p) q"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma put_append[simp]:(*<*)
+    fixes t p q s
+    defines "specify_a_meaningful_term_here \<equiv> put t p (put (get t p) q s)"
+    shows 
+    (*>*) "put t (p@q) s = specify_a_meaningful_term_here"
+    (*<*)
+    unfolding specify_a_meaningful_term_here_def
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+text {* \NumHomework{Remdups}{May 4} *}
+
+text \<open>Your task is to write a function that removes duplicates from a list, using a 
+  BST to efficiently store the set of already encountered elements.
+
+  You may want to start with an auxiliary function, that takes the BST with 
+  the elements seen so far as additional argument, and then define the actual function.
+\<close>
+
+fun bst_remdups_aux :: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
+(*<*) where
+  "bst_remdups_aux _ [] = []"
+| "bst_remdups_aux t (x#xs) = (if isin t x then bst_remdups_aux t xs else x#bst_remdups_aux (ins x t) xs)"
+(*>*)
+
+definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"
+
+
+text \<open>Show that your function preserves the set of elements, and returns a list 
+  with no duplicates (predicate \<open>distinct\<close> in Isabelle).
+  Hint: Generalization!
+\<close>
+(*<*)
+lemma bst_remdups_aux_set[simp]: "bst t \<Longrightarrow> set (bst_remdups_aux t xs) = set xs - set_tree t"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: set_tree_isin set_tree_ins bst_ins)
+  done
+
+lemma bst_remdups_aux_distinct[simp]: "bst t \<Longrightarrow> distinct (bst_remdups_aux t xs)"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: bst_ins set_tree_isin set_tree_ins)
+  done
+(*>*)
+
+lemma "set (bst_remdups xs) = set xs"
+(*<*)
+  by (simp add: bst_remdups_def)
+(*>*)
+
+lemma "distinct (bst_remdups xs)"    
+(*<*)
+  by (simp add: bst_remdups_def)
+(*>*)
+
+text \<open>A list \<open>xs\<close> is a sublist of \<open>ys\<close>,
+  if \<open>xs\<close> can be produced from \<open>ys\<close> by deleting an 
+  arbitrary number of elements.
+
+  Define a function \<open>sublist xs ys\<close> to check whether \<open>xs\<close> is a sublist of \<open>ys\<close>.
+\<close>
+fun sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
+(*<*)where
+  "sublist [] xs \<longleftrightarrow> True"
+| "sublist xs [] \<longleftrightarrow> False"  
+| "sublist (x#xs) (y#ys) \<longleftrightarrow> (x=y \<and> sublist xs ys) \<or> sublist (x#xs) ys"
+(*>*)
+
+text \<open>Show that your remdups function produces a sublist of the original list!
+
+  Hint: Generalization. Auxiliary lemma required.
+\<close>
+
+(*<*)
+lemma [simp]: "sublist xs ys \<Longrightarrow> sublist xs (y#ys)"  
+  by (induction xs) auto
+  
+lemma [simp]: "sublist (bst_remdups_aux t xs) xs"
+  apply (induction xs arbitrary: t)
+  apply auto
+  done
+
+(* In case someone adds the bst precondition: *)
+lemma "bst t \<Longrightarrow> sublist (bst_remdups_aux t xs) xs"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: bst_ins)
+  done
+
+(*>*)
+  
+lemma "sublist (bst_remdups xs) xs"
+(*<*)
+  by (auto simp: bst_remdups_def)
+(*>*)
+ 
+
+
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex03/tmpl03.thy	Fri Apr 27 10:24:36 2018 +0200
@@ -0,0 +1,354 @@
+(*<*)
+theory tmpl03
+imports "../BST_Demo" (** Adapt to fit your path! *)
+begin
+(*>*)
+
+
+
+text {* \ExerciseSheet{3}{27.~4.~2018} *}
+
+text \<open>
+  \Exercise{Membership Test with Less Comparisons}
+
+  In worst case, the @{const isin} function performs two comparisons per node.
+  In this exercise, we want to reduce this to one comparison per node, with the 
+  following idea:
+  
+  One never tests for \<open>>\<close>, but always goes right if not \<open><\<close>. 
+  However, one remembers the value where one should have tested for \<open>=\<close>,
+  and performs the comparison when a leaf is reached.
+\<close>
+      
+fun isin2 :: "('a::linorder) tree \<Rightarrow> 'a option \<Rightarrow> 'a \<Rightarrow> bool" 
+ \<comment> \<open>The second parameter stores the value for the deferred comparison\<close>
+(*<*)
+where
+"isin2 Leaf z x = (case z of None \<Rightarrow> False | Some y \<Rightarrow> x = y) " |
+"isin2 (Node l a r) z x =
+  (if x < a then isin2 l z x else isin2 r (Some a) x)"
+(*>*)  
+
+(*<*)
+lemma isin2_Some:
+  "\<lbrakk> bst t;  \<forall>x \<in> set_tree t. y < x \<rbrakk>
+  \<Longrightarrow> isin2 t (Some y) x = (isin t x \<or> x=y)"
+apply(induction t arbitrary: y)
+apply auto
+done
+(*>*)
+
+text \<open>Show that your function is correct. 
+
+  Hint: Auxiliary lemma for \<open>isin2 t (Some y) x\<close> !
+\<close>
+lemma isin2_None:
+  "bst t \<Longrightarrow> isin2 t None x = isin t x"
+(*<*)
+apply(induction t)
+apply auto
+apply (auto simp: isin2_Some)
+done
+(*>*)
+
+      
+text \<open>
+  \Exercise{Height-Preserving In-Order Join}
+  Write a function that joins two binary trees such that
+  \<^item> The in-order traversal of the new tree is the concatenation of the in-order traversals of the original tree
+  \<^item> The new tree is at most one higher than the highest original tree
+
+  Hint: Once you got the function right, proofs are easy!
+\<close>  
+fun join :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)  
+  where
+"join t Leaf = t" |
+"join Leaf t = t" |
+"join (Node l1 a1 r1) (Node l2 a2 r2) =
+   (case join r1 l2 of
+     Leaf \<Rightarrow> Node l1 a1 (Node Leaf a2 r2) |
+     Node l b r \<Rightarrow> Node (Node l1 a1 l) b (Node r a2 r2))"
+(*>*)
+
+lemma join_inorder[simp]: "inorder(join t1 t2) = inorder t1 @ inorder t2"
+(*<*)  
+apply(induction t1 t2 rule: join.induct)
+apply (auto split: tree.split)
+done
+(*>*)
+
+lemma "height(join t1 t2) \<le> max (height t1) (height t2) + 1"
+(*<*)  
+apply(induction t1 t2 rule: join.induct)
+apply (auto split: tree.split)
+done
+(*>*)
+
+text \<open>
+  \Exercise{Implement Delete}
+  Implement delete using the \<open>join\<close> function from last exercise.
+\<close>  
+
+text \<open>Note: At this point, we are not interested in the implementation details 
+  of join any more, but just in its specification, i.e., what it does to trees.
+  Thus, as first step, we declare its equations to not being automatically unfolded.
+\<close>
+
+declare join.simps[simp del]
+
+text \<open>Both, \<open>set_tree\<close> and \<open>bst\<close> can be expressed by the inorder traversal over trees:\<close>
+
+thm set_inorder[symmetric] bst_iff_sorted_wrt_less
+
+text \<open>Note: As @{thm [source] set_inorder} is declared as simp. 
+  Be careful not to have both directions of the lemma in the simpset at the 
+  same time, otherwise the simplifier is likely to loop.
+  
+  You can use \<open>simp del: set_inorder add: set_inorder[symmetric]\<close>, or
+  \<open>auto simp del: set_inorder simp: set_inorder[symmetric]\<close> to 
+  temporarily remove the lemma from the simpset.
+  
+  Alternatively, you can write \<open>declare set_inorder[simp_del]\<close> to
+  remove it once and forall.
+\<close>
+
+
+text "For the \<open>sorted_wrt\<close> predicate, you might want to use these lemmas as simp:"
+thm sorted_wrt_append sorted_wrt_Cons
+
+text \<open>Show that join preserves the set of entries\<close>
+lemma [simp]: "set_tree (join t1 t2) = set_tree t1 \<union> set_tree t2"
+(*<*)
+  by (simp del: set_inorder add: set_inorder[symmetric])
+(*>*)  
+
+text \<open>Show that joining the left and right child of a BST is again a BST:\<close>
+
+lemma [simp]: "bst (Node l (x::_::linorder) r) \<Longrightarrow> bst (join l r)"
+(*<*)
+  by (simp del: bst_wrt.simps add: bst_iff_sorted_wrt_less sorted_wrt_append sorted_wrt_Cons)
+(*>*)  
+
+text \<open>Implement a delete function using the idea contained in the lemmas above.\<close>  
+fun delete :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)where
+  "delete x Leaf = Leaf"
+| "delete x (Node l v r) = (
+    if x=v then join l r 
+    else if x<v then Node (delete x l) v r
+    else Node l v (delete x r)
+  )"  
+(*>*)  
+
+text \<open>Prove it correct! Note: You'll need the first lemma to prove the second one! \<close>  
+lemma [simp]: "bst t \<Longrightarrow> set_tree (delete x t) = set_tree t - {x}"
+(*<*)
+  apply (induction t)
+  apply auto
+  done
+(*>*)
+
+
+lemma "bst t \<Longrightarrow> bst (delete x t)"
+(*<*)
+  apply (induction t)
+  apply auto
+  done
+(*>*)
+  
+
+text {* \NumHomework{Tree Addressing}{May 4} *}
+text \<open>
+  A position in a tree can be given as a list of 
+  navigation instructions from the root, i.e., whether to go 
+  to the left or right subtree. We call such a list a path.
+\<close>
+  datatype direction = L | R
+  type_synonym path = "direction list"
+
+text \<open>Specify when a path is valid:\<close>  
+  
+  fun valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool" where
+(*<*)
+    "valid t [] \<longleftrightarrow> True"
+  | "valid (Node l v r) (L#ps) \<longleftrightarrow> valid l ps"
+  | "valid (Node l v r) (R#ps) \<longleftrightarrow> valid r ps"
+  | "valid _ _ \<longleftrightarrow> False"  
+(*>*)
+  
+text \<open>Specify a function to return the subtree addressed by a given path:\<close>  
+  fun get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree" 
+(*<*)where
+    "get t [] = t"
+  | "get (Node l v r) (L#ps) = get l ps"
+  | "get (Node l v r) (R#ps) = get r ps"
+(*>*)
+
+  | "get _ _ = undefined" -- \<open>Catch-all clause to get rid of missing patterns warning\<close>
+  
+  
+text \<open>Specify a function \<open>put t p s\<close>, that returns \<open>t\<close>, with the subtree 
+  at \<open>p\<close> replaced by \<open>t\<close>.
+\<close>
+  fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
+(*<*)where
+    "put _ [] s = s"
+  | "put (Node l v r) (L#ps) s = Node (put l ps s) v r"  
+  | "put (Node l v r) (R#ps) s = Node l v (put r ps s)"  
+  | "put t _ _ = t"
+(*>*)
+
+text \<open>Specify your function such that it does nothing if an invalid path 
+  is given, and prove:  
+  \<close>
+
+  lemma put_invalid: "\<not>valid t p \<Longrightarrow> put t p s = t"
+(*<*)
+    apply (induction t p s rule: put.induct) by auto
+(*>*)
+
+text \<open>Note: this convention will simplify some of 
+  the lemmas, reducing the required validity preconditions.
+  
+  Prove the following algebraic laws on \<open>put\<close> and \<open>get\<close>. 
+  Add preconditions of the form \<open>valid t p\<close> where needed!
+  \<close>
+
+  lemma get_put[simp]: "put t p (get t p) = t"  
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma put_put[simp]: "put (put t p s) p s' = put t p s'"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+  lemma put_get[simp]:(*<*)
+    assumes "valid t p" shows
+    (*>*) "get (put t p s) p = s"  
+    (*<*)
+    using assms apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+  lemma valid_put[simp]:(*<*)
+    assumes "valid t p"  shows 
+    (*>*) "valid (put t p s) p"
+    (*<*)
+    using assms apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  text \<open>
+    Show the following lemmas about appending two paths:
+  \<close>  
+  lemma valid_append[simp]: "valid t (p@q) \<longleftrightarrow> valid t p \<and> valid (get t p) q"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma get_append[simp]: "valid t p \<Longrightarrow> get t (p@q) = get (get t p) q"
+    (*<*)
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+    
+  lemma put_append[simp]:(*<*)
+    fixes t p q s
+    defines "specify_a_meaningful_term_here \<equiv> put t p (put (get t p) q s)"
+    shows 
+    (*>*) "put t (p@q) s = specify_a_meaningful_term_here"
+    (*<*)
+    unfolding specify_a_meaningful_term_here_def
+    apply (induction t p rule: get.induct) by auto
+    (*>*)
+
+text {* \NumHomework{Remdups}{May 4} *}
+
+text \<open>Your task is to write a function that removes duplicates from a list, using a 
+  BST to efficiently store the set of already encountered elements.
+
+  You may want to start with an auxiliary function, that takes the BST with 
+  the elements seen so far as additional argument, and then define the actual function.
+\<close>
+
+fun bst_remdups_aux :: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
+(*<*) where
+  "bst_remdups_aux _ [] = []"
+| "bst_remdups_aux t (x#xs) = (if isin t x then bst_remdups_aux t xs else x#bst_remdups_aux (ins x t) xs)"
+(*>*)
+
+definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"
+
+
+text \<open>Show that your function preserves the set of elements, and returns a list 
+  with no duplicates (predicate \<open>distinct\<close> in Isabelle).
+  Hint: Generalization!
+\<close>
+(*<*)
+lemma bst_remdups_aux_set[simp]: "bst t \<Longrightarrow> set (bst_remdups_aux t xs) = set xs - set_tree t"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: set_tree_isin set_tree_ins bst_ins)
+  done
+
+lemma bst_remdups_aux_distinct[simp]: "bst t \<Longrightarrow> distinct (bst_remdups_aux t xs)"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: bst_ins set_tree_isin set_tree_ins)
+  done
+(*>*)
+
+lemma "set (bst_remdups xs) = set xs"
+(*<*)
+  by (simp add: bst_remdups_def)
+(*>*)
+
+lemma "distinct (bst_remdups xs)"    
+(*<*)
+  by (simp add: bst_remdups_def)
+(*>*)
+
+text \<open>A list \<open>xs\<close> is a sublist of \<open>ys\<close>,
+  if \<open>xs\<close> can be produced from \<open>ys\<close> by deleting an 
+  arbitrary number of elements.
+
+  Define a function \<open>sublist xs ys\<close> to check whether \<open>xs\<close> is a sublist of \<open>ys\<close>.
+\<close>
+fun sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
+(*<*)where
+  "sublist [] xs \<longleftrightarrow> True"
+| "sublist xs [] \<longleftrightarrow> False"  
+| "sublist (x#xs) (y#ys) \<longleftrightarrow> (x=y \<and> sublist xs ys) \<or> sublist (x#xs) ys"
+(*>*)
+
+text \<open>Show that your remdups function produces a sublist of the original list!
+
+  Hint: Generalization. Auxiliary lemma required.
+\<close>
+
+(*<*)
+lemma [simp]: "sublist xs ys \<Longrightarrow> sublist xs (y#ys)"  
+  by (induction xs) auto
+  
+lemma [simp]: "sublist (bst_remdups_aux t xs) xs"
+  apply (induction xs arbitrary: t)
+  apply auto
+  done
+
+(* In case someone adds the bst precondition: *)
+lemma "bst t \<Longrightarrow> sublist (bst_remdups_aux t xs) xs"
+  apply (induction xs arbitrary: t)
+  apply (auto simp: bst_ins)
+  done
+
+(*>*)
+  
+lemma "sublist (bst_remdups xs) xs"
+(*<*)
+  by (auto simp: bst_remdups_def)
+(*>*)
+ 
+
+
+(*<*)
+end
+(*>*)
+