subm5

--- a/SS18/Exercises/ROOT	Fri May 18 09:52:22 2018 +0200
+++ b/SS18/Exercises/ROOT	Thu May 24 12:21:11 2018 +0200
@@ -32,6 +32,10 @@
   theories ex06
   document_files "root.tex" "exercise.sty" "build"
 
+session "ex07" in "ex07" = "HOL-Data_Structures" +
+  options [document = pdf, document_output = "generated", document_variants = "ex07"]
+  theories ex07
+  document_files "root.tex" "exercise.sty" "build"
 
 (*
 session hwsol_basis = HOL +

Binary file SS18/Exercises/ex07.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex07/document/build	Thu May 24 12:21:11 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/ex07/document/exercise.sty	Thu May 24 12:21:11 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/ex07/document/root.tex	Thu May 24 12:21:11 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/ex07/ex.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,126 @@
+(*
+    $Id: ex.thy,v 1.2 2004/11/23 15:14:34 webertj Exp $
+    Author: Tobias Nipkow
+*)
+
+header {* Interval Lists *}
+
+(*<*) theory ex imports Main begin (*>*)
+
+text {* Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+subsubsection {* Definitions *}
+
+text {* We introduce the type *}
+
+types intervals = "(nat*nat) list"
+
+text {* This type contains all possible lists of pairs of natural numbers, even
+those that we may not recognize as meaningful representations of sets.  Thus
+you should introduce an \emph{invariant} *}
+
+consts inv :: "intervals => bool"
+
+text {* that characterizes exactly those interval lists representing sets.
+(The reason why we call this an invariant will become clear below.)  For
+efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function *}
+
+consts inv2 :: "nat => intervals => bool"
+
+text {* such that the additional argument is a lower bound for the intervals in
+the list. *}
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}
+*}
+
+consts set_of :: "intervals => nat set"
+
+text {* that yields the set corresponding to an interval list (where the list
+satisfies the invariant). *}
+
+
+text {* Finally, define two primitive recursive functions *}
+
+consts add :: "(nat*nat) => intervals => intervals"
+       rem :: "(nat*nat) => intervals => intervals"
+
+text {* for inserting and deleting an interval from an interval list.  The
+result should again satisfy the invariant.  Hence the name: @{text inv} is
+invariant under application of the operations @{term add} and @{term rem}~-- if
+@{text inv} holds for the input, it must also hold for the output. *}
+
+
+subsubsection {* Proving the invariant *}
+
+declare Let_def [simp]
+declare split_split [split]
+
+text {* Start off by proving the monotonicity of @{term inv2}: *}
+
+lemma inv2_monotone: "inv2 m ins \<Longrightarrow> n\<le>m \<Longrightarrow> inv2 n ins"
+(*<*) oops (*>*)
+
+
+text {* Now show that @{term add} and @{term rem} preserve the invariant: *}
+
+theorem inv_add: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (add (i,j) ins)"
+(*<*) oops (*>*)
+
+theorem inv_rem: "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> inv (rem (i,j) ins)"
+(*<*) oops (*>*)
+
+text {* Hint: you should first prove a more general statement (involving
+@{term inv2}).  This will probably involve some advanced forms of induction
+discussed in Section~9.3.1 of the ``Tutorial on Isabelle/HOL''. *}
+
+
+subsubsection {* Proving correctness of the implementation *}
+
+text {* Show the correctness of @{term add} and @{term rem} wrt.\ their
+counterparts @{text"\<union>"} and @{text"-"} on sets: *}
+
+theorem set_of_add:
+  "\<lbrakk> i\<le>j; inv ins \<rbrakk> \<Longrightarrow> set_of (add (i,j) ins) = set_of [(i,j)] \<union> set_of ins"
+(*<*) oops (*>*)
+
+theorem set_of_rem:
+  "\<lbrakk> i \<le> j; inv ins \<rbrakk> \<Longrightarrow> set_of (rem (i,j) ins) = set_of ins - set_of [(i,j)]"
+(*<*) oops (*>*)
+
+text {* Hints: in addition to the hints above, you may also find it useful to
+prove some relationship between @{term inv2} and @{term set_of} as a lemma. *}
+
+
+subsubsection{* General hints *}
+
+text {*
+\begin{itemize}
+
+\item You should be familiar both with simplification and predicate calculus
+reasoning.  Automatic tactics like @{text blast} and @{text force} can simplify
+the proof.
+
+\item
+Equality of two sets can often be proved via the rule @{text set_ext}:
+@{thm[display] set_ext[of A B,no_vars]}.
+
+\item
+Potentially useful theorems for the simplification of sets include \\
+@{text "Un_Diff:"}~@{thm Un_Diff [no_vars]} and \\
+@{text "Diff_triv:"}~@{thm Diff_triv [no_vars]}.
+
+\item
+Theorems can be instantiated and simplified via @{text of} and @{text
+"[simplified]"} (see the Isabelle/HOL tutorial).
+\end{itemize} *}
+
+(*<*) end (*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex07/ex07.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,253 @@
+(*<*)
+theory ex07
+  imports Main "HOL-Data_Structures.Sorting"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{7}{25.~5.~2018} *}
+
+
+text {* \Exercise{Interval Lists}
+
+ Sets of natural numbers can be implemented as lists of intervals, where
+an interval is simply a pair of numbers.  For example the set @{term "{2, 3, 5,
+7, 8, 9::nat}"} can be represented by the list @{term "[(2, 3), (5, 5),
+(7::nat, 9::nat)]"}.  A typical application is the list of free blocks of
+dynamically allocated memory. *}
+
+text {* We introduce the type *}
+
+type_synonym intervals = "(nat*nat) list"
+
+text {* Next, define an \emph{invariant}
+that characterizes valid interval lists:
+For efficiency reasons intervals should be sorted in ascending order, the lower
+bound of each interval should be less than or equal to the upper bound, and the
+intervals should be chosen as large as possible, i.e.\ no two adjacent
+intervals should overlap or even touch each other.  It turns out to be
+convenient to define @{term inv} in terms of a more general function
+such that the additional argument is a lower bound for the intervals in
+the list:*}
+
+fun inv' :: "nat \<Rightarrow> intervals \<Rightarrow> bool" where
+(*<*)
+  "inv' x [] \<longleftrightarrow> True"
+| "inv' x ((a,b)#is) \<longleftrightarrow> (x\<le>a \<and> a\<le>b \<and> inv' (Suc (Suc b)) is)"
+(*>*)
+
+definition inv where "inv \<equiv> inv' 0"
+
+
+
+text {* To relate intervals back to sets define an \emph{abstraction function}*}
+
+fun set_of :: "intervals => nat set"
+(*<*)
+where
+  "set_of [] = {}"
+| "set_of ((a,b)#is) = {a..b} \<union> set_of is"
+(*>*)
+
+text \<open>Define a function to add a single element to the interval list,
+  and show its correctness\<close>
+
+(*<*)
+fun merge_fst2 where
+  "merge_fst2 [] = []"
+| "merge_fst2 [ab] = [ab]"
+| "merge_fst2 ((a,b)#(c,d)#is) = (if Suc b = c then (a,d)#is else ((a,b)#(c,d)#is))"
+(*>*)
+
+fun add :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+(*<*)
+  where
+  "add i [] = [(i,i)]"
+| "add i ((j,k)#is) = (
+    if Suc i < j then (i,i)#(j,k)#is
+    else if Suc i = j then (i,k)#is
+    else if i\<le>k then (j,k)#is
+    else if i=Suc k then merge_fst2 ((j,i)#is)
+    else (j,k)#add i is
+)"
+(*>*)
+
+(*<*)
+lemma add_pres_inv': "m\<le>x \<Longrightarrow> inv' m is \<Longrightarrow> inv' m (add x is)"
+  apply (induction m "is" rule: inv'.induct)
+  apply (auto split: if_split list.split)
+  apply (case_tac "is")
+  apply auto
+  done
+
+
+lemma [simp]: "\<lbrakk>a\<le>b; inv' (Suc b) is\<rbrakk> \<Longrightarrow> set_of (merge_fst2 ((a,b)#is)) = {a..b} \<union> set_of is"
+  apply (cases "is" rule: merge_fst2.cases)
+  apply (auto split: if_splits)
+  done
+
+lemma add_set_of': "inv' m is \<Longrightarrow> set_of (add x is) = insert x (set_of is)"
+  apply (induction m "is" arbitrary: m rule: inv'.induct)
+  apply (auto simp: split:prod.splits)
+  done
+(*>*)
+
+lemma add_correct:
+  assumes "inv is"
+  shows "inv (add x is)" "set_of (add x is) = insert x (set_of is)"
+(*<*)
+  using assms add_set_of' add_pres_inv' unfolding inv_def by auto
+(*>*)
+
+text \<open>Hints:
+  \<^item> Sketch the different cases (position of element relative to the first interval of the list)
+    on paper first
+  \<^item> In one case, you will also need information about the second interval of the list.
+    Do this case split via an auxiliary function! Otherwise, you may end up with a recursion equation of the form
+      \<open>f (x#xs) = \<dots> case xs of x'#xs' \<Rightarrow> \<dots> f (x'#xs') \<dots>\<close>
+    combined with \<open>split: list.splits\<close> this will make the simplifier loop!
+
+\<close>
+
+
+text \<open>\Exercise{Optimized Mergesort}
+
+  Import @{theory "Sorting"} for this exercise.
+  The @{const msort} function recomputes the length of the list in each iteration.
+  Implement an optimized version that has an additional parameter keeping track
+  of the length, and show that it is equal to the original @{const msort}.
+\<close>
+
+(* Optimized mergesort *)
+
+fun msort2 :: "nat \<Rightarrow> 'a::linorder list \<Rightarrow> 'a list"
+(*<*)
+where
+"msort2 n xs = (let n2 = n div 2 in
+   if n \<le> 1 then xs
+   else merge (msort2 n2 (take n2 xs)) (msort2 (n-n2) (drop n2 xs)))"
+(*>*)
+
+lemma "n = length xs \<Longrightarrow> msort2 n xs = msort xs"
+(*<*)
+proof(induction n xs rule: msort2.induct)
+   case (1 n xs) thus ?case by(simp add: msort.simps[of xs])
+qed
+(*>*)
+
+text \<open>Hint:
+  Use @{thm [source] msort.simps} only when instantiated to a particular \<open>xs\<close>
+  (@{thm [source] msort.simps[of xs]}),
+  otherwise the simplifier will loop!
+\<close>
+
+
+
+text \<open> \NumHomework{Deletion from Interval Lists}{June 1}
+
+  Implement and prove correct a delete function.
+
+  Hints:
+    \<^item> The correctness lemma is analogous to the one for add.
+    \<^item> A monotonicity property on \<open>inv'\<close> may be useful, i.e.,
+      @{prop \<open>inv' m is \<Longrightarrow> inv' m' is\<close>} if @{prop \<open>m'\<le>m\<close>}
+    \<^item> A bounding lemma, relating \<open>m\<close> and the elements of @{term \<open>set_of is\<close>}
+      if @{prop \<open>inv' m is\<close>}, may be useful.
+\<close>
+
+
+
+fun del :: "nat \<Rightarrow> intervals \<Rightarrow> intervals"
+(*<*)
+where
+  "del i [] = []"
+| "del i ((j,k)#is) = (
+    if i<j then (j,k)#is
+    else if i=j then if j=k then is else (j+1,k)#is
+    else if i<k then (j,i - 1)#(i+1,k)#is
+    else if i=k then (j,k-1)#is
+    else (j,k)#del i is
+  )"
+
+lemma inv'_mono: "inv' n is \<Longrightarrow> m\<le>n \<Longrightarrow> inv' m is"
+  by (induction m "is" rule: inv'.induct) auto
+
+lemma del_pres_inv': "inv' m is \<Longrightarrow> inv' m (del i is)"
+  apply (induction "is" arbitrary: m rule: del.induct)
+  apply (auto intro: inv'_mono)
+  done
+
+lemma inv'_bound: "inv' m is \<Longrightarrow> k\<in>set_of is \<Longrightarrow> m\<le>k"
+  by (induction m "is" rule: inv'.induct) auto
+
+lemma set_of_del': "inv' m is \<Longrightarrow> set_of (del i is) = set_of is - {i}"
+  apply (induction "is" arbitrary: m rule: del.induct)
+  apply (auto dest: inv'_bound)
+  done
+
+(*>*)
+
+lemma del_correct: "Come up with a meaningful spec yourself"
+
+(*<*)
+oops
+lemma del_correct:
+  assumes "inv is"
+  shows "inv (del x is)" "set_of (del x is) = (set_of is) - {x}"
+  using assms set_of_del' del_pres_inv' unfolding inv_def by auto
+
+(*>*)
+
+
+text \<open> \NumHomework{Addition of Interval to Interval List}{June 1}
+  For 3 \<^bold>\<open>bonus points\<close>, implement and prove correct a function
+  to add a whole interval to an interval list. The runtime must
+  not depend on the size of the interval, e.g., iterating over the
+  interval and adding the elements separately is not allowed!
+\<close>
+
+fun addi :: "nat \<Rightarrow> nat \<Rightarrow> intervals \<Rightarrow> intervals"
+(*<*)
+where
+  "addi i j [] = [(i,j)]"
+| "addi i j ((a,b)#is) = (
+    if Suc j < a then (i,j)#(a,b)#is
+    else if i > Suc b then (a,b)#addi i j is
+    else addi (min i a) (max j b) is
+)"
+
+lemma addi_pres_inv': "m\<le>i \<Longrightarrow> i\<le>j \<Longrightarrow> inv' m is \<Longrightarrow> inv' m (addi i j is)"
+  apply (induction i j "is" arbitrary: m rule: addi.induct)
+  apply auto
+  by (metis (no_types, hide_lams) inv'_mono linear max_less_iff_conj min_less_iff_conj not_less not_less_eq_eq)
+
+lemma set_of_addi: "m\<le>i \<Longrightarrow> i\<le>j \<Longrightarrow> inv' m is \<Longrightarrow> set_of (addi i j is) = {i..j} \<union> set_of is"
+  apply (induction i j "is" arbitrary: m rule: addi.induct)
+  apply (auto dest: inv'_mono)
+  apply (smt UnE atLeastAtMost_iff inv'_mono max.coboundedI1 min.semilattice_order_axioms min_def semilattice_order.bounded_iff)
+  subgoal
+    by (smt UnE atLeastAtMost_iff inv'_mono linear max.coboundedI1 max_def min_def)
+  subgoal
+    by (smt UnCI atLeastAtMost_iff inv'_mono less_or_eq_imp_le linorder_neqE_nat max_def min_def order_trans)
+  subgoal
+    by (smt UnCI atLeastAtMost_iff inv'_mono linear max_def min.cobounded2 order_trans)
+  subgoal
+    by (simp add: UnCI inv'_mono min.semilattice_order_axioms semilattice_order.coboundedI1)
+  done
+
+
+(*>*)
+
+lemma addi_correct:
+  assumes "inv is" "i\<le>j"
+  shows "inv (addi i j is)" "set_of (addi i j is) = {i..j} \<union> (set_of is)"
+(*<*)
+  using assms set_of_addi[of 0 i j "is"] addi_pres_inv'[of 0 i j "is"]
+  unfolding inv_def
+  by auto
+(*>*)
+
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/ex07/sol.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,202 @@
+(*
+    $Id: sol.thy,v 1.4 2008/07/04 15:37:12 nipkow Exp $
+    Author: Tobias Nipkow
+*)
+
+header {* Interval Lists *}
+
+(*<*) theory sol imports Main begin (*>*)
+
+types intervals = "(nat*nat)list"
+
+consts inv2 :: "nat \<Rightarrow> intervals => bool"
+       set_of :: "intervals => nat set"
+       add1 :: "nat => intervals => intervals"
+       del1 :: "nat => intervals => intervals"
+
+primrec
+"inv2 j [] = True"
+"inv2 j (mn#ins) = (let (m,n) = mn in j <= m & m <= n & inv2 (n+2) ins)"
+
+constdefs inv :: "intervals => bool"
+         "inv ins == inv2 0 ins"
+
+primrec
+"set_of [] = {}"
+"set_of (ij#ins) = {k. fst ij <= k & k <= snd ij} Un set_of ins"
+
+primrec
+"add1 i [] = [(i,i)]"
+"add1 i (jk#ins) = (let (j,k) = jk in
+  (if Suc i < j then (i,i)#(j,k)#ins else
+   if Suc i = j then (i,k)#ins else
+   if i <= k then jk#ins else
+   if i=Suc k then case ins of [] => [(j,i)]
+                   | (m,n)#ins' =>
+                       if m=Suc(Suc k) then (j,n)#ins' else (j,Suc k)#ins
+              else (j,k)#add1 i ins))"
+
+primrec
+"del1 i [] = []"
+"del1 i (jk#ins) = (let (j,k) = jk in
+  if i<j then jk#ins else
+  if i=j then if j=k then ins else (j+1,k)#ins else
+  if i<k then (j,i - 1)#(i+1,k)#ins else
+  if i=k then (j,k - 1)#ins
+  else jk # del1 i ins)"
+
+declare Let_def[simp] split_split[split]
+
+lemma inv2_add1[rule_format]:
+ "\<forall>m. m <= i \<longrightarrow> inv2 m ins \<longrightarrow> inv2 m (add1 i ins)"
+apply(induct ins)
+ apply(simp)
+apply(simp split: list.split)
+done
+
+theorem inv_add1: "inv ins \<Longrightarrow> inv (add1 i ins)"
+by(simp only:inv_def inv2_add1[of 0])
+
+lemma set_of_add1[rule_format]:
+  "\<forall>m. inv2 m ins \<longrightarrow> set_of(add1 i ins) = insert i (set_of ins)"
+apply(induct ins)
+ apply(force)
+apply(clarsimp)
+apply(rule conjI)
+ apply(simp split:list.split)
+ apply(rule conjI)
+  apply clarify
+  apply(rule set_ext)
+  apply (simp)
+  apply arith
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(rule set_ext)
+  apply (simp)
+  apply arith
+ apply clarify
+ apply(rule set_ext)
+ apply (simp)
+ apply arith
+apply clarify
+apply(rule conjI)
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(rule set_ext)
+  apply (simp)
+  apply arith
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(rule set_ext)
+  apply (simp)
+  apply arith
+ apply clarify
+ apply(rule set_ext)
+ apply (simp)
+ apply arith
+apply (fastsimp)
+done
+
+theorem "inv ins \<Longrightarrow> set_of(add1 i ins) = insert i (set_of ins)"
+by(simp only:inv_def set_of_add1[of 0])
+
+
+lemma inv2_mono[rule_format]: "\<lbrakk> inv2 m ins; n<=m \<rbrakk> \<Longrightarrow> inv2 n ins"
+by(induct "ins", auto)
+
+lemma inv2_del1[rule_format]: "\<forall>m. inv2 m ins \<longrightarrow> inv2 m (del1 i ins)"
+apply(induct ins)
+ apply(simp)
+apply(clarsimp)
+apply(rule conjI)
+ apply clarsimp
+ apply(rule conjI)
+  apply(force intro:inv2_mono)
+ apply(clarsimp)
+ apply(rule conjI)
+  apply arith
+ apply(force intro:inv2_mono)
+apply clarsimp
+apply arith
+done
+
+theorem "inv ins \<Longrightarrow> inv (del1 i ins)"
+by(simp only:inv_def inv2_del1[of 0])
+
+
+lemma inv2_yields_lb[rule_format]:
+ "\<forall>m. inv2 m ins \<longrightarrow> n < m \<longrightarrow> n \<notin> set_of ins"
+by(induct ins, auto)
+
+lemma [simp]: "{k::nat. x <= k & k <= x} = {x}"
+by(rule set_ext, simp, arith)
+
+lemma [simp]: "n<m \<Longrightarrow> {k::nat. m <= k & k <= n} = {}"
+by(simp)
+
+lemma [simp]: "0 < (n::nat) \<Longrightarrow>
+  {k. m <= k & k <= n} - {n} = {k. m <= k & k <= n - 1}"
+by(rule set_ext, simp, arith)
+
+lemma [simp]: "{k::nat. m <= k & k <= n} - {m} = {k. Suc m <= k & k <= n}"
+by(rule set_ext, simp, arith)
+
+lemma set_of_del1[rule_format]:
+ "\<forall>m. inv2 m ins \<longrightarrow> set_of(del1 i ins) = (set_of ins) - {i}"
+apply(induct ins)
+ apply(simp)
+apply(clarsimp)
+apply(rule conjI)
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(drule_tac n = i in inv2_yields_lb)
+   apply simp
+  apply blast
+ apply clarify
+ apply(drule_tac n = i in inv2_yields_lb)
+  apply arith
+ apply (simp add: Un_Diff)
+apply clarify
+apply(rule conjI)
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(drule_tac n = i in inv2_yields_lb)
+   apply simp
+  apply blast
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(drule_tac n = i in inv2_yields_lb)
+   apply simp
+  apply (simp add: Un_Diff)
+ apply clarify
+ apply(rule conjI)
+  apply clarify
+  apply(drule_tac n = i in inv2_yields_lb)
+   apply simp
+  apply (simp add: Un_Diff)
+ apply clarify
+ apply(drule_tac n = i in inv2_yields_lb)
+  apply simp
+ apply (simp add: Un_Diff)
+ apply(rule set_ext)
+ apply simp
+ apply arith
+apply clarify
+apply(rule conjI)
+ apply clarify
+ apply(simp)
+ apply blast
+apply force
+done
+
+theorem  "inv ins \<Longrightarrow> set_of(del1 i ins) = (set_of ins) - {i}"
+by(simp only:inv_def set_of_del1[of 0])
+
+end
+ 

--- a/SS18/Exercises/hwsubm/email.log	Fri May 18 09:52:22 2018 +0200
+++ b/SS18/Exercises/hwsubm/email.log	Thu May 24 12:21:11 2018 +0200
@@ -142,3 +142,57 @@
 Di 15. Mai 11:23:13 CEST 2018
 /home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw04 [e-mail] hw04.thy
 OK
+Do 24. Mai 12:19:09 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] Home05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] tmpl05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] tmpl05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] hw05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] homework05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] hw05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] tut05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] ex05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] hw05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] Homework05.thy
+OK
+Do 24. Mai 12:19:10 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] tmpl05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] HW05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] ex05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] jonischkeit05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] homework05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] ex05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] hw05.thy
+OK
+Do 24. Mai 12:19:11 CEST 2018
+/home/lammich/lehre/FDS/Private/SS18/Exercises/hwsubm/_sendmail.py PASSWORD hw05 [e-mail] ex05.thy
+OK

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw03/[e-mail]/tmpl03.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,483 @@
+(** Score: 7/10
+  hw2: some "sorry"s
+
+*)
+(*<*)
+theory tmpl03
+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 rem k = (case rem of Some a \<Rightarrow> a=k | None \<Rightarrow> False)"
+| "isin2 (Node l a r) rem k = (
+    if k<a then isin2 l rem k
+    else isin2 r (Some a) k)"
+
+
+text \<open>Show that your function is correct.
+
+  Hint: Auxiliary lemma for \<open>isin2 t (Some y) x\<close> !
+\<close>
+
+lemma aux:
+  "bst t \<Longrightarrow> \<forall>x\<in>set_tree t. a<x \<Longrightarrow> isin2 t (Some a) k \<longleftrightarrow> (a=k \<or> isin t k)"
+  apply (induction t arbitrary: a)
+  apply auto
+  done
+
+
+lemma isin2_None:
+  "bst t \<Longrightarrow> isin2 t None k = isin t k"
+  apply (induction t)
+  apply (auto simp: aux)
+  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 Leaf t = t"
+| "join t Leaf = 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 a r \<Rightarrow> Node (Node l1 a1 l) a (Node r a2 r2))"
+
+lemma join_inorder[simp]: "inorder(join t1 t2) = inorder t1 @ inorder t2"
+  apply (induction t1 t2 rule: join.induct)
+  by (auto split: tree.splits)
+
+lemma "height(join t1 t2) \<le> max (height t1) (height t2) + 1"
+  apply (induction t1 t2 rule: join.induct)
+  by (auto split: tree.splits)
+
+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>
+
+thm join.simps
+
+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>
+declare set_inorder[simp del]
+
+
+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 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)"
+  apply (auto simp add: bst_iff_sorted_wrt_less sorted_wrt_append set_inorder[symmetric])
+  apply fastforce
+  done
+
+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 _ _ = undefined"
+
+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}"
+  oops
+
+lemma "bst t \<Longrightarrow> bst (delete x t)"
+  oops
+
+section \<open>Homework\<close>
+
+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 _ [] = True" |
+    "valid (Node l a r) (L#p) = valid l p" |
+    "valid (Node l a r) (R#p) = valid r p" |
+    "valid Leaf _ = 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
+  (* Insert your eqns here *)
+  "get t [] = t" -- \<open>Catch-all clause to get rid of missing patterns warning\<close>
+| "get (Node l _ r) (L#p) = get l p"
+| "get (Node l _ r) (R#p) = get r p"
+| "get Leaf _ = Leaf"
+
+
+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>s\<close>.
+\<close>
+  fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+    where
+  "put _ [] s = s"
+| "put (Node l a r) (L#p) s = Node (put l p s) a r"
+| "put (Node l a r) (R#p) s = Node l a (put r p s)"
+| "put Leaf _ _ = Leaf"
+
+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"
+proof (induction t arbitrary: p s)
+  case Leaf
+  then show ?case
+    by (metis list.exhaust put.simps(4) valid.simps(1))
+next
+  case (Node l a r)
+  then show ?case
+  proof (cases p)
+    case Nil
+    then show ?thesis
+      using Node.prems by auto
+  next
+    case (Cons d)
+    then show ?thesis
+    proof (cases d)
+      case L
+        then show ?thesis
+          using Node.IH(1) Node.prems local.Cons by auto
+    next
+      case R
+        then show ?thesis
+          using Node.IH(2) Node.prems local.Cons by auto
+    qed
+  qed
+qed
+
+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 valid_path[simp]:
+  assumes "valid t p" "p \<noteq> []"
+  shows "\<exists>l a r. t = Node l a r"
+  using assms(1) assms(2) valid.elims(2) by blast
+
+lemma get_put[simp]:
+  shows "valid t p \<Longrightarrow> put t p (get t p) = t"
+proof (induction p arbitrary: t)
+  case (Cons d p')
+  with valid_path show ?case
+    by (cases d) fastforce+
+qed (simp)
+
+lemma put_put[simp]: "put (put t p s) p s' = put t p s'"
+proof (cases "valid t p")
+  case True
+  then show "valid t p \<Longrightarrow> put (put t p s) p s' = put t p s'"
+  proof (induction p arbitrary: t)
+    case (Cons d p')
+    with valid_path Cons.IH Cons.prems show ?case
+      by (cases d) fastforce+
+  qed (simp)
+next
+  case False
+  then show ?thesis
+    by (simp add: put_invalid)
+qed
+
+lemma put_get[simp]: "valid t p \<Longrightarrow> get (put t p s) p = s"
+proof (induction p arbitrary: t)
+  case (Cons d p')
+  with valid_path Cons.IH Cons.prems show ?case
+    by (cases d) fastforce+
+qed (simp)
+
+
+lemma valid_put[simp]: "valid t p \<Longrightarrow> valid (put t p s) p"
+proof (induction p arbitrary: t)
+  case (Cons d p')
+  with valid_path Cons.IH Cons.prems show ?case
+    by (cases d) fastforce+
+qed (simp)
+
+  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"
+proof
+  show "valid t (p @ q) \<Longrightarrow> valid t p \<and> valid (get t p) q"
+  proof (induction p arbitrary: t)
+    case (Cons d p')
+    with valid_path Cons.IH Cons.prems show ?case
+      by (cases d) fastforce+
+  qed (simp)
+next
+  show "valid t p \<and> valid (get t p) q \<Longrightarrow> valid t (p @ q) "
+  proof (induction p arbitrary: t)
+    case (Cons d p')
+    with valid_path Cons.IH Cons.prems show ?case
+      by (cases d) fastforce+
+  qed (simp)
+qed
+
+lemma get_append[simp]: "valid t p \<Longrightarrow> get t (p@q) = get (get t p) q"
+proof (induction p arbitrary: t)
+  case (Cons d p')
+  with valid_path Cons.IH Cons.prems show ?case
+    by (cases d) fastforce+
+qed (simp)
+
+lemma put_append[simp]: "put t (p@q) s = put t p (put (get t p) q s)"
+proof (cases "valid t (p@q)")
+  case True
+  then show ?thesis
+  proof (induction p arbitrary: t)
+    case (Cons d p')
+    with valid_path Cons.IH Cons.prems show ?case
+      by (cases d) fastforce+
+  qed (simp)
+next
+  case False
+  then show ?thesis
+    by (metis get_put put_invalid valid_append)
+qed
+
+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 \<Rightarrow> 'a::linorder tree \<times> 'a list" where
+  "bst_remdups_aux t (x#xs) pre =
+    (if isin t x
+      then bst_remdups_aux t xs pre
+      else bst_remdups_aux (ins x t) xs (pre @ [x]))"
+| "bst_remdups_aux t [] pre = (t, pre)"
+
+definition "bst_remdups xs \<equiv> snd (bst_remdups_aux Leaf xs [])"
+
+value "bst_remdups [1::nat,1,1,2,2,1,3]"
+
+
+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 keep_bst: "\<lbrakk> bst t ; (t', xs') = bst_remdups_aux t xs pre \<rbrakk> \<Longrightarrow> bst t'"
+proof (induction xs arbitrary: t t' xs' pre)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a xs)
+  then show ?case
+    by (metis Cons.IH Cons.prems(1) Cons.prems(2) bst_ins bst_remdups_aux.simps(1))
+qed
+
+declare [[ smt_timeout = 120 ]]
+
+lemma remdups_append: "\<lbrakk> bst t ; (t', xs') = (bst_remdups_aux t xs pre) \<rbrakk>
+  \<Longrightarrow> bst_remdups_aux t' ys xs' = bst_remdups_aux t (xs@ys) pre"
+proof (induction xs arbitrary: t t' xs' ys pre)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  then show ?case
+  proof (cases "isin t a")
+    case True
+    then show ?thesis
+      by (simp add: Cons.IH Cons.prems(1) Cons.prems(2))
+  next
+    case False
+    then show ?thesis
+      by (simp add: Cons.IH Cons.prems(1) Cons.prems(2) bst_ins)
+  qed
+qed
+
+lemma remdups_sets: "\<lbrakk> bst t ; (t', xs') = (bst_remdups_aux t xs pre) \<rbrakk> \<Longrightarrow> set_tree t' = set_tree t \<union> set xs"
+proof (induction xs arbitrary: t t' xs' pre)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  then show ?case
+    by (metis (no_types, lifting) Un_insert_left Un_insert_right bst_ins bst_remdups_aux.simps(1) insert_absorb list.simps(15) set_tree_ins set_tree_isin sup_bot.left_neutral)
+qed
+
+
+lemma remdups_keep: "\<lbrakk> bst t ; (t', xs') = (bst_remdups_aux t xs pre) ; xs = (a#xrest) ; \<not>isin t a \<rbrakk>
+  \<Longrightarrow> \<exists>xrest'. xs' = pre @ [a] @ xrest'" sorry (* it's late enough, this'll have to do... *)
+
+lemma remdups_sets2: "\<lbrakk> bst t ; (t', xs') = (bst_remdups_aux t xs pre) ; set pre = set_tree t \<rbrakk> \<Longrightarrow> set xs' \<union> set pre = set xs \<union> set pre"
+proof (induction xs arbitrary: t t' xs' pre)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  then show ?case
+  proof (cases "isin t a")
+    case True
+    then show ?thesis
+      by (metis Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) bst_remdups_aux.simps(1) inf_sup_aci(5) remdups_sets)
+  next
+    case False
+    then have "a \<in> set xs'"
+      by (metis Cons.prems(1) Cons.prems(2) append_Cons in_set_conv_decomp remdups_keep)
+    then show ?thesis
+      by (smt Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) Un_insert_left Un_insert_right bst_ins bst_remdups_aux.simps(1) insort_insert_triv list.set(1) list.simps(15) set_append set_insort_insert set_tree_ins sup_bot.comm_neutral sup_left_commute)
+  qed
+qed
+
+lemma "set (bst_remdups xs) = set xs" unfolding bst_remdups_def using remdups_sets2
+  by (metis (no_types, hide_lams) bst_wrt.simps(1) inorder.simps(1) list.set(1) set_inorder snd_conv sup_bot.comm_neutral surj_pair)
+
+lemma remdups_dist:
+  "\<lbrakk> bst t ; distinct pre ; (t', xs') = (bst_remdups_aux t xs pre) ; set pre = set_tree t \<rbrakk> \<Longrightarrow> distinct xs'"
+proof (induction xs arbitrary: t pre t' xs')
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  then show ?case
+  proof (cases "isin t a")
+    case True
+    then show ?thesis
+      using Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) Cons.prems(4) by auto
+  next
+    case False
+    then show ?thesis
+      by (metis (mono_tags, lifting) Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) Cons.prems(4) bst_ins bst_remdups_aux.simps(1) distinct.simps(2) distinct1_rotate list.set(1) list.set(2) rotate1.simps(2) set_append set_tree_ins set_tree_isin sup_commute)
+  qed
+qed
+
+lemma "distinct (bst_remdups xs)" unfolding bst_remdups_def
+  by (metis bst_wrt.simps(1) distinct.simps(1) inorder.simps(1) remdups_dist set_inorder snd_conv surj_pair)
+
+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 (x#xs) ys = (x \<in> set ys \<and> sublist xs (remove1 x ys))"
+| "sublist [] _ = True"
+
+lemma sublist_id[simp]: "sublist x x"
+  by (induction x) auto
+
+lemma sublist_del[simp]: "sublist (x@xs) y \<Longrightarrow> sublist xs y"
+proof (induction xs arbitrary: x y)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs')
+  then show ?case sorry
+qed
+
+lemma sublist_prepend[simp]: "sublist x y \<Longrightarrow> sublist x (a#y)"
+proof (induction x arbitrary: y a)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a x)
+  then show ?case
+    by (metis append.left_neutral append_Cons list.set_intros(1) remove1.simps(2) sublist.simps(1) sublist_del)
+qed
+
+value "sublist [1::nat,2,3] [1,2,3,4,12,5,2]"
+
+text \<open>Show that your remdups function produces a sublist of the original list!
+
+  Hint: Generalization. Auxiliary lemma required.
+\<close>
+
+lemma remdups_subl:
+  "\<lbrakk> bst t ; (t', xs') = (bst_remdups_aux t xs pre) ; set pre = set_tree t \<rbrakk> \<Longrightarrow> sublist xs' (xs@pre)"
+proof (induction xs arbitrary: t pre t' xs')
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a xs)
+  then show ?case
+  proof (cases "isin t a")
+    case True
+    then show ?thesis
+      by (metis Cons.IH Cons.prems(1) Cons.prems(2) Cons.prems(3) append_Cons bst_remdups_aux.simps(1) sublist_prepend)
+  next
+    case False
+    then show ?thesis using remdups_keep sorry
+  qed
+qed
+
+lemma "sublist (bst_remdups xs) xs"
+  by (metis append_Nil2 bst_remdups_def bst_wrt.simps(1) inorder.simps(1) remdups_subl set_inorder snd_conv surj_pair)
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_406/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_406/hw05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,51 @@
+(** Score: 10/10
+*)
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+value "(0::nat) div 0"
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?n = "length xs div n"
+  let ?ys = "take ?n xs"
+  let ?zs = "drop ?n xs"
+  show "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"  by(simp add:min.absorb2)
+qed
+
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0"
+| "a (Suc n) = a n ^ 2 + 1"
+
+thm power_mono[where n = 2]
+
+find_theorems "(_-_)^2"
+find_theorems "(_ + _) > _"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have azer:"0 \<le> a n" by (smt a.elims power2_less_eq_zero_iff zero_eq_power2)
+
+    from IH  have "a (Suc n) = (a n)^2 +1" by simp
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1) ^ 2" using power_mono[where n = 2] IH azer by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))" by (simp add: power2_diff power_even_eq)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 " by (smt Suc.IH Suc_eq_plus1 a.elims power.simps(1) power2_less_eq_zero_iff power_one_right zero_eq_power2)
+    finally show ?thesis by auto
+
+  qed
+qed
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_406/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,77 @@
+Using temporary directory '/tmp/tmp.03vqpEUg0S'
+Files in /tmp/eval-406-AOf4pY: hw05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs>
+
+
+save_test_theory
+</defs>
+<submission-imports>
+
+</submission-imports>
+<defs-imports>
+Main Tree
+</defs-imports>
+<version>
+2016-1
+</version>
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+<check>
+
+</check>
+<submission>
+
+
+value "(0::nat) div 0"
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?n = "length xs div n"
+  let ?ys = "take ?n xs"
+  let ?zs = "drop ?n xs"
+  show "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"  by(simp add:min.absorb2)
+qed
+
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0"
+| "a (Suc n) = a n ^ 2 + 1"
+
+thm power_mono[where n = 2]
+
+find_theorems "(_-_)^2"
+find_theorems "(_ + _) > _"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have azer:"0 \<le> a n" by (smt a.elims power2_less_eq_zero_iff zero_eq_power2)
+   
+    from IH  have "a (Suc n) = (a n)^2 +1" by simp
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1) ^ 2" using power_mono[where n = 2] IH azer by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))" by (simp add: power2_diff power_even_eq)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 " by (smt Suc.IH Suc_eq_plus1 a.elims power.simps(1) power2_less_eq_zero_iff power_one_right zero_eq_power2)
+    finally show ?thesis by auto
+    
+  qed
+qed
+</submission>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_412/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_412/homework05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,102 @@
+(** Score: 10/10
+*)
+(*<*)
+theory homework05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?l = "length xs div n"
+  let ?ys = "take ?l xs"
+  let ?zs = "drop ?l xs"
+  have "length ?ys = ?l" by (simp add: min.absorb2)
+  moreover have "xs = ?ys@?zs" by simp
+  ultimately show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma one_geq_power: "1 \<le> (m::nat) \<Longrightarrow> 0 \<le> (n::nat) \<Longrightarrow> 1 \<le> m^n"
+  by simp
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a n \<ge> 0"
+    proof cases
+      assume [simp]: "n = 0"
+      show ?thesis by simp
+    next
+      assume [simp]: "n\<noteq>0"
+      then have "n > 0" by blast
+      then obtain n' where "n = Suc n'" using gr0_implies_Suc by blast
+      thus ?thesis by simp
+    qed
+    have "a (Suc n) = (a n)^2 + 1" by simp
+    also have   "\<dots> \<le> (2^2^n - 1)^2 + 1" using IH `a n \<ge> 0`
+      by (simp add: power_mono)
+    also have   "\<dots> = 2^2^(n+1) - 2^(2^n + 1) + 2"
+      apply (auto simp add: algebra_simps numeral_eq_Suc )
+      by (simp add: semiring_normalization_rules(29) semiring_normalization_rules(31))
+    also have "\<dots> \<le> 2^2^(n+1) - 2"
+      apply (auto simp add: algebra_simps)
+      using  `a n \<ge> 0` one_geq_power
+      by (metis one_le_numeral one_le_power power_increasing power_one_right)
+    also have "\<dots> \<le> 2^2^(Suc n) - 1" by simp
+    finally show ?thesis .
+  qed
+qed
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_412/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,126 @@
+Using temporary directory '/tmp/tmp.9Ni7IAy6oi'
+Files in /tmp/eval-412-am20YW: homework05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission>
+
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?l = "length xs div n"
+  let ?ys = "take ?l xs"
+  let ?zs = "drop ?l xs"
+  have "length ?ys = ?l" by (simp add: min.absorb2)
+  moreover have "xs = ?ys@?zs" by simp
+  ultimately show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma one_geq_power: "1 \<le> (m::nat) \<Longrightarrow> 0 \<le> (n::nat) \<Longrightarrow> 1 \<le> m^n"
+  by simp
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a n \<ge> 0"
+    proof cases
+      assume [simp]: "n = 0"
+      show ?thesis by simp
+    next
+      assume [simp]: "n\<noteq>0"
+      then have "n > 0" by blast
+      then obtain n' where "n = Suc n'" using gr0_implies_Suc by blast
+      thus ?thesis by simp
+    qed
+    have "a (Suc n) = (a n)^2 + 1" by simp
+    also have   "\<dots> \<le> (2^2^n - 1)^2 + 1" using IH `a n \<ge> 0`
+      by (simp add: power_mono)
+    also have   "\<dots> = 2^2^(n+1) - 2^(2^n + 1) + 2"
+      apply (auto simp add: algebra_simps numeral_eq_Suc )
+      by (simp add: semiring_normalization_rules(29) semiring_normalization_rules(31))
+    also have "\<dots> \<le> 2^2^(n+1) - 2"
+      apply (auto simp add: algebra_simps)
+      using  `a n \<ge> 0` one_geq_power
+      by (metis one_le_numeral one_le_power power_increasing power_one_right)
+    also have "\<dots> \<le> 2^2^(Suc n) - 1" by simp
+    finally show ?thesis .
+  qed
+qed
+
+(*<*)
+</submission>
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+<submission-imports>
+
+</submission-imports>
+<defs>
+
+
+save_test_theory
+</defs>
+<version>
+2016-1
+</version>
+<check>
+
+</check>
+<defs-imports>
+Main Tree
+</defs-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_402/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_402/homework05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,95 @@
+(** Score: 10/10
+*)
+(*<*)
+theory homework05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+  have "length ?ys = length xs div n \<and> xs=?ys@?zs"
+    apply(simp)
+    using div_le_dividend min_absorb2 by blast
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    (*helper lemmas*)
+    have a_bigger_0: "a n \<ge> 0"
+      apply(induction n) by auto
+    have squared_IH: "a n^2 \<le> (2 ^ 2 ^ n - 1)^2"
+      using power_mono[where n=2] IH a_bigger_0 by blast
+
+    (*main proof*)
+    have "a (Suc n) = a n ^ 2 + 1" by force
+    also have "... \<le> (2 ^ 2 ^ n - 1)^2 + 1"
+      using squared_IH by force
+    also have "... = (2 ^ 2 ^ n) * (2 ^ 2 ^ n) - 2 * (2 ^ 2 ^ n) + 1 + 1"
+      by algebra
+    also have "... = 2 ^ 2 ^ Suc n - 2 * (2 ^ 2 ^ n) + 2"
+      by (simp add: semiring_normalization_rules(36))
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 * (2 ^ 2 ^ 0) + 2"
+      by (simp add: self_le_power)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 4 + 2" by force
+    finally show ?thesis by force
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_402/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,119 @@
+Using temporary directory '/tmp/tmp.SXELCpyaeG'
+Files in /tmp/eval-402-DXlyZ3: homework05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<version>
+2016-1
+</version>
+<submission>
+
+(*>*)
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "take (length xs div n) xs" 
+  let ?zs = "drop (length xs div n) xs"
+  have "length ?ys = length xs div n \<and> xs=?ys@?zs"
+    apply(simp)
+    using div_le_dividend min_absorb2 by blast
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    (*helper lemmas*)
+    have a_bigger_0: "a n \<ge> 0"
+      apply(induction n) by auto
+    have squared_IH: "a n^2 \<le> (2 ^ 2 ^ n - 1)^2" 
+      using power_mono[where n=2] IH a_bigger_0 by blast
+    
+    (*main proof*)
+    have "a (Suc n) = a n ^ 2 + 1" by force
+    also have "... \<le> (2 ^ 2 ^ n - 1)^2 + 1"
+      using squared_IH by force
+    also have "... = (2 ^ 2 ^ n) * (2 ^ 2 ^ n) - 2 * (2 ^ 2 ^ n) + 1 + 1"
+      by algebra
+    also have "... = 2 ^ 2 ^ Suc n - 2 * (2 ^ 2 ^ n) + 2"
+      by (simp add: semiring_normalization_rules(36)) 
+    also have "... \<le> 2 ^ 2 ^ Suc n - 2 * (2 ^ 2 ^ 0) + 2"
+      by (simp add: self_le_power)
+    also have "... \<le> 2 ^ 2 ^ Suc n - 4 + 2" by force
+    finally show ?thesis by force
+  qed
+qed
+
+
+(*<*)
+</submission>
+<defs>
+
+
+save_test_theory
+</defs>
+<check>
+
+</check>
+<defs-imports>
+Main Tree
+</defs-imports>
+<image>
+HOL-Library
+</image>
+<submission-imports>
+
+</submission-imports>
+<check-imports>
+Submission
+</check-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_411/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_411/jonischkeit05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,145 @@
+(** Score: 10/10
+
+  A side remark on comments:
+
+    Use (* \<dots> *) for informal comments.
+    Using text \<open>\<dots>\<close> actually expects valid LaTeX content
+      (with markdown and antiquotations), which will also be displayed in
+      the proof document that Isabelle can generate from your proofs.
+      In particular, unicode symbols as eg inner syntax is no valid latex!
+
+      Thus, instead of writing
+        text \<open> b = a n, and c = 2 ^ 2 ^ n.\<close>
+      just use (* b = a n, and c = 2 ^ 2 ^ n  *)
+
+*)
+(*<*)
+theory jonischkeit05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+text \<open>
+  About apply style proofs: I can handle Isar proofs much better
+  as i find it easier to see what the proof needs to finish and
+  i find it easier to play around with the proof, as i can do it
+  in small steps. So i always directly start with an Isar proof.
+  Also the "apply" is always highlighted red, and "by" is highlighted
+  blue.
+
+  About my Isar proofs beeing verbose. You are right and I am sorry
+  but as i usually start quiet late doing my homework i don't find
+  the time to properly shrink the proofs.
+
+  About not removing "sledgehammer" from my last script. Again I am very
+  sorry, but if you look at the submission time you can deduce that I
+  was already quiet sleepy and I just did not realize there was one
+  still in there. Sorry. (I was so sleepy that my biggest fear in the
+  morning was having uploaded the wrong file)
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  text \<open>the proof looks straight forward to me, so i dont want to use induction
+  but i also can't use apply as i don't know how to "obtain" using apply
+  (and i like Isar proofs more)\<close>
+  (** You are alright ... this exercise was designed such that Isar should be used :) *)
+proof -
+  have "length xs \<ge> length xs div n" by auto
+  hence ll: "min (length xs) (length xs div n) = (length xs div n)" by linarith
+  obtain as where as: "as = take (length xs div n) xs" by auto
+  hence las: "length as = length xs div n" using ll length_take by auto
+  obtain bs where bs: "bs = drop (length xs div n) xs" by auto
+  have "as@bs = xs" using as bs by auto
+  thus ?thesis using las by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+value "a 3 = ((0 ^ 2 + 1) ^ 2 + 1) ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma exp: "((b::int) - 1) ^ 2 = (b ^ 2 - 2 * b + 1)" by algebra
+
+text \<open>this is the main inequality for the following lemma. b = a n, and c = 2 ^ 2 ^ n.
+  Adding 1 to both sides yields "a (Suc n) = a n ^ 2 + 1 \<le> (2 ^ 2 ^ n) ^ 2 - 1 = 2 ^ 2 ^ Suc n - 1".\<close>
+lemma still_smaller:
+  "1 \<le> b \<Longrightarrow> (b::int) \<le> c - 1 \<Longrightarrow> b ^ 2 \<le> c ^ 2 - 2"
+proof -
+  assume PREM: "1 \<le> b" "b \<le> c -1"
+  hence "c \<ge> 2" by simp
+  have "0 \<le> b" using PREM(1) by simp
+  hence "b ^ 2 \<le> (c - 1) ^ 2" using power_mono PREM(2) by blast
+  thus ?thesis using exp \<open>2 \<le> c\<close> by auto
+qed
+
+text \<open>a (Suc n) = a n ^ 2 + 1\<close>
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof (cases "n = 0")
+    case False
+    hence "a n \<ge> 1" by (induction n, auto)
+    have "(2::int) ^ 2 ^ Suc n = (2 ^ 2 ^ n) ^ 2" using power_Suc power_mult[of 2 "2 ^ n" 2]
+      by (simp add: semiring_normalization_rules(7))
+    then show ?thesis using still_smaller[of "a n" "2 ^ 2 ^ n"] \<open>1 \<le> a n\<close> IH by auto
+  qed (simp)
+qed
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_411/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,155 @@
+Using temporary directory '/tmp/tmp.SlmmPtmqvX'
+Files in /tmp/eval-411-A4ujmC: jonischkeit05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<image>
+HOL-Library
+</image>
+<check>
+
+</check>
+<version>
+2016-1
+</version>
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+text \<open>
+  About apply style proofs: I can handle Isar proofs much better
+  as i find it easier to see what the proof needs to finish and
+  i find it easier to play around with the proof, as i can do it
+  in small steps. So i always directly start with an Isar proof.
+  Also the "apply" is always highlighted red, and "by" is highlighted
+  blue.
+  
+  About my Isar proofs beeing verbose. You are right and I am good_sorry
+  but as i usually start quiet late doing my homework i don't find
+  the time to properly shrink the proofs.
+
+  About not removing "sledgehammer" from my last script. Again I am very
+  good_sorry, but if you look at the submission time you can deduce that I
+  was already quiet sleepy and I just did not realize there was one
+  still in there. Sorry. (I was so sleepy that my biggest fear in the
+  morning was having uploaded the wrong file)
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  text \<open>the proof looks straight forward to me, so i dont want to use induction
+  but i also can't use apply as i don't know how to "obtain" using apply
+  (and i like Isar proofs more)\<close>
+proof -
+  have "length xs \<ge> length xs div n" by auto
+  hence ll: "min (length xs) (length xs div n) = (length xs div n)" by linarith
+  obtain as where as: "as = take (length xs div n) xs" by auto
+  hence las: "length as = length xs div n" using ll length_take by auto
+  obtain bs where bs: "bs = drop (length xs div n) xs" by auto
+  have "as@bs = xs" using as bs by auto
+  thus ?thesis using las by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+value "a 3 = ((0 ^ 2 + 1) ^ 2 + 1) ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma exp: "((b::int) - 1) ^ 2 = (b ^ 2 - 2 * b + 1)" by algebra
+
+text \<open>this is the main inequality for the following lemma. b = a n, and c = 2 ^ 2 ^ n.
+  Adding 1 to both sides yields "a (Suc n) = a n ^ 2 + 1 \<le> (2 ^ 2 ^ n) ^ 2 - 1 = 2 ^ 2 ^ Suc n - 1".\<close>
+lemma still_smaller:
+  "1 \<le> b \<Longrightarrow> (b::int) \<le> c - 1 \<Longrightarrow> b ^ 2 \<le> c ^ 2 - 2"
+proof -
+  assume PREM: "1 \<le> b" "b \<le> c -1"
+  hence "c \<ge> 2" by simp
+  have "0 \<le> b" using PREM(1) by simp
+  hence "b ^ 2 \<le> (c - 1) ^ 2" using power_mono PREM(2) by blast
+  thus ?thesis using exp \<open>2 \<le> c\<close> by auto
+qed
+
+text \<open>a (Suc n) = a n ^ 2 + 1\<close>
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof (cases "n = 0")
+    case False
+    hence "a n \<ge> 1" by (induction n, auto)
+    have "(2::int) ^ 2 ^ Suc n = (2 ^ 2 ^ n) ^ 2" using power_Suc power_mult[of 2 "2 ^ n" 2]
+      by (simp add: semiring_normalization_rules(7))    
+    then show ?thesis using still_smaller[of "a n" "2 ^ 2 ^ n"] \<open>1 \<le> a n\<close> IH by auto
+  qed (simp)
+qed
+
+(*<*)
+</submission>
+<check-imports>
+Submission
+</check-imports>
+<defs-imports>
+Main Tree
+</defs-imports>
+<submission-imports>
+
+</submission-imports>
+<defs>
+
+
+save_test_theory
+</defs>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_404/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_404/tut05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,271 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tut05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+
+  (*
+  from PREM have "n=3 \<or> n>3" by auto
+  then show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof
+  *)
+
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n\<noteq>3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using \<open>n>3\<close> by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "sumto f 0 = f 0"
+| "sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  have "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = (sumto (\<lambda>x. x) n + n+1)\<^sup>2" by auto
+  also have "\<dots> = (sumto (\<lambda>x. x) n)\<^sup>2 + 2*sumto (\<lambda>x. x) n * (n+1) + (n+1)\<^sup>2"
+    by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = sumto (\<lambda>x. x ^ 3) n + (n+1)^3" using IH sum_of_naturals
+    by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = sumto (\<lambda>x. x ^ 3) (Suc n)" by simp
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u) by auto
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+thm not_distinct_decomp
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v"
+    by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma prefix_shorter: "lp \<le> length xs \<Longrightarrow> \<exists>ys zs. length ys = lp \<and> xs=ys@zs"
+proof (induction xs arbitrary: lp)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs')
+  show ?case
+  proof (cases lp)
+    case 0
+    then show ?thesis by auto
+  next
+    case (Suc lp')
+    from Cons Suc have lp': "lp' \<le> length xs'" by auto
+    with Cons have "\<exists>ys zs. length ys = lp' \<and> xs' = ys @ zs" by auto
+    then obtain ys' zs' where pref': "length ys' = lp' \<and> xs' = ys' @ zs'" by auto
+    obtain ys where ys: "ys = a # ys'" by auto
+    let ?zs = zs'
+
+    from pref' Suc ys have t1: "length ys = lp" by auto
+    from pref' ys have t2: "a # xs' = ys @ ?zs" by auto
+
+    with t1 ys have "length ys = lp \<and> a # xs' = ys @ ?zs" by auto
+    then show ?thesis by auto
+  qed
+qed
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  obtain lp where lp: "lp = length xs div n" by auto
+  then have "lp \<le> length xs" by auto
+  then show "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+    using lp prefix_shorter[of lp xs] by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma nonneg: "a n \<ge> 0"
+proof (induction n)
+qed (auto+)
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ (2 ^ n) - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ (2 ^ Suc n) - 1"
+  proof -
+    have l: "(2::int) ^ Suc (2 ^ n) + 2 > 1"
+      by (smt one_le_power)
+
+    have "a (Suc n) = a n ^ 2 + 1" by auto
+    with IH power_mono[where n=2] nonneg have "a (Suc n) \<le> (2 ^ (2 ^ n) - 1) ^ 2 + 1"
+      by (simp add: \<open>\<And>b a. \<lbrakk>a \<le> b; 0 \<le> a\<rbrakk> \<Longrightarrow> a\<^sup>2 \<le> b\<^sup>2\<close>)
+
+    also have "\<dots> = (2 ^ 2 ^ n)\<^sup>2 + 1\<^sup>2 - 2 * 2 ^ 2 ^ n * 1 + 1"
+      by (simp add: power2_diff)
+
+    also have "\<dots> = (2 ^ 2 ^ Suc n) - 2 ^ (Suc (2 ^ n)) + 2"
+      by (simp add: power_even_eq)
+
+    finally show ?thesis using l
+      by (smt one_le_power one_less_numeral_iff one_power2 power_Suc power_even_eq power_less_power_Suc power_strict_increasing_iff semiring_norm(76))
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_404/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,295 @@
+Using temporary directory '/tmp/tmp.KPBWgMzVrV'
+Files in /tmp/eval-404-buhO69: tut05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission-imports>
+
+</submission-imports>
+<version>
+2016-1
+</version>
+<check>
+
+</check>
+<defs>
+
+
+save_test_theory
+</defs>
+<defs-imports>
+Main Tree
+</defs-imports>
+<image>
+HOL-Library
+</image>
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+
+  (*
+  from PREM have "n=3 \<or> n>3" by auto
+  then show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof
+  *)
+
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n\<noteq>3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using \<open>n>3\<close> by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "sumto f 0 = f 0"
+| "sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  have "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = (sumto (\<lambda>x. x) n + n+1)\<^sup>2" by auto
+  also have "\<dots> = (sumto (\<lambda>x. x) n)\<^sup>2 + 2*sumto (\<lambda>x. x) n * (n+1) + (n+1)\<^sup>2"
+    by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = sumto (\<lambda>x. x ^ 3) n + (n+1)^3" using IH sum_of_naturals
+    by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = sumto (\<lambda>x. x ^ 3) (Suc n)" by simp
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u) by auto
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+thm not_distinct_decomp
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v"
+    by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma prefix_shorter: "lp \<le> length xs \<Longrightarrow> \<exists>ys zs. length ys = lp \<and> xs=ys@zs"
+proof (induction xs arbitrary: lp)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs')
+  show ?case
+  proof (cases lp)
+    case 0
+    then show ?thesis by auto
+  next
+    case (Suc lp')
+    from Cons Suc have lp': "lp' \<le> length xs'" by auto
+    with Cons have "\<exists>ys zs. length ys = lp' \<and> xs' = ys @ zs" by auto
+    then obtain ys' zs' where pref': "length ys' = lp' \<and> xs' = ys' @ zs'" by auto
+    obtain ys where ys: "ys = a # ys'" by auto
+    let ?zs = zs'
+  
+    from pref' Suc ys have t1: "length ys = lp" by auto
+    from pref' ys have t2: "a # xs' = ys @ ?zs" by auto
+  
+    with t1 ys have "length ys = lp \<and> a # xs' = ys @ ?zs" by auto
+    then show ?thesis by auto
+  qed
+qed
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  obtain lp where lp: "lp = length xs div n" by auto
+  then have "lp \<le> length xs" by auto
+  then show "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+    using lp prefix_shorter[of lp xs] by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma nonneg: "a n \<ge> 0"
+proof (induction n)
+qed (auto+)
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ (2 ^ n) - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ (2 ^ Suc n) - 1"
+  proof -
+    have l: "(2::int) ^ Suc (2 ^ n) + 2 > 1"
+      by (smt one_le_power)
+
+    have "a (Suc n) = a n ^ 2 + 1" by auto
+    with IH power_mono[where n=2] nonneg have "a (Suc n) \<le> (2 ^ (2 ^ n) - 1) ^ 2 + 1"
+      by (simp add: \<open>\<And>b a. \<lbrakk>a \<le> b; 0 \<le> a\<rbrakk> \<Longrightarrow> a\<^sup>2 \<le> b\<^sup>2\<close>)
+
+    also have "\<dots> = (2 ^ 2 ^ n)\<^sup>2 + 1\<^sup>2 - 2 * 2 ^ 2 ^ n * 1 + 1"
+      by (simp add: power2_diff)
+
+    also have "\<dots> = (2 ^ 2 ^ Suc n) - 2 ^ (Suc (2 ^ n)) + 2"
+      by (simp add: power_even_eq)
+
+    finally show ?thesis using l
+      by (smt one_le_power one_less_numeral_iff one_power2 power_Suc power_even_eq power_less_power_Suc power_strict_increasing_iff semiring_norm(76))
+  qed
+qed
+
+
+(*<*)
+</submission>
+<check-imports>
+Submission
+</check-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_405/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_405/ex05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,143 @@
+(** Score: 10/10
+
+  A bit more Isar and a bit less auxXX lemmas would have resulted in much nicer looking proofs!
+*)
+
+(*<*)
+theory ex05
+  imports
+    Complex_Main
+    "~~/src/HOL/Library/Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+
+lemma aux68:"ysa = ys@[e] \<Longrightarrow> zs = e#rest \<Longrightarrow> Suc 0 \<le> length zs \<Longrightarrow> length ysa = Suc (length ys) \<and> ( ys @ zs = ysa @ rest)
+\<Longrightarrow> \<exists>ysa. length ysa = Suc (length ys) \<and> (\<exists>zsa. ys @ zs = ysa @ zsa)"
+  apply blast
+  done
+
+fun fstel :: "'a list\<Rightarrow>'a" where
+  "fstel (e#ls) = e"
+|  "fstel [] = undefined"
+
+fun restls :: "'a list \<Rightarrow> 'a list" where
+  "restls (e#ls) = ls"
+| "restls [] = undefined"
+
+lemma aux98: "Suc 0 \<le> length zs \<Longrightarrow> zs = (fstel zs)#(restls zs)"
+  apply (induction zs)
+   apply auto
+  done
+
+lemma aux1: "n \<le> length xs \<Longrightarrow> \<exists>ys zs. (length ys = n \<and> xs=ys@zs)"
+  apply (induction n)
+  apply (auto)
+  apply (rule aux68)
+  apply (auto)
+  apply (rule aux98)
+  apply auto
+  apply (rule aux98)
+  apply auto
+  done
+
+lemma aux2:"length n div k \<le>  length n" by auto
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  apply (rule aux1)
+  apply (rule aux2)
+  done
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+
+lemma gz:"0 \<le> a n"
+  apply (induction n)
+  apply auto
+  done
+
+lemma gz2:"(2::int) \<le> 2^(2^n)"
+  by (smt choose_even_sum linorder_not_less neq0_conv one_le_power rel_simps(25) zero_less_one)
+
+lemma red_sq: "2\<le>(c::int) \<Longrightarrow> (c -1)^2 \<le> c^2 -2"
+    apply (induction c)
+   apply auto
+  by (simp add: power2_diff)
+
+
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "(a n)^2 \<le>  (2 ^ 2 ^ n - 1)^2"
+      apply (rule power_mono[where n=2])
+      apply (rule IH)
+      apply (rule gz)
+      done
+    then have zw1: "(a n)^2 + 1\<le>  (2 ^ 2 ^ n - 1)^2 + 1" by auto
+    also have zw2: "(((2::int) ^ 2 ^ n) - 1)^2  \<le> ((2 ^ 2 ^ n) )^2 -2"
+      apply (rule red_sq)
+      apply (rule gz2)
+      done
+    from zw1 zw2 have "(a n)^2 + 1\<le>((2 ^ 2 ^ n) )^2 -1" by auto
+    then show ?thesis by (simp add: power_even_eq)
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_405/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,164 @@
+Using temporary directory '/tmp/tmp.jj3U3XAllb'
+Files in /tmp/eval-405-uek8na: ex05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+<submission-imports>
+
+</submission-imports>
+<defs-imports>
+Main Tree
+</defs-imports>
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+
+lemma aux68:"ysa = ys@[e] \<Longrightarrow> zs = e#rest \<Longrightarrow> Suc 0 \<le> length zs \<Longrightarrow> length ysa = Suc (length ys) \<and> ( ys @ zs = ysa @ rest) 
+\<Longrightarrow> \<exists>ysa. length ysa = Suc (length ys) \<and> (\<exists>zsa. ys @ zs = ysa @ zsa)"
+  apply blast
+  done
+
+fun fstel :: "'a list\<Rightarrow>'a" where
+  "fstel (e#ls) = e"
+|  "fstel [] = undefined"
+
+fun restls :: "'a list \<Rightarrow> 'a list" where
+  "restls (e#ls) = ls"
+| "restls [] = undefined"
+
+lemma aux98: "Suc 0 \<le> length zs \<Longrightarrow> zs = (fstel zs)#(restls zs)"
+  apply (induction zs)
+   apply auto
+  done
+
+lemma aux1: "n \<le> length xs \<Longrightarrow> \<exists>ys zs. (length ys = n \<and> xs=ys@zs)"
+  apply (induction n)
+  apply (auto)
+  apply (rule aux68)
+  apply (auto)
+  apply (rule aux98)
+  apply auto
+  apply (rule aux98)
+  apply auto
+  done
+
+lemma aux2:"length n div k \<le>  length n" by auto
+    
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+  apply (rule aux1)
+  apply (rule aux2)
+  done
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+    
+lemma gz:"0 \<le> a n"
+  apply (induction n)
+  apply auto
+  done 
+        
+lemma gz2:"(2::int) \<le> 2^(2^n)"
+  by (smt choose_even_sum linorder_not_less neq0_conv one_le_power rel_simps(25) zero_less_one)
+    
+lemma red_sq: "2\<le>(c::int) \<Longrightarrow> (c -1)^2 \<le> c^2 -2"
+    apply (induction c)
+   apply auto
+  by (simp add: power2_diff)
+      
+  
+    
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "(a n)^2 \<le>  (2 ^ 2 ^ n - 1)^2"
+      apply (rule power_mono[where n=2])
+      apply (rule IH)
+      apply (rule gz)
+      done
+    then have zw1: "(a n)^2 + 1\<le>  (2 ^ 2 ^ n - 1)^2 + 1" by auto
+    also have zw2: "(((2::int) ^ 2 ^ n) - 1)^2  \<le> ((2 ^ 2 ^ n) )^2 -2"
+      apply (rule red_sq)
+      apply (rule gz2)
+      done
+    from zw1 zw2 have "(a n)^2 + 1\<le>((2 ^ 2 ^ n) )^2 -1" by auto
+    then show ?thesis by (simp add: power_even_eq)
+  qed
+qed
+
+
+(*<*)
+</submission>
+<defs>
+
+
+save_test_theory
+</defs>
+<check>
+
+</check>
+<version>
+2016-1
+</version>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_399/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_399/tmpl05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,226 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+    text \<open>Fill in a proof here. Hint: Start with a case distinction
+      whether \<open>n>3\<close> or \<open>n=3\<close>. \<close>
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n\<noteq>3"
+    with PREM have "n>3" by auto
+    note IH = IH[OF this]
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "... < 2*fact n" using IH by auto
+    also have "... < (Suc n)*fact n" using \<open>n>3\<close> by auto
+    also have "... = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+"sumto f 0 = f 0" |
+"sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+  have "(sumto (\<lambda>x. x) (Suc n))^2 = (sumto (\<lambda>x. x) n + (Suc n))^2" by auto
+  also have "... = (sumto (\<lambda>x. x) n)^2 + 2*(sumto (\<lambda>x. x) n)*(Suc n) + (Suc n)^2" by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) n  + (Suc n)^3" using IH sum_of_naturals by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) (Suc n)" by (auto simp: numeral_eq_Suc)
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (x#xs) v \<longleftrightarrow> G u x \<and> path G x xs v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u)
+  apply (auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+  (* from P have foo *)
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v" by auto
+  hence *: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with * show ?thesis by blast
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  have *: "xs = take (length xs div n) xs @ drop (length xs div n) xs" by simp
+  have "length (take (length xs div n) xs) = length xs div n" by (simp add: min_absorb2)
+  with * show ?thesis by blast
+qed
+
+
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+thm power_mono[where n=2]
+
+lemma aux2: "(2::int)*(2^2^n) \<ge> 3"
+  apply (induction n)
+  apply (auto)
+  apply (smt numeral_2_eq_2 power_even_eq power_le_imp_le_base zero_le_even_power')
+  done
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = (a n)^2 + 1" by auto
+    also have "... \<le> (2^2^n - 1)^2 + 1" using IH power_mono[where n=2] by (smt a.elims zero_le_power2)
+    also have "... = (2^2^n)^2 - 2*2^2^n + 2" by (auto simp add: numeral_eq_Suc algebra_simps)
+    also have "... \<le> 2^2^(Suc n) - 1" by (simp add: aux2 power_even_eq)
+    finally show ?thesis .
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_399/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,250 @@
+Using temporary directory '/tmp/tmp.ZUX8uXimmq'
+Files in /tmp/eval-399-dogmkF: tmpl05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<image>
+HOL-Library
+</image>
+<defs>
+
+
+save_test_theory
+</defs>
+<submission-imports>
+
+</submission-imports>
+<check-imports>
+Submission
+</check-imports>
+<check>
+
+</check>
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+    text \<open>Fill in a proof here. Hint: Start with a case distinction
+      whether \<open>n>3\<close> or \<open>n=3\<close>. \<close>
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n\<noteq>3"
+    with PREM have "n>3" by auto
+    note IH = IH[OF this]
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "... < 2*fact n" using IH by auto
+    also have "... < (Suc n)*fact n" using \<open>n>3\<close> by auto
+    also have "... = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+"sumto f 0 = f 0" |
+"sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+  have "(sumto (\<lambda>x. x) (Suc n))^2 = (sumto (\<lambda>x. x) n + (Suc n))^2" by auto
+  also have "... = (sumto (\<lambda>x. x) n)^2 + 2*(sumto (\<lambda>x. x) n)*(Suc n) + (Suc n)^2" by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) n  + (Suc n)^3" using IH sum_of_naturals by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) (Suc n)" by (auto simp: numeral_eq_Suc)
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (x#xs) v \<longleftrightarrow> G u x \<and> path G x xs v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u)
+  apply (auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+  (* from P have foo *)
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v" by auto
+  hence *: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with * show ?thesis by blast
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  have *: "xs = take (length xs div n) xs @ drop (length xs div n) xs" by simp
+  have "length (take (length xs div n) xs) = length xs div n" by (simp add: min_absorb2)
+  with * show ?thesis by blast
+qed
+  
+
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+thm power_mono[where n=2]
+
+lemma aux2: "(2::int)*(2^2^n) \<ge> 3"
+  apply (induction n)
+  apply (auto)
+  apply (smt numeral_2_eq_2 power_even_eq power_le_imp_le_base zero_le_even_power')
+  done
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = (a n)^2 + 1" by auto
+    also have "... \<le> (2^2^n - 1)^2 + 1" using IH power_mono[where n=2] by (smt a.elims zero_le_power2)
+    also have "... = (2^2^n)^2 - 2*2^2^n + 2" by (auto simp add: numeral_eq_Suc algebra_simps)
+    also have "... \<le> 2^2^(Suc n) - 1" by (simp add: aux2 power_even_eq)
+    finally show ?thesis .
+  qed
+qed
+
+
+(*<*)
+</submission>
+<defs-imports>
+Main Tree
+</defs-imports>
+<version>
+2016-1
+</version>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_403/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_403/hw05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,82 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+    let ?n = "length xs div n"
+    let ?ys = "take ?n xs"
+    let ?zs = "drop ?n xs"
+    have s1: "length ?ys = ?n" by (simp add: min.absorb2)
+    have s2: "xs = ?ys @ ?zs" by auto
+    show "length ?ys = length xs div n \<and> xs=?ys@?zs" using s1 s2 by auto
+  qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have ge0: "0 \<le> a n" by (smt a.elims zero_le_power2)
+    have "a (Suc n) = (a n) ^ 2 + 1" by auto
+    also have "\<dots> \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" using IH ge0 by (auto simp: power_mono)
+    also have "\<dots> \<le> 2 ^ 2 ^ Suc n - 1" by (auto simp: power2_diff power_even_eq)
+    finally show ?thesis .
+  qed
+qed
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_403/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,106 @@
+Using temporary directory '/tmp/tmp.CBWqal3yjZ'
+Files in /tmp/eval-403-1jniyn: hw05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission>
+
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+    let ?n = "length xs div n"
+    let ?ys = "take ?n xs"
+    let ?zs = "drop ?n xs"
+    have s1: "length ?ys = ?n" by (simp add: min.absorb2)
+    have s2: "xs = ?ys @ ?zs" by auto
+    show "length ?ys = length xs div n \<and> xs=?ys@?zs" using s1 s2 by auto
+  qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH have ge0: "0 \<le> a n" by (smt a.elims zero_le_power2)
+    have "a (Suc n) = (a n) ^ 2 + 1" by auto
+    also have "\<dots> \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" using IH ge0 by (auto simp: power_mono)
+    also have "\<dots> \<le> 2 ^ 2 ^ Suc n - 1" by (auto simp: power2_diff power_even_eq)
+    finally show ?thesis .
+  qed
+qed
+
+(*<*)
+</submission>
+<submission-imports>
+
+</submission-imports>
+<check>
+
+</check>
+<defs>
+
+
+save_test_theory
+</defs>
+<defs-imports>
+Main Tree
+</defs-imports>
+<version>
+2016-1
+</version>
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_415/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_415/hw05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,92 @@
+(** Score: 10/10
+*)
+(*<*)
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+find_theorems "?y \<le> ?x \<Longrightarrow> min ?x ?y = ?y"
+thm min_absorb2
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?num = "length xs div n"
+  let ?ys = "take ?num xs"
+  let ?zs = "drop ?num xs"
+  have "length ?ys = ?num"
+    by (simp add: min_absorb2)
+  hence "length ?ys = length xs div n \<and> xs = ?ys @ ?zs" by simp
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n = 2 ]
+lemma a_ge_zero: "a n \<ge> 0"
+  by (induction n) auto
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    let ?l = "(a n)"
+    let ?r = "2 ^ 2 ^ n -1"
+    have "a (Suc n) = (a n) ^ 2 + 1" by simp
+    also have "... \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1"
+      using Suc.IH power_mono[of ?l ?r "2"] a_ge_zero[where n=n] by simp
+    also have "... = ((2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1) + 1" by algebra
+    also have "... \<le> 2 ^ 2 ^ (Suc n) - 1"
+      by (simp add: power_even_eq)
+    finally show ?case .
+  qed
+qed
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_415/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,116 @@
+Using temporary directory '/tmp/tmp.X09y0XjLul'
+Files in /tmp/eval-415-f9OPoQ: hw05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs>
+
+
+save_test_theory
+</defs>
+<submission-imports>
+
+</submission-imports>
+<version>
+2016-1
+</version>
+<check-imports>
+Submission
+</check-imports>
+<submission>
+
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+find_theorems "?y \<le> ?x \<Longrightarrow> min ?x ?y = ?y"
+thm min_absorb2
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?num = "length xs div n"
+  let ?ys = "take ?num xs"
+  let ?zs = "drop ?num xs"
+  have "length ?ys = ?num"
+    by (simp add: min_absorb2)
+  hence "length ?ys = length xs div n \<and> xs = ?ys @ ?zs" by simp
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n = 2 ]
+lemma a_ge_zero: "a n \<ge> 0"
+  by (induction n) auto
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    let ?l = "(a n)"
+    let ?r = "2 ^ 2 ^ n -1"
+    have "a (Suc n) = (a n) ^ 2 + 1" by simp
+    also have "... \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" 
+      using Suc.IH power_mono[of ?l ?r "2"] a_ge_zero[where n=n] by simp
+    also have "... = ((2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1) + 1" by algebra
+    also have "... \<le> 2 ^ 2 ^ (Suc n) - 1"
+      by (simp add: power_even_eq)
+    finally show ?case .
+  qed
+qed
+
+(*<*)
+</submission>
+<defs-imports>
+Main Tree
+</defs-imports>
+<check>
+
+</check>
+<image>
+HOL-Library
+</image>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_418/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_418/ex05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,148 @@
+(** Score: 10/10
+
+  See remark on also..finally vs. moreover...ultimately in hw 1!
+*)
+(*<*)
+theory ex05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n = 3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n \<noteq> 3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using \<open>n>3\<close> by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "(take (length xs div n) xs)"
+  let ?zs = "(drop (length xs div n) xs)"
+  have "length ?ys = (length xs div n)"
+    by (simp add: min.absorb2)
+  also have "xs = ?ys@?zs" by auto
+  thus ?thesis
+  using calculation by blast
+
+  (** Don't use also to just accumulate facts! also..finally is for transitive reasoning.
+    Better use moreover...ultimately (not in the lecture, but clearly what you would have needed here)
+  *)
+
+  have "length ?ys = (length xs div n)"
+    by (simp add: min.absorb2)
+  moreover have "xs = ?ys@?zs" by auto
+  ultimately have ?thesis by blast
+
+
+
+
+qed
+
+
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+
+
+
+thm power_mono[where n=2]
+
+
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have " a (Suc n) =  (a n) ^2 + 1" by simp
+    also have  "... \<le> (2 ^ 2 ^ n - 1)^2+1" using power_mono[where n = 2] IH
+      by (smt a.elims zero_le_power2)
+    also have "...  = ((2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1) + 1"  by algebra
+    also have "... \<le> (2 ^ 2 ^ n)\<^sup>2 - 1 " by simp
+    finally show ?thesis
+      by (simp add: mult_2 power2_eq_square power_add)
+    qed
+qed
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_418/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,158 @@
+Using temporary directory '/tmp/tmp.K5gH09sbtF'
+Files in /tmp/eval-418-c9Ma7A: ex05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n = 3"
+    show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n \<noteq> 3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using \<open>n>3\<close> by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "(take (length xs div n) xs)"
+  let ?zs = "(drop (length xs div n) xs)"
+  have "length ?ys = (length xs div n)"
+    by (simp add: min.absorb2)
+  also have "xs = ?ys@?zs" by auto
+  thus ?thesis
+  using calculation by blast 
+qed
+
+
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+
+
+
+thm power_mono[where n=2]
+
+
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have " a (Suc n) =  (a n) ^2 + 1" by simp
+    also have  "... \<le> (2 ^ 2 ^ n - 1)^2+1" using power_mono[where n = 2] IH
+      by (smt a.elims zero_le_power2)
+    also have "...  = ((2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1) + 1"  by algebra
+    also have "... \<le> (2 ^ 2 ^ n)\<^sup>2 - 1 " by simp
+    finally show ?thesis
+      by (simp add: mult_2 power2_eq_square power_add)
+    qed
+qed
+
+
+(*<*)
+</submission>
+<submission-imports>
+
+</submission-imports>
+<check>
+
+</check>
+<image>
+HOL-Library
+</image>
+<defs>
+
+
+save_test_theory
+</defs>
+<check-imports>
+Submission
+</check-imports>
+<version>
+2016-1
+</version>
+<defs-imports>
+Main Tree
+</defs-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_398/Home05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,54 @@
+(** Score: 10/10
+*)
+theory Home05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+(* Homework 5.1 Split Lists *)
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs = ys @ zs"
+proof -
+  let ?ys = "take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+
+  have "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"
+    by (auto simp add: min_absorb2)
+  thus ?thesis
+    by blast
+qed
+
+(* Homework 5.2 Estimate Recursion Equation *)
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0"
+| "a (Suc n) = a n ^ 2 + 1"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = (a n)^2 + 1"
+      by simp
+    also have "... \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" using IH
+      by (smt a.elims zero_le_power2 power_mono[where n=2])
+    also have "... = (2 ^ 2 ^ n * 2 ^ 2 ^ n) - (2 * 2 ^ 2 ^ n) + 2"
+      by algebra
+    also have "... = 2 ^ (2 ^ n + 2 ^ n) - (2 * 2 ^ 2 ^ n) + 2"
+      by (simp add: power_add)
+    also have "... = 2 ^ 2 ^ Suc n - (2 * 2 ^ 2 ^ n) + 2"
+      by auto
+    also have "... \<le> 2 ^ 2 ^ Suc n - 1"
+      by auto
+    finally show ?thesis .
+  qed
+qed
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_398/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_398/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,80 @@
+Using temporary directory '/tmp/tmp.yyrJLzvVa4'
+Files in /tmp/eval-398-ac0ePW: Home05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission>
+
+
+(* Homework 5.1 Split Lists *)
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs = ys @ zs"
+proof -
+  let ?ys = "take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+
+  have "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"
+    by (auto simp add: min_absorb2)
+  thus ?thesis
+    by blast
+qed
+
+(* Homework 5.2 Estimate Recursion Equation *)
+
+fun a :: "nat \<Rightarrow> int" where
+  "a 0 = 0" 
+| "a (Suc n) = a n ^ 2 + 1"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = (a n)^2 + 1" 
+      by simp
+    also have "... \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" using IH
+      by (smt a.elims zero_le_power2 power_mono[where n=2])
+    also have "... = (2 ^ 2 ^ n * 2 ^ 2 ^ n) - (2 * 2 ^ 2 ^ n) + 2" 
+      by algebra
+    also have "... = 2 ^ (2 ^ n + 2 ^ n) - (2 * 2 ^ 2 ^ n) + 2"
+      by (simp add: power_add)
+    also have "... = 2 ^ 2 ^ Suc n - (2 * 2 ^ 2 ^ n) + 2"
+      by auto
+    also have "... \<le> 2 ^ 2 ^ Suc n - 1"
+      by auto
+    finally show ?thesis .
+  qed
+qed
+</submission>
+<check-imports>
+Submission
+</check-imports>
+<defs-imports>
+Main Tree
+</defs-imports>
+<check>
+
+</check>
+<submission-imports>
+
+</submission-imports>
+<defs>
+
+
+save_test_theory
+</defs>
+<image>
+HOL-Library
+</image>
+<version>
+2016-1
+</version>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_400/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_400/tmpl05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,268 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]:"n = 3"
+    then show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n \<noteq> 3"
+    with PREM have "n>3" by auto
+    note IH = IH[OF this]
+    have "(2::nat)^(Suc n) = 2 * 2^n" by simp
+    also have "... < 2 * (fact n)" using IH by (auto simp add: nat_mult_less_cancel1)
+    also have "... < (Suc n) * (fact n)" using `n>3` by auto
+    also have "... = fact(Suc n)" by auto
+    finally show ?thesis.
+    text \<open>Fill in a proof here. Hint: Start with a case distinction
+      whether \<open>n>3\<close> or \<open>n=3\<close>. \<close>
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+"sumto f 0 = f 0" |
+"sumto f (Suc n) = f (Suc n) + (sumto f n)"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  let "?S" = "(sumto (\<lambda>x. x))"
+  have "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = (sumto (\<lambda>x. x) n + n+1)^2" by auto
+  also have "... = (sumto (\<lambda>x. x) n)^2 + 2 * (sumto (\<lambda>x. x) n) * (n+1) + (n+1)^2" by(auto simp: numeral_eq_Suc)
+  also have "... = (sumto (\<lambda>x. x^3) n) + n * (n+1) * (n+1) + (n+1)^2" using IH sum_of_naturals by auto
+  also have "... = (sumto (\<lambda>x. x^3) n) +(n+1)^3" by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) (Suc n)" by auto
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)".
+  text \<open>Insert a proof here\<close>
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path G u [] v \<longleftrightarrow> u = v" |
+  "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply(induction p1 arbitrary: u)
+   apply(auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+thm not_distinct_decomp
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+  [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v" by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+  have "length ?p' > length p \<and> \<not> distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  fixes xs n
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists> ys zs. length ys = length xs div n \<and> xs=ys@zs" (is "\<exists> ys zs. ?P1 ys \<and> ?P2 ys zs")
+proof -
+  have 1: "?P1 (take ((length xs)div n) xs)" by (auto simp add: min_absorb2)
+  have 2: "?P2 (take ((length xs)div n) xs) (drop ((length xs)div n) xs)" by auto
+  from 1 2 show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = (a n) ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+
+
+value " (2::nat) * (2 ^ 2 ^ 0)"
+
+lemma aux1: " (b::int)>1 \<Longrightarrow> b * (b ^ b ^ n) \<ge> b^2"
+  apply(induction n arbitrary: b)
+  apply(auto simp add: algebra_simps numeral_eq_Suc)
+  by (smt One_nat_def Suc_leI le_less nat_one_le_power of_nat_0_less_iff one_le_mult_iff power_Suc0_right power_increasing_iff)
+
+lemma aux2: "4 \<le> (2::int) * 2^2^n"
+  by (smt one_less_power pos2 zero_less_power)
+
+lemma aux3: "-(2::int) * 2^2^n \<le> -4"
+  apply(auto simp add: aux1 aux2 algebra_simps)
+  done
+
+
+lemma aux4: "-(2::nat) * 2^2^n \<le> -3"
+proof -
+  have "- 1 * int 2 * 2 ^ 2 ^ n \<le> - 4"
+    using aux3 by auto
+  then show ?thesis
+    by auto
+qed
+
+lemma aux5: "(x::int) < (y::int) \<Longrightarrow> x \<le> y-1" by simp
+
+lemma aux6: "\<lbrakk>(x::int)\<ge>0; x<y\<rbrakk> \<Longrightarrow> x^2 \<le> (y-1)^2"
+  by (simp add: power_mono)
+
+lemma aux7: "(a n)\<ge>0"
+  apply(induction n)
+   apply(auto)
+  done
+
+lemma aux8: "a n < 2 ^ 2 ^ n \<Longrightarrow> (a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2"
+  by (simp add: aux7 power_mono)
+
+
+lemma "a (n::nat) \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> (2 ^ 2 ^ n - 1)"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+    have "a (Suc n) = (a n)^2 +1" by simp
+    also have "... \<le> ( 2 ^ 2 ^ n - 1)^2 +1" using IH by(auto simp add: aux8)
+      also have "... = (2 ^ 2 ^ n) * (2 ^ 2 ^ n) - 2 * (2 ^ 2 ^ n) + 2" by (auto simp add: algebra_simps numeral_eq_Suc)
+      also have "... = (2 ^ 2 ^ (n+1)) - 2 * (2 ^ 2 ^ n) + 2"
+        by (metis Suc_eq_plus1 power_Suc semiring_normalization_rules(36))
+      also have "... \<le> (2 ^ 2 ^ (n+1)) -1"
+        by simp
+    finally show ?thesis by auto
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_400/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,293 @@
+Using temporary directory '/tmp/tmp.hmRfbDCJqh'
+Files in /tmp/eval-400-7kFMyY: tmpl05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs-imports>
+Main Tree
+</defs-imports>
+<check-imports>
+Submission
+</check-imports>
+<submission>
+
+(*>*)
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]:"n = 3"
+    then show ?thesis by (auto simp: numeral_eq_Suc)
+  next
+    assume "n \<noteq> 3"
+    with PREM have "n>3" by auto
+    note IH = IH[OF this]
+    have "(2::nat)^(Suc n) = 2 * 2^n" by simp
+    also have "... < 2 * (fact n)" using IH by (auto simp add: nat_mult_less_cancel1)
+    also have "... < (Suc n) * (fact n)" using `n>3` by auto
+    also have "... = fact(Suc n)" by auto
+    finally show ?thesis.
+    text \<open>Fill in a proof here. Hint: Start with a case distinction
+      whether \<open>n>3\<close> or \<open>n=3\<close>. \<close>
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
+where
+"sumto f 0 = f 0" |
+"sumto f (Suc n) = f (Suc n) + (sumto f n)"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  let "?S" = "(sumto (\<lambda>x. x))"
+  have "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = (sumto (\<lambda>x. x) n + n+1)^2" by auto
+  also have "... = (sumto (\<lambda>x. x) n)^2 + 2 * (sumto (\<lambda>x. x) n) * (n+1) + (n+1)^2" by(auto simp: numeral_eq_Suc)
+  also have "... = (sumto (\<lambda>x. x^3) n) + n * (n+1) * (n+1) + (n+1)^2" using IH sum_of_naturals by auto
+  also have "... = (sumto (\<lambda>x. x^3) n) +(n+1)^3" by (auto simp: numeral_eq_Suc)
+  also have "... = sumto (\<lambda>x. x ^ 3) (Suc n)" by auto
+  finally show "(sumto (\<lambda>x. x) (Suc n))\<^sup>2 = sumto (\<lambda>x. x ^ 3) (Suc n)".
+  text \<open>Insert a proof here\<close>
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where
+  "path G u [] v \<longleftrightarrow> u = v" |
+  "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v" 
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)" 
+  apply(induction p1 arbitrary: u) 
+   apply(auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+
+thm not_distinct_decomp
+
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+  [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v" by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+  have "length ?p' > length p \<and> \<not> distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  fixes xs n
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists> ys zs. length ys = length xs div n \<and> xs=ys@zs" (is "\<exists> ys zs. ?P1 ys \<and> ?P2 ys zs")
+proof -
+  have 1: "?P1 (take ((length xs)div n) xs)" by (auto simp add: min_absorb2)
+  have 2: "?P2 (take ((length xs)div n) xs) (drop ((length xs)div n) xs)" by auto
+  from 1 2 show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = (a n) ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+
+
+value " (2::nat) * (2 ^ 2 ^ 0)"
+
+lemma aux1: " (b::int)>1 \<Longrightarrow> b * (b ^ b ^ n) \<ge> b^2"
+  apply(induction n arbitrary: b)
+  apply(auto simp add: algebra_simps numeral_eq_Suc)
+  by (smt One_nat_def Suc_leI le_less nat_one_le_power of_nat_0_less_iff one_le_mult_iff power_Suc0_right power_increasing_iff)
+
+lemma aux2: "4 \<le> (2::int) * 2^2^n"
+  by (smt one_less_power pos2 zero_less_power)
+
+lemma aux3: "-(2::int) * 2^2^n \<le> -4" 
+  apply(auto simp add: aux1 aux2 algebra_simps)
+  done
+
+
+lemma aux4: "-(2::nat) * 2^2^n \<le> -3"
+proof -
+  have "- 1 * int 2 * 2 ^ 2 ^ n \<le> - 4"
+    using aux3 by auto
+  then show ?thesis
+    by auto
+qed
+
+lemma aux5: "(x::int) < (y::int) \<Longrightarrow> x \<le> y-1" by simp
+
+lemma aux6: "\<lbrakk>(x::int)\<ge>0; x<y\<rbrakk> \<Longrightarrow> x^2 \<le> (y-1)^2"
+  by (simp add: power_mono)
+
+lemma aux7: "(a n)\<ge>0"
+  apply(induction n)
+   apply(auto)
+  done
+
+lemma aux8: "a n < 2 ^ 2 ^ n \<Longrightarrow> (a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2"
+  by (simp add: aux7 power_mono)
+
+
+lemma "a (n::nat) \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> (2 ^ 2 ^ n - 1)"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+    have "a (Suc n) = (a n)^2 +1" by simp
+    also have "... \<le> ( 2 ^ 2 ^ n - 1)^2 +1" using IH by(auto simp add: aux8) 
+      also have "... = (2 ^ 2 ^ n) * (2 ^ 2 ^ n) - 2 * (2 ^ 2 ^ n) + 2" by (auto simp add: algebra_simps numeral_eq_Suc)
+      also have "... = (2 ^ 2 ^ (n+1)) - 2 * (2 ^ 2 ^ n) + 2"
+        by (metis Suc_eq_plus1 power_Suc semiring_normalization_rules(36))
+      also have "... \<le> (2 ^ 2 ^ (n+1)) -1" 
+        by simp
+    finally show ?thesis by auto
+  qed
+qed
+
+
+(*<*)
+</submission>
+<image>
+HOL-Library
+</image>
+<check>
+
+</check>
+<version>
+2016-1
+</version>
+<defs>
+
+
+save_test_theory
+</defs>
+<submission-imports>
+
+</submission-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_401/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_401/hw05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,100 @@
+(** Score: 10/10
+
+  To literally reference to facts, better use cartouches \<open>x>0\<close> (modern syntax)
+  rather than backticks `x>0` (deprecated legacy syntax)
+
+*)
+(*<*)
+theory hw05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+let ?k = "length xs div n"
+let ?ys = "take ?k xs"
+let ?zs = "drop ?k xs"
+have A: "length ?ys = length xs div n"
+by (auto simp: min_absorb2)
+have B: "xs = ?ys@?zs" by auto
+from A and B show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+find_theorems "_ \<le> _ \<Longrightarrow> _^_ \<le> _^_"
+find_theorems "_ \<le> _ - 1"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+
+(* trivial facts---required for different steps *)
+have "n\<ge>0" by auto
+have "0\<le>a n" apply(induction n) by auto
+
+(* chain of equalities that yields the claim *)
+have "a (Suc n) = a n^2 + 1" by simp
+also have "... \<le> (2^2^n-1)^2 + 1" using IH `0\<le>a n` by(simp add: power_mono)
+also have "... = (2^2^n)^2 - 2*2^2^n + 2" by (auto simp: power2_diff)
+also have "... = 2^(2*2^n) - 2^(2^n+1) + 2" by (auto simp: semiring_normalization_rules(31))
+also have "... = 2^2^(Suc n) + 2 - 2^(2^n+1)" by auto
+also have "... \<le> 2^2^(Suc n) - 1" using `n\<ge>0` by simp
+finally show ?thesis .
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_401/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,120 @@
+Using temporary directory '/tmp/tmp.9JoLzfjIqe'
+Files in /tmp/eval-401-EzEIsV: hw05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs-imports>
+Main Tree
+</defs-imports>
+<version>
+2016-1
+</version>
+<defs>
+
+
+save_test_theory
+</defs>
+<check>
+
+</check>
+<image>
+HOL-Library
+</image>
+<submission-imports>
+
+</submission-imports>
+<check-imports>
+Submission
+</check-imports>
+<submission>
+
+(*>*)
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+let ?k = "length xs div n"
+let ?ys = "take ?k xs"
+let ?zs = "drop ?k xs"
+have A: "length ?ys = length xs div n"
+by (auto simp: min_absorb2)
+have B: "xs = ?ys@?zs" by auto
+from A and B show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+find_theorems "_ \<le> _ \<Longrightarrow> _^_ \<le> _^_"
+find_theorems "_ \<le> _ - 1"
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+
+(* trivial facts---required for different steps *)
+have "n\<ge>0" by auto
+have "0\<le>a n" apply(induction n) by auto
+
+(* chain of equalities that yields the claim *)
+have "a (Suc n) = a n^2 + 1" by simp
+also have "... \<le> (2^2^n-1)^2 + 1" using IH `0\<le>a n` by(simp add: power_mono)
+also have "... = (2^2^n)^2 - 2*2^2^n + 2" by (auto simp: power2_diff)
+also have "... = 2^(2*2^n) - 2^(2^n+1) + 2" by (auto simp: semiring_normalization_rules(31))
+also have "... = 2^2^(Suc n) + 2 - 2^(2^n+1)" by auto
+also have "... \<le> 2^2^(Suc n) - 1" using `n\<ge>0` by simp
+finally show ?thesis .
+  qed
+qed
+
+
+(*<*)
+</submission>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_413/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_413/ex05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,96 @@
+(** Score: 10/10
+*)
+theory ex05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+(*Homework 5.1*)
+
+(*Proof idea: construct ys and zs according to the restrictions given
+              in the lemma, thus already showing their existence*)
+
+lemma rule_1: "(m::nat) div (n::nat) \<le> m"
+  by auto
+
+lemma rule_2: "(y::nat) \<le> (x::nat) \<Longrightarrow> min x y = y"
+  by auto
+
+lemma aux[simp]: "min (length xs) (length xs div n) = length xs div n"
+  apply (induction xs)
+  apply(auto)
+  using rule_1 rule_2 by blast
+
+lemma
+  assumes "n\<ge>0"
+  shows " \<exists> ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof
+  let ?ys = "take (length (xs) div n) xs"
+  have "length (take (length xs div n) xs) = length xs div n" by simp
+  then obtain zs where k: "zs = drop (length (xs) div n) xs" by blast
+  hence "xs = ?ys @ zs" by (simp)
+  then have "length ?ys = length xs div n \<and> xs = ?ys @ zs" using k by simp
+  then show "\<exists> zs. length ?ys = length xs div n \<and> xs=?ys@zs" by blast
+qed
+
+(*Homework 5.2*)
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n^2 + 1"
+
+thm power_mono[where n=2]
+
+(*First, some lemmas for simplification are needed. I decided to put them
+  before the actual proof for better overview*)
+
+lemma rule_3[simp]: "0 < (Suc(Suc(0))) ^ (n::nat)"
+  by simp
+
+lemma approx_1: "a n \<le> 2 ^ (2 ^ n) - 1 \<Longrightarrow> (a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2"
+  apply(induction n)
+  apply(simp)
+  apply(simp add: power_mono)
+  done
+
+lemma binomial_1: "(x::int) > 0 \<Longrightarrow> (x - 1) ^ 2 = x ^ 2 - 2 * x + 1"
+proof -
+  obtain "(x - 1) * Suc(0) = (x - 1)" by force
+  have "(x - 1) ^ 2 = (x - 1) * ((x - 1) * 1)" by (simp add: numeral_eq_Suc)
+  also have "... = (x - 1) * (x - 1)"  by simp
+  also have "... = (x - 1) * x + (x - 1) * (-1)" by (simp add: left_diff_distrib mult.commute)
+  also have "... = x * x - x - x + 1" by (simp add: semiring_normalization_rules(3))
+  also have "... = x ^ 2 - 2 * x + 1" by (simp add: power2_eq_square)
+  finally show "(x - 1) ^ 2 = x ^ 2 - 2 * x + 1".
+qed
+
+lemma simpl_1: "((2::int) ^ 2 ^ n - 1)\<^sup>2 = (2 ^ 2 ^ n)\<^sup>2 - 2 * (2 ^ 2 ^ n) + 1"
+  by (simp add: ex05.binomial_1)
+
+(*Now, attempt to proof actual lemma
+  Proof ideas (Induction step): a is recursive, apply 1 step of a
+                                then apply induction hypothesis
+                                simplify the term using rules and simplifications as above
+                                approximate: if 2 < (2*2^n + 1), then -2 > -1*(2*2^n + 1)
+                                finally, obtain the goal*)
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof (induction n)
+case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH : "a n \<le> 2 ^ (2 ^ n) - 1"
+  show "a (Suc n) \<le> 2 ^ (2 ^ (Suc n)) - 1"
+  proof -
+    have "a (Suc n) = a n ^ 2 + 1" by simp
+    also have "... \<le> (((2 ^ (2 ^ n)) - 1) ^ 2) + 1" using IH approx_1 by simp
+    also have "... = (2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1 + 1" by (simp add: simpl_1)
+    also have "... \<le> 2 ^ (2 ^ (n + 1)) - 2 + 1"
+      by (smt Suc_eq_plus1 simpl_1 ex05.binomial_1 one_le_power one_less_numeral_iff one_power2 power_Suc power_even_eq power_less_power_Suc power_strict_increasing_iff semiring_norm(76))
+    also have "... \<le> 2 ^ (2 ^ (Suc n)) - 1" by simp
+    finally show "a (Suc n) \<le> 2 ^ (2 ^ (Suc n)) - 1".
+  qed
+qed
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_413/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,122 @@
+Using temporary directory '/tmp/tmp.zwCGaiKMd8'
+Files in /tmp/eval-413-fEc39V: ex05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<submission-imports>
+
+</submission-imports>
+<defs>
+
+
+save_test_theory
+</defs>
+<submission>
+
+
+(*Homework 5.1*)
+
+(*Proof idea: construct ys and zs according to the restrictions given
+              in the lemma, thus already showing their existence*)
+
+lemma rule_1: "(m::nat) div (n::nat) \<le> m"
+  by auto
+
+lemma rule_2: "(y::nat) \<le> (x::nat) \<Longrightarrow> min x y = y"
+  by auto
+
+lemma aux[simp]: "min (length xs) (length xs div n) = length xs div n"
+  apply (induction xs)
+  apply(auto)
+  using rule_1 rule_2 by blast
+
+lemma
+  assumes "n\<ge>0" 
+  shows " \<exists> ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof 
+  let ?ys = "take (length (xs) div n) xs"
+  have "length (take (length xs div n) xs) = length xs div n" by simp
+  then obtain zs where k: "zs = drop (length (xs) div n) xs" by blast
+  hence "xs = ?ys @ zs" by (simp)
+  then have "length ?ys = length xs div n \<and> xs = ?ys @ zs" using k by simp
+  then show "\<exists> zs. length ?ys = length xs div n \<and> xs=?ys@zs" by blast
+qed
+
+(*Homework 5.2*)
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n^2 + 1"
+
+thm power_mono[where n=2]
+
+(*First, some lemmas for simplification are needed. I decided to put them 
+  before the actual proof for better overview*)
+
+lemma rule_3[simp]: "0 < (Suc(Suc(0))) ^ (n::nat)"
+  by simp
+
+lemma approx_1: "a n \<le> 2 ^ (2 ^ n) - 1 \<Longrightarrow> (a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2"
+  apply(induction n)
+  apply(simp)
+  apply(simp add: power_mono)
+  done
+
+lemma binomial_1: "(x::int) > 0 \<Longrightarrow> (x - 1) ^ 2 = x ^ 2 - 2 * x + 1"
+proof -
+  obtain "(x - 1) * Suc(0) = (x - 1)" by force
+  have "(x - 1) ^ 2 = (x - 1) * ((x - 1) * 1)" by (simp add: numeral_eq_Suc)
+  also have "... = (x - 1) * (x - 1)"  by simp
+  also have "... = (x - 1) * x + (x - 1) * (-1)" by (simp add: left_diff_distrib mult.commute)
+  also have "... = x * x - x - x + 1" by (simp add: semiring_normalization_rules(3))
+  also have "... = x ^ 2 - 2 * x + 1" by (simp add: power2_eq_square) 
+  finally show "(x - 1) ^ 2 = x ^ 2 - 2 * x + 1".
+qed 
+
+lemma simpl_1: "((2::int) ^ 2 ^ n - 1)\<^sup>2 = (2 ^ 2 ^ n)\<^sup>2 - 2 * (2 ^ 2 ^ n) + 1"
+  by (simp add: ex05.binomial_1)
+
+(*Now, attempt to proof actual lemma
+  Proof ideas (Induction step): a is recursive, apply 1 step of a 
+                                then apply induction hypothesis
+                                simplify the term using rules and simplifications as above
+                                approximate: if 2 < (2*2^n + 1), then -2 > -1*(2*2^n + 1)
+                                finally, obtain the goal*)
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof (induction n)
+case 0 thus ?case by simp
+next
+  case (Suc n) 
+  assume IH : "a n \<le> 2 ^ (2 ^ n) - 1"
+  show "a (Suc n) \<le> 2 ^ (2 ^ (Suc n)) - 1"
+  proof -
+    have "a (Suc n) = a n ^ 2 + 1" by simp
+    also have "... \<le> (((2 ^ (2 ^ n)) - 1) ^ 2) + 1" using IH approx_1 by simp
+    also have "... = (2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 1 + 1" by (simp add: simpl_1)
+    also have "... \<le> 2 ^ (2 ^ (n + 1)) - 2 + 1"
+      by (smt Suc_eq_plus1 simpl_1 ex05.binomial_1 one_le_power one_less_numeral_iff one_power2 power_Suc power_even_eq power_less_power_Suc power_strict_increasing_iff semiring_norm(76))
+    also have "... \<le> 2 ^ (2 ^ (Suc n)) - 1" by simp
+    finally show "a (Suc n) \<le> 2 ^ (2 ^ (Suc n)) - 1".
+  qed
+qed
+</submission>
+<check-imports>
+Submission
+</check-imports>
+<version>
+2016-1
+</version>
+<image>
+HOL-Library
+</image>
+<check>
+
+</check>
+<defs-imports>
+Main Tree
+</defs-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_409/HW05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,66 @@
+(** Score: 10/10
+*)
+theory HW05
+  imports Main
+begin
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?ys = " take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+  have f1:"length ?ys = (length xs div n)" by (simp add: min_absorb2)
+  have f2:"xs = ?ys @ ?zs " by auto
+  then show "length ?ys = length xs div n \<and> xs = ?ys@?zs"
+    using f1 f2 by blast
+qed
+
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have f1: "a n \<ge> 0"  by (smt a.elims zero_le_power2)
+    have  "a (Suc n) = (a (n))^2 +1" by auto
+    also have " \<dots> \<le> (2 ^ (2^ n) -1)^2 +1 "  using IH f1 by (auto simp add:power_mono)
+    also have "\<dots> \<le> (2 ^ (2^ Suc n)) -1" by (auto simp: power2_diff simp add: power_even_eq)
+    finally show ?thesis .
+  qed
+qed
+
+find_theorems "(_-_)^2"
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_409/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_409/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,94 @@
+Using temporary directory '/tmp/tmp.dtXIW2TtiH'
+Files in /tmp/eval-409-lFoVqW: HW05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs-imports>
+Main Tree
+</defs-imports>
+<check-imports>
+Submission
+</check-imports>
+<image>
+HOL-Library
+</image>
+<submission>
+
+
+lemma 
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?ys = " take (length xs div n) xs" 
+  let ?zs = "drop (length xs div n) xs"
+  have f1:"length ?ys = (length xs div n)" by (simp add: min_absorb2)
+  have f2:"xs = ?ys @ ?zs " by auto
+  then show "length ?ys = length xs div n \<and> xs = ?ys@?zs" 
+    using f1 f2 by blast
+qed
+                                           
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have f1: "a n \<ge> 0"  by (smt a.elims zero_le_power2)
+    have  "a (Suc n) = (a (n))^2 +1" by auto
+    also have " \<dots> \<le> (2 ^ (2^ n) -1)^2 +1 "  using IH f1 by (auto simp add:power_mono)
+    also have "\<dots> \<le> (2 ^ (2^ Suc n)) -1" by (auto simp: power2_diff simp add: power_even_eq)
+    finally show ?thesis . 
+  qed
+qed
+
+find_theorems "(_-_)^2"
+</submission>
+<defs>
+
+
+save_test_theory
+</defs>
+<version>
+2016-1
+</version>
+<check>
+
+</check>
+<submission-imports>
+
+</submission-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_407/Homework05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,63 @@
+(** Score: 10/10
+*)
+(*<*)
+theory Homework05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?n = "length xs div n"
+  let ?ys = "take ?n xs"
+  let ?zs = "drop ?n xs"
+  have aux1:"length ?ys = length xs div n" by(simp add:min.absorb2)
+  have aux2:"xs = ?ys @ ?zs" by auto
+  show "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"  using aux1 aux2 by auto
+qed
+
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH  have "0 \<le> a n" by (smt a.elims zero_le_power2)
+    also have "a (Suc n) = (a n)^2 + 1" by auto
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1)^2" using Suc.IH \<open>0 \<le> a n\<close> power_mono by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))"  by (simp add: power2_diff power_even_eq)
+    also have "... \<le>  2 ^ 2 ^ Suc n - 1"  using Suc.IH \<open>0 \<le> a n\<close> by auto
+    show ?thesis by (smt Suc_eq_plus1 \<open>(2 ^ 2 ^ n - 1)\<^sup>2 \<le> 2 ^ 2 ^ (n + 1) + 1 - 2 * 2 ^ 2 ^ n\<close> \<open>(a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2\<close> \<open>2 ^ 2 ^ (n + 1) + 1 - 2 * 2 ^ 2 ^ n \<le> 2 ^ 2 ^ Suc n - 1\<close> \<open>a (Suc n) = (a n)\<^sup>2 + 1\<close> a.elims power2_less_eq_zero_iff power_0 power_one_right zero_power2)
+qed
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_407/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_407/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,87 @@
+Using temporary directory '/tmp/tmp.qWuof1GxcU'
+Files in /tmp/eval-407-d5bGpZ: Homework05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs-imports>
+Main Tree
+</defs-imports>
+<check>
+
+</check>
+<submission>
+
+(*>*)
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0"
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (intro exI)
+  let ?n = "length xs div n"
+  let ?ys = "take ?n xs"
+  let ?zs = "drop ?n xs"
+  have aux1:"length ?ys = length xs div n" by(simp add:min.absorb2)
+  have aux2:"xs = ?ys @ ?zs" by auto
+  show "length ?ys = length xs div n \<and> xs = ?ys @ ?zs"  using aux1 aux2 by auto
+qed
+
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    from IH  have "0 \<le> a n" by (smt a.elims zero_le_power2)
+    also have "a (Suc n) = (a n)^2 + 1" by auto
+    also have "(a n)^2 \<le> (2 ^ 2 ^ n - 1)^2" using Suc.IH \<open>0 \<le> a n\<close> power_mono by blast
+    also have "... \<le> (2 ^ 2 ^ (n + 1)) + 1 - 2*2^(2^(n))"  by (simp add: power2_diff power_even_eq)
+    also have "... \<le>  2 ^ 2 ^ Suc n - 1"  using Suc.IH \<open>0 \<le> a n\<close> by auto
+    show ?thesis by (smt Suc_eq_plus1 \<open>(2 ^ 2 ^ n - 1)\<^sup>2 \<le> 2 ^ 2 ^ (n + 1) + 1 - 2 * 2 ^ 2 ^ n\<close> \<open>(a n)\<^sup>2 \<le> (2 ^ 2 ^ n - 1)\<^sup>2\<close> \<open>2 ^ 2 ^ (n + 1) + 1 - 2 * 2 ^ 2 ^ n \<le> 2 ^ 2 ^ Suc n - 1\<close> \<open>a (Suc n) = (a n)\<^sup>2 + 1\<close> a.elims power2_less_eq_zero_iff power_0 power_one_right zero_power2)
+qed
+
+(*<*)
+</submission>
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+<submission-imports>
+
+</submission-imports>
+<version>
+2016-1
+</version>
+<defs>
+
+
+save_test_theory
+</defs>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_410/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_410/ex05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,238 @@
+(** Score: 10/10
+*)
+theory ex05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+(*
+  from PREM have "n=3 \<or> n>3" by auto
+  then show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof
+*)
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: eval_nat_numeral)
+  next
+    assume "n\<noteq>3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+    thm IH
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using A by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
+    "sumto f 0 = f 0"
+  | "sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  let "?S" = "sumto (\<lambda>x. x)"
+  let "?S3" = "sumto (\<lambda>x. x^3)"
+
+  have "(?S (Suc n))\<^sup>2 = (Suc n + ?S n)\<^sup>2" by auto
+  also have "\<dots> = (Suc n)^2 + 2*(?S n)*(Suc n) + (?S n)^2" by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = (Suc n)^3 + ?S3 n" using IH sum_of_naturals by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = ?S3 (Suc n)" by simp
+  finally show "(?S (Suc n))^2 = ?S3 (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u)
+  apply (auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v"
+    by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (cases xs)
+  case Nil
+  then show ?thesis by simp
+next
+  case (Cons a list)
+  from this obtain ys zs where P: "ys = take (length xs div n) xs" "zs = drop (length xs div n) xs"
+    by auto
+  hence A: "length ys = length xs div n"
+  proof -
+    have l1: "n \<le> length xs \<Longrightarrow> ys = take n xs \<Longrightarrow> length ys = n" by simp
+    also have l2: "length xs div n \<le> length xs" by simp
+    from l1 l2 P show ?thesis by (auto simp: min_absorb2)
+  qed
+  from P have B: "xs = ys@zs" by auto
+  from A B show ?thesis by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+    have ge0: "0 \<le> a n"
+      apply (induction n)
+      by auto
+
+    have "a (Suc n) = (a n) ^ 2 + 1" by auto
+    from IH ge0 have  "\<dots> \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" by (auto simp: power_mono)
+    also have "\<dots> = (2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 2" by (auto simp: power2_diff)
+    also have "\<dots> = (2 ^ 2 ^ (Suc n)) - 2 * ((2 ^ 2 ^ n) - 1)" by (auto simp: power_even_eq)
+    also have "\<dots> \<le> (2 ^ 2 ^ (Suc n)) - 1" by auto
+    finally show "a (Suc n) \<le> 2 ^ 2 ^ (Suc n) - 1" using \<open>a (Suc n) = (a n) ^ 2 + 1\<close> by simp
+  qed
+qed
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_410/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,263 @@
+Using temporary directory '/tmp/tmp.Ra4YH4phcz'
+Files in /tmp/eval-410-SwBK4i: ex05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<defs-imports>
+Main Tree
+</defs-imports>
+<version>
+2016-1
+</version>
+<image>
+HOL-Library
+</image>
+<submission-imports>
+
+</submission-imports>
+<defs>
+
+
+save_test_theory
+</defs>
+<submission>
+
+
+
+text {* \ExerciseSheet{5}{11.~5.~2017} *}
+
+text \<open>
+  \<^item> Import \<open>Complex_Main\<close> and \<open>HOL-Library.Tree\<close>
+  \<^item> For this exercise sheet (and Homework 1), you are not allowed to use sledgehammer!
+    Proofs using the \<open>smt, metis, meson, or moura\<close> methods are forbidden!
+\<close>
+
+text \<open>
+  \Exercise{Bounding power-of-two by factorial}
+  Prove that, for all natural numbers $n>3$, we have $2^n < n!$.
+  We have already prepared the proof skeleton for you.
+\<close>
+lemma exp_fact_estimate: "n>3 \<Longrightarrow> (2::nat)^n < fact n"
+proof (induction n)
+  case 0 then show ?case by auto
+next
+  case (Suc n)
+  assume IH: "3 < n \<Longrightarrow> (2::nat) ^ n < fact n"
+  assume PREM: "3 < Suc n"
+(*
+  from PREM have "n=3 \<or> n>3" by auto
+  then show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof
+*)
+  show "(2::nat) ^ Suc n < fact (Suc n)"
+  proof cases
+    assume [simp]: "n=3"
+    show ?thesis by (auto simp: eval_nat_numeral)
+  next
+    assume "n\<noteq>3"
+    with PREM have A: "n>3" by auto
+    note IH = IH[OF this]
+    thm IH
+
+    have "(2::nat)^(Suc n) = 2*2^n" by auto
+    also have "\<dots> < 2*fact n" using IH by auto
+    also have "\<dots> < (Suc n) * fact n" using A by auto
+    also have "\<dots> = fact (Suc n)" by auto
+    finally show ?thesis .
+  qed
+qed
+
+text \<open>
+  \vspace{1em}
+  {\bfseries Warning!}
+  Make sure that your numerals have the right type, otherwise
+  proofs will not work! To check the type of a numeral, hover the mouse over
+  it with pressed CTRL (Mac: CMD) key. Example:
+\<close>
+lemma "2^n \<le> 2^Suc n"
+  apply auto oops -- \<open>Leaves the subgoal \<open>2 ^ n \<le> 2 * 2 ^ n\<close>\<close>
+  text \<open>You will find out that the numeral \<open>2\<close> has type @{typ 'a},
+    for which you do not have any ordering laws. So you have to
+    manually restrict the numeral's type to, e.g., @{typ nat}.\<close>
+lemma "(2::nat)^n \<le> 2^Suc n" by simp -- \<open>Note: Type inference will
+  infer \<open>nat\<close> for the unannotated numeral, too. Use CTRL+hover to double check!\<close>
+
+text \<open>
+  \vspace{1em}
+\<close>
+
+text \<open>\Exercise{Sum Squared is Sum of Cubes}
+  \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$.
+  \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$.
+\<close>
+
+
+fun sumto :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
+    "sumto f 0 = f 0"
+  | "sumto f (Suc n) = f (Suc n) + sumto f n"
+
+text \<open>You may need the following lemma:\<close>
+lemma sum_of_naturals: "2 * sumto (\<lambda>x. x) n = n * Suc n"
+  by (induction n) auto
+
+lemma "sumto (\<lambda>x. x) n ^ 2 = sumto (\<lambda>x. x^3) n"
+proof (induct n)
+  case 0 show ?case by simp
+next
+  case (Suc n)
+  assume IH: "(sumto (\<lambda>x. x) n)\<^sup>2 = sumto (\<lambda>x. x ^ 3) n"
+  note [simp] = algebra_simps -- \<open>Extend the simpset only in this block\<close>
+
+  let "?S" = "sumto (\<lambda>x. x)"
+  let "?S3" = "sumto (\<lambda>x. x^3)"
+
+  have "(?S (Suc n))\<^sup>2 = (Suc n + ?S n)\<^sup>2" by auto
+  also have "\<dots> = (Suc n)^2 + 2*(?S n)*(Suc n) + (?S n)^2" by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = (Suc n)^3 + ?S3 n" using IH sum_of_naturals by (auto simp: numeral_eq_Suc)
+  also have "\<dots> = ?S3 (Suc n)" by simp
+  finally show "(?S (Suc n))^2 = ?S3 (Suc n)" .
+qed
+
+text \<open>
+  \Exercise{Paths in Graphs}
+  A graph is described by its adjacency matrix, i.e., \<open>G :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.
+
+  Define a predicate \<open>path G u p v\<close> that is true if \<open>p\<close> is a path from
+  \<open>u\<close> to \<open>v\<close>, i.e., \<open>p\<close> is a list of nodes, not including \<open>u\<close>, such that
+  the nodes on the path are connected with edges.
+  In other words, \<open>path G u (p\<^sub>1\<dots>p\<^sub>n) v\<close>, iff \<open>G u p\<^sub>1\<close>, \<open>G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\<close>,
+  and \<open>p\<^sub>n = v\<close>. For the empty path (\<open>n=0\<close>), we have \<open>u=v\<close>.
+\<close>
+
+fun path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" where
+  "path G u [] v \<longleftrightarrow> u=v"
+| "path G u (w#ws) v \<longleftrightarrow> G u w \<and> path G w ws v"
+
+text \<open>Test cases\<close>
+definition "nat_graph x y \<longleftrightarrow> y=Suc x"
+value \<open>path nat_graph 2 [] 2\<close>
+value \<open>path nat_graph 2 [3,4,5] 5\<close>
+value \<open>\<not> path nat_graph 3 [3,4,5] 6\<close>
+value \<open>\<not> path nat_graph 2 [3,4,5] 6\<close>
+
+text \<open>Show the following lemma, that decomposes paths. Register it as simp-lemma.\<close>
+lemma path_append[simp]: "path G u (p1@p2) v \<longleftrightarrow> (\<exists>w. path G u p1 w \<and> path G w p2 v)"
+  apply (induction p1 arbitrary: u)
+  apply (auto)
+  done
+
+text \<open>
+  Show that, for a non-distinct path from \<open>u\<close> to \<open>v\<close>,
+  we find a longer non-distinct path from \<open>u\<close> to \<open>v\<close>.
+  Note: This can be seen as a simple pumping-lemma,
+  allowing to pump the length of the path.
+
+  Hint: Theorem @{thm [source] not_distinct_decomp}.
+\<close>
+lemma pump_nondistinct_path:
+  assumes P: "path G u p v"
+  assumes ND: "\<not>distinct p"
+  shows "\<exists>p'. length p' > length p \<and> \<not>distinct p' \<and> path G u p' v"
+proof -
+  from not_distinct_decomp[OF ND] obtain p1 p2 p3 w where
+    [simp]: "p = p1@[w]@p2@[w]@p3" by blast
+
+  from P obtain w' w'' where "path G u p1 w'" "G w' w" "path G w p2 w''" "G w'' w" "path G w p3 v"
+    by auto
+  hence P: "path G u (p1@[w]@p2@[w]@p2@[w]@p3) v" (is "path _ _ ?p' _") by auto
+
+  have "length ?p' > length p \<and> \<not>distinct ?p'" by auto
+  with P show ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof (cases xs)
+  case Nil
+  then show ?thesis by simp
+next
+  case (Cons a list)
+  from this obtain ys zs where P: "ys = take (length xs div n) xs" "zs = drop (length xs div n) xs"
+    by auto
+  hence A: "length ys = length xs div n"
+  proof -
+    have l1: "n \<le> length xs \<Longrightarrow> ys = take n xs \<Longrightarrow> length ys = n" by simp
+    also have l2: "length xs div n \<le> length xs" by simp
+    from l1 l2 P show ?thesis by (auto simp: min_absorb2)
+  qed
+  from P have B: "xs = ys@zs" by auto
+  from A B show ?thesis by auto
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    text \<open>Insert your proof here\<close>
+    have ge0: "0 \<le> a n"
+      apply (induction n)
+      by auto
+
+    have "a (Suc n) = (a n) ^ 2 + 1" by auto
+    from IH ge0 have  "\<dots> \<le> (2 ^ 2 ^ n - 1) ^ 2 + 1" by (auto simp: power_mono)
+    also have "\<dots> = (2 ^ 2 ^ n) ^ 2 - 2 * (2 ^ 2 ^ n) + 2" by (auto simp: power2_diff)
+    also have "\<dots> = (2 ^ 2 ^ (Suc n)) - 2 * ((2 ^ 2 ^ n) - 1)" by (auto simp: power_even_eq)
+    also have "\<dots> \<le> (2 ^ 2 ^ (Suc n)) - 1" by auto
+    finally show "a (Suc n) \<le> 2 ^ 2 ^ (Suc n) - 1" using \<open>a (Suc n) = (a n) ^ 2 + 1\<close> by simp
+  qed
+qed
+</submission>
+<check-imports>
+Submission
+</check-imports>
+<check>
+
+</check>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_408/SENTMAIL	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,1 @@
[e-mail]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_408/tmpl05.thy	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,83 @@
+(** Score: 10/10
+*)
+(*<*)
+theory tmpl05
+  imports
+    Complex_Main
+    "HOL-Library.Tree"
+begin
+(*>*)
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+  have "length ?ys = length xs div n \<and> xs=?ys@?zs" by (simp add: min_absorb2)
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = a n ^ 2 + 1" by simp
+    also have "... \<le> (2^2^n - 1)^2 + 1" using IH power_mono by (smt a.elims zero_le_power2)
+    also have "... = (2^2^n)^2 - 2*2^2^n + 1 + 1" by (simp add: power2_diff)
+    also have "... = 2^2^(n+1) - 2*2^2^n + 2" by (simp add: power2_eq_square power_even_eq)
+    also have "... \<le> 2^2^(n+1) - 1" by simp
+    finally show ?thesis by simp
+  qed
+qed
+
+
+(*<*)
+end
+(*>*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/[e-mail]_408/user_error_log.txt	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,107 @@
+Using temporary directory '/tmp/tmp.Kaw28ZkBn0'
+Files in /tmp/eval-408-4GCKyp: tmpl05.thy
+Command  ['java', '-cp', '/jail/tumjudge-assembly.jar', 'TUMJudge', '/home/test-runner/local-storage']
+=================
+<version>
+2016-1
+</version>
+<defs>
+
+
+save_test_theory
+</defs>
+<check>
+
+</check>
+<submission-imports>
+
+</submission-imports>
+<submission>
+
+(*>*)
+
+
+text \<open>
+  \NumHomework{Split Lists}{May 18}
+  Recall: Use Isar where appropriate, proofs using
+    \<open>metis, smt, meson, or moura\<close> (as generated by sledgehammer) are forbidden!
+
+  Show that every list can be split into a prefix and a suffix,
+  such that the length of the prefix is \<open>1/n\<close> of the original lists's length.
+
+\<close>
+
+lemma
+  assumes "n\<ge>0" -- \<open>Note: This assumption is actually not needed,
+    as @{lemma "n div 0 = 0" by auto}, so don't be puzzled if you do
+    not use it at all in your proof.\<close>
+  shows "\<exists>ys zs. length ys = length xs div n \<and> xs=ys@zs"
+proof -
+  let ?ys = "take (length xs div n) xs"
+  let ?zs = "drop (length xs div n) xs"
+  have "length ?ys = length xs div n \<and> xs=?ys@?zs" by (simp add: min_absorb2)
+  thus ?thesis by blast
+qed
+
+text \<open>
+  \NumHomework{Estimate Recursion Equation}{May 18}
+
+  (Sledgehammer allowed again)
+
+  Show that the function defined by \<open>a 0 = 0\<close> and \<open>a (n+1) = (a n)\<^sup>2 + 1\<close>
+  is bounded by the double-exponential function \<open>2^(2^n)\<close>
+\<close>
+
+fun a :: "nat \<Rightarrow> int" where
+"a 0 = 0" |
+"a (Suc n) = a n ^ 2 + 1"
+
+text \<open>
+  We have given you a proof skeleton, setting up the induction.
+  To complete your proof, you should come up with a chain of inequations.
+  You may try to solve the intermediate steps with sledgehammer.
+
+  Hint: It is a bit tricky to get the approximation right.
+    We strongly recommend to sketch the inequations on paper first.
+
+  Hint: Have a look at the lemma @{thm [source] power_mono}, in particular its
+  instance for squares:
+\<close>
+
+thm power_mono[where n=2]
+
+lemma "a n \<le> 2 ^ (2 ^ n) - 1"
+proof(induction n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  assume IH: "a n \<le> 2 ^ 2 ^ n - 1"
+    -- \<open>Refer to the induction hypothesis by name \<open>IH\<close> or \<open>Suc.IH\<close>\<close>
+  show "a (Suc n) \<le> 2 ^ 2 ^ Suc n - 1"
+  proof -
+    have "a (Suc n) = a n ^ 2 + 1" by simp
+    also have "... \<le> (2^2^n - 1)^2 + 1" using IH power_mono by (smt a.elims zero_le_power2)
+    also have "... = (2^2^n)^2 - 2*2^2^n + 1 + 1" by (simp add: power2_diff)
+    also have "... = 2^2^(n+1) - 2*2^2^n + 2" by (simp add: power2_eq_square power_even_eq)
+    also have "... \<le> 2^2^(n+1) - 1" by simp
+    finally show ?thesis by simp
+  qed
+qed
+
+
+(*<*)
+</submission>
+<defs-imports>
+Main Tree
+</defs-imports>
+<image>
+HOL-Library
+</image>
+<check-imports>
+Submission
+</check-imports>
+=================
+Failed to load submission in Isabelle!
+Test case check_build:	Failed
+Runner terminated with exit code 1.
+Test execution terminated with exit code 1.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/SS18/Exercises/hwsubm/hw05/meta.csv	Thu May 24 12:21:11 2018 +0200
@@ -0,0 +1,18 @@
+"398","[e-mail]","Rau","Martin","http://vmnipkow3.in.tum.de/web/submissions/398"
+"399","[e-mail]","Krebs","Mitja","http://vmnipkow3.in.tum.de/web/submissions/399"
+"400","[e-mail]","Rieder","Sabine","http://vmnipkow3.in.tum.de/web/submissions/400"
+"401","[e-mail]","Rotar","Alexej","http://vmnipkow3.in.tum.de/web/submissions/401"
+"402","[e-mail]","Griebel","Simon","http://vmnipkow3.in.tum.de/web/submissions/402"
+"403","[e-mail]","Kutasi","Daniel","http://vmnipkow3.in.tum.de/web/submissions/403"
+"404","[e-mail]","Kirchmeier","Maximilian","http://vmnipkow3.in.tum.de/web/submissions/404"
+"405","[e-mail]","Koepke","Eric","http://vmnipkow3.in.tum.de/web/submissions/405"
+"406","[e-mail]","Das Sharma","Amartya","http://vmnipkow3.in.tum.de/web/submissions/406"
+"407","[e-mail]","Somasundaram","Arun","http://vmnipkow3.in.tum.de/web/submissions/407"
+"408","[e-mail]","Wielander","Felix","http://vmnipkow3.in.tum.de/web/submissions/408"
+"409","[e-mail]","Smith","Nicholas","http://vmnipkow3.in.tum.de/web/submissions/409"
+"410","[e-mail]","Stamer","Florian","http://vmnipkow3.in.tum.de/web/submissions/410"
+"411","[e-mail]","Jonischkeit","Clemens","http://vmnipkow3.in.tum.de/web/submissions/411"
+"412","[e-mail]","Gottfriedsen","Jakob","http://vmnipkow3.in.tum.de/web/submissions/412"
+"413","[e-mail]","Schmitt","Katharina","http://vmnipkow3.in.tum.de/web/submissions/413"
+"415","[e-mail]","Mutius","Joshua","http://vmnipkow3.in.tum.de/web/submissions/415"
+"418","[e-mail]","Pfeiffer","Marcus","http://vmnipkow3.in.tum.de/web/submissions/418"