exam draft
authorlammich <lammich@in.tum.de>
Tue, 03 Jul 2018 11:20:53 +0200
changeset 69939 a7655a4900e5
parent 69936 221867bb14cd
child 69940 e04bcdda9c3a
exam
SS18/Exercises/ROOT
SS18/Exercises/ex12/ex12sol.thy
SS18/Exercises/ex12sol.pdf
SS18/Exercises/ex13.pdf
SS18/Exercises/ex13/Q_Balanced_Insert.thy
SS18/Exercises/ex13/Q_Tree_Same_Struct.thy
SS18/Exercises/ex13/document/build
SS18/Exercises/ex13/document/exercise.sty
SS18/Exercises/ex13/document/root.tex
SS18/Exercises/ex13/ex13.thy
SS18/Exercises/ex13/hw13.thy
SS18/Exercises/exam.pdf
SS18/Exercises/exam/Q_Amortized.thy
SS18/Exercises/exam/Q_Balanced_Insert.thy
SS18/Exercises/exam/Q_Induction.thy
SS18/Exercises/exam/Q_Min_BST.thy
SS18/Exercises/exam/Q_Tree_Same_Struct.thy
SS18/Exercises/exam/Q_Trie.thy
SS18/Exercises/exam/Q_Unique_SBN.thy
SS18/Exercises/exam/document/build
SS18/Exercises/exam/document/exercise.sty
SS18/Exercises/exam/document/root.tex
SS18/Exercises/exam/exam.thy
--- a/SS18/Exercises/ROOT	Mon Jul 02 11:33:43 2018 +0200
+++ b/SS18/Exercises/ROOT	Tue Jul 03 11:20:53 2018 +0200
@@ -68,6 +68,18 @@
   theories ex12sol
   document_files "root.tex" "exercise.sty" "build"
 
+session "ex13" in "ex13" = "HOL-Data_Structures" +
+  options [document = pdf, document_output = "generated", document_variants = "ex13"]
+  theories [document = false]
+    "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
+  theories ex13 Q_Balanced_Insert Q_Tree_Same_Struct hw13
+  document_files "root.tex" "exercise.sty" "build"
+
+session "exam" in "exam" = "HOL-Data_Structures" +
+  options [document = pdf, document_output = "generated", document_variants = "exam"]
+  theories exam
+  document_files "root.tex" "exercise.sty" "build"
+
 
 (*
 session hwsol_basis = HOL +
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex12/ex12sol.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,271 @@
+
+theory ex12sol
+imports
+  Complex_Main
+  "HOL-Library.Multiset"
+begin
+
+text {* \ExerciseSheet{12}{29.~6.~2018} *}
+
+text \<open>
+  \Exercise{Sparse Binary Numbers}
+
+  Implement operations carry, inc, and add on sparse binary numbers,
+  analogously to the operations link, ins, and meld on binomial heaps.
+
+  Show that the operations have logarithmic worst-case complexity.
+\<close>
+
+type_synonym rank = nat
+type_synonym snat = "rank list"
+
+abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> sorted_wrt op< s"
+definition \<alpha> :: "snat \<Rightarrow> nat" where "\<alpha> s = (\<Sum>i\<leftarrow>s. 2^i)"
+
+lemmas [simp] = sorted_wrt_Cons sorted_wrt_append
+
+
+
+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
+
+
+
+fun carry :: "rank \<Rightarrow> snat \<Rightarrow> snat"
+
+  where
+  "carry r [] = [r]"
+| "carry r (r'#rest) = (if r<r' then r#r'#rest else carry (r+1) rest)"
+
+
+lemma carry_invar[simp]:
+
+  assumes "invar rs"
+  shows "invar (carry r rs)"
+  using assms
+  apply (induction r rs rule: carry.induct)
+  apply (auto)
+  done
+
+
+lemma carry_\<alpha>:
+
+  assumes "invar rs"
+  assumes "\<forall>r'\<in>set rs. r\<le>r'"
+  shows "\<alpha> (carry r rs) = 2^r + \<alpha> rs"
+  using assms
+  by (induction r rs rule: carry.induct) force+
+
+
+
+lemma carry_rank_bound:
+  assumes "r' \<in> set (carry r rs)"
+  assumes "\<forall>r'\<in>set rs. r\<^sub>0 < r'"
+  assumes "r\<^sub>0 < r"
+  shows "r\<^sub>0 < r'"
+  using assms
+  by (induction r rs rule: carry.induct) (auto split: if_splits)
+
+
+
+definition inc :: "snat \<Rightarrow> snat"
+
+  where "inc rs = carry 0 rs"
+
+
+lemma inc_invar[simp]: "invar rs \<Longrightarrow> invar (inc rs)"
+
+  unfolding inc_def by auto
+
+
+lemma inc_\<alpha>[simp]: "invar rs \<Longrightarrow> \<alpha> (inc rs) = Suc (\<alpha> rs)"
+
+  unfolding inc_def by (auto simp: carry_\<alpha>)
+
+
+fun add :: "snat \<Rightarrow> snat \<Rightarrow> snat"
+
+  where
+  "add rs [] = rs"
+| "add [] rs = rs"
+| "add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = (
+    if r\<^sub>1 < r\<^sub>2 then r\<^sub>1#add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
+    else if r\<^sub>2<r\<^sub>1 then r\<^sub>2#add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
+    else carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2)
+    )"
+
+
+
+lemma add_rank_bound:
+  assumes "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)"
+  assumes "\<forall>r'\<in>set rs\<^sub>1. r < r'"
+  assumes "\<forall>r'\<in>set rs\<^sub>2. r < r'"
+  shows "r < r'"
+  using assms
+  apply (induction rs\<^sub>1 rs\<^sub>2 arbitrary: r' rule: add.induct)
+  apply (auto split: if_splits simp: carry_rank_bound)
+  done
+
+
+lemma add_invar[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "invar (add rs\<^sub>1 rs\<^sub>2)"
+
+  using assms
+proof (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)
+  case (3 r\<^sub>1 rs\<^sub>1 r\<^sub>2 rs\<^sub>2)
+
+  consider (LT) "r\<^sub>1 < r\<^sub>2"
+         | (GT) "r\<^sub>1 > r\<^sub>2"
+         | (EQ) "r\<^sub>1 = r\<^sub>2"
+    using antisym_conv3 by blast
+  then show ?case proof cases
+    case LT
+    then show ?thesis using 3
+      by (force elim!: add_rank_bound)
+  next
+    case GT
+    then show ?thesis using 3
+      by (force elim!: add_rank_bound)
+  next
+    case [simp]: EQ
+
+    from "3.IH"(3) "3.prems" have [simp]: "invar (add rs\<^sub>1 rs\<^sub>2)"
+      by auto
+
+    have "r\<^sub>2 < r'" if "r' \<in> set (add rs\<^sub>1 rs\<^sub>2)" for r'
+      using that
+      apply (rule add_rank_bound)
+      using "3.prems" by auto
+    with EQ show ?thesis by auto
+  qed
+qed simp_all
+
+
+lemma add_\<alpha>[simp]:
+  assumes "invar rs\<^sub>1"
+  assumes "invar rs\<^sub>2"
+  shows "\<alpha> (add rs\<^sub>1 rs\<^sub>2) = \<alpha> rs\<^sub>1 + \<alpha> rs\<^sub>2"
+
+  using assms
+  apply (induction rs\<^sub>1 rs\<^sub>2 rule: add.induct)
+  apply (auto simp: carry_\<alpha> Suc_leI add_rank_bound)
+  done
+
+
+
+lemma size_snat:
+  assumes "invar rs"
+  shows "2^length rs \<le> \<alpha> rs + 1"
+
+proof -
+  have "(2::nat)^length rs = (\<Sum>i\<in>{0..<length rs}. 2^i) + 1"
+    by (simp add: sum_power2)
+  also have "\<dots> \<le> \<alpha> rs + 1"
+    using assms unfolding \<alpha>_def
+    by (simp add: sorted_wrt_less_sum_mono_lowerbound)
+  finally show ?thesis .
+qed
+
+
+fun t_carry :: "rank \<Rightarrow> snat \<Rightarrow> nat"
+
+  where
+  "t_carry r [] = 1"
+| "t_carry r (r'#rest) = (if r<r' then 1 else 1 + t_carry (r+1) rest)"
+
+
+definition t_inc :: "snat \<Rightarrow> nat"
+
+  where "t_inc rs = t_carry 0 rs"
+
+
+lemma t_inc_bound:
+  assumes "invar rs"
+  shows "t_inc rs \<le> log 2 (\<alpha> rs + 1) + 1"
+
+proof -
+  have "t_carry r rs \<le> length rs + 1" for r
+    by (induction r rs rule: t_carry.induct) auto
+  hence "t_inc rs \<le> length rs + 1" unfolding t_inc_def by auto
+  hence "(2::nat)^t_inc rs \<le> 2^(length rs + 1)"
+    by (rule power_increasing) auto
+  also have "\<dots> \<le> 2*(\<alpha> rs + 1)" using size_snat[OF \<open>invar rs\<close>] by auto
+  finally have "2 ^ t_inc rs \<le> 2 * (\<alpha> rs + 1)" .
+  from le_log2_of_power[OF this] show ?thesis
+    by (simp only: log_mult of_nat_mult) auto
+qed
+
+
+fun t_add :: "snat \<Rightarrow> snat \<Rightarrow> nat"
+
+  where
+  "t_add rs [] = 1"
+| "t_add [] rs = 1"
+| "t_add (r\<^sub>1#rs\<^sub>1) (r\<^sub>2#rs\<^sub>2) = 1 + (
+    if r\<^sub>1 < r\<^sub>2 then t_add rs\<^sub>1 (r\<^sub>2#rs\<^sub>2)
+    else if r\<^sub>2<r\<^sub>1 then t_add (r\<^sub>1#rs\<^sub>1) rs\<^sub>2
+    else t_carry (r\<^sub>1 + 1) (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2
+    )"
+
+
+
+lemma l_carry_estimate:
+  "t_carry r rs + length (carry r rs) = 2 + length rs"
+  by (induction r rs rule: carry.induct) auto
+
+lemma l_add_estimate:
+  "length (add rs\<^sub>1 rs\<^sub>2) + t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1"
+  apply (induction rs\<^sub>1 rs\<^sub>2 rule: t_add.induct)
+  apply (auto simp: l_carry_estimate algebra_simps)
+  done
+
+
+lemma t_add_bound:
+  fixes rs\<^sub>1 rs\<^sub>2
+  defines "n\<^sub>1 \<equiv> \<alpha> rs\<^sub>1"
+  defines "n\<^sub>2 \<equiv> \<alpha> rs\<^sub>2"
+  assumes INVARS: "invar rs\<^sub>1" "invar rs\<^sub>2"
+  shows "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
+
+proof -
+  define n where "n = n\<^sub>1 + n\<^sub>2"
+
+  from l_add_estimate[of rs\<^sub>1 rs\<^sub>2]
+  have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1" by auto
+  hence "(2::nat)^t_add rs\<^sub>1 rs\<^sub>2 \<le> 2^(2 * (length rs\<^sub>1 + length rs\<^sub>2) + 1)"
+    by (rule power_increasing) auto
+  also have "\<dots> = 2*(2^length rs\<^sub>1)\<^sup>2*(2^length rs\<^sub>2)\<^sup>2"
+    by (auto simp: algebra_simps power_add power_mult)
+  also note INVARS(1)[THEN size_snat]
+  also note INVARS(2)[THEN size_snat]
+  finally have "2 ^ t_add rs\<^sub>1 rs\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
+    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
+  from le_log2_of_power[OF this] have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 \<dots>"
+    by simp
+  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
+    by (simp add: log_mult log_nat_power)
+  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"
+    by auto
+  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
+    by auto
+  also have "log 2 2 \<le> 2" by auto
+  finally have "t_add rs\<^sub>1 rs\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
+  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
+qed
+
+
+
+
+
+end
+
Binary file SS18/Exercises/ex12sol.pdf has changed
Binary file SS18/Exercises/ex13.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex13/Q_Balanced_Insert.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,56 @@
+(*<*)
+theory Q_Balanced_Insert
+imports
+  Complex_Main
+  "HOL-Library.Multiset"
+  "HOL-Data_Structures.Tree_Set"
+begin
+(*>*)
+
+  text \<open>\Exercise{Converting List for Balanced Insert}\<close>
+  (*<*)
+  consts preprocess :: "'a::linorder list \<Rightarrow> 'a list"
+  (*>*)
+
+  text \<open>
+    Recall the standard insertion function for unbalanced binary search trees.
+    @{theory_text [display] \<open>
+      fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+      "insert x Leaf = Node Leaf x Leaf" |
+      "insert x (Node l a r) =
+        (case cmp x a of
+           LT \<Rightarrow> Node (insert x l) a r |
+           EQ \<Rightarrow> Node l a r |
+           GT \<Rightarrow> Node l a (insert x r))"
+    \<close>}
+
+    We define the function \<open>from_list\<close>, which inserts the elements of a
+    list into an initially empty search tree:
+  \<close>
+  definition from_list :: "'a::linorder list \<Rightarrow> 'a tree" where
+    "from_list l = fold insert l Leaf"
+
+  text \<open>
+    Your task is to specify a function @{term_type preprocess},
+    that preprocesses the list such that the resulting tree is balanced.
+
+    You may assume that the list
+    is sorted, distinct, and has exactly \<open>2^k - 1\<close> elements for some \<open>k\<close>.
+    That is, your \<open>preprocess\<close> function must satisfy:
+  \<close>
+  lemma
+    assumes "sorted l" and "distinct l" and  "length l = 2^k-1"
+    shows "set (preprocess l) = set l" and "balanced (from_list (preprocess l))"
+    (*<*) oops (*>*)
+
+  text \<open>
+    Note: {\bf No proofs required}, only a specification of the \<open>preprocess\<close> function!
+  \<close>
+
+  (* Solution does not work any more in Isabelle2017, and may be cumbersome to restore,
+    b/c the stuff instantiated in Tree_Set is nearly unusable *)
+
+(*<*)
+end
+(*>*)
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex13/Q_Tree_Same_Struct.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,87 @@
+(*<*)
+theory Q_Tree_Same_Struct
+imports
+  Complex_Main
+  "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
+begin
+(*>*)
+
+  text \<open>\Exercise{Trees with Same Structure}\<close>
+  (*<*)
+  fun same where
+    "same Leaf Leaf = True" |
+    "same (Node l a r) (Node l' a' r') = (same l l' \<and> same r r')" |
+    "same _ _ = False"
+  (*>*)
+
+  (*<*)
+  lemma same_insert: "same t t'
+     \<Longrightarrow> same (insert x t) (insert y t')"
+    by (induction t t' arbitrary: x y rule: same.induct) auto
+  (*>*)
+
+  text \<open>
+    \textbf{Question 1}
+
+    Specify the recursion equations of a function
+    @{term_type same} that returns true if and only if the two trees
+    have the same structure (i.e., ignoring values).
+  \<close>
+
+  text \<open>
+    \textbf{Question 2}
+
+    Show, by computation induction wrt.~\<open>same\<close>, that insertion
+    of arbitrary elements into two Braun heaps with the same structure
+    yields heaps with the same structure again.
+    @{thm [display] same_insert}
+    For your proof, it is enough to cover the (Node,Node) case.
+    If you get analogous sub-cases, only elaborate one of them!
+
+    Hint: Here is the definition of @{const insert}:
+    @{theory_text [display] \<open>
+  fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "insert a Leaf = Node Leaf a Leaf" |
+  "insert a (Node l x r) =
+   (if a < x then Node (insert x r) a l else Node (insert a r) x l)"
+      \<close>}
+  \<close>
+
+  (*<*)
+  subsubsection \<open>Solution\<close>
+  lemma "same t t'
+     \<Longrightarrow> same (insert x t) (insert y t')"
+  proof (induction t t' arbitrary: x y rule: same.induct)
+    case (2 l a r l' a' r')
+
+    have -- \<open>Induction hypothesis, generalized over \<open>x,y\<close>! \<close>
+      IH1: "same (insert x l) (insert y l')" and
+      IH2: "same (insert x r) (insert y r')" for x y
+      using 2 by auto
+
+    assume PREM: "same \<langle>l, a, r\<rangle> \<langle>l', a', r'\<rangle>"
+
+    show "same (insert x \<langle>l, a, r\<rangle>) (insert y \<langle>l', a', r'\<rangle>)"
+    proof -
+      -- \<open>We get four cases\<close>
+      consider \<open>x<a \<and> y<a'\<close> | \<open>x<a \<and> y\<ge>a'\<close> | \<open>x\<ge>a \<and> y<a'\<close> | \<open>x\<ge>a \<and> y\<ge>a'\<close>
+        by force
+      then show ?thesis proof cases
+        case 1
+        hence
+          "insert x \<langle>l,a,r\<rangle> = \<langle>insert a r, x, l\<rangle>"
+          "(insert y \<langle>l', a', r'\<rangle>) = \<langle>insert a' r', y, l'\<rangle>"
+          by simp_all
+        moreover from PREM have "same l l'" by simp
+        moreover note IH2
+        ultimately show ?thesis by simp
+        -- \<open>The other cases are analogous\<close>
+      qed (insert IH1 IH2 PREM; auto)+
+    qed
+  qed auto -- \<open>The other cases are simple\<close>
+
+  (*>*)
+
+(*<*)
+end
+(*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex13/document/build	Tue Jul 03 11:20:53 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/ex13/document/exercise.sty	Tue Jul 03 11:20:53 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/ex13/document/root.tex	Tue Jul 03 11:20:53 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/ex13/ex13.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,27 @@
+(*<*)
+theory ex13
+imports Main
+begin
+(*>*)
+text {* \ExerciseSheet{13}{6.~7.~2018}*}
+
+text  \<open>{
+  \large\bf Presentation of Mini-Projects}
+
+  You are invited, on a voluntary basis, to give a short presentation
+  of your mini-projects in the tutorial on July 13.
+
+  Depending on how many presentations we have, the time slots
+  will be 5 to 10 minutes, plus 2 minutes for questions.
+
+  If you are interested, please write me a short email until Wednesday, July 11.
+\<close>
+
+
+text \<open>
+  The following are old exam questions!
+\<close>
+
+(*<*)
+end
+(*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex13/hw13.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,56 @@
+(*<*)
+theory hw13
+imports Main
+begin
+(*>*)
+
+text \<open>\Homework{Amortized Complexity}{13.07.2018}
+
+  This is an old exam question, which we have converted to a homework to
+  be done with Isabelle!
+\<close>
+
+text \<open>A ``stack with multipop'' is a list with the following two interface functions:\<close>
+
+fun push :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"push x xs = x # xs"
+
+fun pop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pop n xs = drop n xs"
+
+text \<open>You may assume\<close>
+
+definition t_push :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_push x xs = 1"
+
+definition t_pop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_pop n xs = min n (length xs)"
+
+text \<open>Use the potential method to show that
+the amortized complexity of \<open>push\<close> and \<open>pop\<close> is constant.
+
+Provide complete proofs in Isabelle!
+
+Original text here was:
+\emph{
+If you need any properties of the auxiliary functions \<open>length\<close>, \<open>drop\<close> and \<open>min\<close>,
+you should state them but you do not need to prove them.}\<close>
+
+(*<*)
+subsubsection \<open>Solution\<close>
+fun \<Phi> :: "'a list \<Rightarrow> nat" where
+"\<Phi> xs = length xs"
+
+lemma "t_push x xs + \<Phi>(push x xs) - \<Phi> xs = 2"
+by(simp add: t_push_def)
+
+lemma "t_pop n xs + \<Phi>(pop n xs) - \<Phi> xs = 0"
+by(simp add: t_pop_def)
+
+(*>*)
+
+(*<*)
+end
+(*>*)
+
+
Binary file SS18/Exercises/exam.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Amortized.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,45 @@
+(*<*)
+theory Q_Amortized
+imports Main
+begin
+(*>*)
+section "Amortized Complexity"
+
+text \<open>A ``stack with multipop'' is a list with the following two interface functions:\<close>
+
+fun push :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"push x xs = x # xs"
+
+fun pop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"pop n xs = drop n xs"
+
+text \<open>You may assume\<close>
+
+definition t_push :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_push x xs = 1"
+
+definition t_pop :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
+"t_pop n xs = min n (length xs)"
+
+text \<open>Use the potential method to show that
+the amortized complexity of \<open>push\<close> and \<open>pop\<close> is constant.
+If you need any properties of the auxiliary functions \<open>length\<close>, \<open>drop\<close> and \<open>min\<close>,
+you should state them but you do not need to prove them.\<close>
+
+subsubsection \<open>Solution\<close>
+fun \<Phi> :: "'a list \<Rightarrow> nat" where
+"\<Phi> xs = length xs"
+
+lemma "t_push x xs + \<Phi>(push x xs) - \<Phi> xs = 2"
+by(simp add: t_push_def)
+
+lemma "t_pop n xs + \<Phi>(pop n xs) - \<Phi> xs = 0"
+by(simp add: t_pop_def)
+  
+(*<*)  
+end
+(*>*)  
+text_raw \<open>\blankpage\<close>
+  
+  
+  
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Balanced_Insert.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,285 @@
+(*<*)    
+theory Q_Balanced_Insert
+imports  
+  Complex_Main
+  "~~/src/HOL/Library/Multiset"
+  "../../../Public/Demos/BST_Demo"
+begin
+(*>*)
+    
+  section \<open>Converting List for Balanced Insert\<close>  
+  (*<*)
+  consts preprocess :: "'a::linorder list \<Rightarrow> 'a list" 
+  (*>*)
+
+  text \<open>
+    Recall the standard insertion function for unbalanced binary search trees.
+    @{theory_text [display] \<open>
+      fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+      "ins x Leaf = Node Leaf x Leaf" |
+      "ins x (Node l a r) =
+        (if x < a then Node (ins x l) a r else
+         if x > a then Node l a (ins x r)
+         else Node l a r)"
+    \<close>}
+
+    We define the function \<open>from_list\<close>, which inserts the elements of a 
+    list into an initially empty search tree:
+  \<close>
+  definition from_list :: "'a::linorder list \<Rightarrow> 'a tree" where 
+    "from_list l = fold ins l Leaf"
+
+  text \<open>  
+    Your task is to specify a function @{term_type preprocess}, 
+    that preprocesses the list such that the resulting tree is balanced.
+
+    You may assume that the list
+    is sorted, distinct, and has exactly \<open>2^k - 1\<close> elements for some \<open>k\<close>.
+    That is, your \<open>preprocess\<close> function must satisfy:
+  \<close>
+  lemma 
+    assumes "sorted l" and "distinct l" and  "length l = 2^k-1"
+    shows "set (preprocess l) = set l" and "balanced (from_list (preprocess l))"
+    (*<*) oops (*>*)
+
+  text \<open>    
+    Note: {\bf No proofs required}, only a specification of the \<open>preprocess\<close> function!
+  \<close>  
+
+  subsubsection \<open>Solution\<close>  
+    
+    
+  definition split :: "'a list \<Rightarrow> ('a list \<times> 'a \<times> 'a list)" where
+    "split l = (let n=length l in (take (n div 2) l, l!(n div 2), drop (n div 2 + 1) l))"
+  
+  (*<*)    
+  lemma split_lemma:
+    assumes "(l,x,r) = split xs" 
+    assumes "xs\<noteq>[]"  
+    shows "xs = l@x#r"
+    using assms unfolding split_def  
+    by (cases "even (length xs)"; auto elim!: dvdE simp: id_take_nth_drop)  
+
+  lemma split_lemma':
+    assumes "(l,x,r) = split xs" 
+    assumes "length xs = 2^(Suc k) - 1"  
+    shows "length r = length l" "length l = 2^k - 1" "xs = l@x#r"
+    using assms unfolding split_def  
+    apply -  
+    apply (auto simp: min_def)
+    apply (smt One_nat_def Suc_double_not_eq_double Suc_eq_plus1 Suc_mult_two_diff_one add_diff_cancel_left diff_Suc_1 dvd_mult_div_cancel mult_2 nonzero_mult_div_cancel_left odd_Suc_div_two power_not_zero zero_not_eq_two)
+    by (metis One_nat_def Suc_mult_two_diff_one assms(1) list.size(3) nonzero_mult_div_cancel_left one_div_two_eq_zero power_not_zero split_lemma zero_not_eq_two)
+      
+  lemma [simp]: "(l,a,r) = split (x#xs) \<Longrightarrow> length l < Suc (length xs) \<and> length r < Suc (length xs)"
+    using split_lemma[of l a r "x#xs"] 
+    apply auto
+    apply (metis append_eq_conv_conj diff_self_eq_0 length_Cons length_drop length_take linorder_neqE_nat min.strict_order_iff nat.distinct(1))
+    by (metis Suc_le_lessD le_add2 length_Cons length_append)  
+
+  (*>*)
+      
+  fun preproc :: "'a list \<Rightarrow> 'a list" where
+    "preproc [] = []"
+  | "preproc xs = (let (l,x,r) = split xs in x#preproc l@preproc r)"
+      
+
+  (*<*)    
+  lemma split_mset: 
+    "\<lbrakk> split (x#xs) = (l,a,r) \<rbrakk> \<Longrightarrow> add_mset x (mset xs) = add_mset a (mset l + mset r)"  
+    apply (drule split_lemma[OF sym]) 
+    apply simp  
+    apply (drule arg_cong[where f=mset])
+    by auto  
+    
+  lemma L_mset_preserve[simp]: "mset (preproc l) = mset l"  
+    apply (induction l rule: preproc.induct)
+    apply simp
+    apply (auto dest: split_mset split:prod.split)
+    done        
+
+  theorem L_set_preserve[simp]: "set (preproc l) = set l"  
+    by (metis L_mset_preserve set_mset_mset)
+      
+  lemma L_len_preserve[simp]: "length (preproc l) = length l"  
+    by (metis L_mset_preserve size_mset)
+      
+  lemma ins_left:
+    assumes "\<forall>x\<in>set xs. x<a"
+    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>fold ins xs l,a,r\<rangle>" 
+    using assms
+    by (induction xs arbitrary: l) auto  
+    
+  lemma ins_right:
+    assumes "\<forall>x\<in>set xs. x>a"
+    shows "fold ins xs \<langle>l, a, r\<rangle> = \<langle>l,a,fold ins xs r\<rangle>" 
+    using assms
+    by (induction xs arbitrary: r) auto
+    
+  (* TODO: Move *)    
+  lemma empty_balanced[simp]: "balanced \<langle>\<rangle>" unfolding balanced_def by auto
+      
+  lemma bst_size_card_set: "bst t \<Longrightarrow> size t = card (set_tree t)"
+    apply (induction t) apply (auto)
+    using not_less_iff_gr_or_eq  
+    by (subst card_Un_disjoint card_insert_disjoint; auto)+
+      
+  lemma bst_fold_ins: "bst t \<Longrightarrow> bst (fold ins xs t)"
+    by (induction xs arbitrary: t) (auto simp: bst_ins)
+
+  lemma bst_from_list: "bst (from_list xs)"
+    unfolding from_list_def by (simp add: bst_fold_ins)
+      
+  lemma ss_aux: "bst t \<Longrightarrow> distinct xs \<Longrightarrow> set xs \<inter> set_tree t = {} \<Longrightarrow> card (set_tree (fold ins xs t)) = length xs + card (set_tree t)"
+  proof (induction xs arbitrary: t)
+    case Nil
+    then show ?case by auto
+  next
+    case (Cons a xs)
+    from Cons.IH[of "ins a t"] Cons.prems
+    have "card (set_tree (fold ins xs (ins a t))) = length xs + 1 + card (set_tree t)"
+      by (auto simp: bst_ins set_tree_ins)
+    then show ?case
+      by simp
+  qed
+      
+  lemma ss: "bst t \<Longrightarrow> distinct xs \<Longrightarrow> size (from_list xs) = length xs"  
+    by (simp add: bst_fold_ins ss_aux bst_size_card_set from_list_def)
+    
+      
+  lemma height_if_complete: "complete t \<Longrightarrow> height t = log 2 (size t + 1)" 
+    apply (drule size_if_complete)
+    by (auto simp: ln_realpow log_def)
+      
+      
+  theorem "\<lbrakk>sorted xs; distinct xs; length xs = 2^k - 1\<rbrakk> \<Longrightarrow> complete (from_list (preproc xs))"
+  proof (induction xs arbitrary: k rule: preproc.induct)
+    case 1
+    then show ?case by (auto simp: from_list_def split:prod.split)
+  next
+    case (2 v va)
+     
+    obtain l x r where  
+      X1[simp]: "split (v # va) = (l,x,r)"
+      by (cases "split (v # va)")
+
+    from split_lemma[OF X1[symmetric]] have
+      U: "v # va = l @ x # r"
+      by simp_all
+      
+    note PREMS = "2.prems"[unfolded U]
+      
+    from PREMS(3) obtain kk where KK[simp]: "k=Suc kk" 
+      by (cases k) auto
+    from split_lemma'[of l x r "v#va" kk, OF sym, OF X1]
+    have [simp]: "length r = length l" "length l = 2 ^ kk - 1" 
+      unfolding U using PREMS(3) by auto
+        
+    from PREMS have X2: "\<forall>y\<in>set (preproc l). y<x" "\<forall>y\<in>set (preproc r). x<y"
+      by (force simp: sorted_append sorted_Cons)+
+      
+    from PREMS(2) have [simp]: "distinct (preproc l)" "distinct (preproc r)"
+      by (clarsimp; auto simp: distinct_count_atmost_1)+
+        
+    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have 
+      C[simp]: "complete (from_list (preproc l))" "complete (from_list (preproc r))"
+      by (auto simp:sorted_Cons sorted_append)
+        
+    show ?case
+      apply (simp add: from_list_def)
+      apply (auto simp: ins_left ins_right X2)  
+      apply (fold from_list_def)  
+      apply simp_all  
+      using height_if_complete[OF C(1)] height_if_complete[OF C(2)]  
+      by (simp add: ss[OF bst_from_list])
+  qed 
+
+    
+  (*  attempt to prove for arbitrary sizes. Stopped at the following lemma for balanced!
+  lemma
+    assumes "balanced l"
+    assumes "balanced r"  
+    assumes "size r \<le> size l"  
+    assumes "size l \<le> size r + 1"  
+    shows "balanced \<langle>l,a,r\<rangle>"  
+  proof -
+    from assms(3,4) consider "size l = size r" | "size l = size r + 1"
+      by force
+    then show ?thesis proof (cases)
+      case 1
+        
+      with balanced_optimal[of l r] balanced_optimal[of r l] assms (1,2)
+      have "height l = height r" by auto
+        
+      then show ?thesis 
+        unfolding balanced_def
+        apply auto
+        by (metis One_nat_def assms(1) assms(2) balanced_def min_def)  
+    next
+      case 2
+        
+      with balanced_optimal[of r l] assms (1,2)
+      have "height r \<le> height l" by auto  
+      then show ?thesis
+        unfolding balanced_def
+        using assms(1,2) unfolding balanced_def  
+        apply (auto simp: max_def min_def not_le)
+        
+    qed    
+    
+  lemma "sorted xs \<Longrightarrow> distinct xs \<Longrightarrow> balanced (from_list (L xs))"
+  proof (induction xs rule: L.induct)
+    case 1
+    then show ?case by (auto simp: from_list_def split:prod.split)
+  next
+    case (2 v va)
+     
+    obtain l x r where  
+      X1[simp]: "split (v # va) = (l,x,r)"
+      by (cases "split (v # va)")
+
+    from split_lemma[OF X1[symmetric]] have
+      LEN: "length r \<le> length l" "length l \<le> length r + 1"
+      and U: "v # va = l @ x # r"
+      by simp_all
+      
+    note PREMS = "2.prems"[unfolded U]
+      
+    from PREMS have X2: "\<forall>y\<in>set (L l). y<x" "\<forall>y\<in>set (L r). x<y"
+      by (force simp: sorted_append sorted_Cons)+
+      
+    from PREMS(2) have [simp]: "distinct (L l)" "distinct (L r)"
+      by (clarsimp; auto simp: distinct_count_atmost_1)+
+        
+    from "2.IH"[unfolded X1, OF refl refl refl] PREMS have 
+      "balanced (from_list (L l))" "balanced (from_list (L r))"
+      by (auto simp:sorted_Cons sorted_append)
+        
+    have "size (from_list (L r)) \<le> size (from_list (L l))" "size (from_list (L l)) \<le> size (from_list (L r)) + 1"
+      using LEN
+      by (simp_all add: ss[OF bst_from_list])
+      
+        
+        
+        
+    show ?case
+      apply (simp add: from_list_def)
+      apply (auto simp: ins_left ins_right X2)  
+      apply (fold from_list_def)  
+        
+      
+  qed
+    apply (auto split: prod.split)  
+    apply (auto simp: from_list_def)  
+    apply (frule split_lemma(3)[OF sym]; simp)  
+    apply (clarsimp simp: sorted_append sorted_Cons ins_left)  
+      
+      
+    
+  *)  
+
+(*>*)    
+   
+(*<*)    
+end
+(*>*)    
+text_raw \<open>\blankpage\<close>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Induction.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,63 @@
+(*<*)
+theory Q_Induction
+imports Main
+begin
+(*>*)
+
+section \<open>Recursive Functions and Induction\<close>
+
+text \<open>Delta-encoding encodes a list of integers as follows:
+  The first element is unchanged, and every next element
+  indicates the difference to its predecessor.
+
+  For example:\\
+    \<open>enc [1,2,4,8] = [1,1,2,4]\<close>\\
+    \<open>enc [3,4,1] = [3,1,-3]\<close>\\
+    \<open>enc [5] = [5]\<close>\\
+    \<open>enc [] = []\<close>
+
+\<close>
+
+subsection \<open>Part 1\<close>
+
+text \<open> Specify a function to encode a list with delta-encoding.
+  The first argument is used to represent the previous value, and can be initialized to 0.\<close>
+
+fun denc :: "int \<Rightarrow> int list \<Rightarrow> int list"
+  (*<*) where
+  "denc prv [] = []"
+| "denc prv (x#xs) = (x-prv)#denc x xs"
+  (*>*)
+
+text_raw \<open>\vspace{5em}\<close>
+
+
+text \<open>Specify the decoder. Again, the first argument represents the previous
+    decoded value, and can be initialized to 0.\<close>
+fun ddec :: "int \<Rightarrow> int list \<Rightarrow> int list"
+  (*<*) where
+  "ddec prv [] = []"
+| "ddec prv (d#ds) = (prv+d) # ddec (prv+d) ds"
+  (*>*)
+
+text_raw \<open>\vspace{5em}\<close>
+
+subsection \<open>Part 2\<close>
+
+text \<open>Prove that encoding and then decoding yields the original list:\<close>
+
+(*<*)
+lemma dec_enc_id_aux: "ddec s (denc s l) = l"
+  by (induction l arbitrary: s) auto
+(*>*)
+
+lemma "ddec 0 (denc 0 l) = l"
+(*<*)
+  by (simp add: dec_enc_id_aux)
+(*>*)
+
+
+(*<*)
+end
+(*>*)
+text_raw \<open>\blankpage\<close>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Min_BST.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,135 @@
+(*<*)
+theory Q_Min_BST
+imports
+  Main
+  "HOL-Data_Structures.Set_by_Ordered"
+begin
+(*>*)
+  section \<open>Binary Search Trees with Priority Annotations\<close>
+  text \<open>Recall the standard annotated tree data type, where \<open>'a\<close> are
+    the items stored in the tree and \<open>'b\<close> is some node annotation.\<close>
+  datatype ('a,'b) tree = Leaf | Node 'b "('a,'b) tree" 'a "('a,'b) tree"
+
+  subsection \<open>Part 1\<close>
+  text \<open>Specify the inorder traversal function:\<close>
+
+  fun inorder :: "('a,'p)tree \<Rightarrow> 'a list"
+  (*<*)
+  where
+    "inorder Leaf = []" |
+    "inorder (Node _ l a r) = inorder l @ a # inorder r"
+  (*>*)
+  text_raw \<open>\vspace{5em}\<close>
+
+  subsection \<open>Part 2\<close>
+  text \<open>Now assume we have linearly ordered items of type \<open>'a::linorder\<close>.
+    Moreover, we have a (fixed) function \<open>prio :: 'a \<Rightarrow> 'p::linorder\<close> that
+    assigns each item a priority.
+  \<close>
+  context
+    fixes prio :: "'a::linorder \<Rightarrow> 'p::linorder"
+  begin
+
+    text \<open>The annotation of each node shall be an item with minimum priority
+      in the subtree rooted at this node.
+
+      Specify a function \<open>inva\<close> that expresses that the annotations are correct
+      as specified above:
+     \<close>
+    fun inva :: "('a, 'a) tree \<Rightarrow> bool"
+    (*<*)
+    where
+      "inva Leaf \<longleftrightarrow> True"
+    | "inva (Node p l a r) \<longleftrightarrow>
+          inva l \<and> inva r
+        \<and> p\<in>set (inorder l @ a # inorder r)
+        \<and> (\<forall>x\<in>set (inorder l @ a # inorder r). prio p \<le> prio x)"
+
+    definition "invar t \<longleftrightarrow> inva t \<and> sorted_wrt op< (inorder t)"
+
+    lemma [simp]: "invar Leaf" by (auto simp: invar_def)
+
+    (*>*)
+
+    subsection \<open>Part 3\<close>
+    text \<open>Specify a function to insert an element into a BST, preserving
+      the search tree property and the correctness of the annotations.
+
+      \textbf{No proofs required!}
+      \<close>
+
+    (*<*)
+    fun min_item where
+      "min_item a [] = a"
+    | "min_item a (Leaf#ns) = min_item a ns"
+    | "min_item a (Node b _ _ _ # ns) = min_item (if prio a \<le> prio b then a else b) ns"
+
+    definition "node l a r \<equiv> Node (min_item a [l,r]) l a r"
+
+    fun the_annot where "the_annot (Node m _ _ _) = m"
+
+    definition "node' l a r \<equiv> let
+      m = if l\<noteq>Leaf \<and> prio (the_annot l) < prio a then
+            if r\<noteq>Leaf \<and> prio (the_annot r) < prio (the_annot l) then the_annot r
+            else the_annot l
+          else if r\<noteq>Leaf \<and> prio (the_annot r) < prio a then the_annot r
+          else a
+    in Node m l a r"
+
+    lemma "node' l a r = node l a r"
+      by (cases l; cases r; auto simp: node_def node'_def)
+
+    (*>*)
+
+    fun insert :: "'a \<Rightarrow> ('a, 'a) tree \<Rightarrow> ('a, 'a) tree"
+    (*<*)
+    where
+      "insert a Leaf = Node a Leaf a Leaf"
+    | "insert a (Node m l b r) = (
+        if a<b then node (insert a l) b r
+        else if a>b then node l b (insert a r)
+        else (Node m l b r)
+    )"
+    (*>*)
+
+    text \<open>Hint:
+      Computing the annotation for a newly constructed node naively may yield
+      many case distinctions whether the left and right subtrees are leafs or nodes.
+     \<close>
+
+    (*<*)
+    lemma [simp]: "inva l \<Longrightarrow> inva r \<Longrightarrow> inva (node l a r)"
+      unfolding node_def apply (cases l; cases r)
+      apply auto []
+      apply force
+      apply force
+      apply clarsimp
+      apply (intro allI ballI impI conjI; simp?)
+      apply (metis Un_iff order_trans)
+      apply (metis)
+      apply (metis (full_types) Un_iff le_cases order_trans)
+      apply (metis)
+      apply (metis (full_types) Un_iff order_trans)
+      apply (metis)
+      apply (metis (full_types) Un_iff le_cases order_trans)
+      done
+
+    lemma [simp]: "inorder (node l a r) = inorder l @ a # inorder r"
+      unfolding node_def by auto
+
+    lemma "inva t \<Longrightarrow> inva (insert x t)"
+      by (induction t) auto
+
+    lemma inorder_insert:
+      "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
+      by(induction t) (auto simp: ins_list_simps)
+
+    (*>*)
+
+(*<*)
+  end
+
+end
+(*>*)
+text_raw \<open>\blankpage\<close>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Tree_Same_Struct.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,87 @@
+(*<*)
+theory Q_Tree_Same_Struct
+imports
+  Complex_Main
+  "$AFP/Priority_Queue_Braun/Priority_Queue_Braun"
+begin
+(*>*)  
+  
+  section \<open>Trees with Same Structure\<close>
+
+  fun same where
+    "same Leaf Leaf = True" |
+    "same (Node l a r) (Node l' a' r') = (same l l' \<and> same r r')" |
+    "same _ _ = False"
+
+  (*<*)  
+  lemma same_insert: "same t t'
+     \<Longrightarrow> same (insert_pq x t) (insert_pq y t')"
+    by (induction t t' arbitrary: x y rule: same.induct) auto  
+  (*>*)  
+    
+  subsection \<open>Question 1\<close>    
+  text \<open>
+    Specify the recursion equations of a function 
+    @{term_type same} that returns true if and only if the two trees
+    have the same structure (i.e., ignoring values).
+  \<close>
+  subsubsection \<open>Solution\<close> 
+  text \<open>See above\<close>
+    
+
+  subsection \<open>Question 2\<close>  
+  text \<open>
+    Show, by computation induction wrt.~\<open>same\<close>, that insertion 
+    of arbitrary elements into two Braun heaps with the same structure
+    yields heaps with the same structure again. 
+    @{thm [display] same_insert}
+    For your proof, it is enough to cover the (Node,Node) case. 
+    If you get analogous sub-cases, only elaborate one of them!
+
+    Hint: Here is the definition of @{const insert_pq}:
+    @{theory_text [display] \<open>
+  fun insert_pq :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+  "insert_pq a Leaf = Node Leaf a Leaf" |
+  "insert_pq a (Node l x r) =
+   (if a < x then Node (insert_pq x r) a l else Node (insert_pq a r) x l)"
+      \<close>}
+  \<close>
+
+  subsubsection \<open>Solution\<close>  
+  lemma "same t t'
+     \<Longrightarrow> same (insert_pq x t) (insert_pq y t')"
+  proof (induction t t' arbitrary: x y rule: same.induct)
+    case (2 l a r l' a' r')
+      
+    have -- \<open>Induction hypothesis, generalized over \<open>x,y\<close>! \<close>
+      IH1: "same (insert_pq x l) (insert_pq y l')" and 
+      IH2: "same (insert_pq x r) (insert_pq y r')" for x y
+      using 2 by auto
+      
+    assume PREM: "same \<langle>l, a, r\<rangle> \<langle>l', a', r'\<rangle>"
+        
+    show "same (insert_pq x \<langle>l, a, r\<rangle>) (insert_pq y \<langle>l', a', r'\<rangle>)"
+    proof -  
+      -- \<open>We get four cases\<close>
+      consider \<open>x<a \<and> y<a'\<close> | \<open>x<a \<and> y\<ge>a'\<close> | \<open>x\<ge>a \<and> y<a'\<close> | \<open>x\<ge>a \<and> y\<ge>a'\<close>
+        by force
+      then show ?thesis proof cases
+        case 1
+        hence 
+          "insert_pq x \<langle>l,a,r\<rangle> = \<langle>insert_pq a r, x, l\<rangle>" 
+          "(insert_pq y \<langle>l', a', r'\<rangle>) = \<langle>insert_pq a' r', y, l'\<rangle>"
+          by simp_all
+        moreover from PREM have "same l l'" by simp
+        moreover note IH2    
+        ultimately show ?thesis by simp  
+        -- \<open>The other cases are analogous\<close>
+      qed (insert IH1 IH2 PREM; auto)+ 
+    qed  
+  qed auto -- \<open>The other cases are simple\<close>
+
+(*<*)    
+end
+(*>*)  
+text_raw \<open>\blankpage\<close>
+text_raw \<open>\blankpage\<close>
+text_raw \<open>\blankpage\<close>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Trie.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,172 @@
+(*<*)
+theory Q_Trie
+imports Main
+begin
+(*>*)
+
+section \<open>Tries with Compression\<close>
+
+text \<open>The following kind of tree is a variant of a trie that
+  \<^item> contains only \<open>bool list\<close>s of the same length
+  \<^item> can compress subtrees that are full (or empty),
+    i.e. that contain every (or no) \<open>bool list\<close> of some length.
+
+\<close>
+
+datatype bt = Lf bool | Nd bt bt
+
+text \<open>The abstraction function that maps a \<open>bt\<close> into a \<open>bool list set\<close> is defined as follows:\<close>
+
+fun \<alpha> :: "bt \<Rightarrow> nat \<Rightarrow> bool list set" where
+"\<alpha> (Lf b) d = (if b then {bs. length bs = d} else {})" |
+"\<alpha> (Nd l r) d = Cons True ` \<alpha> l (d-1) \<union> Cons False ` \<alpha> r (d-1)"
+
+text \<open>where the the infix operator \<open>`\<close> is the image of a function over a set:
+\<open>f ` A = {b. \<exists>a \<in> A. b = f a}\<close>. The parameter \<open>d\<close> specifies the length of the \<open>bool list\<close>s
+in the tree. It is necessary because \<open>Lf True\<close> represents all lists of some unspecified length.
+Parameter \<open>d\<close> should be at least the height of the tree, otherwise the tree is cut off below depth \<open>d\<close>.
+
+Here are some examples:\<close>
+
+(*<*)
+lemma
+(*>*)
+  "\<alpha> (Lf True) 0 = {[]}"
+  "\<alpha> (Lf True) 1 = {[True], [False]}"
+  "\<alpha> (Nd (Lf True) (Nd (Lf False) (Lf True))) 2 = {[True,True], [True,False], [False,False]}"
+(*<*)
+by(auto simp: length_Suc_conv)
+(*>*)
+
+text \<open>
+In this question you are asked to write a number of small functional programs.
+They should not use sets and in particular not \<open>\<alpha>\<close> itself.
+
+\textbf{You do not need to prove anything!}
+
+  \<^enum> Define a function \<open>isin :: bt \<Rightarrow> bool list \<Rightarrow> bool\<close>
+    with the specification \<open>isin t bs \<longleftrightarrow> bs \<in> \<alpha> t (length bs)\<close>.
+  \<^enum> Define an intersection function \<open>inter :: bt \<Rightarrow> bt \<Rightarrow> bt\<close>
+    with the specification \<open>\<alpha> (inter t1 t2) d = \<alpha> t1 d \<inter> \<alpha> t2 d\<close> and \<open>d\<ge>ht (inter t1 t2)\<close>
+    if \<open>d \<ge> ht t1\<close> and \<open>d \<ge> ht t2\<close>.
+  \<^enum> Define a compression function \<open>compress :: bt \<Rightarrow> bt\<close> that
+    compresses full (and empty!) subtrees into leaves as much as possible.
+  \<^enum> Define a function \<open>compressed :: bt \<Rightarrow> bool\<close> that
+    tests if all subtrees in a tree are fully compressed.
+
+\<close>
+
+(*<*)
+fun ht :: "bt \<Rightarrow> nat" where
+"ht (Lf _) = 0" |
+"ht (Nd l r) = max (ht l) (ht r) + 1"
+
+lemma l1: "Suc (ht r) \<le> d \<Longrightarrow> ht r \<le> d - Suc 0"
+by simp
+
+lemma alpha_subset: "d \<ge> ht t \<Longrightarrow> \<alpha> t d \<subseteq> {bs. length bs = d}"
+apply(induction t d rule: \<alpha>.induct)
+apply simp
+apply (auto simp add: max_def l1 split: if_splits)
+done
+
+fun isin :: "bt \<Rightarrow> bool list \<Rightarrow> bool" where
+"isin (Lf b) bs = b" |
+"isin (Nd l r) [] = False" |
+"isin (Nd l r) (b#bs) = isin (if b then l else r) bs"
+
+lemma "isin t bs \<longleftrightarrow> bs \<in> \<alpha> t (length bs)"
+by(induction t bs rule: isin.induct) auto
+
+fun inter :: "bt \<Rightarrow> bt \<Rightarrow> bt" where
+"inter (Lf b) t = (if b then t else Lf False)" |
+"inter t (Lf b) = (if b then t else Lf False )" |
+"inter (Nd l1 r1) (Nd l2 r2) = Nd (inter l1 l2) (inter r1 r2)"
+
+lemma "d \<ge> ht t1 \<Longrightarrow> d \<ge> ht t2 \<Longrightarrow> d \<ge> ht (inter t1 t2)"
+  apply(induction t1 t2 arbitrary: d rule: inter.induct)
+  by auto presburger+
+
+lemma "d \<ge> ht t1 \<Longrightarrow> d \<ge> ht t2 \<Longrightarrow> \<alpha> (inter t1 t2) d = \<alpha> t1 d \<inter> \<alpha> t2 d"
+apply(induction t1 t2 arbitrary: d rule: inter.induct)
+apply simp
+  using alpha_subset apply fastforce
+apply simp
+  apply (metis Int_absorb1 Suc_eq_plus1 \<alpha>.simps(2) add.left_neutral alpha_subset ht.simps(2) inf_sup_aci(1))
+apply (auto simp add: max_def split: if_splits)
+done
+
+fun compressed :: "bt \<Rightarrow> bool" where
+"compressed (Lf _) = True" |
+"compressed (Nd (Lf bl) (Lf br)) = (bl \<noteq> br)" |
+"compressed t = True"
+
+fun compress :: "bt \<Rightarrow> bt" where
+"compress (Lf b) = Lf b" |
+"compress (Nd l r) = (case (compress l,compress r) of
+   (Lf bl, Lf br) \<Rightarrow> if bl = br then Lf bl else Nd (Lf bl) (Lf br) |
+   (cl,cr) \<Rightarrow> Nd cl cr)"
+
+
+lemma "d \<ge> ht t \<Longrightarrow> \<alpha>(compress t) d = \<alpha> t d"
+proof (induction t arbitrary: d)
+  case (Lf x)
+  then show ?case by auto
+next
+  case (Nd t1 t2)
+
+  from Nd.prems obtain d' where [simp]: "d = Suc d'"
+    and HTS: "ht t1 \<le> d'" "ht t2 \<le> d'"
+    by (cases d) auto
+  note IH = Nd.IH(1)[OF HTS(1)] Nd.IH(2)[OF HTS(2)]
+
+  {
+    fix b
+    assume "compress t1 = Lf b"
+    hence "\<alpha> t1 d' = (if b then {bs. length bs = d'} else {})"
+      using IH(1) by auto
+
+  } note this[simp]
+
+  {
+    fix b
+    assume "compress t2 = Lf b"
+    hence "\<alpha> t2 d' = (if b then {bs. length bs = d'} else {})"
+      using IH(2) by auto
+
+  } note this[simp]
+
+  {
+    fix l r
+    assume "compress t1 = Nd l r"
+    hence "\<alpha> t1 d' = \<alpha> (Nd l r) d'"
+      using IH(1) by auto
+  } note this[simp]
+
+  {
+    fix l r
+    assume "compress t2 = Nd l r"
+    hence "\<alpha> t2 d' = \<alpha> (Nd l r) d'"
+      using IH(2) by auto
+  } note this[simp]
+
+
+  note \<alpha>.simps[simp del]
+
+  note \<alpha>.simps[where d="Suc d'", simp]
+  note \<alpha>.simps(1)[simp]
+
+
+  show ?case
+    by (auto split!: bt.splits if_splits simp: image_iff length_Suc_conv IH)
+qed
+
+lemma "compressed (compress t)"
+  by (induction t) (auto split: bt.splits)
+
+
+end
+
+(*>*)
+text_raw \<open>\blankpage\<close>
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/Q_Unique_SBN.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,130 @@
+(*<*)
+theory Q_Unique_SBN
+imports Main
+begin
+(*>*)
+
+section \<open>Sparse Binary Numbers\<close>
+
+text \<open>Recall that a sparse binary number (SBN) is a list of natural numbers in
+  strictly ascending order, such that each element of the list represents the
+  position of a 1-digit:\<close>
+
+type_synonym rank = nat
+type_synonym snat = "rank list"
+
+abbreviation invar :: "snat \<Rightarrow> bool" where "invar s \<equiv> sorted_wrt op< 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
+(*>*)
+
+subsection \<open>Part 1\<close>
+
+text \<open>We assume that all elements of an SBN \<open>s\<close> are less than \<open>K\<close>.
+  Specify an upper bound for the number represented by \<open>s\<close> in terms of \<open>K\<close>!
+
+  \textbf{No proof required!}
+\<close>
+
+lemma SBN_upper_bound:
+  assumes "invar s"
+  assumes "\<forall>r\<in>set s. r<K"
+  (*<*)
+  defines "upper_bound \<equiv> 2^K"
+  (*>*)
+  shows "\<alpha> s < upper_bound"
+(*<*)
+  using assms(1,2) unfolding upper_bound_def
+proof (induction s arbitrary: K rule: rev_induct)
+  case Nil
+  then show ?case by simp
+next
+  case (snoc r s)
+
+  from snoc.prems have "\<alpha> (s@[r]) = 2^r + \<alpha> s"
+    by auto
+  moreover
+  from snoc.prems have "\<forall>x\<in>set s. x<r" "invar s"
+    by (auto simp: sorted_wrt_append)
+  with snoc.IH have "\<alpha> s < 2^r" by auto
+  ultimately have "\<alpha> (s@[r]) < 2^(r+1)" by auto
+  also have "r+1\<le>K" using snoc.prems by (auto)
+  finally show ?case by auto
+qed
+(*>*)
+
+text \<open>
+  \vspace{1em}
+  \<open>upper_bound\<close> = \underline{\hspace{5cm}}\\[1em]
+
+  Note: \<open>upper_bound\<close> may only depend on \<open>K\<close>, in particular, it must not depend on \<open>s\<close>!
+\<close>
+
+subsection \<open>Part 2\<close>
+text \<open>Prove that sparse binary number representation is unique,
+  i.e., if two SBNs \<open>s\<^sub>1\<close> and \<open>s\<^sub>2\<close> represent the same number, they are already equal:
+\<close>
+lemma
+  assumes "invar s\<^sub>1" "invar s\<^sub>2" "\<alpha> s\<^sub>1 = \<alpha> s\<^sub>2"
+  shows "s\<^sub>1 = s\<^sub>2"
+(*<*)
+  using assms
+proof (induction s\<^sub>1 arbitrary: s\<^sub>2 rule: rev_induct)
+  case Nil
+  then show ?case by (cases s\<^sub>2) auto
+next
+  case (snoc r\<^sub>1 s\<^sub>1 xs\<^sub>2)
+
+  text \<open>Obviously, \<open>xs\<^sub>2\<close> cannot be empty. We select the highest rank \<open>r\<^sub>2\<close>: \<close>
+  from snoc.prems obtain r\<^sub>2 s\<^sub>2 where [simp]: "xs\<^sub>2 = s\<^sub>2@[r\<^sub>2]"
+    by (cases xs\<^sub>2 rule: rev_cases) auto
+
+  text \<open>The invariants also hold for the prefixes of the numbes, and the
+    ranks in the prefixes are bounded by the highest digit.\<close>
+  from snoc.prems have "invar s\<^sub>1" "invar s\<^sub>2"
+    and RANKS: "\<forall>r\<in>set s\<^sub>1. r<r\<^sub>1" "\<forall>r\<in>set s\<^sub>2. r<r\<^sub>2"
+    by (auto simp: sorted_wrt_Cons sorted_wrt_append)
+
+  text \<open>We compare the highest digits\<close>
+  consider (EQ) "r\<^sub>1 = r\<^sub>2" | (LT) "r\<^sub>1 < r\<^sub>2" | (GT) "r\<^sub>1 > r\<^sub>2"
+    using less_linear by blast
+  thus ?case proof (cases)
+    case EQ text \<open>If the highest digits are equal, the proposition follows immediately by induction hypothesis.\<close>
+    then show ?thesis using snoc by (auto simp: sorted_wrt_Cons sorted_wrt_append)
+  next
+    case LT text \<open>\<open>r\<^sub>1 < r\<^sub>2\<close>\<close>
+    text \<open>Hence, all digits of the fist number are bounded by \<open>r\<^sub>2\<close>\<close>
+    with RANKS(1) have "\<forall>r\<in>set (s\<^sub>1@[r\<^sub>1]). r<r\<^sub>2" by auto
+    text \<open>Which gives as a strict upper bound of \<open>2^r\<^sub>2\<close> for the fist number\<close>
+    with SBN_upper_bound[OF \<open>invar (s\<^sub>1@[r\<^sub>1])\<close> this] have "\<alpha> (s\<^sub>1@[r\<^sub>1]) < 2^r\<^sub>2" by fastforce
+    also
+    text \<open>However, the second number is at least \<open>2^r\<^sub>2\<close>, as it contains the rank \<open>r\<^sub>2\<close>\<close>
+    have "2^r\<^sub>2 \<le> \<alpha> xs\<^sub>2" by simp
+    finally
+    text \<open>This yields a contradiction to the assumption that both numbes are equal.\<close>
+    have False using \<open>\<alpha> (s\<^sub>1 @ [r\<^sub>1]) = \<alpha> xs\<^sub>2\<close> by auto
+    thus ?thesis ..
+  next
+    case GT
+    text \<open>Analogously\<close>
+    with RANKS(2) have "\<forall>r\<in>set (xs\<^sub>2). r<r\<^sub>1" by auto
+    with SBN_upper_bound[OF \<open>invar (xs\<^sub>2)\<close> this] have "\<alpha> (xs\<^sub>2) < 2^r\<^sub>1" by fastforce
+    also have "2^r\<^sub>1 \<le> \<alpha> (s\<^sub>1 @ [r\<^sub>1])" by simp
+    finally have False using \<open>\<alpha> (s\<^sub>1 @ [r\<^sub>1]) = \<alpha> xs\<^sub>2\<close> by auto
+    thus ?thesis ..
+  qed
+qed
+(*>*)
+(*<*)
+end
+(*>*)
+text_raw \<open>\blankpage\<close>
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/exam/document/build	Tue Jul 03 11:20:53 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/exam/document/exercise.sty	Tue Jul 03 11:20:53 2018 +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/SS18/Exercises/exam/document/root.tex	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,137 @@
+\documentclass[11pt,a4paper]{scrartcl}
+\usepackage{isabelle,isabellesym}
+\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{\blankpage}{\newpage\phantom{blabla}\clearpage}
+
+\begin{center}
+ {\sf
+{\Huge Final Exam} \\  \ \\
+{\Large Functional Data Structures} \\ \ \\
+{\Large   31. 07. 2017}}
+\end{center}
+
+\fbox{\fbox{
+\begin{minipage}{15cm}
+\vspace*{2mm}
+\begin{tabular}{lp{1cm}l}\\[.6cm]
+  {\sf\Large First name: } && \underline{\hspace{7cm}} \\[1cm]
+  {\sf\Large Last name: } && \underline{\hspace{7cm}} \\[1cm]
+  {\sf\Large Student-Id {\small(Matrikelnummer)}: } && \underline{\hspace{7cm}} \\[1cm]
+  {\sf\Large Signature: } && \underline{\hspace{7cm}} \\
+\end{tabular}
+\vspace*{1mm}
+\end{minipage}
+}}
+
+\vspace*{1cm}
+
+\fbox{\fbox{
+\begin{minipage}{15cm}
+\vspace*{2mm}
+\begin{enumerate}
+\item You may only use a pen/pencil, eraser, and one A4 sheets of notes to solve
+  the exam. Switch off your mobile phones!
+\item Please write on the sheets of this exam. At the end of the exam, there
+  are two extra sheets. If you need more sheets, ask the supervisors during the   exam.
+\item You have 120 minutes to solve the exam.
+\item Please put your student ID and ID-card or driver's license on the table
+  until we have checked it.
+\item Please do not leave the room in the last 20 minutes of the exam --- you
+  may disturb other students who need this time.
+\item All questions of this exam are worth the same number of points.
+\end{enumerate}
+\vspace*{1mm}
+\end{minipage}
+}}
+
+\clearpage
+
+\paragraph{Proof Guidelines:} We expect detailed, rigorous,
+mathematical proofs --- but we do not ask you to write Isabelle proof
+scripts! You are welcome to use standard mathematical notation; you do
+not need to follow Isabelle syntax. Proof steps should be explained in
+ordinary language like a typical mathematical proof.
+
+Major proof steps, especially inductions, need to be stated
+explicitly. For each case of a proof by induction, you must list the
+{\bf inductive hypotheses} assumed (if any), and the
+{\bf goal} to be proved.
+
+Minor proof steps (corresponding to by simp, by blast etc)
+need not be justified if you think they are obvious, but you should
+say which facts they follow from. You should be explicit whenever you
+use a function definition or an introduction rule for an inductive
+predicate --- especially for functions and predicates that are specific
+to an exam question. (You need not reference individual lemmas for
+standard concepts like integer arithmetic, however, and in any case we
+do not ask you to recall lemma names from any Isabelle theories.)
+\blankpage
+
+
+
+
+
+
+
+% 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/exam/exam.thy	Tue Jul 03 11:20:53 2018 +0200
@@ -0,0 +1,11 @@
+(*<*)
+theory exam
+imports
+  Q_Induction
+  Q_Unique_SBN
+  Q_Min_BST
+  Q_Trie
+begin
+
+end
+(*>*)