diff -r a33bbac43359 -r ba194424b895 src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Thu Oct 20 18:41:58 2016 +0200
+++ b/src/HOL/Library/Stream.thy	Thu Oct 20 18:41:59 2016 +0200
@@ -242,7 +242,7 @@
 lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)"
   by (induct n arbitrary: m s) auto
 
-partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
+partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
   "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
 
 lemma sdrop_while_SCons[code]:
@@ -342,7 +342,7 @@
   by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
 
 lemma sset_cycle[simp]:
-  assumes "xs \<noteq> []" 
+  assumes "xs \<noteq> []"
   shows "sset (cycle xs) = set xs"
 proof (intro set_eqI iffI)
   fix x
@@ -408,6 +408,14 @@
 lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
   by (simp add: streams_iff_sset)
 
+lemma streams_empty_iff: "streams S = {} \<longleftrightarrow> S = {}"
+proof safe
+  fix x assume "x \<in> S" "streams S = {}"
+  then have "sconst x \<in> streams S"
+    by (intro sconst_streams)
+  then show "x \<in> {}"
+    unfolding \<open>streams S = {}\<close> by simp
+qed (auto simp: streams_empty)
 
 subsection \<open>stream of natural numbers\<close>
 
@@ -442,11 +450,11 @@
 lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
   by (cases ws) auto
 
-lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
+lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then
   shd s ! n else flat (stl s) !! (n - length (shd s)))"
   by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less)
 
-lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> 
+lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow>
   sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
 proof safe
   fix x assume ?P "x : ?L"